Abstract
In this paper we consider a powerful mechanism, called Regular XPath, for expressing queries and constraints over XML data, including DTDs and existential path constraints and their negation. Regular XPath extends XPath with binary relations over XML nodes specified by means two-way regular path queries. Our first contribution deals with checking satisfiability of Regular XPath constraints. While this problem could be reduced in terms of reasoning in repeat converse deterministic PDL, a well-known variant Propositional Dynamic Logic (PDL), the resulting technique would be of little practical use, due to the notorious difficulty of implementing efficient reasoners for such a logic. We therefore propose a direct algorithm for Regular XPath constraints satisfiability, based on checking emptiness of two way alternating automata on finite trees. We show how this algorithm can be implemented symbolically, by using Binary Decision Diagrams (BDDs) as the underlying data structure, which can be significantly more efficient than explicit graph-based algorithms. We then move to query containment and view based query answering for Regular XPath, and show that both problems can be reduced to checking satisfiability of Regular XPath constraints, thus allowing for taking advantage of the techniques developed for constraints satisfiability.