Forward-XPath and extended register automata

Diego Figueira (1)

1 DAHU - Verification in databases

We consider a fragment of XPath named 'forward-XPath', which contains all descendant and rightwards sibling axes as well as data equality and inequality tests. The satisfiability problem for forward-XPath in the presence of DTDs and even of primary key constraints is shown here to be decidable. To show decidability we introduce a model of alternating au-tomata on data trees that can move downwards and right-wards in the tree, have one register for storing data and compare them for equality, and have the ability to (1) non-deterministically guess a data value and store it, and (2) quantify universally over the set of data values seen so far during the run. This model extends the work of Jurdzi´nskiJurdzi´nski and Lazi´cLazi´c. Decidability of the finitary non-emptiness problem for this model is obtained by a direct reduction to a well-structured transition system, contrary to previous approaches. Another consequence that we explore is the satis-fiability problem for the Linear Temporal Logic (LTL) over data words with one register and quantification over data values, which is shown to be decidable.

Mots clés: alternating tree register automata; XML; forward XPath; unranked ordered tree; data-tree; infinite alphabet

Domaines: Base de données [cs.DB]; Logique en informatique [cs.LO]

Diego Figueira. Forward-XPath and extended register automata. International Conference on Database Theory (ICDT), Mar 2010, Lausanne, Switzerland. ⟨10.1145/1804669.1804699⟩. ⟨hal-01806093⟩