Diego Figueira

Forward-XPath and extended register automata

Keywords: I.7.2 [Document Preparation]: Markup Languages, H.2.3 [Database Management]: Languages, H.2.3 [Languages]: Query Languages Algorithms, Languages alternating tree register automata, XML, forward XPath, unranked ordered tree, data-tree, infinite

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 automata on data trees that can move downwards and rightwards in the tree, have one register for storing data and compare them for equality, and have the ability to (1) nondeterministically 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ński and Lazić. 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 satisfiability problem for the Linear Temporal Logic (LTL) over data words with one register and quantification over data values, which is shown to be decidable.

INTRODUCTION

This work is motivated by the increasing importance of reasoning tasks in xml research. An xml document can be seen as an unranked ordered tree where each node carries a label from a finite alphabet and a set of attributes, each with an associated datum from some infinite domain.

XPath is arguably the most widely used xml node selecting language, part of XQuery and XSLT; it is an open standard and a W3C Recommendation [START_REF] Clark | XML path language (XPath)[END_REF]. Static analysis on xml languages is crucial for query optimization tasks, consistency checking of xml specifications, type checking transformations, or many applications on security. Among the most important problems are those of query equivalence and query containment. By answering these questions we can decide at compile time whether the query contains a contradiction, and thus whether the computation of the query on the document can be avoided, or if one query can be safely replaced by another one. For logics closed under boolean combination, these problems reduce to satisfiability checking, and hence we focus on this problem. Unfortunately, the satisfiability problem for XPath with data tests is undecidable, even when the data domain has no structure [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF] (i.e., where the only data relation available is the test for equality or inequality). It is then natural to identify and study decidable expressive fragments. In this work we adopt an automata-theoretic approach to find such fragments. The main contributions can be summarized as follows.

• A new register automata model for xml is introduced. This is an extension of the model treated in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] with a decidable finitary emptiness problem. The decidability proof we propose simplifies the previous approaches of [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] and facilitates the pursuit and identification of decidable extensions. This is evidenced here by the introduction of two extensions that preserve decidability.

• The satisfiability for the 'forward' fragment of XPath with data test equalities and inequalities is shown to be decidable, even in the presence of DTDs and primary key constraints. This settles a natural question left from the work in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF], also mentioned in [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF][START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. As a consequence this also answers positively the open question raised in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] on whether the downward fragment of XPath in the presence of DTDs is decidable. 1 In fact, we give a decision procedure for the satisfiability problem in the presence of any regular tree language, and we can therefore code the core of XML Schema (stripped of functional dependencies, except of unary primary keys) or Relax NG document types.

• We show that the temporal logic for words with data defined in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] extended with quantification over data values is decidable. This is a consequence of considering our automata model over words rather than trees.

Automata. The automata model we define is based on the ATRA model (for Alternating Tree Register Automata). It is a tree walking automaton with alternating control and one register to store and compare data values. This automaton can move downwards and rightwards over an unranked ordered tree with data. It is a decidable model that has been studied in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] and corresponds to the extension to trees of the automaton over words of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. The proofs of decidability of these automata models are based on non-trivial reductions to a class of decidable counter automata with faulty increments. In the present work, decidability is directly shown by interpreting the semantics of the automaton in the theory of well quasi-orderings in terms of a well-structured transition system [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. The object of this alternative proof is twofold.

On the one hand, we propose a simpler proof of the main decidability results of [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. On the other, our approach easily yields the decidability of the non-emptiness problem for two powerful extensions of ATRA. These extensions consist in the following abilities: (a) the automaton can nondeterministically guess any data value of the domain and store it in the register; and (b) it can make a certain kind of universal quantification over the data values seen along the run of the automaton, in particular over the ancestors' data values. We name these extensions guess and spread respectively, and the model of alternating tree register automata with these extensions as ATRA(guess, spread).

In the context of xml documents, we show that this model of automata can decide a large fragment of XPath. Moreover, when restricted to words with data it can decide and capture some extensions of temporal logics.

XML. We study and show decidability of the satisfiability problem for a fragment of XPath by a reduction to the nonemptiness problem of ATRA(guess, spread). Let us describe this logic. Core-XPath [START_REF] Gottlob | Efficient algorithms for processing XPath queries[END_REF] is the fragment of XPath that captures all the navigational behavior of XPath. It has been well studied and its satisfiability problem is known to be decidable in ExpTime in the presence of DTDs [START_REF] Marx | XPath with conditional axis relations[END_REF]. We consider an extension of this language with the possibility to make equality and inequality tests between attributes of xml elements. This logic is named Core-Data-XPath in [START_REF] Miko Laj Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF], and its satisfiability problem is undecidable [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF]. The present work contributes to the study of different navigational fragments of XPath with equality tests in the attempt to find decidable and computationally well-behaved logics.

Here we address a large fragment named 'forward XPath', that contains the child, descendant, self-or-descendant, nextsibling, following-sibling, and self-or-following-sibling axes. For economy of space we refer to these axes as ↓, ↓ + , ↓ * , →, → + , → * respectively. Note that → + and → * are interdefinable in the presence of →, and similarly with ↓ + and ↓ * . We then refer to this fragment as XPath(↓, ↓ * , →, → * ). Although our automata model cannot capture this logic in terms of expressiveness, we show that there is a non-trivial reduction to the nonemptiness problem of ATRA(guess, spread). By the fact that these automata can code any regular language (in particular a DTD), and that XPath(↓, ↓ * , →, → * ) can express unary primary key constraints, it follows that satisfiability of forward-XPath in the presence of DTDs and primary key constraints is decidable.

Words. ATRA(guess, spread) interpreted over words with data also yield new decidability results on the satisfiability for some extensions of the temporal logic with one register denoted by LTL ↓ (U, X) in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. This logic contains a 'freeze' operator to store the current datum and a 'test' operator to test the current datum against the stored one. Our automata model captures an extension of this logic with quantification over data values, where we can express "for all data values in the past, ϕ holds", or "there exists a data value in the future where ϕ holds". Indeed, none of these two types of properties can be expressed in the previous formalisms of [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] and [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. These quantifiers may be added to LTL ↓ (U, X) over data words without losing decidability. However, adding the dual of any of these operators results in undecidability.

Related work

In [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] a fragment of XPath(↓, ↓ * , →, → * ) is treated. The language is restricted to data test formulae of the form ε = α (or ε = α), that is, sentences that test whether there exists an element accessible via the α-relation with the same (resp. different) data value as the current node of evaluation. This logic was shown to be expressible in the ATRA automaton defined in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. However, this restricted form of data tests cannot express, e.g., that there are two leaves with the same datum, or that all the elements with a certain symbol have different data value (i.e, a primary key constraint). The problem regarding the decidability of the full forward fragment with arbitrary data tests is a non-trivial natural question left from [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] that is positively answered here.

The work in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] investigates the satisfiability problem for many XPath logics, mostly fragments without negation or without data equality tests in the absence of sibling axes. Also, in [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF] there is a thorough study of the satisfiability problem for all the downward XPath queries with and without data equality tests. Notably, none of these works considers horizontal axes to navigate between siblings: By exploiting the bisimulation invariance property enjoyed by these logics, the complexity of the satisfiability problem is kept relatively low (at most ExpTime) in the presence of data values. However, when horizontal axes are present, most of the problems have a non-primitive recursive complexity (including the fragment of [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF], or even much simpler ones without the one-step '→' axis [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]). In [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF], several fragments with horizontal axes are treated. The only fragment with data tests and negation studied there is incomparable with the forward fragment, and it is shown to be undecidable.

First-order logic with two variables and data equality tests is explored in [START_REF] Miko Laj Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF], where it is shown that F O 2 with local one-step relations to move around the data tree and a data equality test relation is decidable. [START_REF] Miko Laj Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF] also shows the decidability of a fragment of XPath(↑, ↓, ←, →) with sibling and upward axes but restricted to local elements and to data for- mulae of the kind ε = α (or =), while our fragment cannot move upwards but features transitive axes and unrestricted data tests.

a, 2 a, 2 b, 2 b, 9 b, 5 b, 3 a, 2 b, 1 b, 2

DATA TREES AND XML DOCUMENTS

In this article we work with data trees instead of xml documents, being a simpler formalism to work with, from where results can be transferred to the class of xml documents. We discuss below how all the results we give on XPath over data trees, also hold for the class of xml documents.

A data tree is an unranked ordered tree whose every node is labeled by a symbol from a finite alphabet and a datum from an infinite domain, as in the example of Fig. 1. Let ℘(S) denote the power set of S, let N be the set of positive integers, and let us fix D to be any infinite domain of data values.

In our examples we will consider D = N. We define Pos ⊆ ℘(N * ) to be the set of sets of finite tree positions (we write for the empty word, corresponding to the root's position).

X ∈ Pos iff (a) X ⊆ N * , |X| < ∞; (b) it is prefix- closed; and (c) if n(i + 1) ∈ X then ni ∈ X. Given a finite
alphabet Σ, a finite data tree over Σ is a tuple T = P, σ with P ∈ Pos and σ : P → Σ×D, as in Fig. 1. The functions π1 and π2 project the first and second component of an element of Σ × D. We define type T : P → { , ¯ } × {£, £} that specifies whether a node has children and/or siblings to the right. That is, type T (p) := (a, b) where a = iff p1 ∈ P , and where b = £ iff p = p i and p (i + 1) ∈ P .

While a data tree has one data value for each node, an xml document may have several attributes at a node, each with a data value. Every attribute of an xml element can be encoded as a child node in a data tree labeled by the attribute's name, as in Fig. 2. This coding can be enforced by the formalisms we present below, and we can thus transfer all the decidability results to the class of xml documents.

In fact, it suffices to demand that all the attribute symbols can only occur at the leaves of the data tree and to interpret attribute expressions like '@attrib1 ' of XPath formulae as child path expressions 'child[attrib1]'.

THE ATRA MODEL

In this section we present the model of computation that will enable us to show decidability of XPath and temporal logic fragments.

An Alternating Tree Register Automaton (ATRA) consists in a top-down walking automaton with alternating control and one register to store and test data. In [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] it was shown that its finitary emptiness problem is decidable and non primitive recursive. Here, we consider an extension of ATRA with two operators: spread and guess. We call this model ATRA(spread, guess).

Definition 3.1. A forward alternating register automaton ATRA(spread, guess) is a tuple Σ, Q, qI , δ s.t.

Σ is a finite alphabet;

Q is a finite set of states; qI ∈ Q is the initial state; and δ : Q → Φ is the transition function, where Φ is defined by the grammar

a | ā | ? | set(q) | eq | eq | q ∧ q | q ∨ q | q | £q | guess(q) | spread(q, q )
where a ∈ Σ, q, q ∈ Q, ∈ { , ¯ , £, £}. This formalism without the guess and spread transitions is equivalent to the automata model of [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] on finite data trees, where and £ are to move to the first child or to the next sibling, set(q) stores the current datum and eq (resp. eq) tests that the current node's value is (resp. not) equal to the stored.

As this automaton is one-way, we define its semantics as a set of 'threads' for each node that progress synchronously. That is, all threads at a node move one step forward simultaneously and then perform some non-moving transitions independently. This is done for the sake of simplicity of the formalism, which simplifies the presentation of the decidability proof.

Next we define a configuration of a node and a configuration of a tree to then give a notion of a run over a data tree T = P, σ . A node configuration is a tuple p, α, γ, H that describes the partial state of the execution at a given node. p ∈ P is the node position in the tree T , γ = σ(p) ∈ Σ × D is the current node's symbol/datum, and α = type T (p) is the tree type of the node. Finally, H ∈ ℘(Q×D) is a finite collection of active threads of execution, each thread q, d consisting in a state q and the value stored in the register d. By ConfN we denote the set of all node configurations. A tree configuration is a finite set of node configurations, like { , α, γ, H , 1211, α , γ , H , . . . }. The run will be defined in such a way that a tree configuration never contains node configurations in a descendant/ancestor relation. We call ConfT = ℘(ConfN ) the set of all finite tree configurations. Given a set of threads we write data(H) := {d | q, d ∈ H}, and data( p, α, (a, d), H ) := {d} ∪ data(H).

To define a run we first introduce three transition relations over node configurations: the non-moving relation →ε, the first-child relation → , and the next-sibling relation →£.

We start with →ε. If the transition corresponding to a thread is a set(q), the automaton sets the register with current data value and continues the execution of the thread with state q; if it is eq, the thread accepts (and in this case disappears from the configuration) if the current datum is equal to that of the register, otherwise the computation for that thread cannot continue. The reader can check that the rest of the cases follow the intuition of an alternating automaton. Let ρ = p, α, (s, d), { q, d } ∪ H . Then,

ρ →ε p, α, (s, d), { qi, d } ∪ H if δ(q) = q1 ∨ q2, i ∈ {1, 2} (1)
ρ →ε p, α, (s, d), { q1, d , q2, d } ∪ H if δ(q) = q1 ∧ q2 (2)
ρ →ε p, α, (s, d), { q , d } ∪ H if δ(q) = set(q ) (3) ρ →ε p, α, (s, d), H if δ(q) = eq and d = d (4)
ρ →ε p, α, (s, d), H if δ(q) = eq and d = d

ρ →ε p, α, (s, d), H if δ(q) = ? and is in α (6)

ρ →ε p, α, (s, d), H if δ(q) = s (7) ρ →ε p, α, (s, d), H if δ(q) = r for r = s (8)
The following cases correspond to our extensions to the model of [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. The 'guess' instruction extends the model with the ability of storing any datum from the domain D. Whenever δ(q) = guess(q ) is executed, a data value (nondeterministically chosen) is saved in the register.

ρ →ε p, α, (s, d), { q , e } ∪ H if δ(q) = guess(q ), e ∈ D (9)
The 'spread' instruction is an unconventional operator in the sense that it depends on the data of all threads in the current configuration with a certain state. Whenever δ(q) = spread(q2, q1) is executed, a new thread with state q1 and datum d is created for each thread q2, d present in the configuration. With this operator we can code a universal quantification over all the ancestors' data values. For convenience, we demand that this transition may only be applied if all other possible →ε kind of transitions were already executed. Or, in other words, that only spread transitions or moving transitions are present in the configuration (the moving transitions being those defined as ' q' and '£q').

ρ →ε p, α, (s, d), { q1, d | q2, d ∈ H} ∪ H if δ(q) = spread(q2, q1) and for all q, d ∈ H : either δ(q) = spread(q1, q2), δ(q) = q1, or δ(q) = £q1 for some q1, q2 ∈ Q (10)
The → and →£ transitions advance all threads of the node simultaneously, and are defined, for any type α1 ∈ { , ¯ , £, £} and symbol and with data value

γ1 ∈ Σ × D, p, ( , r), γ, H → p 1, α1, γ1, H , (11)
pi, (l, £), γ, H →£ p(i + 1), α1, γ1, H£

iff (i) the configuration is 'moving' (i.e., all the threads q, d contained in H are of the form δ(q) = q or δ(q) = £q );

(ii) for ∈ { , £}, H = { q , d | q, d ∈ H, δ(q) = q }; and (iii) α1 and γ1 are consistent with the position p1 in the case of ( 11), or with p(i + 1) in the case of [START_REF] Gottlob | Efficient algorithms for processing XPath queries[END_REF].

Finally, we define the transition between tree configurations that we call t . This corresponds to applying a 'non-moving' →ε to a node configuration, or to apply a 'moving' → , →£, or both to a node configuration according to its type. That is, we define S1 t S2 iff one of the following conditions holds:

1. S1 = {ρ} ∪ S , S2 = {τ } ∪ S , ρ →ε τ ; 2. S1 = {ρ} ∪ S , S2 = {τ } ∪ S , ρ = p, ( , £), γ, H , ρ → τ ; 3. S1 = {ρ} ∪ S , S2 = {τ } ∪ S , ρ = p, ( ¯ , £), γ, H , ρ →£ τ ; 4. S1 = {ρ} ∪ S , S2 = {τ1, τ2} ∪ S , ρ = p, ( , £), γ, H , ρ → τ1, ρ →£ τ2.
A run over a data tree T = P, σ is a non-empty sequence S1 t • • • t Sn with S1 = { , α0, γ0, H0 } and H0 = { qI , π2(σ( )) } (i.e., the thread consisting in the initial state with the root's datum), such that for every

i ∈ [1..n], p, α, γ, H ∈ Si: (1) p ∈ P ; (2) γ = σ(p); and
(3) α = type T (p). We say that the run is accepting iff

Sn ⊆ { p, α, γ, ∅ | p, α, γ, ∅ ∈ ConfN }.
The ATRA model is closed under all boolean operations [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. However, the extensions introduced guess and spread, while adding expressive power, are not closed under complement as a trade-off for decidability. Proof (sketch). (a) is based on the fact that while with guess we can express "there are two leaves with equal datum", with ATRA we cannot do it(more details in the Appendix). Here we focus on the proof of (b). We show a property P that can be expressed in ATRA(spread) and such that its negation permits to code an undecidable problem.

Hence, P cannot be expressed in ATRA since it is both closed under complement and decidable.

Given Σ = {a, b}, let P be the following property: "there exists an inner node labeled b such that there is no ancestor labeled a with the same data value" as depicted in Fig. 3. Let us see how P can be coded into ATRA(spread). Assuming q0 is the initial state, the transitions should reflect that every a seen along the run is saved with a state qa, and that this state is in charge of propagating this datum everywhere in the tree. Then, we non-deterministically choose a b and check that all these stored values under qa are different from the current one. For succinctness we write the transitions as positive boolean combinations of the basic operations. P , on the other hand, cannot be expressed by the ATRA model. Were it expressible, then the negation "for every inner node b there exists an ancestor a with the same data value" would also be. It can be seen that with this kind of property one can code an accepting run of a Minsky automaton along a branch by using data to assure that (i) for every increment there is a corresponding future decrement; and by using this property that (ii) for every decrement there exists a corresponding previous increment. This is absurd, as the ATRA model is decidable. We refer the reader to [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Figueira | Future-looking logics on data words and trees[END_REF] for more details on these kind of codings.

δ(q0) = (b ∧ ? ∧ spread(qa, q1))∨ (ā ∨ set(qa)) ∧ ( ¯ ? ∨ q0) ∧ ( £? ∨ £q0) , δ(q1) = eq, δ(qa) = ( ¯ ? ∨ qa) ∧ ( £? ∨ £qa).
Proposition 3.2. ATRA(spread, guess) models have the following properties: (i) they are closed under union, (ii) they are closed under intersection, (iii) they are not closed under complement.

Proof (sketch). (i) and (ii) are straightforward if we notice that the first argument of spread ensures that this transition is always relative to the states of one of the automata being under intersection or union. (iii) is a consequence of the proof of Proposition 3.1 item (b), combined with the fact that the model will be shown to be decidable.

Decidability of the emptiness problem

We dedicate this section to prove the decidability of the ATRA(guess, spread) emptiness problem. The main argument consists in interpreting the automaton's execution as a transition system in the theory of well quasi-orderings with some good properties that allow us to obtain an effective procedure for the emptiness problem. This is known in the literature as a well-structured transition system (WSTS) [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. The following are standard definitions. Definition 3.2. (A, ≤) is a well quasi-order (wqo) iff '≤' ⊆ A × A is a relation that is reflexive, transitive and for every infinite succession w1, w2, . . . ∈ A ω there are two indexes i < j such that wi ≤ wj.

Definition 3.3. Given a transition system (A, →), we define Succ(a) := {a | a → a }, Succ * (a) := {a | a → * a }.
Given a wqo (A, ≤) and A ⊆ A, we define ↑ A := {a | a ∈ A , a ≤ a}. Definition 3.4. We say that a transition system (A, →) is finitely branching iff Succ(a) is finite for all a ∈ A. If Succ(a) is also effectively computable for all a, we say that (A, →) is effective. Definition 3.5. A wqo (A, ≤) is reflexive downwards compatible (rdc) with respect to a transition system (A, →) iff for every a1, a2, a 1 ∈ A such that a 1 ≤ a1 and a1 → a2, there exists a 2 ∈ A such that a 2 ≤ a2 and either a 1 → a 2 or

a 1 = a 2 .
Decidability will be shown as a consequence of the following known result. Proof. As already mentioned, decidability for ATRA was proved in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. Here we propose an alternative approach that simplifies the proof of decidability of the two extensions spread and guess.

The proof goes as follows. We will define a wqo ≺ over the node configurations and show that (ConfN , ≺) is rdc w.r.t. →ε, → and →£ (Lemma 3.2). We will then apply a useful result (Proposition 3.4) to lift this result to the set of tree configurations and prove for some decidable wqo `that (ConfT , `) is rdc w.r.t. t . Note that strictly speaking t is an infinite-branching transition system as → or →£ may take any value from the infinite set D, and →ε can also guess any value. However, it can trivially be restricted to an effective finitely branching one. Then, by Proposition 3.3, t has an effectively computable upward-closed reachability set, and this implies that the emptiness problem of ATRA(guess, spread) is decidable.

We first define the relation '≺' ⊆ ConfN × ConfN between node configurations p, α, (s, d), H ≺ p , β, (s , d ), H iff there exists an injective mapping f : {d}∪data(H) → D such that 1. if q, e ∈ H then q, f (e) ∈ H , 2. f (d) = d , and 3. s = s and α = β.

Whenever it is necessary to make explicit the witnessing function f that enables the relation, we write ρ ≺ f τ . The following lemma follows from the definition just seen. The proof is in the Appendix. Proof. We shall show that for all ρ, τ, ρ ∈ ConfN such that ρ τ and ρ ≺ ρ, there is τ such that τ ≺ τ and either ρ τ or τ = ρ . The proof is a simple case analysis of the definitions for . All cases are treated alike, here we present the most representative. Suppose first that performs a →ε, then one of the definition conditions of →ε must apply.

If (4), let ρ = p, α, (s, d), { q, d } ∪ H τ = p, α, (s, d), H
with δ(q) = eq. Let ρ = p , α, (s, e ), H ≺ f ρ. If there is q, e ∈ H such that f (e) = d, then by injectivity of f , e = e and we can then apply the same →ε-transition obtaining ρ →ε τ ρ →ε τ witenessed by the map f . Otherwise, we can safely take ρ = τ and check that τ ≺ f τ .

If (3), let ρ = p, α, (s, d), { q, d } ∪ H τ = p, α, (s, d), { q , d } ∪ H
with ρ →ε τ and δ(q) = set(q ). Again let ρ ≺ f ρ containing q, e ∈ H with f (e) = d . In this case we can apply the same →ε-transition arriving to τ where τ ≺ f τ . Else, we take ρ = τ .

If a guess is performed [START_REF] Figueira | Future-looking logics on data words and trees[END_REF], let

ρ = p, α, (s, d), { q, d } ∪ H →ε τ = p, α, (s, d), { q , e } ∪ H
with δ(q) = guess(q ). Let ρ = p , α, (s, d 1 ), H ≺ f ρ. Suppose there is q, d 2 ∈ H such that f (d 2 ) = d , then we then take a guess transition from ρ obtaining some τ . If e ∈ Im(f ), we obtain τ by guessing f -1 (e) and hence τ ≺ f τ . If e ∈ Im(f ), τ is obtained by guessing a 'new' value e2 different from all those of data(ρ ), and by defining

f := f [e2 → e] we have τ ≺ f τ . Otherwise, if there is no q, d 2 ∈ H such that f (d 2 ) = d , we take τ = ρ and check that τ ≺ f τ .
Finally, if a spread is performed [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], let

ρ = p, α, γ, { q, d } ∪ H →ε τ = p, α, γ, { q1, d | q2, d ∈ H} ∪ H
with δ(q) = spread(q2, q1). Let ρ = p , α, γ , H ≺ f ρ and suppose there is q, e ∈ H such that f (e) = d (otherwise τ = ρ works). We then take a spread instruction ρ →ε τ and see that τ ≺ f τ , because any q1, e in τ generated by the spread must come from q2, e of ρ , and hence from some q2, f (e) of ρ; now by the spread applied on ρ, q1, f (e) is in τ . The remaining cases of →ε are only easier.

There can be 3 other possible 'moving' applications of depending on the tree type of the node configuration in question. We will only analyze one case, as the others are symmetric. Suppose that we have

ρ = p, ( , £), (a, d), H τ = p1, α1, (a1, d1), H1
where ρ → τ . Let ρ = p , ( , £), (a, d ), H ≺ f ρ. If ρ is such that ρ ≺ τ , the relation is trivially compatible. Otherwise, we shall prove that there is τ such that ρ τ and τ ≺ τ . Condition (i) of → holds for ρ , because all the states present in ρ are also in ρ (by definition of ≺ f ) where the condition must hold. Then, we can apply the → transition to ρ and obtain τ of the form p 1, α1, (a1, d 1 ), H 1 . Notice that we are taking α1 and a1 exactly as in τ , and that H 1 is completely determined by the → transition from H . We only need to describe the value d 1 that will serve our purpose. As before, if d1 ∈ Im(f ) we take d 1 = f -1 (d1) and check τ ≺ f τ ; and if d1 ∈ Im(f ) we take d 1 to be a new value not in data(H ) and check τ ≺ f τ with

f := f [d 1 → d1].
We just showed that for node configurations, (ConfN , ) is rdc w.r.t. (ConfN , ≺). We now lift this result to tree configurations, by considering that a tree configuration can be equivalently seen as an element from (ConfN ) * , and showing that the transition system ((ConfN ) * , t ) is rdc w.r.t. the embedding order over (ConfN , ≺) that we define next.

Definition 3.6. The embedding order (A * , `) over an order (A, ≤) is defined as follows.

(w1 • • • wn) `(v1 • • • vm) iff there exist 1 ≤ i1 < i2 < • • • < in ≤ m such that wj ≤ vi j for all j ∈ [1..n].
The lifting result is a standard argument, and can be stated in this general proposition, whose proof can be found in the Appendix.

Proposition 3.4. Let ≤, →1 ⊆ A ×A, `, →2 ⊆ A * ×A *
where `is the embedding order over (A, ≤) and →2 is such that if s →2 t then: s and t are of the form s = ū a v, t = ū b v where b = b1 • • • bm such that a →1 bz for every z ∈ [1..m]. Then, if (A, ≤) is a wqo which is rdc with →1, then (A * , `) is a wqo which is rdc with →2.

We can apply this proposition by taking →1 as , ≤ as ≺, and taking that a ConfT configuration can be seen as an element of (ConfN ) * by sorting the set by the lexicographic order on the first component (i.e., the node's position on the tree), and vice versa every element of (ConfN ) * can be seen as an element from ConfT . We instantiate →2 to be t as it verifies the conditions demanded for →2. As a result we have that (ConfT , t ) is rdc w.r.t. (ConfT , `) and the condition (1) of Proposition 3.3 is met.

As already mentioned, the transition t does not need to have infinite branching. This is just a consequence of the fact that the t -image of any configuration has only a finite number of configurations up to isomorphism of the data values contained (remember that only equality between data values matters), and representatives for every class are effectively computable. We can then take t 2 ⊂ t to have only one representative element for each class of equivalence and it then follows that the reachable classes of equivalence of t and t 2 are the same. Hence, we have that condition (2) from Proposition 3.3 is also met. Finally, condition (3) holds as `is a wqo (by Proposition 3.4) that is computable. We can then apply Proposition 3.3 and it follows that the reachability and non-emptiness problems are decidable. Indeed, an ATRA(guess, spread) M is non-empty iff there exists an element of the finite basis of ↑ Succ * ({ ε, α, (a, d0), { qI , d0 } }) -for any fixed d0 and some α ∈ { , ¯ } × {£, £} and a ∈ Σ-in which every node configuration has an empty set of threads.

DECIDABILITY OF XPATH

This section is mainly dedicated to the decidability of the satisfiability problem for a fragment of XPath with downward and rightward axes known as 'forward-XPath'. This is proved by a reduction to the ATRA(guess, spread) nonemptiness problem.

Definitions

We consider a fragment of the navigational part of XPath 1.0 with data equality and inequality. In particular this logic is here defined over data trees. However, an xml document may typically have not one data value per node, but a set of attributes, each carrying a data value. This is not a problem since every attribute of an xml element can be encoded as a child node in a data tree labeled by the attribute's name. Thus, all the decidability results hold also for XPath with attributes over xml documents.

Let us define a simplified syntax for this logic. XPath is a two-sorted language, with path expressions (α, β, . . . ) and node expressions (ϕ, ψ, . . . ). We write XPath(O) to denote the data-aware fragment with the set of axes O ⊆ {↓, ↓ * , →, → * , ←, * ←, ↑, ↑ * }. It is defined by mutual recursion as follows,

α, β ::= o | [ϕ] | αβ | α ∪ β o ∈ O ∪ {ε} ϕ, ψ ::= a | ¬ϕ | ϕ ∨ ψ | ϕ ∧ ψ | α | α = β | α = β
where a ∈ Σ, and Σ is a finite alphabet. A formula of XPath(O) is either a node expression or a path expression. We define the 'forward' set of axes as F := {↓, ↓ * , →, → * }, and consequently the fragment 'forward-XPath' as XPath(F). We also refer by XPath -(F) to the fragment considered in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] where data tests are of the restricted form ε = α or ε = α. 2 There have been efforts to extend XPath to have the full expressivity of MSO, e.g. by adding a least fix-point operator (cf. [3, Sect. 4.2]), but these logics generally lack clarity and simplicity. However, a form of recursion can be added by means of the Kleene star, which allows us to take the transitive closure of any path expression. Although in general this is not enough to already have MSO [START_REF] Balder Ten | XPath, transitive closure logic, and nested tree walking automata[END_REF], it does give an intuitive language with counting ability. By regXPath(O) we refer to the enriched language where path expressions are extended by allowing the Kleene star on any path expression.

α, β :: [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] refers to XPath -(F) as 'forward XPath'. Here, 'forward XPath' is the unrestricted fragment XPath(F).

= o | [ϕ] | αβ | α ∪ β | α * o ∈ O ∪ {ε} 2
Let T = P, σ be a data tree. The semantics of XPath is defined as the set of elements (in the case of node expressions) or pairs of elements (in the case of path expressions) selected by the expression. The data aware expressions are the cases α = β and α = β.

[[→]]

T := {(xi, x(i + 1)) | x(i + 1) ∈ P } [[↓]] T := {(x, xi) | xi ∈ P } [[α * ]] T := the reflexive transitive closure of [[α]] T [[ε]] T := {(x, x) | x ∈ P } [[αβ]] T := {(x, z) | ∃y.(x, y) ∈ [[α]] T , (y, z) ∈ [[β]] T } [[[ϕ]]] T := {(x, x) | x ∈ [[ϕ]] T } [[α ∪ β]] T := [[α]] T ∪ [[β]] T [[¬ϕ]] T := P \ [[ϕ]] T [[ α ]] T := {x ∈ P | ∃y.(x, y) ∈ [[α]] T } [[ϕ ∨ ψ]] T := [[ϕ]] T ∪ [[ψ]] T [[α = β]] T := {x ∈ P | ∃y, z.(x, y) ∈ [[α]] T , (x, z) ∈ [[β]] T , π2(σ(y)) = π2(σ(z))} [[ϕ ∧ ψ]] T := [[ϕ]] T ∩ [[ψ]] T [[α = β]] T := {x ∈ P | ∃y, z.(x, y) ∈ [[α]] T , (x, z) ∈ [[β]] T , π2(σ(y)) = π2(σ(z))} [[a]] T := {x ∈ P | π1(σ(x)) = a}
For instance, in the model of Fig. 1,

[[ ↓ * [b ∧ ↓ [b] =↓ [b]] ]] T = { , 1, 12}.
We define sub(ϕ) to denote the set of all subformulae of ϕ, psub(ϕ) := {α | α ∈ sub(ϕ), α is a path expression}, and nsub(ϕ) := {ψ | α ∈ sub(ϕ), ψ is a node expression}.

Primary key. It is worth noting that XPath(F) -contrary to XPath -(F)-can express unary primary key constraints. That is, whether for some symbol a, all the a-elements in the tree have different data values. Lemma 4.1. For every a ∈ Σ let pk(a) be the property over a tree T = P, σ : "For every two different positions p, p ∈ P of the tree, if π1(p) = π1(p ) = a, then π2(p) = π2(p )". Then, pk(a) is expressible in XPath for any a.

Proof. It is easy to see that the negation of this property can be tested by first guessing the closest common ancestor of two different a-elements with equal datum in the underlying 'first child'-'next sibling' binary tree coding. At this node, we verify the presence of two a-nodes with equal datum, one accessible with a "↓ * " relation and the other with a compound "→ + ↓ * " relation (hence the nodes are different). The expressibility of the property then follows from the logic being closed under negation. The reader can check that the following formula expresses the property, where '↓ + ' = '↓↓ * ' and '→ + ' = '→→ * '.

pk(a) ≡ ¬ ↓ * [ ε[a] =↓ + [a] ∨ ↓ * [a] =→ + ↓ * [a] ]

Reduction to ATRA non-emptiness

In this section we show how satisfiability of forward-XPath can be decided with the help of the automata model introduced in Section 3. First let us fix some nomenclature. Definition 4.1. We say that a class of automata S captures a logic L iff there exists a translation t : L → S such that for every ϕ ∈ L and data tree T , we have that T verifies ϕ if and only if t(ϕ) has an accepting run over T . [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] shows that ATRA captures the fragment 'XPath -(F)'. It is immediate to see that ATRA can easily capture the Kleene star operator on any path formula, obtaining decidability of regXPath -(F). However, these decidability results cannot be generalized to the full unrestricted forward fragment XPath(F) as ATRA is not powerful enough to capture the expressivity of the logic. It cannot express, for instance, that there are two different leaves with the same data value. Unfortunately, the model ATRA(guess, spread) introduced in this article can neither capture XPath(F). Concretely, data tests of the form ¬(α = β) are impossible to perform for ATRA(guess, spread) as this would require -in some sensethe ability to guess two disjoint sets of data values S1, S2 such that all α-paths lead to a data value of S1, and all β-paths lead to a data value of S2. Still, in the sequel we show that there exists a reduction from the satisfiability of regXPath(F) to the emptiness of ATRA(guess, spread). This result settles an open question regarding the decidability of the satisfiability problem for the forward-XPath fragment: XPath(F). The main results that will be shown in Section 4.3 are the following. Theorem 4.1. Satisfiability of regXPath(F) in the presence of DTDs and unary primary key constraints is decidable, non primitive recursive.

And hence the next corollary follows from the logic being closed under boolean operations.

Corollary 4.1. The query containment and the query equivalence problems are decidable for XPath(F).

Moreover, these decidability results hold for regXPath(F) and even for two extensions:

• a navigational extension with upward axes (in Section 4.4), and • a generalization of the data tests that can be performed (in Section 4.5).

Allowing arbitrary data tests

This section is devoted to the proof of the following statement.

Proposition 4.1. For every η ∈ regXPath(F) there exists an effectively computable ATRA(guess, spread) automaton M such that M is non-empty iff η is satisfiable.

The proof can be sketched as follows:

• We define a strategy of evaluation consisting of a restriction of the transition t of ATRA(guess, spread) that is referred to as t • ⊆ t . This strategy verifies that there exists an accepting run under t iff there exists an accepting run under t

• . • We give a translation from forward XPath formulae to ATRA(guess, spread) automata such that (1) any tree accepted by the automaton M with the evaluation strategy t

• verifies the XPath formula η, and (2) any tree verified by the formula η is accepted by the automaton M .

Intuitively, t

• is the restriction of t to a finitely branching transition system, where each data value introduced non deterministically (either from a guess or from a → or →£ transition) verifies that either it already existed in the current node configuration, or it has not appeared so far along the whole execution of the automaton. Note that with this semantics the automaton accepts strictly less data trees. However, this can be done preserving the existence of data trees with accepting runs since from an accepting t sequence one can construct a similar accepting t

• sequence.

Indeed, for any data tree T accepted under the t semantics, there is another data tree T , that only differs in T in the data values of some nodes, which is accepted both under the t • semantics and the t semantics. A similar restriction applies for ρ = pi, . . . →£ τ and θ(p(i + 1), 1). Finally, ρ = p, . . . →ε τ applies only if either 1. a non-guess transition is performed; 2. a guess transition is performed and a data value already in data(ρ) is guessed; or 3. a guess transition is performed and the guessed data value is θ(p, imin), where

imin = min{i | θ(p, i) ∈ data(ρ)}.
We note this restriction of t by t • .

The following lemma follows from the definition above(see the Appendix for more details).

Lemma 4.2. Let M be an ATRA(guess, spread). M has an accepting run under t iff it has an accepting run under t • .

Based on the semantics of t • , we define a translation from regXPath(F) formulae to ATRA(guess, spread) automata. Let η be a regXPath(F) formula and let M be the corresponding ATRA(guess, spread) automaton defined by the translation.

We show that (i) if a data tree T is accepted by M under the t

• strategy, then T verifies η, and (ii) if a data tree T verifies η, then T is accepted by M (under t ). The emptiness problem for M under t and t

• are equivalent as already discussed, and thus Proposition 4.1 follows.

The translation

Let η be a regXPath(F) node expression in negated normal form (nnf for short). For succinctness and simplicity of the translation, we assume that η is in a normal form such that the ↓-axis is interpreted as the leftmost child. To obtain this normal form, it suffices to replace every appearance of '↓' by '↓→ * '. For every path expression α ∈ psub(η), consider a deterministic complete finite automaton Hα over the alphabet Ση = {ϕ | ϕ ∈ nsub(η)} ∪ {↓, →} which corresponds to that regular expression. We assume the following names of its components: Hα = Ση, δα, Qα, 0, Fα , with Qα ⊂ N the finite set of states and 0 ∈ Qα the initial state. We next show how to translate η into an ATRA(guess, spread) automaton M . For the sake of readability we define the transitions as positive boolean combinations of ∨ and ∧ over the set of basic tests and states. Any of these -take for instance δ(q) = (set(q1) ∧ q2) ∨ (q3 ∧ ā)-can be rewritten into an equivalent ATRA with at most one boolean connector per transition (as in Definition 3.1) in polynomial time. The most important cases are those relative to the following data tests:

1. α = β 2. α = β 3. ¬(α = β) 4. ¬(α = β)
We define the ATRA(guess, spread) automaton

M := Σ, Q, (|ϕ| ), δ with
Q := {(|ϕ| ), (|α| ) C,i , (|α| ) F , (|α, β| ) C,i,E,j | ϕ ∈ nsub ¬ (η), α, β ∈ psub ¬ (η), ∈ {=, =, ¬=, ¬ =}, i ∈ Qα, C ⊆ Qα, j ∈ Q β , E ⊆ Q β }
where op ¬ is the smallest superset of op closed under negation under nnf, i.e., if ϕ ∈ op ¬ (η) then nnf(¬ϕ) ∈ op ¬ (η). The sets C, E are not essential to understand the general construction, and they have as only purpose to disallow nonmoving loops in the definition of δ. As an example we first take care of the boolean connectors and the simplest tests.

δ((|a|

)) := a δ((|ϕ ∨ ψ| )) := (|ϕ| ) ∨ (|ψ| ) δ((|¬a| )) := ā δ((|ϕ ∧ ψ| )) := (|ϕ| ) ∧ (|ψ| )
The tests α and ¬ α are coded in a standard way, see [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] for more details. Here we focus on the data-aware cases.

Using the guess operator, we can easily define the cases corresponding to the data test cases 1 and 2 as follows. Here, (|α| ) F holds at the endpoint of a path matching α.

δ((|α = β| )) := guess((|α, β| ) = ) δ((|α, β| ) = ) := (|α| ) = ∅,0 ∧ (|β| ) = ∅,0 δ((|α| ) = F ) := eq δ((|α = β| )) := guess((|α, β| ) = ) δ((|α, β| ) = ) := (|α| ) = ∅,0 ∧ (|β| ) = ∅,0 δ((|α| ) = F ) := eq
We define the transitions associated to each Hα, for i ∈

Qα, C ⊆ Qα, ∈ {=, =}. δ((|α| ) C,i ) := ϕ∈nsub(α), i :=δ α (ϕ,i), i ∈C (|ϕ| ) ∧ (|α| ) C∪{i },i ∨ (|α| ) ∅,δα(↓,i) ∨ £(|α| ) ∅,δα(→,i) ∨ i∈Fα (|α| ) F
The test case 4 involves also an existential quantification over data values. In fact, ¬(α = β) means that either [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] there are no nodes reachable by α, or (2) there are no nodes reachable by β, or (3) there exists a data value d such that both (a) all elements reachable by α have datum d, and (b) all elements reachable by β have datum d.

δ((|¬α = β| )) := (|¬ α | ) ∨ (|¬ β | ) ∨ guess((|α, β| ) ¬ = ) δ((|α, β| ) ¬ = ) := (|α| ) ¬ = ∅,0 ∧ (|β| ) ¬ = ∅,0 δ((|α| ) ¬ = F ) := eq δ((|α| ) ¬= F ) := eq δ((|α| ) ¬ C,i ) := ϕ∈nsub(α), i :=δ α(ϕ,i), i ∈C ((| φ| ) ∨ (|α| ) ¬ C∪{i },i ) ∧ ( ¯ ? ∨ (|α| ) ¬ ∅,δα(↓,i) ) ∧ ( £? ∨ £(|α| ) ¬ ∅,δα(→,i) ) ∧ i∈Fα (|α| ) ¬ F
where φ stands for nnf(¬ϕ).

The difficult part is the translation of the data test case 3. The main reason for this difficulty is the fact that ATRA automata do not have the expressivity to make these kinds of tests. An expression ¬(α = β) forces the set of data values reachable by an α-path and the set of those reachable by a β-path to be disjoint. We show that nonetheless the automaton can test for a condition that is sat-equivalent to ¬(α = β). Suppose first that η = ¬(↓ α =→ β) is to be checked for satisfiability. One obvious answer would be to test separately α and β. If both tests succeed, we can then build a model satisfying η out of the two witnessing trees by making sure they have disjoint sets of values. Otherwise, η is clearly unsatisfiable. Suppose now that we have η = ϕ ∧ ¬(↓ α =→ β), where ϕ is any formula with no data tests of type 3. One could build the automaton for ϕ and then ask for "spread((| ↓ α| ) ¬= 0 ∨ (| → β| ) ¬= 0 )" in the automaton. This corresponds to the property "for every data value d taken into account by the automaton (as a result of the translation of ϕ), either all elements reachable by α do not have datum d, or all elements reachable by β do not have datum d". If ϕ contains a α = β formula, this translates to a guessing of a witnessing data value d. Then the use of spread takes care of this particular data value, and indeed of all other data values that were guessed to satisfy similar demands. In other words, it is not because of d that ¬(↓ α =→ β) will be falsified. But then, the t • semantics ensures that no pair of nodes accessible by α and β share the same datum. This is the main idea we encode next. Here, spread(q) := q ∈Q spread(q , q), and we define δ((|¬(α = β)| )) := (|α, β| ) ¬= ∅,0,∅,0 . Given ¬(α = β), the automaton systematically looks for the closest common ancestor of every pair (x, y) of nodes accessible by α and β respectively, and tests, for every data value d in the node configuration, that either (1) all data values accessible by the remaining path of α are different from d, or (2) all data values accessible by the remaining path of β are different from d.

δ((|α, β|

) ¬= C 1 ,i,C 2 ,j ) := spread (|α| ) ¬= ∅,i ∨ (|β| ) ¬= ∅,j ∧ (|α, β| ) ¬= ∅,δα(↓,i),∅,δ β (↓,j) ∧ £(|α, β| ) ¬= ∅,δα(→,i),∅,δ β (→,j) ∧ i∈Fα (|β| ) ¬= ∅,j ∧ j∈Fα (|α| ) ¬= ∅,i ∧ ϕ∈nsub(α), i :=δ α (ϕ,i), i ∈C 1 ((| φ| ) ∨ (|α, β| ) ¬= C 1 ∪{i },i ,C 2 ,j ) ∧ ϕ∈nsub(β), j :=δ β (ϕ,j), j ∈C 2 ((| φ| ) ∨ (|α, β| ) ¬= C 1 ,i,C 2 ∪{j },j )
The following lemmas then follow from the discussion above.

Lemma 4.3. For any data tree T , if T verifies η, then M accepts T under the t semantics. Proof of Theorem 4.1. By Proposition 4.2, satisfiability of regXPath(F) is reducible to the nonemptiness problem for ATRA(guess, spread). On the other hand, we remark that ATRA(guess, spread) automata can code any regular tree language -in particular a DTD, the core of XML Schema, or Relax NG-and are closed under intersection by Proposition 3.2. Also, the logic can express any unary primary key constraint as stated in Lemma 4.1. Hence, by Theorem 3.1 the decidability follows.

It is known that even much simpler fragments of XPath have non primitive recursive complexity [START_REF] Figueira | Future-looking logics on data words and trees[END_REF].

Allowing upward axes

Here we explore one possible decidable extension to the logic regXPath(F), whose decidability can be reduced to that of ATRA(guess, spread).

Consider the data test expressions of the types

¬(α b = β f ) and ¬(α b = β f )
where β f ∈ regXPath(F) and α b ∈ regXPath(B), with B := {↑, ↑ * , ←, * ←}. We can decide the satisfaction of these kinds of expressions by means of the spread(•, •), using carefully its first parameter to select the desired threads from which to collect the data values we are interested in. Intuitively, along the run we throw threads that save current data value and try out all possible ways to verify α r b ∈ regXPath(F), where Furthermore, α b need not be necessarily in regXPath(B), as its intermediate node tests can be formulae from regXPath(F). More formally, let regXPath B (F) be the fragment of regXPath(F ∪ B) defined by the grammar

ϕ, ψ ::= ¬a | a | ϕ ∧ ψ | ϕ ∨ ψ | α f | α b | α f β f | ¬(α f β f ) | ¬(α b = β f ) | ¬(α b = β f )
with ∈ {=, =}, a ∈ Σ, and

α f , β f ::= [ϕ] | α f β f | o α f | (α f ) * o ∈ {↓, →, ε}, α b , β b ::= [ϕ] | α b β b | o α b | (α b ) * o ∈ {↑, ←, ε}.
We must note that regXPath B (F) contains the full dataunaware fragment (i.e., with no data tests) of regXPath(B), and that it is not closed under negation. In fact, were it closed under negation, its satisfiability would be undecidable. As mentioned, we can decide the satisfiability problem for this fragment.

Theorem 4.2. Satisfiability for regXPath B (F) under primary key constraints and DTDs is decidable. Note that now we can express α = β as { {α∼, β∼} } and α = β as { {α∼, β ∼} }. Let us call regXPath + (F) to regXPath(F) extended with the construction just explained. This is a more expressive formalism since the first mentioned property -or, to give another example,

Allowing stronger data tests

{ {↓ * [a]∼, ↓ * [b]∼, ↓ * [a] ∼, ↓ * [b] ∼} }- is not expressible in regXPath(F).
We argue that satisfiability for this extension can be decided in the same way as for regXPath(F). It is straightforward to see that positive appearances can easily be translated with the help of the guess operator. On the other hand, for negative appearances, like ¬{ {α1s1, . . . , αnsn} }, we proceed in the same way as we did for regXPath(F). The only difference being that in this case the automaton will simulate the simultaneous evaluation of the n expressions and calculate all possible configurations of the closest common ancestors of the endpoints, performing a spread at each of these intermediate points.

Theorem 4.3. Satisfiability of regXPath + (F) under primary key constraints and DTDs is decidable.

TEMPORAL LOGICS ON DATA WORDS

The logic LTL ↓ (X, F, U) is a logic for data words that corresponds to the extension of the Linear Temporal Logic LTL(X, F, U) with the ability to use one register for storing a data value for later comparisons. Here, a data word is understood as a non-branching data tree. More formally, sentences are defined

ϕ, ψ ::= a | ↓ ϕ | ↑ | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | Xϕ | Fϕ | U(ϕ, ψ) | | ⊥
where a ∈ Σ. Here, X is the next element operator, F is the future operator (i.e., the transitive closure of X), and U(ϕ, ψ) is the until operator stating that we can move forward by elements satisfying ψ until an element satisfying ϕ is reached. We denote by X, G and Ū the respective dual operators of X, F, and U. These are such that ¬Xϕ ≡ X¬ϕ, ¬Fϕ ≡ G¬ϕ and ¬U(ϕ, ψ) ≡ Ū(¬ϕ, ¬ψ), and hence enables us to work with sentences in negated normal form (nnf) without loss of generality. With the operator ↓ we store the current datum in the register and continue the evaluation of the formula, and with the operator ↑ we test current data value against the one stored in the register. In this logic we can express properties like "for every a element there is a future b element with the same data value" as G(¬a ∨ ↓ (F(b ∧ ↑))).

This logic has been studied in [START_REF] Demri | On the freeze quantifier in constraint LTL: Decidability and complexity[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] where satisfiability and expressivity issues have been addressed. [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] established that the satisfiability problem for LTL ↓ (X, F) and LTL ↓ (X, F, U) are decidable and non primitive recursive on data words. It was also shown that the two way extension LTL ↓ (X, F, F -1 ) is undecidable over data words and, similarly, that the extension to having two registers is undecidable. 3 The decidability results have been established by means of the Alternating Register Automaton (ARA) that corresponds to the ATRA model evaluated on data words rather than data trees. Thus, we call ARA(guess, spread) our model evaluated over data words (we remark that ATRA can force the model to be linear by asking that everywhere ' £' must hold). This automaton corresponds to having only node configurations and →ε and → as only transitions. Then, the decidability of the emptiness problem immediately follows.

We propose the following logic for data words, which is an extension of LTL ↓ (X, U, F) with two other operators. The operator ∀ ↓ ≤ ϕ states that for all data value occurring in the data word at a previous position than the current one, ϕ must hold. The operator ∃ ↓ ≥ ϕ states that for some data value occurring at a future position of the data word, ϕ holds. However, we do not allow the dual operators ∀ ↓ ≥ or ∃ ↓ ≤ as this results in an undecidable logic, so we deal with a logic with much added expressive power but that is not closed under negation. In this context, the 'forward' operators are F := {U, Ū, F, G, X, X}. By LTL ↓ nnf (O) we denote the logic restricted to the operators O considering that the formulae are in negated normal form. It is not hard to see that we can then code LTL ↓ nnf (F, ∀ ↓ ≥ , ∃ ↓ ≤ ) into ARA(guess, spread). 4 We 3 What is more, all the lower bounds hold even in the absence of the X modality [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. 4 Note that this logic already contains LTL ↓ (X, U, F).

then obtain the following results.

Theorem 5.1. Let ∃ ↓ < be the operator ∃ ↓ ≤ restricted only to the data values occurring strictly before the current point of evaluation. Then, on finite data words:

(i) satisfiability of LTL ↓ nnf (F, G, ∃ ↓ < ) is undecidable; (ii) satisfiability of LTL ↓ nnf (F, G, ∀ ↓ ≥ ) is undecidable; and (iii) satisfiability of LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ) is decidable.
Proof. To prove (i) and (ii) we show that these logics can code an accepting run of a 2-counter Minsky Automaton, that is known to be undecidable. For this, we build on some previous results [START_REF] Figueira | Future-looking logics on data words and trees[END_REF] showing that LTL ↓ nnf (F, G) can code some weak notion of counter automaton 5 where a decrement instruction can always be applied, even to a counter with value 0, in which case the counter's value remains unchanged. Here data values are used to ensure that, along the run, every increment instruction occurring before a test for zero has a corresponding decrement in between. In this coding, an increment is linked to a decrement of the same counter by means of sharing the same data value. We show that both LTL ↓ nnf (F, G, ∃ ↓ < ) and LTL ↓ nnf (F, G, ∀ ↓ ≥ ) can ensure that for every decrement there is a previous increment with the same data value. Hence, in this case we are coding an accepting run of a Minsky Automaton, where decrements cannot be performed to non-positive counters, and with an undecidable emptiness problem. Let us see how.

(i) The LTL ↓ nnf (F, G, ∃ ↓ < ) formula G(deci → ∃ ↓ < ↑
) states that the data value of every decrement must not be new, and in the context of this coding this means that it must have been introduced by an increment instruction. (ii) The LTL ↓ nnf (F, G, ∀ ↓ ≥ ) formula ∀ ↓ ≥ (F(deci∧ ↑) → F(inci∧ ↑)) evaluated at the first element of the data word expresses that for every data value: if there is a decrement with that value, then there is an increment with that value. It is then easy to ensure that they appear in the correct order (first the increment, then the increment).

The addition of any of these conditions to the coding of [START_REF] Figueira | Future-looking logics on data words and trees[END_REF] results in a coding of an n-counter Minsky Machine, whose emptiness problem is undecidable.

The item (iii) is a consequence of Theorem 5.2 stated below.

Corollary 5.1. The finitary satisfiability problem for both

LTL ↓ nnf (F, ∃ ↓ ≤ ) and LTL ↓ nnf (F, ∀ ↓ ≥ ) are undecidable. Proof. Condition (i) can be also coded in LTL ↓ nnf (F, ∃ ↓ ≤ ) as G(X(deci) → ∃ ↓ ≤ (X ↑))
. 5 This automaton is called Incrementing Counter Automaton, and can equivalently be seen as a a counter automaton where counters may have faulty increments along the run.

Theorem 5.2. For every formula ϕ

∈ LTL ↓ nnf (F, ∀ ↓ ≤ , ∃ ↓ ≥ )
there exists an effectively computable ARA(spread, guess) M such that for every data word w, w satisfies ϕ iff M accepts w.

Proof. The translation for LTL ↓ nnf (F) is like the one presented in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] and presents no complications whatsoever. For the coding of the ∀ ↓ ≤ operator, we first make sure to maintain all the data values seen so far as threads of the configuration. We can do this easily. δ(q1) := set(q2) δ(q2) := ( ¯ ? ∨ q1) ∧ qsave δ(qsave) := ¯ ? ∨ qsave Now we can assume that at any point of the run, we maintain the data values of all the previous elements of the data word as threads qsave, d . Note that these threads are maintained until the last element of the data word, at which point the test ¯ ? is satisfied and they are accepted. At the last element we cannot be sure to have the qsave threads with the data needed, but this is not a problem. In fact, a ∀ ↓ ≤ operator evaluated at the last element of a word can be simulated without using the ∀ ↓ ≤ , as the last element is a distinguished one. That is, a formula ∀ ↓ ≤ ( X⊥ ∧ ϕ) results in the same automaton as the translation of G(↓ F( X⊥ ∧ ϕ)). Then, for the inner nodes we translate a formula ∀ ↓ ≤ (X ∧ ϕ) as δ(q) := ? ∧ spread(qsave, qϕ), where qϕ codes the formula ϕ.

On the other hand, a formula like ∃ ↓ ≥ ϕ is simply translated as δ(q) = guess(q ) with δ(q ) = qϕ ∧ q F↑ , where qϕ is the translation of ϕ and q F↑ is the translation of F ↑.

Moreover, we argue that these extensions add expressive power.

Proposition 5.1. On finite data words:

(i) The logic LTL ↓ nnf (F, ∀ ↓ ≤ ) is strictly more expressive than LTL ↓ nnf (F); (ii) The logic LTL ↓ nnf (F, ∃ ↓ ≥ ) is strictly more expressive than LTL ↓ nnf (F).
Proof. (i) follows from the proof of Proposition 3.1 and the fact that ATRA captures LTL ↓ nnf (F).

For (ii), we propose to consider the property "there exists a future data value d such that all the positions labeled with a have data values different from d". This can be expressed by the formula ∃ ↓ ≥ G(a → ¬ ↑). However, we argue that this property cannot be expressed by a LTL ↓ nnf (F) formula.

CONCLUDING REMARKS

We presented a simplified framework to work with 1-way alternating register automata on data words andtrees, enabling the possibility to easily show decidability of new operators by proving that they preserve the downward compatibility of a well-structured transition system. It would be interesting to hence explore more decidable extensions, to study the expressiveness limits of decidable logics and automata for data trees.

Also, this work argues in favor of exploring models that although they might be not closed under all boolean operations, can serve to show decidability of logics closed under negation -such as forward-XPath-or expressive natural extensions of existing logics-such as LTL ↓ nnf (F, ∃ ↓ ≥ , ∀ ↓ ≤ ). As a ≤ a and ≤ is rdc with →1, one possibility is that for each a →1 bz we can apply a a →1 b z with b z ≤ bz. In this case we obtain ū av →2 ū b v `ū bv. The only case left to analyze is when, for some a →1 bz the compatibility is reflexive, that is, a ≤ bz. But then we take a reflexive compatibility as well, the reader can check that in this case ū a v `ū bv.

Finally, in the case where a has no pre-image is only easier as we can take the exact same element.

Proof of Lemma 4.2. Any t step shot by a →ε, → , or →£ from a node configuration ρ leading to τ can be reproduced by t

• from an isomorphic copy ρ of ρ leading to an isomorphic copy of τ which is in the same relation to ρ as τ is to ρ. This can be safely done without any collateral effects as the executions of two different node configurations p, . . . , p , . . . have no interference one with another and are completely independent. The fact of whether one node configuration takes a data value that happens to be equal or not to a data value of another configuration no impact whatsoever in the execution. It suffices to examine the definition to see that t

• depends on the transitions → , →£ and →ε of the node configurations.

C. EXPRESSIVITY

Proof of Proposition 3.1, item (a). We show an example of the expressiveness that guess adds to ATRA. We force two incomparable nodes to have the same data value without any further data constraint. Note that this datum does not necessarily has to appear at some common ancestor of the nodes. Consider the ATRA(guess) defined over Σ = {a} with δ(q0) = guess(q1), δ(q1) = q2, δ(q2) = q3 ∧ q4, δ(q3) = q5, δ(q4) = £q5, δ(q5) = eq.

Consider the two data trees of Fig 4. It is easy to see that for any ATRA, either both are accepted, or both rejected. However, the ATRA(guess) we just built distinguishes them.

D. FORMAL SEMANTICS OF LTL WITH REGISTERS

LTL ↓ n (U, X) is the Linear Temporal Logic with the freeze quantifier (↓i), test predicate (↑i) and next (X) and until (U) temporal operators studied in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Demri | On the freeze quantifier in constraint LTL: Decidability and complexity[END_REF]. As it was shown in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], LTL ↓ n (U, X) is undecidable as soon as n > 1. We will then focus on the language that uses only one register: LTL ↓ (U, X). We study an extension of this language with a restricted form of quantification over data values. We will actually add two sorts of quantification. On the one hand the ∀ ↓ ≤ and ∃ ↓ ≤ quantifies universally or existentially over all the data values occurred before the current point of evaluation. Similarly, ∀ ↓ ≥ and ∃ ↓ ≥ quantifies over the future elements on the data word. For our convenience and wlog, we will work in Negated Normal Form (nnf), and we use Ū to denote the dual operator of U, and similarly for X. Sentences of LTL ↓ 1 (U, Ū, X, X, O), where O ⊆ {∀ ↓ ≤ , ∃ ↓ ≤ , ∀ ↓ ≥ , ∃ ↓ ≥ } are defined:

ϕ ::= a | ¬a |↑| ¬ ↑|↓ ϕ | Xϕ | Xϕ | U(ϕ, ϕ) | Ū(ϕ, ϕ) | op ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ
where a is a symbol from a finite alphabet Σ, and op ranges over O. For economy of space we will write LTL ↓ nnf (F, O) to denote this logic 6 .

A data word is an element from (Σ × D) * , where Σ is a finite set of symbols, and D is an infinite domain of data values. For simplicity and wlog we can assume that D = N. Given a data word σ, we write σ[i] for the ith element (pair) of the word, and π1, π2 for the projections on Σ and D. We show next the most significant cases of the definition of the satisfaction relation |=: where 1 ≤ i ≤ |σ|. We say that ϕ satisfies σ, written σ |= ϕ, if σ, 1 |= d 0 ϕ with d0 = π2(σ [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]). Notice that the future modality can be defined Fϕ := U(ϕ, ) ∨ ϕ and its dual G as the nnf of ¬F¬ϕ, provided that ϕ ∈ LTL ↓ nnf (F).

(σ, i) |= d a iff π1(σ[i]) = a (σ, i) |= d ↑ iff d = π2(σ[i]) (σ, i) |= d ↓ ϕ iff (σ, i) |= π 2 (σ[i]

Figure 1 :Figure 2 :

 12 Figure 1: A data tree. a, 0 b, 0

Proposition 3 . 1 .

 31 (a) ATRA(guess) has more expressive power than ATRA; (b) ATRA(spread) has more expressive power than ATRA.

Figure 3 :

 3 Figure 3: A property not expressible in ATRA.

Proposition 3 .

 3 3. ([10, Proposition 5.4]) If (A, ≤) is a wqo and (A, →) a transition system such that (1) it is rdc, (2) it is effective, and (3) ≤ is decidable; then for any a ∈ A it is possible to compute a finite set A ⊆ A such that ↑ A = ↑ Succ * (a). Theorem 3.1. Non-emptiness of ATRA(guess, spread) is decidable.

Lemma 3 .

 3 1. (ConfN , ≺) is a well quasi-order. Let := →ε ∪ → ∪ →£ ⊆ ConfN × ConfN . The core of this proof is centered in the following lemma. Lemma 3.2. (ConfN , ≺) is reflexive downward compatible (rdc) with respect to .

Definition 4 . 2 .

 42 Let us fix θ : N * × N → D an injective map. Consider the restriction where ρ = p, . . . → τ applies only if 1. τ introduces a data value already in data(ρ), or 2. if it introduces the value θ(p1, 1).

Lemma 4 . 4 .

 44 For any data tree T , if M accepts T under the t• semantics, then T verifies η. Lemmas 4.3 and 4.4 together with Lemma 4.2 conclude the proof of Proposition 4.1. We then have that Theorem 4.1 holds.

•

  r stands for the reverse of the regular expression. Let the automaton arrive at a configuration (|α b | ), d whenever α r b is verified. This signals that there is a backwards path from the current node in the relation α b that arrives at a node with data value d. Hence, at any given position, the instruction spread((|α b | ), (|α f | ) ¬ ) translates correctly the expression ¬(α b β f ).

  Consider the property "there are three descendant nodes labeled a, b and c with the same data value". That is, there exists some data value d such that there are three nodes accessible by ↓ * [a], ↓ * [b] and ↓ * [c] respectively, all carrying the datum d. Let us denote the fact that they have the same or different datum by introducing the symbols '∼' and ' ∼', and appending it at the end of the path. Then in this case we write that the elements must satisfy ↓ * [a]∼, ↓ * [b]∼, and ↓ * [c]∼. We then introduce the node expression { {α1s1, . . . , αnsn} } where αi is a path expression and si ∈ {∼, ∼} for all i ∈ [1..n]. Semantically, it is a node expression that denotes all the tree positions p from which we can access n nodes p1, . . . , pn such that there exists d ∈ D where for all i ∈ [1..n] the following holds: (p, pi) ∈ [[αi]]; if si = ∼ then π2(σ(pi)) = d; and if si = ∼ then π2(σ(pi)) = d.

2 Figure 4 :

 24 Figure 4: Two indistinguishable data trees for ATRA.

  ) ϕ (σ, i) |= d U(ϕ, ψ) iff for some i ≤ j ≤ |σ|and for all i ≤ k < j we have (σ, j)|= d ϕ and (σ, k) |= d ψ (σ, i) |= d Xϕ iff i < |σ| and (σ, i + 1) |= d ϕ (σ, i) |= d ∃ ↓ ≥ ϕ iff there exists i ≤ j ≤ |σ| such that (σ, i) |= π 2 (σ[j]) ϕ (σ, i) |= d ∀ ↓ ≤ ϕ iff for all 1 ≤ j ≤ i we have (σ, i) |= π 2 (σ[j]) ϕ

here F is to mark that we have all the forward modalities: U, Ū, X, X, F, G

Acknowledgment. We acknowledge the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599.

B. MISSING PROOFS

Proof of Lemma 3.1. The fact that ≺ is a quasi-order (= reflexive and transitive) is immediate from its definition. To show that it is a well quasi-order, suppose we have an infinite sequence of configurations ρ1ρ2ρ3 • • • . It is easy to see that it contains an infinite subsequence τ1τ2τ3 • • • such that all its elements are of the form α0, (a0, d), T with • α0 and a0 fixed, and

where h T (d) = {q | q, d ∈ T }. This is because we can see each of these elements as a finite coloring, and apply the pigeonhole principle on the infinite set {ρi}i.

Consider then the function g

) for all C. By Dickson's Lemma ≺ † is a wqo, and then there are two τi = α0, (s0, di), Ti , τj = α0, (s0, dj), Tj , i < j such that Ti ≺ † Tj. For each C ⊂ Q, there exists an injective mapping fC :

as the latter set is bigger than the former by ≺ † . We define the desired injection f as the (disjoint) union of all fC's. In the case h T (di) = h T (dj) = ∅, we also define f (di) = dj. Hence, τi ≺ τj.

Proof of Proposition 3.4. The fact that (A * , `) is a wqo is given by Higman's Lemma. The rdc property with