Bottom-up automata on data trees and vertical XPath

TL;DR

This paper introduces a bottom-up automaton model for data trees with a register, enabling decision procedures for the satisfiability of the vertical XPath fragment, which includes common axes like child, descendant, parent, and ancestor.

Contribution

It presents a novel automaton model with a decidable emptiness problem that captures the expressive power of a significant XPath fragment.

Findings

Decidable emptiness problem for the automaton model.

Automaton captures the vertical XPath fragment's expressive power.

Provides a decision procedure for XPath satisfiability.

Abstract

A data tree is a finite tree whose every node carries a label from a finite alphabet and a datum from some infinite domain. We introduce a new model of automata over unranked data trees with a decidable emptiness problem. It is essentially a bottom-up alternating automaton with one register that can store one data value and can be used to perform equality tests with the data values occurring within the subtree of the current node. We show that it captures the expressive power of the vertical fragment of XPath - containing the child, descendant, parent and ancestor axes - obtaining thus a decision procedure for its satisfiability problem.