Diego Figueira

Satisfiability of Downward XPath with Data Equality Tests *

Keywords: . I.7.2 [Document Preparation]: Markup Languages, H.2.3 [Database Management]: Languages, H.2.3 [Languages]: Query Languages General Terms. Algorithms, Languages Keywords. XML, XPath, unranked unordered tree, datatree, infinite alphabet, data values, BIP automaton

In this work we investigate the satisfiability problem for the logic XPath(↓ * , ↓, =), that includes all downward axes as well as equality and inequality tests. We address this problem in the absence of DTDs and the sibling axis. We prove that this fragment is decidable, and we nail down its complexity, showing the problem to be ExpTime-complete. The result also holds when path expressions allow closure under the Kleene star operator. To obtain these results, we introduce a new automaton model over data trees that captures XPath(↓ * , ↓, =) and has an ExpTime emptiness problem. Furthermore, we give the exact complexity of several downward-looking fragments.

Introduction

XPath is arguably the most widely used xml query language. It is implemented in XSLT and XQuery and it is used as a constituent part of several specification and update languages. XPath is fundamentally a general purpose language for addressing, searching, and matching pieces of an xml document. It is an open standard and constitutes a World Wide Web Consortium (W3C) Recommendation [START_REF] Clark | XML path language (XPath)[END_REF], implemented in most languages and xml packages.

Arguably the most important static analysis problem of a query language is that of optimization, which studies the problem of query containment and query equivalence. In logics closed by boolean operators, these problems reduce to satisfiability checking: does a given query express some property? I.e., is there a document where this query has a non-empty result? By answering this question 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. Moreover, this problem becomes crucial for many applications on security, type checking transformations, and consistency of xml specifications.

Core-XPath (introduced in [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 even in the presence of DTDs. We consider an extension of this language with the possibility to make equality and inequality tests between attributes of elements in the xml document. This logic is named Core-Data-XPath in [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF], and as shown in [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF], its satisfiability problem is undecidable. It is then reasonable to study the interaction between different navigational fragments of XPath with equality tests to be able to find decidable and computationally well-behaved fragments. In the present work, we focus on the downwardlooking fragments of XPath, where navigation between elements can only be done in the downward direction.

Our main contribution is that the satisfiability problem for XPath(↓ * , ↓, =) is decidable. This is the fragment with data equality and inequality tests, with the ↓ * axis that can access descendant nodes at any depth and the ↓ axis to access child elements. We prove a stronger result, showing the decidability of the satisfiability of regXPath(↓, =), which is the extension of XPath(↓ * , ↓, =) with the Kleene star operator to take reflexive-transitive closures of arbitrary path expressions. Moreover, we nail down the precise complexity showing an ExpTime decision procedure (recall that XPath(↓, ↓ * ) is already ExpTime-hard [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]). In order to do this, we introduce a new class of automata that captures all the expressivity of regXPath(↓, =). On the other hand, we prove that the fragment XPath(↓ * , =) without the ↓ axis is ExpTime-hard, even for a restricted fragment of XPath(↓ * , =) without unions of path expressions. This reduction can only be done by using data equality tests, as the corresponding fragment XPath(↓ * ) without unions is shown to be PSpace-complete. We thus prove that the satisfiability problem for XPath(↓ * , =), XPath(↓ * , ↓, =) and regXPath(↓, =) are all ExpTime-complete. Additionally, we present a natural fragment of XPath(↓ * , =) that is PSpace-complete. We complete the picture showing that satisfiability for XPath(↓, =) is also PSpace-complete. Altogether, we establish the precise complexity for all downward fragments of XPath with and without data tests (cf. Figure 4 in Section 6).

Related work

In [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] there is a study of the satisfiability problem for many XPath logics, mostly fragments without negation or without data equality tests. Also, the fragment XPath(↓, =) is proved to be in NExpTime. We improve this result by providing an optimal PSpace upper bound. It is also known that XPath(↓ ) is already PSpace-hard, and in this work we match the upper bound showing PSpace-completeness. Furthermore, in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] XPath(↓, ↓ * ) is proved ExpTime-complete. In this work we prove that this complexity is preserved in the presence of data values and even under closure with Kleene star. We also consider a fragment that is not mentioned in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]: XPath(↓ * , =) and show that XPath(↓ * ) is PSpace-complete while XPath(↓ * , =) is ExpTime-complete. In this case, data tests make a real difference in complexity.

First-order logic with two variables and data equality tests is investigated in [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF]. Although in the absence of data values F O 2 is expressive-equivalent to Core-XPath (cf. [START_REF] Marx | First order paths in ordered trees[END_REF]), F O 2 with data equality tests becomes incomparable with respect to all the data aware fragments treated here. [START_REF] 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 accessible by a 'one step' relation, and to data formulae of the kind ε = p (or =). However, most of the fragments we treat here disallow upward and sibling axes but allow the descendant ↓ * axis and arbitrary p = p data test expressions.

In [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF] a fragment of XPath(↓, ↓ * , →, → * , =) is treated, denominated 'forward XPath'. In the cited work, the full set of downward and rightward axes are allowed, while the fragments treated here only allow the downward axis. As in [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF], the language is restricted to data test formulae of the form ε = p contrary to the ones studied here, and hence no decidability results can be inferred. It is shown that its satisfiability problem is decidable, but with a non-primitive recursive algorithm, while in our work all the fragments considered are in ExpTime. The question of whether the forward fragment with arbitrary tests is decidable is still open.

Statement of the problem and main result 2.1 Data trees

The structure of an xml document can be seen as an unranked tree with attributes and data values in its nodes. We work with an abstraction that we call data tree, that is, an unranked finite tree where every node contains a symbol from a finite alphabet Σ and a data value from some infinite domain ∆. Below we show an example of a data tree with Σ = {a, b} and ∆ = N.

Example 1.

It is important to mention that this model has only one data value on each node, whilst an xml document element may typically have several (0 or more) attributes, each with a data value associated. We address this issue by coding each attribute element by a child as shown next.

<library> <book ID="5" title="Ficciones"> <author lastname="Borges"/> </book> </library>

In the above example the data values of the nodes tagged with non-attribute elements (library, book, author) may have any data value. For every fragment of XPath with the child axis (↓) we can enforce that attributes are leaves and we can translate any XPath expression on xml to an equivalent one on data trees. For the fragments with the single descendant axis ↓ * , this is not true anymore, but a more careful analysis shows that all complexity results still hold in this case. Indeed, any XPath(↓ * , =) formula on data trees can be seen as an XPath(↓ * , =) formula on xmls that makes use of only one fixed attribute, and we can thus transfer the lower bound (the upper bound follows from the more expressive fragment XPath(↓ * , ↓, =)). Summing up, all our forthcoming results also hold on arbitrary xml documents with multiple attributes per element. This implies, for example, that the results hold for the satisfiability problem for data trees that may have some nodes with no data values.

We use the standard representation of unranked trees by a nonempty, prefix-closed set T of elements from N * such that whenever x(i + 1) ∈ T then xi ∈ T ; together with a labeling function σ : T → Σ and a data value function δ : T → ∆. A data tree model T is then a tuple T, σ, δ , and we call Pos(T ) = T the set of positions of T . We denote by T | x the subtree of T with root x, and δ(T ) = {δ(x) | x ∈ Pos(T )}. In the Example 1 presented before, T = {ε, 1, 2, 11, 12, 121, 122, 123, 22}.

The logic XPath

We work with a simplification of XPath, stripped of its syntactic sugar. Actually, we consider fragments of XPath that correspond to the navigational part of XPath 1.0 with data equality and inequality. Let us give the formal definition of this logic. XPath is a two-sorted language, with path expressions (α, β, . . .) and node expressions (ϕ, ψ, . . .). The fragment XPath(O, =), with O ⊆ {↓, ↓ * } is defined by mutual recursion as follows:

α ::= o | α[ϕ] | [ϕ]α | αβ | α ∪ β o ∈ O ∪ {ε} ϕ ::= a | ¬ϕ | ϕ ∧ ψ | α | α β ∈ {=, =}, a ∈ Σ A formula of XPath(O, =
) is either a node expression or a path expression of the logic. XPath(O) is the fragment XPath(O, =) without the node expressions of the form α β.

There have been efforts to extend this navigational core of XPath in order to have the full expressivity of MSO, e.g. by adding a least fix-point operator (cf. [START_REF] Cate | The expressivity of XPath with transitive closure[END_REF]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 to take the transitive closure of any path expression. Although in general this is not enough to already have MSO -as shown in [START_REF] Cate | XPath, transitive closure logic, and nested tree walking automata[END_REF]-, it does give an intuitive language with counting ability. By regXPath(↓, =) we refer to the language where path expressions are extended

α ::= o | α[ϕ] | [ϕ]α | αβ | α ∪ β | α * o ∈ {↓, ε}
by allowing the Kleene star on any path expression. In terms of expressivity, we see that

XPath(↓ * , =) ⊂ XPath(↓ * , ↓, = ) ⊂ regXPath(↓, =) = regXPath(↓ * , ↓, =).
Let T = T, σ, δ , we define the semantics of XPath:

[[↓]] T = {(x, xi) | xi ∈ T } [[α * ]] T = the reflexive transitive closure of [[α]] T [[ε]] T = {(x, x) | x ∈ T } [[αβ]] T = {(x, z) | ∃y.(x, y) ∈ [[α]] T , (y, z) ∈ [[β]] T } [[α ∪ β]] T = [[α]] T ∪ [[β]] T [[α[ϕ]]] T = {(x, y) ∈ [[α]] T | y ∈ [[ϕ]] T } [[[ϕ]α]] T = {(x, y) ∈ [[α]] T | x ∈ [[ϕ]] T } [[a]] T = {x ∈ T | σ(x) = a} [[ α ]] T = {x ∈ T | ∃y.(x, y) ∈ [[α]] T } [[¬ϕ]] T = T \ [[ϕ]] T [[ϕ ∧ ψ]] T = [[ϕ]] T ∩ [[ψ]] T [[α = β]] T = {x ∈ T | ∃y, z.(x, y) ∈ [[α]] T , (x, z) ∈ [[β]] T , δ(y) = δ(z)} [[α = β]] T = {x ∈ T | ∃y, z.(x, y) ∈ [[α]] T , (x, z) ∈ [[β]] T , δ(y) = δ(z)} For instance, in the model of Example 1, [[ ↓ * [b∧ ↓ [b] =↓ [b]] ]] T = {ε, 1, 12}.
We now state the problem we will address. Definition 1. The satisfiability problem SAT-L consists in, given an L-formula η, to decide whether there exists a data tree T such that

[[η]] T = ∅.
It turns out that -as we are working with downward-looking fragments of XPaththis is equivalent to asking if there is a model where the formula η is satisfied at its root. Moreover, for this problem we can restrict ourselves to the case where η is a node expression. We remind the reader that although we state the problem in terms of data trees, all our results hold on the class of all xml documents with multiple attributes.

Main contribution

Our main results are the following.

Theorem 1. SAT-regXPath(↓, =) is decidable, with complexity in ExpTime.

Theorem 2. SAT-XPath(↓ * , =) is hard for ExpTime. Consequently, for a logic L ∈ {XPath(↓ * , =), XPath(↓ * , ↓ , =), regXPath(↓, =)}, SAT-L is ExpTime-complete.
The strategy of the proof can be outlined as follows.

1. We introduce a model of automata that captures all the expressivity of regXPath(↓, =). Automata of this new class are called Bottom-up Interleaved Path automata (bip). The automaton relies on an interaction between the runs of two kinds of automata, which corresponds to the two sorts of formulae of XPath. 2. We show that the translation from regXPath(↓, =) to bip automata can be done in PTime. 3. The main result is that the emptiness problem for the class of bip automata is in ExpTime. We show this by a reduction to the non-emptiness problem of classical bottom-up tree automata over trees with bounded branching width. Given a bip automaton M , we construct a bottom-up tree automaton A whose states describe the behavior of M for certain data values. We show it is sufficient to consider both the branching width and the number of data values to be polynomially bounded by the bip automaton M . We show that M is non-empty iff A is non-empty. 4. Finally, we prove that XPath(↓ * , =) is ExpTime-hard by a reduction from the two-player corridor tiling game.

Here, the challenge is to be able to move from one square of the game board to the next one, without counting with the '↓' operator in the language.

A new class of automata

We introduce a new automaton that we call Bottom-up Interleaved Path automata (bip for short) that in its transition function uses another automaton, the Pathfinder automaton that runs over the already executed bip run. This interleaving mechanism of running one automaton as a condition of the transition function of the other one corresponds exactly to the two sorts of formulae of XPath. Thanks to this duality, we obtain an automaton that captures the whole expressivity of regXPath(↓, =). It is worth noting that although the bip automaton does not contain 'registers' per se, it can do an unbounded number of equality and inequality tests between any pair of nodes of the tree. However strong this automaton may appear to be, we prove that the emptiness problem is only in ExpTime.

Definitions

A Pathfinder automaton is a bottom-up non deterministic automaton that basically can only recognize a path from some node to the root and retrieve one data value from it. The automaton retrieves a data value d with state k if there is a run that starts in a node with data value d and ends at the root with state k. Its definition is very weak as it can only retrieve a data value, but it cannot test it against any other. It runs over a data tree over the alphabet Σ = 2 Q (i.e., where the labeling function σ : T → 2 Q tags each node with a subset of Q), where Q is a finite set of symbols that -as we will see shortly-consists of the states of another automaton (the bip). It is defined as the tuple P = K, k I , Q, ν where K is a finite set of states, k I ∈ K is a distinguished initial state, and ν is the transition function. At each transition, the automaton can either (1) check the presence of some element of Q in the label of the node (we call this a 'non-moving' transition), or (2) move up in the tree (we call this a 'moving' transition).

ν : (Q ∪ {up}) × K → 2 K
For example, the non-moving transition ν(q 1 , k 1 ) = {k 2 , k 3 } indicates that if we are in state k 1 at some node labeled with a set S ⊆ Q such that q 1 ∈ S, then we can label it with one of the states among k 2 , k 3 . On the other hand, if ν(up, k 1 ) = {k 4 } and if we are in state k 1 , then the father of this node can be labeled with state k 4 .

Observe that, although this automaton runs on models labeled with subsets of Q, the transition function takes only one state of Q at a time, its intended meaning being that it applies to any set that contains the specified state. We do so in order to obtain a polynomial time translation from XPath(↓ * , ↓, =) to a pathfinder automaton and to prove the precise upper-bound of ExpTime. Otherwise, we would have a translation on models with an exponential number of states. This will become clear in the following.

A run ρ of a pathfinder P = K, k I , Q, ν on a data tree T = T, σ, δ is a non-empty list of states with positions ρ ∈ (K×Pos(T )) + . We denote by ρ(i) the ith element of the run, starting from 0. The run must be such that ρ(0) = (k, p) with k = k I , and ρ(N ) = (k , p) with p = ε for N = |ρ|-1. For any two positions ρ(i) = (k , x ), ρ(i+1) = (k, x) either (1) x = x and a 'non-moving' transition applies between k and k for x, or (2) xn = x for some n ∈ N and a 'moving' transition applies between k and k for xn. We define that a 'non moving' transition applies between k and k for x iff k ∈ ν(k , q) for some q ∈ σ(x), and that a 'moving' transition applies iff k ∈ ν(k , up).

Runs of pathfinder automata are noted by the symbol ρ. The output of a run ρ, denoted by o(ρ), is defined as the pair (k, d), where ρ(N ) = (k, ε), and d = δ(p) with ρ(0) = (k I , p), N = |ρ|-1. We also define the non-moving closure of a pathfinder P w.r.t. a state k and label S ⊆ Q (noted cl(k, S)) as the set of states k that can be reached by 'nonmoving' transitions on a node labeled S starting with the state k. Formally, cl(k, S) := n≥0 f n S ({k}) , with f S (K) := {k 1 | k 1 ∈ ν(q, k 2 ), q ∈ S, k 2 ∈ K}. Observe that this set can be built in time polynomial in the set S and the automaton P. We do not give accepting conditions because this automaton is used by the bip automaton as we shall see.

Example 2. Consider

P = {k I , k 1 , k ↓1 , k 2 , k ↓2 , k 3 }, k I , {q 1 , q 2 , q f }, ν that recognizes (q 1 q 2 ) + , that is, where ν(k I , q 2 ) = {k 2 }, ν(k 2 , up) = {k ↓2 }, ν(k ↓2 , q 1 ) = {k 1 }, ν(k 1 , up) = {k ↓1 }, ν(k ↓1 , q 2 ) = {k 2 }, ν(k I , q 1 ) = {k 3 }, ν(k 3 , up) = {k 3 }.
Any run of P that ends in k 1 retrieves a data value that can be accessed by a 'path' like

Q 1 1 Q 2 2 . . . Q t-1 1 Q t 2 where for any i, q 1 ∈ Q i 1 and q 2 ∈ Q i 2 .
Any run that ends in k 3 retrieves a data value from a node that is labeled by q 1 . As we show next, the runs of the pathfinder are the basic means for the bip automaton to test for data (in)equalities.

A bottom-up Interleaved Path automaton (bip) M is a tuple Σ, Q, µ, F, P , where Σ is a finite set of symbols, Q is a finite set of states, F ⊆ Q is the set of final states, P = K, k I , 2 Q , ν is a Pathfinder automaton, and µ : Q → Form M is the transition function, where Form M is defined:

ϕ ::= a | ϕ ∧ ψ | ϕ ∨ ψ | ¬ϕ | ∃(k 1 , k 2 ) where ϕ, ψ ∈ Form M , a ∈ Σ, ∈ {=, =}, k 1 , k 2 ∈ K.
Intuitively, ∃(k 1 , k 2 ) tests for the values retrieved by pathfinder runs (quantified existentially).

A run of the bip automaton over a data tree T is a labeling function λ : Pos(T ) → 2 Q . In general if T = T, σ, δ we define as λ(T ) the data tree T, λ, δ . Remember that T | n is the subtree that has n as a root, and let λ| n (i) = λ(ni). A run λ must fulfill, for every position n, that q ∈ λ(n) iff T | n , λ| n |= µ(q), where |= is defined as follows • T , λ |= a iff σ(ε) = a, that is, the root's symbol is a, • T , λ |= ¬ϕ iff T , λ |= ϕ, and all boolean connectors are defined in the standard way, and

• T , λ |= ∃(k 1 , k 2 ) with
∈ {=, =} iff there exist two runs ρ 1 , ρ 2 of P over the run-labeled tree λ(T )

such that o(ρ 1 ) = (k 1 , d), o(ρ 2 ) = (k 2 , d ) and d d .
Note that the run λ of M on T is unique by definition. The run is accepting if λ(ε) ∩ F = ∅.

Example 3. Consider the bip automaton Σ, {q 1 , q 2 , q f }, µ, {q f }, P , where Σ = {a, b}, and P is the one defined in Example 2. We can define µ to accept the trees that contain two elements accessible by a (ab) + path from the root, with different data values:

µ(q f ) = ∃(k ↓1 , k ↓1 ) = ∧ ¬∃(k I , k 3 ) = , µ(q 1 ) = a, µ(q 2 ) = b. Note that it corresponds to the XPath formula (↓ [a] ↓ [b]) + = (↓ [a] ↓ [b]) + ∧ ¬ε =↓ * [a]
, and that it accepts the tree of Example 1.

From regXPath to BIP automata

Theorem 3. Given a node expression η ∈ regXPath(↓, =), there is a bip automaton M such that for any model T , ε ∈ [[η]] T iff M accepts T . Moreover, this automaton can be obtained in PTime.

Proof. Let η be a formula of regXPath(↓, =). We build the bip automaton M = Σ, Q, µ, F, P where Σ = {a | a a label in η} ∪ {a ⊥ }, Q = {q ψ | ψ is a node expression in sub(η)} ∪ {q } where sub(η) is the set of subformulae of η, and F = {q η }. Intuitively, for every state q ψ where ψ is a node expression, µ associates it to a formula that is -exactly as ψa boolean combination of symbol and data equality tests. For formulae whose principal operator is a boolean connector, the transition is straightforward. E.g., µ(q ψ1∧ψ2 ) = µ(q ψ1 )∧µ(q ψ2 ). If ψ is of the form α α , then µ(q ψ ) = ∃(k α , k α ) , and if

ψ = α , µ(q ψ ) = ∃(k α , k α ) = .
On the other hand, any path expression α ∈ sub(η) can be seen as a regular expression over the alphabet Σ η = {e | e is a node expression of η} ∪ {↓}. Then, for any path α we can make the standard PTime translation of α r into a NFA over Σ, where α r stands for the reverse of α (it is enough to exactly reverse the symbols, as path expressions are closed under reversal). This is necessary because although XPath path expressions name the path from the root to the leaves, the pathfinder automaton reads the branch from the leaves to the root. We thus obtain a NFA A α = K α , Σ η , k 0 α , F α , δ α for each path expression α ∈ sub(η) where we name the states

K α = {k 0 α , k 1 α , . . .}. We then define P = K, k I , Q, ν the pathfinder where K = {k I } ∪ α ({k α } ∪ K α ), and ν(k I , q ϕ ) = {k 0 α | k 0 α ∈ K}, ν(k i α , q ϕ ) = δ α (ϕ, k i α ) ∪ {k α | δ α (ϕ, k i α ) ∩ F α = ∅}, ν(k i α , up) = δ α (↓, k i α ) ∪ {k α | δ α (ϕ, k i α ) ∩ F α = ∅}.
We can check that all the runs that end in k α -for α some path subformula of ηretrieve a data value of a path accessed via α, and conversely that it can retrieve all of them.

It is not surprising that the translation is so direct, as the bip automaton mimicks closely XPath semantics.

bip automata are more expressive than regXPath(↓, =), but if we restrict the definition of bip to have a bounded number of mutual recursions between the bip and the pathfinder, we precisely characterize regXPath(↓, =): for each bip there is an equivalent regXPath(↓, =) formula, and viceversa. In a sense, the restriction disallows the existence of two states q, k (the former of bip, the latter of pathfinder) in mutual recursion, where k is named in µ(q) and q in ν(k, •).

Main result

We devote this section to prove that emptiness of bip automata is in ExpTime and that the satisfiability problem for XPath(↓ * , =) is ExpTime-hard. In this way we obtain that the satisfiability problem for XPath(↓ * , =), XPath(↓ * , ↓, =) and regXPath(↓, =) are all ExpTime-complete.

Upper bound

Theorem 4. Emptiness of bip automata is in ExpTime.

Proof. The proof consists in a reduction from the bip emptiness problem into the emptiness of a classical bottomup non deterministic tree automaton over trees with bounded branching width. Moreover, the tree automaton has at most an exponential number of states, and therefore its emptiness problem can be solved in ExpTime. A state of this automaton (that we call extended state to avoid confusion with states of bip automata) contains the description of the behavior of the bip automaton w.r.t. some data values. More precisely, each data value d is described by the set of states of the pathfinder by which d can be reached (cf. Ex. 4 below).

We guarantee that for each extended state reachable by the tree automaton, there is a witnessing data tree that consists in any tree that reaches this state at the root, together with an assignment for data values. For the extended states that correspond to the leaves, the witnessing data tree is the leaf with an arbitrary data value. For an extended state of an inner node, the witnessing tree is constructed bottom-up, by identifying the data values that are described in the states of the witnessing subtrees inductively obtained, and 'merging' them according to an equivalence relation associated to the transition.

In Proposition 1, we show that given an accepting run of the tree automaton, we can easily build a run of the bip automaton on a witnessing data tree, and in Proposition 2 we show that if there is an accepting run on the bip automaton, there must be a model with an accepting run in the tree automaton. As a byproduct of this reduction, we obtain a small model property. We establish that if a bip automaton accepts at least one data tree, then it accepts in particular a model with polynomial branching width and exponential height, such that for any pair of disjoint subtrees there are only a polynomial number of data values in common.

Example 4. We give the main idea for checking emptiness of bip automata by abstracting runs. Let M be the bip that accepts the models satisfying ϕ

= ↓ [a] ∧ ¬[a] =↓ [a] ∧ ↓ * [b] =↓ * [b]
, and consider the model below that verifies ϕ.

Below, we give an intuition about the nature of the extended states of the tree automaton A M built from M , and what would be an accepting run for this particular data tree.

To each subtree, we associate an extended state that contains the description of some data values. Each data value d (here represented by a balloon like 1 ) is described by a set of states of the pathfinder automaton. Here, for simplicity's sake, such states are represented by (sub)path expressions that can reach d. Additionally, the extended state specifies, for each path expression, whether it can retrieve (a) only one data value, (b) more than one, or (c) no data values. In the case (a), we specify which is the only data value retrieved. Both leaves have the same extended state. We read the state as follows: there is only one data value reachable by the path ↓ * [b], and this data value is denoted by 1 . There is also only one data value reached by [b], which is also denoted by 1 (hence, they are the same). There are no data values reachable by a path ↓ [a] (as it is a leaf) or [a] (as it is labeled 'b'). Finally, we describe the data value denoted by 1 with the set of path expressions that may reach it:

{[b], ↓ * [b]}.
Intuitively, 1 makes reference to the current node's data value, that is why 1 and the datum are surrounded by the same area, to denote that they are equal.

In the next step, we apply a transition, which specifies how the data values between the balloons are merged. In this case we demand that the balloon of the left leaf and that of the right must be different, otherwise they would be surrounded in the same grey area. Consequently, we will have that there are more than one data value reached by ↓ * [b], which is reflected in the extended state. In this transition, we define balloons that describe the same data values as the ones of the leaves (the case of 1 and 2 ), and we define 3 as denoting the data value of the current element a, 2 . Observe that the extended state of the root depends only on (1) the root's symbol, (2) the descriptions of the data values of its children, and (3) the way of 'merging' these data values. Here, we show how the last transition leads to a final state. Once this transition is performed we can see that it implies that the formula ϕ is satisfied. In the following, we show how to build this tree automaton systematically.

Let M be a bip automaton M = Σ, Q, µ, F, P with P = K, k I , Q, ν . In the development below we make use of two parameters t 0 (related to the number of data values described in each extended state) and u 0 (the maximum branching width of the witnessing tree) which we assume to be bounded by two polynomials on |K|. As usual, we write ' ' to denote any element of {=, =}. We define a tree automaton A M = Σ, Q A , τ, F A where Q A is the set of extended states, and

F A is the set of final states. Finally, τ ⊆ 2 Q A ≤u0 × Σ × Q A (where 2 Q A ≤u0
stands for the set of subsets of Q A with at most u 0 elements) is the transition function that, given the root's symbol and the set of states of its children, labels the root with a state.

Abstracting runs.

An extended state is the building block to abstract the runs of M . It is a pair c = v, D where Let T = T, σ, δ be a data tree and λ be the unique run of M on T . We denote by λ(T ) the data tree labeled with the run T, λ, δ . Given a valuation v :

• v is a valuation, i.e.,
atForm M → {0, 1}, we define C(v) = {q | q ∈ Q with µ(q) true under the valuation v}. If d ∈ ∆, let Reach(d) = {k | there is ρ run of P on λ(T ), such that o(ρ) = (k, d)}.
We fix χ to be any bijection

χ : K → [1.
.|K|], and χ(k) = i stands just as a correlation between k ∈ K and the element described in position i of the tuple D = (we note this as D = (i)). We then say that an extended state c = v, D abstracts the run λ of M on T (notation: T £ c) iff λ(ε) = C(v) and the following two conditions are met.

• For every k ∈ K, either D = (χ(k)) = Reach(d 0 ) for d 0 ∈ ∆ such that for every run ρ of P on λ(T ), if o(ρ) = (k, d) then d = d 0 ; or D = (χ(k)) = ∅ if
D (i) = Reach(d i ),
provided that d i is not already described in D = . I.e., we must ensure that

( i D (i)) ∩ {k | D = (χ(k)) = ∅} = ∅.
The set Q A consists of all the exponentially many possible extended states, and

F A = { v, D ∈ Q A | C(v) ∩ F = ∅}.
We next describe the transition function τ .

We start with the transitions that correspond to the leaves. Let t = ∅, a, c with c an extended state and a a symbol. We define that t ∈ τ iff (a, 1) £ c, where (a, 1) is the singleton tree with symbol a and datum 1 (it could be any). Now we show how to obtain the recursive transitions. We explain how, from u ≤ u 0 extended states, we can construct the state that is supposed to represent the root of the tree.

For convenience of notation, by c i we refer to the extended state v i , D i . Suppose we have a tuple t = {c 1 . . . c u }, a, c 0 with u > 0. We now show how to check if t ∈ τ . Remember that A is non-deterministic and the different possibilities for c 0 depend on the way the data values in c 1 . . . c u are merged. We must then describe how these descriptions are merged together, and ensure that transitions are consistent with the merging. For example, if c 0 describes a datum that can be reached in two steps with label a, or in at least one step with label b (e.g. because we want to check '↓↓ [a] =↓↓ * [b]') then some c i must describe a datum accessible through '↓ [a]', some c j must describe a datum accessible through '↓ * [b]', and these two descriptions must be of the same data value.

We define that t ∈ τ iff there exists a merging ≡ E such that c 0 is coherent w.r.t. ≡ E and {c 1 . . . c u }. We next define what is a 'merging' and which are the 'coherence' conditions.

Merging data values.

We describe the ways of merging the u(t 0 + |K|) data values described by the (non-empty) elements of D 1 . . . D u . For this purpose, we consider an equivalence relation '≡ E ' on {( , i, j) | D i (j) = ∅} ∪ {(=, i, j) | D = i (j) = ∅} ∪ {root} that describes exactly how these data values are going to be collapsed between them and w.r.t. the root's data value. However we check one condition in

≡ E . If k 1 ∈ D = i (χ(k 2 )) then either D = i (χ(k 1 )) = ∅ or (=, i, χ(k 1 )) ≡ E (=, i, χ(k 2 )
), as they make reference to the exact same data value (by definition of D = ). An example of merging is shown in Fig. 1.

We consider that the only data values that can be merged among the trees represented by the u extended states are those described in ≡ E . In other words, we can consider that the witnessing data tree for c 0 is composed of the witnessing trees for each c i with the following property. For every c i we associate a data value to each description, and two data values from two different subtrees i, j are equal if and only if (1) they are described in c i , c j respectively, and (2) both descriptions are in same equivalence class of ≡ E . Observe that this is a strong restriction, the emptiness algorithm of bip relies on at most u 0 (t 0 + |K|) data values at every point of a branch. However, we remark that the automaton M can make at any step, any number of comparisons between any number of data values that can be found in the subtree.

Checking coherence of c 0 with respect to ≡ E . We require that {c 1 . . . c u }, a, c 0 ∈ τ exactly when there exists a merging ≡ E such that the conditions below hold true. We first define the following relation:

step-up(k , k) iff k ∈ ν(k , up) and k ∈ cl(k , C(v 0 )).
To start with, we must verify that v 0 is correct. For a ∈ Σ, v 0 (a ) = 1 iff a = a. And v 0 (∃(k 1 , k 2 ) = ) = 1 iff any of the 4 conditions below holds (they are depicted in Fig. 2).

1. There are some k 1 , k 2 states that retrieve equal data in some subtree, and moving one step up with P we obtain k 1 and k 2 . I.e., for some i,

v i (∃(k 1 , k 2 ) = ) = 1, step-up(k 1 , k 1 )
, and step-up(k 2 , k 2 ). 2. Both k 1 , k 2 can be obtained as runs that start and end at the root (and hence both carry root's data value)

k 1 , k 2 ∈ cl(k I , C(v 0 )). 3. k 2 is
like in the preceding case, and k 1 retrieves a data value declared in ≡ E to be equal to the root. For some

i, k 2 ∈ cl(k I , C(v 0 )), ∃ , α (α, i, ) ≡ E root, k 1 ∈ D α i ( ), step-up(k 1 , k 1 )
(or the converse, swapping k 1 and k 2 ). 4. k 1 and k 2 retrieve data values from different subtrees that are equal according to the merging ≡ E . For some i, j, there exist m, , α, β s.t.

k 1 ∈ D α i (m), k 2 ∈ D β j ( ), (α, i, m) ≡ E (β, j, ), step-up(k 1 , k 1 ), step-up(k 2 , k 2 ).
And v 0 (∃(k 1 , k 2 ) = ) = 1 iff any of the similar conditions previously described in 1, 3, 4 holds (changing = by =), or 4. One of the states is not described in D = , and hence it retrieves at least 2 different data values, which means that the = constraint can be met: D = 0 (χ(k 1 )) = ∅ and v 0 (∃(k 2 , k 2 ) = ) = 1 (or the converse).

We must check now the coherence of D = 0 and D 0 . We concentrate on the former as it is the most involved. Let B k be the set of all the descriptions of data values that can be reached at the root with state k,

B k = {(α, i, j) | k ∈ D α i (j), step-up(k , k)}. We require that D = 0 (χ(k)) = ∅ iff:
• There is no , i, j ∈ B k , as this would mean that k retrieves at least two data values. Note that any state k in D i (j) retrieves more than one data value (otherwise the datum would be described in

D = i (χ(k ))).
• Any pair of data values that may be reached with state k at the root must be equal: for all a, b ∈ B k , a ≡ E b. • D = 0 (χ(k)) consists of every state from the descriptions of B k , or from any other description that is declared to be equal in

≡ E . D = 0 (χ(k)) = {k | a ∈ B k , a ≡ E α, i, j , k ∈ D α i (j), step-up(k , k )}.
With respect to D 0 we simply need to state that it cannot contain elements already in D = 0 . This completes the definition of τ . It is easy to see that checking all the preceding conditions consumes at most an exponential amount of time and hence that A M can be built in ExpTime.

We have completely described the tree automaton A M . As it contains an exponential amount of extended states, the emptiness problem for this automaton can be computed in ExpTime. We have that M is empty iff A M is empty. Proposition 1. (Soundness) For every accepting run of A M on T there is an accepting run of M on some T .

Proof. It is easy to show by induction that for any run of A M on T we can define data values for all the nodes of T such that the data tree defined corresponds to an abstraction of the extended states in the run. The way of merging the data values in the inductive step is completely described by the relation ≡ E .

Proposition 2. (Completeness) For every accepting run of M on T there is an accepting run of A M on some T .

Proof. The proof can be sketched as follows. We first show that bip automata are closed under subtree duplication. More concretely, the data tree a, d (t 1 , t 2 ) (where a, d is the root and t 1 , t 2 its two immediate subtrees) is accepted by a bip M iff a, d (t 1 , t 2 , t 2 ) is accepted by M .

We then show a bounded-branching model property:

1. For each atomic formula ∃(k 1 , k 2 ) = that holds at a node z, we mark (at most) two of their immediate subtrees that 'witness' this fact. It could be that we only need to mark one or none, if one of the two components k 1 or k 2 is directly witnessed at z. Each marking consists in a label that indicates a state and data value necessary to witness the formula, for example '(k , d )'. We proceed similarly for ∃(k 1 , k 2 ) = . 2. Moreover, this can be done in such a way that we don't mark twice the same subtree. We can ensure this by duplicating sibling subtrees if necessary. 3. In this way, we have that each node marks at most some bounded number of subtrees (say N ), and at the same time it may be marked by its father. It is easy to see that N is polynomially bounded by the number of states |K|. Given a marking of a node z (coming from its father) it could be that (1) the marking is 'witnessed' at z, or (2) that it actually needs a subtree. In the case of (2) we add the marking to the corresponding subtree, always making sure that no subtree is marked twice. 4. We then have that each node has marked (at most) N +1 immediate subtrees. The rest of the subtrees that are not marked can be safely removed from the tree. This can be done with a top-down algorithm, where the root is the only node to mark at most N nodes (as it has no father).

Finally, we associate an extended state of A M to each node. Consider the marking just explained. For each node z we build the extended state, where D = is completely determined by the tree T | z , and we use D to ensure that for each of the markings (k , d ) generated by z, d is described. There are at most N + 1 such markings, and we especially choose a sufficiently large size of D (i.e., of t 0 ) to be able to accommodate all of them. We can then check that this is indeed a correct accepting run of A M .

Corollary 1. SAT-regXPath(↓, =) is in ExpTime.

Proof. A direct consequence of Theorems 3 and 4.

In the presence of document type definitions.

The bip automaton can be extended to have transitions that may demand conditions on the states of the child nodes stating, for example, that a node can be labeled by state q 1 if it has a child tagged with state q 2 . It is actually easy to see that this can be simulated using the pathfinder automaton. Furthermore, consider the extension of its formulae by positive occurrences of #q ≥ n where n ∈ N is a constant, with the intended meaning that it is verified whenever there are at least n child nodes labeled with state q. Similarly, #q = 0 states that there are no children with state q, but formulae #q ≤ n are not allowed.

It can be checked that a similar emptiness algorithm can be applied, the only difference being that the maximum branching width of the algorithm depends on the greatest constant n 0 used in the definition of the automaton. We obtain then an algorithm of time exponential in n 0 .

So, in the case where n 0 is fixed, or where we consider constraints #q ≥ n with n encoded with a unary representation, we still have an ExpTime algorithm for emptiness.

Consider the document types definable with a tree automaton on unranked trees with this 'zero/many' counting ability, where at each transition we can check either that there is no child with a certain state, that there are at least n with a certain state for some n, or conjunctions and disjunctions of these kind of conditions. It is possible thus to check the satisfiability of any regXPath(↓, =) under these document types in ExpTime.

To verify this, we should mention that intersection of two bip automata M 1 and M 2 can be simply obtained by a bip with the Q M1 × Q M1 an defining µ M1∩M2 (q 1 , q 2 ) = µ M1 (q 1 ) ∧ µ M2 (q 2 ). Observe that all positive occurrences of the #q ≥ n formulae remain positive.

Inclusion and equivalence problems.

We can finally mention that as regXPath(↓, =) is closed under negation and boolean operations, we also get a decision procedure for the equivalence and the inclusion problems for node expressions (ϕ ⊂ ψ iff ϕ ∧ ¬ψ is not satisfiable). However, we cannot solve the problems of path expressions inclusion or equivalence with this kind of automata.

Lower bound

In this section we prove ExpTime-hardness of satisfiability of XPath(↓ * , =). Remarkably, this logic cannot express a one step down in the tree as it does not possess the ↓ axis, and this will be the major obstacle in the coding.

Theorem 5. SAT-XPath(↓ * , =) is ExpTime-hard.

Proof. The proof is by reduction from the two-player corridor tiling game. An instance of this game consists in a size of the corridor n (encoded in unary), a set of tiles T = {T 1 , . . . , T s }, a special winning tile T s , the set of initial tiles {T 0 1 . . . T 0 n }, and the horizontal and vertical tiling relations H, V ⊆ T × T . The game is played in an n × N board where the initial configuration of the first row is given by T 0 1 . . . T 0 n . At any moment during the game any pair of horizontal consecutive tiles must be in the relation H and every pair of vertical consecutive tiles in the relation V . The game is played by two players: Abelard and Eloise. Each player takes turn in placing a tile of his choice, filling the board from left to right, from bottom to top, always respecting the horizontal and vertical constraints H and V . Eloise is the first to play, and she wins iff during the game the winning tile T s is placed on the board. If the game ends without this configuration being reached, or if it runs infinitely, the game is won by Abelard. It is known that deciding whether Eloise has a winning strategy is ExpTime-complete. For more details on this game we refer the reader to [START_REF] Chlebus | Domino-tiling games[END_REF].

Representation of a winning strategy.

It is easy to see that in this game Eloise has a winning strategy iff she has a strategy to win before the row s n of the board is reached (where s is the number of tiles). Then each game between Eloise and Abelard can be coded as a succession of at most s n rows of n tiles each. Wlog we assume that n is an even number, and hence all odd positions are played by Eloise, while even ones by Abelard. We can then represent a winning strategy as a tree, where at each even position there exists one branch for every possible play of Abelard and where all branches of the tree contain the winning tile T s .

We must now come up with a way to encode all possible games for all possible choices of Abelard in XPath(↓ * , =), and verify that all of them are won by Eloise and hence that they consist in a winning strategy for Eloise.

Our alphabet consists in the symbols I 1 . . . I n that indicate the current column of the corridor, the symbols b 0 . . . b m where m = (n + 1).log(s) that act as bits to count from 0 to s n (it is enough that they count at least up to s n ), and the symbols T 1 . . . T s to code the tile placed at each move. The coding makes use of a symbol # to separate rows, and an extra symbol $ whose role will be explained later.

Each block of nodes between two consecutive # codes the evolution of the game for a particular row. Each node labeled I i has a tile associated, coded as a descendant node T j with the same data value. In Fig. 3 the first column I 1 of the current row is associated to the tile T 3 , because T 3 , 1 is a descendant of I 1 , 1 with the same data value. Similarly, each occurrence of # is associated to a number, coded by the b i elements. In the example, #, 0 is associated to the bits b 0 and b 2 that give the binary number 101.

Finally, the symbol $ is used to delimit the region where the next element of the coding must appear, this will be our way of thinking the next step of the coding. Intuitively, between I i and the $ with the same data value, only a I i+1 may appear. This mechanism of coding a very relaxed 'one step' is the building block of our coding. As the logic lacks the ↓ axis, we need to restrict the appearance of the next move of the game to a limited fragment of the model. By means of this element $, we can state, for example, that whenever we are in a I 2 element, then in this restricted portion I 3 must be true by stating

ε =↓ * [I 3 ] ↓ * [$].
In a similar way we can demand that all elements verify I 3 (except, perhaps, a prefix of I 2 elements). However, we cannot avoid having more than one element before the $ as shown in the figure. We may have 'repeated' elements or extra branches, but this does not spoil the coding.

We are actually able to force properties for all branches and all possible extra elements that the tree may contain. Intuitively, any extra element or branching induces more copies of winning strategies for Eloise.

In Fig. 3 we show an example of a possible extract of the tree between the # associated to the counting of 5 until the next # of counting 6. The coding forces a branching as it contains all possible answers of Abelard at even positions.

Building up the coding.

Let us define some useful predicates. s k σ (ϕ) evaluates ϕ at a node at k-steps (with our way of coding a step as we have seen before) from the current point of evaluation, given that the current symbol is σ. For this purpose we first define next(I i ) := I i+1 (if i < n), next(I n ) := # and next(#) := I 1 . Hence, for a ∈ {#, I 1 , . . . , I n },

s 0 a (ϕ) := a ∧ ϕ s k+1 a (ϕ) := a ∧ ε =↓ * [s k next(a) (ϕ)] ↓ * [$]
Similarly, t j checks that the tile of the current node I corre-sponds to T j , bit i checks that the i-bit of the counter's binary encoding of a #-node is one [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF], and G forces a property to hold at all nodes of the tree.

t i := ε =↓ * [T i ] G(ϕ) := ¬ ↓ * [¬ϕ] bit i := ε =↓ * [b i ]
We now describe all the conditions to force the aforementioned encoding. We also exhibit the XPath formula counterparts of the non-trivial conditions.

1. Every I i , T i , and # along the tree has different data value. As we have only the transitive closure axis, we actually express that whenever there are two elements with the same symbol a such that there is a third element in the middle with another symbol different from a (and then they can be effectively distinguished), they must have different data value. Actually, the fact that there could be a sequence of elements with equal label does not cause any problem. Let us see the case for

I i : ¬ ↓ * [I i ∧ ε =↓ * [¬I i ] ↓ * [I i ]].

Every I i has a next element, unless it contains the winning tile, G(I

i ∧ ¬t s → s 1 Ii ( )) ∧ G(# → s 1 # ( )).
3. $ are leaves, in the sense that no other symbol may appear as descendant:

¬ ↓ * [$ ∧ ↓ * [¬$] ] . 4. Every I i has its corresponding $: G(I i → ε =↓ * [$]).
5. Each I i has a unique tile: G(¬(t ∧ t j )) for = j.

6. All I i+1 inside a step along a branch must have the same tile. (And a similar condition for I 1 .) That is, for every i < n

and j = k, G(I i → ¬ε =↓ * [I i+1 ∧ t j ] ↓ * [I i+1 ∧ t k ] ↓ * [$]).
7. Between I i , i < n and its corresponding $ only I i+1 may appear. (And also for I n and #, and for # and I 1 .) That is, for any i < n and j ∈ {i, i + 1}, G(

I i → ¬ε =↓ * [I j ] ↓ * [$]), and G(I i → ¬ε =↓ * [I i+1 ] ↓ * [I i ] ↓ * [$]).

The tiles match horizontally: for every k and T

i , T j such that ¬H(T i , T j ), ¬ ↓ * [I k ∧ t i ∧ s 1 I k (t j )]
. Moreover, the tiles match vertically, for every k and T i , T j such that

¬V (T i , T j ), ¬ ↓ * [I k ∧ t i ∧ s n+1
I k (t j )] . 9. All the elements corresponding to the first row match with T 0 1 . . . T 0 n . That is, for all i ∈ [1.

.n] and tile T j such that ¬V (T 0 i , T j ), then ¬s i # (t j ) must hold at the root.

10. All possible moves of Abelard are taken into account. For every triple of tiles

T i , T j , T k such that H(T j , T k ), V (T i , T k ), each time Abelard can play T k , he must play it. ¬ ↓ * I 2 ∧ t i ∧ s n I 2 I 2 -1 ∧ t j ∧ ¬s 1 I 2 -1 (t k )
11. There is no # element that has all the b i bits in 1. Because that would mean that Eloise was not able to put a T s tile in less than s n rounds.

12. The data value of a # element is associated to a counter. It is easy to code that the first # is all-zero. The increment of the counter between two # is coded as G(# ∧ f lip(i) → zero <i ∧ turn i ∧ copy >i ), where

f lip(i) = ¬bit i ∧ j<i bit j zero <i = j<i ¬s n+1 # (bit j ) turn i = ¬s n+1 # (¬bit i ) copy >i = j>i (bit j ∧ ¬s n+1 # (¬bit j )) ∨ (¬bit j ∧ ¬s n+1 # (bit j ))
This completes the coding. It is easy to see that each one of the formulae described has a polynomial length on s and n. It can be shown then that Eloise has a winning strategy in the two-player corridor tiling game iff the conjunction of the formulae just described is satisfiable.

PSpace fragments

We now turn to some other downward fragments of XPath. We complete the picture of the complexity for all possible combinations of downward axis in the presence and in the absence of data values. We first need to introduce a basic definition that we use throughout the section. Definition 2. We say that the logic L has the poly-depth model property if there exists a polynomial f such that for every formula ϕ ∈ L, ϕ is satisfiable iff ϕ is satisfiable in a data tree model of depth at most f (|ϕ|).

We can now prove the following statement that we will use to show PSpace-completeness for XPath(↓, =). Theorem 6. Every fragment L of regXPath(↓, =) with the poly-depth model property is in PSpace.

Proof. Suppose that if a formula η ∈ L is satisfiable in a model, then it is satisfiable in a model of height h with h ≤ f (|η|) where f is a polynomial.

We can then translate η into a bip automaton M . We show next how to modify the emptiness algorithm to make it work in non-deterministic polynomial space by means of f . We define an algorithm by recursion on the height of the tree h. The algorithm receives three parameters: (1) a bip automaton M , (2) an extended state c 0 , and (3) h, the maximum height of the tree to reach the extended state. The algorithm must verify that c 0 can be reached in a tree of height at most h in non-deterministic polynomial space in h. Now the emptiness algorithm for A M must be done on the fly, that is, we do not build the set of all possible extended states. The base case is when h = 1. In this case we can easily check the existence of a singleton tree that satisfies c 0 in polynomial space.

Suppose now the height is h = n + 1. The algorithm guesses c 1 . . . c u extended states corresponding to the immediate subtrees and verifies that c 0 and c 1 . . . c u are in a transition of A M . To do this, we guess a relation ≡ E and test that all the conditions described in the construction of A M seen before are satisfied. Finally, by inductive hypothesis we can check that each one of c 1 . . . c u extended states are satisfied in a model of depth at most n, and this test can be done in space polynomial in n. In terms of space complexity this algorithm uses (a) the space to store c 1 . . . c u where u is a polynomial in M and the space required to store each c i is polynomial in M , (b) the space to store the relation ≡ E to check their correctness, that can be bounded by 2.u.(2|K| 2 + 3|K| + 2) and also remains polynomial in M , and (c) some polynomially bounded space on n (call it S(n)) to do the u recursive calls. Then the space required is S(n + 1) = (a) + (b) + S(n). It is then immediate that the algorithm is in NPSpace.

The main algorithm can be sketched as follows. Given η, we compile η into M in PTime, we guess an extended state c 0 that contains a final state of M and we check the guessing is correct by calling the algorithm just described. Thus, as NPSpace = PSpace the theorem follows. Proposition 3. SAT-XPath(↓, =) is PSpace-complete.

Proof. XPath(↓) is shown to be PSpace-hard in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]. For the upper bound, we show the poly-depth model property. It is easy to show that if η is satisfiable in T , then it is satisfiable in T n where n is the maximum quantity of nested ↓ of the formula, and T n is the submodel of T consisting of all the nodes that are at distance at most n from the root. Hence, by Theorem 6, XPath(↓) is in PSpace.

So far we have that, in the presence of data values, the ability to have the descendant axis (↓ * ) produces an increase in the complexity from PSpace to ExpTime 1 . However, we argue that it is not the ability to test for data equality of distant elements what produces this raise in complexity. It is, as a matter of fact, in the ability to test data values against that of the root in formulae like ε =↓ * [a]. We show that if we actually eliminate this kind of data tests, we can prove the resulting logic to be only in PSpace. Definition 3. We denote by XPath(↓ * , =)\ε the fragment of XPath(↓ * , =) where the ε path formulae are forbidden, and in general where there are no ε-testing in a path (like in

[ϕ] ↓ * ), α ::=↓ * | α[ϕ] | αβ | α ∪ β. Proposition 4. SAT-XPath(↓ * , =)\ε is PSpace-complete.
Proof (sketch). The proof is done by proving the poly-depth model property. The key observation is that any XPath(↓ * , =)\ε path expression that is satisfied at a node n of a tree, is also satisfied in any ancestor of n, this is basically because all path expressions start with a ↓ * axis. This means that for any pair of nodes n, n such that n is an ancestor of n , the set of formulae of the type p , p = p or p = p (with p, p path expressions) that are satisfied in n is a subset of those that are satisfied in n. Thus, if ϕ is a formula satisfied in T , for a given branch there is only a polynomial number of configurations of the (sub)paths in ϕ verified in each of its nodes. Long branches with a repeated description can actually be pruned into a shorter branch, preserving satisfiability of ϕ in T . 1 In the case PSpace = ExpTime. If for some node both α and β hold, then α and β are witnessed by two disjoint branches of polynomial depth.

Concluding remarks

We have shown the complexity of various downward fragments of XPath. The highest complexity class we obtained is ExpTime. In the presence of data equality tests, this is a well behaved fragment considering that in the presence of all the axes XPath is undecidable. One important reason for this, is the absence of sibling axis. Actually, in the presence of arbitrary DTDs we can show that the satisfiability problem of the downward fragment is either undecidable, or decidable with a non-primitive recursive algorithm. We have shown however that we can evaluate some restricted fragment of DTDs that cannot express sibling order nor limit the quantity of occurrences of nodes of a certain type, but that can demand, for example, that any a has at least five b children and no c child. By solving the satisfiability problem we are also able to solve the inclusion and equivalence problems of node expressions for free. We leave open the question of whether the inclusion of path expressions (as binary relations) is also decidable in ExpTime.

We introduced the new class of bip automata that capture all the expressivity of regXPath(↓, =). By the proof of decidability, we conclude that there is a very strong normal form of the model for this logic. If a formula η ∈ regXPath(↓, =) is satisfiable, then it is satisfiable in a model of exponential height and polynomial branching width, whose data values are such that only a polynomial number of data values can be shared between any two disjoint subtrees. This small model property is reflected by the fact that the emptiness of the automaton only depends on a polynomial number of data values at every point of a branch. However, there is no syntactic restriction in the automaton, it can retrieve and compare any number of data values between them and the root's data value at each step of the execution of M .

APPENDIX A. From XML to data tree

As outlined before, xml documents may have multiple attributes with data values on each element, while data trees can only have one. Let us consider now that our finite set of symbols Σ = Σ attr ∪ Σ elem is divided between the names for attributes and the symbols of the xml elements. We can now have the models as T, σ, δ where δ ⊆ T × Σ attr × ∆ is a relation that may have a data value for for some attribute symbols on any node. Let us consider then the extension of the languages where different attributes may be compared, where node expressions are defined

ϕ :: a | ¬ϕ | ϕ ∧ ψ | α | α@attr1 β@attr2
where ∈ {=, =}, a ∈ Σ and attr1, attr2 ∈ Σ attr . Let us call this logic attrXPath. It is easy to see that this language with the expected semantics can well encode any XPath request on an xml document.

However, as already mentioned, each xml document can be coded in a data tree by adding one child for each attribute with its corresponding value. We can force this kind of model using XPath(↓ * , ↓, =) by stating that all the nodes with a symbol from Σ attr are leaves.

ϕ struct = ¬ ↓ * [ s∈Σattr ∧ ↓]
In addition we can transform any XPath formula with attributes like '↓ *

[a] ↓ @attr1 =↓ [b]@attr2' into a formula '↓ * [a] ↓↓ [attr1] =↓ [b] ↓ [attr2]', let us call this translation tr.
We can then decide the satisfiability of a formula ψ of attrXPath on trees with multiple attributes by transforming it to an equivalent one on data trees by 'tr(ψ) ∧ ϕ struct '. We have then an ExpTime decidability procedure for the full downward fragment of attrXPath even with the Kleene star operator (as the translation is clearly in PTime).

On the other hand any XPath formula on data trees can be thought of a attrXPath formula that uses at most one attribute. We can then deduce the ExpTime-hardness result of attrXPath(↓ * , =) from that of XPath(↓ * , =).

For the case of attrXPath(↓, =) we can do the same translation the only difference being that for a formula ψ ∈ attrXPath(↓, =) the structure can be forced by

ϕ struct = 0≤n≤d+1 ¬ ↓ n [ s∈Σattr ∧ ↓]
where d is the maximum quantity of nested ↓ of ψ. It is easy to see that this forces the requested property for all the portion of the data tree that we are interested in. That is, for the whole region where tr(ψ) can access. This is associated with the poly-depth model property of the logic. We then have that attrXPath(↓, =) is PSpace-complete.

Finally, for the case of attrXPath(↓ * , =)\ε we are not able to force the wanted structure of the data tree. However it can be shown that if a formula ϕ ∈ attrXPath(↓ * , =)\ε is satisfiable, then it is satisfiable in a model where each node has at most one attribute.

The basic idea is that any node with multiple attribute can be 'split' into several nodes each one of them with only one attribute.

It can be checked that this transformation preserves the satisfaction of all attrXPath(↓ * , =)\ε formulae. We then have a trivial transformation into data trees and the same result of PSpace-completeness of attrXPath(↓ * , =)\ε.

B. Characterizing regXPath(↓, =)

We now show that we can easily identify the class of bip automata that correspond to the logic of regXPath(↓, =). Intuitively, we need to make certain that there are no mutual unbounded recursion between the main bip automaton and its pathfinder. Definition 4. We say that a bip automaton M = Σ, Q, µ, F, P with P = K, k I , Q, µ P has the bounded interleaving property if there is a partition

Q = Q 1 ∪ . . . ∪ Q n where ∀i = j : Q i ∩ Q j = ∅ and K = K 1 ∪ . . . ∪ K m where ∀i = j : K i ∩ K j = ∅, such that for every i ∈ [1..n],
if q ∈ Q i then µ(q) ∈ Form( j≤i K j ), and on the other hand for every

i ∈ [1..m] if k ∈ K i then ν(k, q) = ∅ ∀q ∈ j≥i Q j .
That is, if we do not have mutual recursion between a state q from the bip automaton and a state k of the pathfinder automaton it contains. Proposition 6. For every bip automaton M with the bounded interleaving property there exists a regXPath(↓ , =)-formula η such that for every model T , M accepts

T iff [[η]] T = ∅.
Proof. It is easy to see that the set of runs leading to a state k ∈ K i from the pathfinder automaton can be coded into a regular expression over the alphabet Q 1 . . . Q i-1 . Conversely, every state q ∈ Q i of the bip automaton can be straightforwardly coded into a node expression where, instead of data-expressions like ↓ [a] ↓ [b] = (↓ [c]) * , we have states from the pathfinder of the form ↓ k 5 =↓ k 7 .

It is then just a matter of replacing states of bip automaton by node expressions in the path expressions, and vice-versa replacing states of the pathfinder automaton by path expressions in the node expressions. The bounded interleaving property forces that we only need n + m replacement steps. The formula η then consists in the disjunction of all node expressions associated to final bip states.

Remark. Note that the expressivity of the bip automaton is indeed very close to that of regXPath(↓, =). The essence of what bip can express that regXPath(↓, =) cannot do is the recursiveness between node and path expressions, that would correspond to a 'star' operator on the nesting of the formula. More concretely, bip automata can express, for instance, the disjunction of all the formulae defined by the grammar A ::

ε =↓ [A] | b.
That is, the property of having a 'chain' of equal data until a b, which is not something expressible in regXPath(↓, =).

C. Completeness of emptiness of BIP

Proof of Proposition 2. We show that whenever there is a model T accepted by M , there is another one T such that it is both accepted by M and by A M . Note that A M can run on data trees by simply ignoring the values of the nodes. We will show that not only there is an accepting run of A M on T , but there is an accepting run with some extra information, where we can associate a concrete data value of the tree T to each of the descriptions of the extended state. We will call this a 'data run' of A M .

We first need to introduce the following definition of equivalence between trees. We now consider a special kind of run of A M on a tree for that run, that we call 'data run'. Together with the run we maintain a witness tree that is a representation of the extended states indicated in the run. The proof then consists in giving an accepting data run α and a witness tree T for every time the automaton M is non-empty (i.e., every time there is a tree T that is accepted by M ).

We will make use of the two parameters u 0 and t 0 which are bounds, polynomial in the bip: t 0 = 2|K| 2 + 2 and u 0 = (2|K| 2 + |K| + 2)|K|. u 0 is a bound for the maximum branching width of A M , and t 0 is the maximum number of data descriptions that D may have at any extended state. .|K|] → ∆ a partial mapping for the D = . And:

• T | p £ c p , • for all i, j ∈ N s.t. i = j, pi, pj ∈ Pos(T ), if d ∈ δ(T | pi ) ∩ δ(T | pj ), then d ∈ (Im(cd = pi ) ∪ Im(cd pi )) ∩ (Im(cd = pj )∪Im(cd pj ))
, where Im stands for the image of the function. We now show that given an accepting run of M for T , we can find a model T that is also accepted by M together with a data run on it. Moreover we show that we can assume that M is ranked. In this way we explicitly present the steps that A M needs to perform to reach the desired final extended state. We can see that having a data run on a ranked tree implies having a run in A M and then in the emptiness algorithm, as the ≡ E -relation needed at each step can be deduced from the cd functions of the involved nodes.

• for every i ∈ N, pi ∈ Pos(T ), if δ(p) ∈ δ(T | pi ), then δ(p) ∈ Im(cd = pi ) ∪ Im(cd pi ), • (Im(cd = p )∪Im(cd p )) ⊆ pi∈Pos(T ) (Im(cd = pi )∪ Im(cd pi ) ∪ {δ(p)}) • for each atomic formula ∃(k 1 , k 2 ) ∈ atForm M such that v p (∃(k 1 , k 2 ) ) = 1,
Let λ be the run of the automaton M on a model T . We show that there exists a model T and data run α such that for every p ∈ Pos(T ), α(p) = (c p , cd = p , cd p ) and 1. T is S-strongly equivalent to T for some S, 2. C(v ε ) = λ(ε) for v ε the valuation of c ε , 3. for every p, δ(p) ∈ Im(cd = p ) ∪ Im(cd p ), 4. α(ε) is incomplete, 5. T and T have the same height, 6. S ∩ δ(T ) = ∅.

We proceed by induction on the height of the tree T . The general strategy is first to apply inductive hypothesis on all the immediate subtrees of the root. Then, we select the data values necessary to validate all the formulae at the root. For example, if in the root of T the formula ∃(k 1 , k 2 ) = is true, then we select two data values that 'witness' this formula in T . Equivalently, if for a certain state k all the runs ending in k retrieve the same data value d, then the component D = (χ(k)) of the extended state at the root must describe the datum d. In this case, we also select the data value (d) to witness this. For each subtree that contains one of these data values, we make sure that it is described by the extended state by a 'Completion Lemma' we will later prove.

The base case is immediate by definition. So let us suppose we are in a model T such that the root has u immediate descendants 1 . . . u for any u ∈ N. Suppose by inductive hypothesis that we have data runs α 1 . . . α u for some models T 1 . . . T u such that they are all incomplete in the root and T i is X i -strongly equivalent to T | i for some X i ⊂ ∆. Wlog we can assume that i X i ∩ δ(T ) = ∅ and that ∀i = j : X i ∩ X j = ∅ (it is an easy exercise using condition 6 to see that otherwise we can do a data transformation via a bijection).

Let v ε : Form → {0, 1} be the valuation witnessed in the root of T . In the following construction we use a set G which initially is {d}, with d the data value of the root. The idea is that depending on the valuation v ε we collect in G all the data values of T necessary to witness all existential formulae and place them all in the D-component of c 0 . Here, using the strong S-equivalence property of T

1 . . . T u wrt T | 1 . . . T | u , we know that if d ∈ δ(T | i ) is a witness in T | i , then d ∈ δ(T i )
and it is also a witness.

If v ε (∃(k 1 , k 2 ) ) = 1, then there are two (or one) data values d 1 , d 2 involved in the satisfaction of this formula. We pick any two, and add them to G. For every immediate subtree T i and data run that contains d 1 we can apply the Completion Lemma we will see next, extending this model into a S d1 i -strongly equivalent one T d1 i (for some S d1 i ) such that there exists a data run α i where if

α i (ε) = (c i , cd = i , cd i ) then d 1 ∈ Im(cd = i ) ∪ Im(cd i ).
We repeat the process for d 2 and for all formulae ∃(k 1 , k 2 ) that hold in the root. We do this for all the existential formulae whose valuation is 1.

It is easy to see that we can assume that all the S d i are disjoint, and that they are also disjoint from δ(T ). This is due to the fact that

S d i ∩ (Im(cd = i ) ∪ Im(cd i )) = ∅ by the Completion Lemma.
We then build the model T as s, d (T 1 . . . T z ) where T 1 . . . T z are all the models T d i obtained before, and s, d is the root of T . We can verify then that the height between T and T remains unchanged (condition 5). Wlog we assume that for any of the data values 'd' that were considered before (i.e., the ones in G), d ∈ δ(T d j ) iff d = d . We can always apply a data bijection to the subtrees to be sure that this is the case.

We define α as follows: α(ε) = (c ε , cd = ε , cd ε ) where c ε = (v, D = , D ) and v, D = and cd = ε are the ones inferred from the model T (that is, the only ones such that T £ c ε ). In order to obtain D ε and cd ε , we use the set G that contains the data values that witness the existential formulae.

If G = {d 1 , . . . d r }, define D (i) = Reach(d i ) if i ≤ r and d i ∈ Im(cd = ε ) and also define cd ε (i) = d i . Otherwise, D (i) = ∅ and cd ε (i) is undefined. It is easy to see that as |G| ≤ 2|K| 2 + 2|K| + 1 < t 0 , α(ε) is clearly incomplete (condition 4). Finally, define S = i X i ∪ i S i . By this definition of S condition 6 is valid.
We can see that condition 2 holds and that α is a welldefined data run. All existential formulae ∃(k 1 , k 2 ) with true valuation in v ε at the root of T are witnessed by the D-components of the immediate subtrees of the root and hence continue to be true. On the other hand, the formulae such that ∃(k 1 , k 2 ) = with false valuation in T are taken care of by the D = -component. Finally, the formulae ∃(k 1 , k 2 ) = with false valuation obviously continue to be false because we are collapsing only data values of the D-component. Note that the difference is that now we are exactly under the hypothesis of the algorithm, where only the data values of the D-component are merged, according to the cd functions. We can then check that α is a well defined data run.

We have then showed the existence of a data run and a witnessing tree for every model accepted by M . In order to finally show that there is a run of algorithm that reaches the extended state of the root of the data run, we must show that all this can be done with a tree with bounded rank. Moreover, with the rank used in the emptiness algorithm (2|K| 2 +|K|+2)|K|. This is shown with a simple argument by the Bounded Rank Lemma. This concludes the proof of correctness of the emptiness algorithm. Lemma 1. [Incompletion Lemma] For any data run α on T there is another one α on the same model T such that the extended state of the root is incomplete.

Proof. If α(ε) is complete, it means that all 2|K| 2 + 2 registers of D are defined, where we use 'register' to refer to each of the components of the D tuple. It is easy to see that in order to witness all the existential formulae that hold in v ε we need only -at most-2|K| 2 . If the data value of the root is also preserved, we need not more than 2|K| 2 + 1 data values. Then there must be an element D(i) that is either the empty set, or that is not necessary to verify all the existential formulae of v ε . We can then replace Otherwise, d is included in one (and only one) subtree i among the u immediate subtrees of the root. The uniqueness is due to the fact that we are working with a data run, under the hypothesis that data values that can be shared among the subtrees are those declared in the cd functions (which is the case we have already ruled out).

D = D[i → ∅], cd = cd[i → ⊥].
If α(i) is complete, applying the Incompletion Lemma we obtain β i an incomplete data run on T | i , and in this way we 'make room' for d. We now apply inductive hypothesis on T | i , β i with the datum d. We obtain a data run γ i , the model T i and a data set S i . We can assume wlog that S i is different from δ(T ) and that T i has a data set different from T except perhaps in the data values of the cd functions of γ

i . So, δ(T i ) ∩ δ(T ) ⊆ Im(cd = i ) ∪ Im(cd i )
, where cd a i are the ones defined in γ i (ε).

Let d be a fresh data value not in δ(T ) nor in S i and define the data transformation f = id[d → d ], and

T b i = f (T | i ).
We call that a sub-branch of B ν i . . . ν j is a 'safe zone' iff it is a maximal subbranch such that it does not contain elements with label 'wit : e' for some e. As a direct consequence of the bound on the number of witness elements, there are at most 2|η| 2 + 1 safe zones in B.

If two elements ν i , ν j , i < j inside the same safe zone are tagged with the same label, we claim that the branch can be shortened preserving the satisfaction of all the subformulae of η at the nodes ν 1 . . . ν i . The operation consists in replacing in T the subtree of ν i by that of ν j .

It is easy to see that the satisfaction of e i -formulae is preserved as all its witness are maintained. It is easy to see that there will not be new elements that satisfy a path subformula, because we only erased nodes from the tree, preserving the descendant relation. This is due to the fact that any path expression that is true in the modified model, was true in the previous one.

We can conclude that we can assume that in a safe zone there are no more than |η| 3 different tags, and different elements (otherwise we can shorten the branch). Thus, we have that a branch has at most 2|η| 2 witnesses and 2|η| 2 + 1 safe zones of |η| 3 elements each. Then we can bound the length of any branch by 2|η| 2 + (2|η| 2 + 1).|η| 3 and thereby the height of the tree is polynomially bounded. Proof. The proof consists in coding an instance of the QBF validity problem in satisfiability of XPath(↓ * ).

Let ϕ = Q 1 p 1 . . . Q n p n .ψ where p i are propositional variables (pairwise distinct), Q i ∈ {∀, ∃} and ψ is a formula of the propositional calculus in CNF.

The idea is to force a model in which every branch contains a full valuation for the variables p 1 , . . . , p n where we force that all valuations present in the tree are contained in those specified by the quantifiers. The alphabet of this tree is Σ = {p 1 , . . . , p n , p1 , . . . , pn , X}, and every branch lists a valuation in order, that is, first there is a node with a label in {p 1 , p1 }, then another in {p 2 , p2 }, etc. The label X simply marks the ending of a valuation in a branch. Although there could be more valuations on p 1 . . . p n after an X, these are redundant, as there has been defined before X as well. After this marking we build the tree that satisfies ψ and finally we check that there are no inconsistencies with respect to its valuation.

Let v i be the formula that specifies that the node is a valuation for the propositional variable p i : v i = p i ∨ pi .

• If Q 1 = ∀, then f 1 = ↓ * [p 1 ] ∧ ↓ * [p 1 ] . If Q 1 = ∃, then f 1 = ↓ * [p 1 ] ∨ ↓ * [p 1 ] . • (i > 1) If Q i = ∀, then f i = ¬ ↓ * [v i-1 ∧ ¬( ↓ * [p i ] ∧ ↓ * [p i ])] . If Q i = ∃, then f i = ¬ ↓ * [v i-1 ∧ ¬( ↓ * p i ∨ ↓ * pi )] .
• ϕ X forces that the label X always appears once the valuation for all propositions has been defined.

ϕ X = ¬ ↓ * [v 1 ] ↓ * [v 2 ] • • • ↓ * [v n-1 ] ↓ * [v n ∧ ¬ ↓ * [X] ]
• For all X we build the formula for ψ = C 1 ∧ . . . ∧ C t where C i = t 1 ∨ . . . ∨ t ji and each t is a valuation for some p i . That is:

τ = Ci t∈Ci ↓ * [t]
where t is p j or pj for some j. And this must hold for all X-valued node:

ϕ ψ = ¬ ↓ * [X ∧ ¬τ ]
• Finally, we must check that no inconsistencies are to be found between the p i .

ϕ inc = n i=1 ¬ ↓ * [p i ] ↓ * [p i ] ∧ ¬ ↓ * [p i ] ↓ * [p i ]
The final formula is then

ϕ F = n i=1 f i ∧ ϕ X ∧ ϕ ψ ∧ ϕ inc
Lemma 4. ϕ is QBF-valid iff ϕ F is XPath(↓ * )-satisfiable.

Proof. The proof is straightforward and is left to the reader. Proposition 9. XPath(↓ * ) is in PSpace Proof. For any path formula p ∈ XPath(↓ * ) satisfied in T , by k witnesses of a branch ν 1 ≺ ν 2 ≺ . . . ≺ ν k . By induction on k using Lemma 5 we can easily show that it is then satisfiable in a model T where the witness ν i is at depth i for all 1 ≤ i ≤ k. This can be done for all path formulae that hold at the root.

On the other hand, by Lemma 6 below we can also assume that every internal node is the witness of -at most-one path subformula of an ancestor node. The normal form for a model T consists in:

1. For all nodes ν, ν , ν ∈ Pos(T ) and path formulae p, p ∈ XPath(↓ * ), if ν ∈ wit T (ν , p), ν ∈ wit T (ν , p ), then ν = ν . By the normal form we have that there will not be a repeated node in wit T (ν), and that all nodes will be of the form νi, with i ∈ N.

Suppose now that we have a branch B = ν 1 . . . ν z such that there exists a path formula p where (ν i , p) ∈ wit T (ν i-1 ), (ν j , p) ∈ wit T (ν j-1 ), that is, the path p is witnessed at two nodes ν i ≺ ν j along the branch B. Then we can safely replace T | i by T | j . Lemma 5. (Subtree copy.) XPath(↓ * ) is closed under subtree copy. That is, for every pair of contexts C 1 , C 2 , tree T and η ∈ XPath(↓ * ),

C 1 [C 2 [T ]] |= η iff C 1 [T , C 2 [T ]] |= η
where C[T 1 , T 2 ] is the operation of replacing the hole by a forest, in this case of two trees. Proof. It can easily seen by using Corollary 3.

Figure 1 :

 1 Figure 1: An example of merging, where D = may be assumed to be empty.

Figure 2 :

 2 Figure 2: The 4 cases for making ∃(k 1 , k 2 ) = true.

Figure 3 :

 3 Figure 3: Part of the model coding all the plays of row 5, which is between the #-element associated to 5 (101 in binary), and the element # with number 6 (110).

  complete Cor 1, Th 5 regXPath(↓, =) ExpTime-complete Cor 1, Th 5 XPath(↓ * , =) \ ε PSpace-complete Prop 4 All the results hold also in the absence of path unions.

Figure 4 :

 4 Summary of results. Proposition 5. SAT-XPath(↓ * ) is PSpace-complete. Proof (sketch). The lower bound is shown by coding the QBF problem. The upper bound is shown via the polydepth model property. It is slightly involved and requires to show a normal form of the model with the following property.

Definition 5 .

 5 [Strong S-equivalence] A context C is a data tree with a hole, we denote by C[T ] the substitution of the hole by T in C. We say that two models T and T are strongly S-equivalent for some S ⊆ ∆ if and only if for every context C such that δ(C) ∩ S = ∅ and for every bip automaton M , M accepts C[T ] iff M accepts C[T ].

Definition 6 .

 6 A data run on T is a labeling function α such that for every p ∈ Pos(T ), α(p) = (c p , cd = p , cd p ) where c p is an extended state, cd p : [1..t 0 ] → ∆ is a partial mapping from the D elements of c p to the represented data values in the model T and cd = p : [1.

  there exist at most two data values in Im(cd = p ) ∪ Im(cd p ) that witness the formula. That is, for example, if ∃(k 1 , k 2 ) = , then there are two data values d, d ∈ Im(cd = p ) ∪ Im(cd p ) and two runs ρ, ρ of the pathfinder automaton such that o(ρ) = (k 1 , d), o(ρ ) = (k 2 , d ) and d = d .If we also have that T has its rank bounded by the polynomial used by A M (2|K| 2 + |K| + 2)|K|, it is then easy to see that for every internal node p ∈ Pos(T ) the extended state corresponds to a transition of A M . We say that an extended state c is incomplete if D ε (i) = ∅ for some i ∈ [1..t 0 ] (or complete otherwise). We say that (c, cd = , cd ) is a dcompletion of (c , cd = , cd ) for d ∈ ∆ if either (i) all the components are equal (c = c , cd i = cd i ) and d ∈Im(cd = ) ∪ Im(cd ), or (ii) cd = = cd = , cd = cd [r → d]for some r such that cd (r) is undefined, and c and c differ only in that D (r) = ∅ in c .

Lemma 2 .

 2 [Completion Lemma] For any data run α on T with an incomplete extended state in the root, and for any d ∈ δ(T ) there is another run α on T and a set S ⊆ ∆ such that 1. T and T are strongly S-equivalent, 2. T and T have the same height, 3.δ(T ) ∩ S = ∅, d ∈ S, 4. α (ε) is a d-completion of α(ε),Proof. Suppose that r is such that D (r) = ∅ in the root and that α is the data run on T such that α(p) = (c p , cd = p , cd p ) for every p ∈ Pos(T ). If d was already in Im(cd = ε ) ∪ Im(cd ε ), there is nothing to be done. If d is in some Im(cd a i ) a ∈ {=, }, i ∈ N, then we only need to define cd ε (r) = d, D ε (r) = Reach(d) and S = ∅.

Corollary 2 .

 2 XPath(↓ * , =)\ε is PSpace-complete Proof. The membership in PSpace is an immediate consequence of Theorem 6 and Proposition 7. We can prove that XPath(↓ * ) is hard for PSpace by a reduction from the QBF-validity problem that can be found in Appendix E. E. Complexity of XPath(↓ * ) Proposition 8. XPath(↓ * ) is hard for PSpace.

2 .

 2 For every node ν ∈ Pos(T ) and path p, if wit T (ν, p) = . . . ν i , ν i+1 . . ., then ν i+1 = ν i n with n ∈ N.Let us define the set of subformulae sub as followssub(↓ * p) = {↓ * p} ∪ sub(p) sub([ϕ]p) = {[ϕ]p} ∪ sub(p) ∪ sub(ϕ) sub(εp) = sub(p) sub((p 1 ∪ p 2 )p 3 ) = {(p 1 ∪ p 2 )p 3 } ∪ sub(p 1 ) • p 3 ∪ sub(p 2 ) • p 3 ∪ sub(p 3 )Given a formula ϕ ∈ sub(η) satisfied in a node ν ∈ Pos(T ), it can either be• completely satisfied in ν in the case [[ϕ]] T (ν, ν)• partially satisfied in ν and witnessed in another node ν ν such that ν satisfies a formula of the next step of ϕ, ns(ϕ).ns((p1 ∪ p 2 )p 3 ) = ns(p 1 ) • p 3 ∪ ns(p 2 • p 3 ∪ ns(p 3 ) ns(p 1 p 2 ) = ns(p 1 ) • p 2 ∪ ns(p 2 ) ns(εp) = ns(p) ns([ψ]p) = ns(p) ns(↓ * p) = {p}It is easy to see that ns(p) ⊆ sub(p). We can then assume that there exists a function wit T (ν) ⊆ Pos(T ) × sub(η) that describes for each node ν, a finite set of witnesses. For example, if (↓ * [a] ∪ ε) ↓ * [b] holds in ν, then it could be that (ν , [a] ↓ * [b]) ∈ wit T (ν), or (ν , ↓ * [b]) ∈ wit T (ν) for some node ν ν.

Proof.

  It is easy to see that all path formulae that hold at the root ofC 1 [C 2 [T ]], hold also in C 1 [T , C 2 [T ]] |= η as it is an extension of the tree. On the other hand, any path formula that is satisfied by a succession of nodes in a branch inC 1 [T , C 2 [T ]] |= η, can also be found in C 1 [C 2 [T ]].In other words, the logic XPath(↓ * ) is closed under subtree copy. Corollary 3. XPath(↓ * ) is closed under replication of subtrees. Lemma 6. (Demand splitting) If η is satisfiable, then it is satisfiable in a model such that all the path subformulae p ∈ sub(η) are satisfied in incomparable subtrees. More formally, if p, p ∈ sub(η) such that p, p |= T with wit T (p) = ν 1 . . ., wit T (p ) = ν 1 . . ., then ν 1 ≺ ν 1 and ν 1 ≺ ν 1 .

  a function v : atForm M → {0, 1} that specifies which of the formulae of M hold at the abstracted node. Here, atForm M is the (finite) subset of atomic formulae (i.e., with no boolean connectors) of Form M .• D = D , D = consistsin two descriptions of a polynomial number of data values. D = ∈ (2 K ) |K| describes at most |K| data values, and D ∈ (2 K ) t0 at most t 0 . We will later detail exactly what this represents. It is easy to check that |Q A | is exponential in |M |. In Example 4, D = is represented by the path expressions α s.t.

#α = 1 and the data descriptions associated to them, and D by the remaining data descriptions. Each extended state represents a class of models. Before presenting the abstraction, let us fix some notation.

Acknowledgments. I am grateful to Luc Segoufin and Stéphane Demri for helpful discussions and for critically reading this manuscript.

* 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.

Then the final model is,

, where G = (Im(cd = γ ) ∪ Im(cd γ )) ∩ δ(T ) with the maps cd = γ and cd γ defined in γ(ε); and (s ε , d ε ) is the root symbol and datum of T .

By this definition, S is different from all the data values of T and from d, and then condition 3 is then satisfied. The data run α for this model is defined by

It is immediate that α is a completion of α (condition 4). It can be verified that by construction α is a well-defined data run on T , and that T and T are equivalent for contexts with no data values in S. This is mainly because when the copy of the tree is made, we are careful enough not to change the data values contained in the cd functions (especially cd = ). It is evident that the height was preserved (condition 2). Lemma 3. (Bounded rank) Given a data run α on T , there is another one α on T such that

• T is a subtree of T .

Proof. In α(ε) we have the description of at most 2|K| 2 + |K| + 2 data values, each one with its description in D = or D . Let d be one of the data values of Im(cd = ε ) ∪ Im(cd ε ), and let S ⊆ K be the description of it. It is easy to see that in order to preserve the description we need to keep at most |S| immediate subtrees, as in the worst case each one of them would contribute with one state of S. Doing this for all data values we obtain that we just need to select at most (2|K| Proof. For any formula η and data tree we show that we can describe each element of a given branch using only a polynomial number of descriptions. As a result, we prove that there is a polynomial bound on the height of the tree. Otherwise, we show show long branches can be 'shortened' preserving satisfiability of η.

For any two positions p 1 , p 2 ∈ Pos(T ), let us call p 1 ≺ p 2 iff p 1 is a prefix of p 2 , which means that p 2 is a descendant of p 1 . The key observation for this proof is that

∈ {=, =} is true at a certain position ν ∈ Pos(T ), then it is true at all positions µ ≺ ν. That is, at all nodes that occur before ν (i.e., closer to the root).

• If a formula of the type ¬(↓ * p 1 ↓ * p 2 ), ∈ {=, =} is true at a certain position ν ∈ Pos(T ), then it is true at all positions µ ∈ Pos(T ) such that µ ν. That is, at all the nodes that are in the subtree generated by ν.

We can see that this fact also extends to unions and then to any path formula of the fragment, as any of the basic bricks of the path start always with ↓ * .

Let η be a formula that is satisfied in a model T . Let B = ν 1 . . . ν k be a maximal branch of this model where ν 1 is the root and ν k is a leaf. We show that this branch can be bounded by a polynomial on |η|. We order all the path subformulae of η in a sequence E whose elements we denote by e i and are of the from p or p p (with p, p path expressions). Each one of these formulae has associated a position in the branch, pos B (e) = i iff ν i satisfies e and there is no ν j with j < i that satisfies it. We assume then that E = (e 1 . . . e t ) is ordered according to this notion of first or last appearance given by pos B . Here, t is clearly bounded by the number of subformulae of η, bounded by 2|η|. We can then label each node ν of the branch by an index i (0 ≤ i ≤ t) meaning that {e 1 . . . e i } is the set of path subformulae of η that are verified in ν.

On the other hand, for every e i ∈ E, we must consider the succession of nodes necessary for witnessing this formula in this model. For instance, the formula ↓ * [ϕ] ↓ * [ψ] may need two nodes to be satisfied. In general, a path expression p that contains n appearances of ↓ * needs at most n 'witness' nodes to be satisfied, and as in our case p is a subformula of η we can safely bound n by |η|. The strategy is to preserve all the nodes necessary to witness e i in the node ν pos B (ei) . The idea is that by preserving all the nodes necessary to satisfy the formula at this node, we are actually making sure that all precedent nodes also satisfy the formula. Some of them will be in the (sub-)branch ν pos B (ei) . . . ν k , some not. For those that are on the branch we label each element with the tag 'wit : e i ', for those that are not on the branch, we tag their projection on the branch (i.e., the closest ancestor on B) with 'wit : e i '. Summing up, for each 1 ≤ i ≤ e we have at most |η| elements of B tagged by 'wit : e i ', and then at most 2|η| 2 number of witnesses of any formula along the branch.

We then have as tag of each element of B a triple of (1) an index i of path subformulae that are satisfied, (2) the symbol of the node a ∈ Σ, and (3) perhaps the label wit : e if it is witness of a path formula.