Diego Figueira

Decidability of downward XPath

Keywords: I.7.2 [Document Preparation]: Markup Languages, H.2.3 [Database Management]: Languages, H.2.3 [Languages]: Query Languages Algorithms, Languages data tree, XML, XPath, downward data automata, DD automata, data values, infinite alphabet, emptiness, satisfiability, extensible language

We investigate the satisfiability problem for downward-XPath, the fragment of XPath that includes the child and descendant axes, and tests for (in)equality of attributes' values. We prove that this problem is decidable, ExpTime-complete. These bounds also hold when path expressions allow closure under the Kleene star operator. To obtain these results, we introduce a Downward Data automata model (DD automata) over trees with data, which has a decidable emptiness problem. Satisfiability of downward-XPath can be reduced to the emptiness problem of DD automata and hence its decidability follows. Although downward-XPath does not include any horizontal axis, DD automata are more expressive and can perform some horizontal tests. Thus, we show that the satisfiability remains in ExpTime even in the presence of the regular constraints expressible by DD automata. However, the same problem in the presence of any regular constraint is known to have a non-primitive recursive complexity. Finally, we give the exact complexity of the satisfiability problem for several fragments of downward-XPath.

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

Query containment and query equivalence are important static analysis problems, which are useful to query optimization tasks. In logics closed under boolean operators, these problems reduce to checking for satisfiability: Is there a document on which a given query has a non-empty result? By answering this question we can decide at compile time whether the query contains a contradiction and thus the computation of the query (or subquery) on the document can be avoided. Or, Author's address: 10 Crichton Street, Edinburgh EH8 9AB, UK. The author acknowledges 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. Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee. c 2000 ACM 1529-3785/2000/0700-0001 $5.00 by answering the query equivalence problem, one can test if a query can be safely replaced by another one which is more optimized in some sense (e.g., in the use of some resource). Moreover, the satisfiability problem is crucial for applications on security [START_REF] Fan | Secure XML querying with security views[END_REF], type checking transformations [START_REF] Martens | Frontiers of tractability for typechecking simple xml transformations[END_REF], and consistency of xml specifications.

Core-XPath (term introduced in [START_REF] Gottlob | Efficient algorithms for processing XPath queries[END_REF]) is the fragment of XPath 1.0 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. The extension of this language with the possibility to make equality and inequality tests between attributes of elements in the xml document is named Core-Data-XPath in [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF]]. The satisfiability problem for this logic is undecidable, as shown in [Geerts and Fan 2005]. It is then reasonable to study the interaction between different navigational fragments of XPath with equality tests with the aim of finding decidable and computationally well-behaved fragments. In the present work, we focus on the downward-looking fragments of XPath, from now on denoted by XPath(↓ * , ↓, =), where navigation between nodes can only be done in the downward direction: from the root towards the leaves. With this logic one can express, for example, that every node labeled a has a descendant b with the same data value, or that there are no two descendant nodes labled with c and d with the same data value. We remark that the logics we treat here correspond to subsets of the W3C standard XPath 1.0 [START_REF] Clark | XML path language (XPath)[END_REF], for a complete formal semantics see [START_REF] Gottlob | Efficient algorithms for processing xpath queries[END_REF]. XPath 2.0 is a radically different language than XPath 1.0. It integrates XPath and XQuery in a common syntax, and includes variables and explicit quantification. These constructs are out of the scope of the current work.

Our main contribution is that the satisfiability problem for XPath(↓ * , ↓, =) is decidable. This is the fragment with equality and inequality tests of attributes' values, the ↓ * axis that can access descendant nodes at any depth and the ↓ axis to access child elements.1 Actually, 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. We nail down the precise complexity showing an ExpTime decision procedure. The problem is hence ExpTime-complete since XPath(↓, ↓ * ) is already ExpTime-hard by [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]. To obtain this bound, we introduce the class of Downward Data automata (DD automata). We show that any regXPath(↓, =) formula can be efficiently translated to an equivalent DD automaton. This automata model has a 2ExpTime emptiness problem, but can be shown to be decidable in ExpTime when restricted to the sub-class of automata needed to capture regXPath(↓, =). In this way we obtain an ExpTime procedure for the satisfiability of regXPath(↓, =).

In fact, DD automata are more expressive than regXPath(↓, =), and this is true even for the aforementioned sub-class of automata. For example, although regXPath(↓, =) does not include any horizontal axis, DD automata can test for • 3 certain horizontal properties. This model can express, for instance, that the sequence of children of the root is described by the regular expression (a b c) * . It will then follow that the satisfiability problem for regXPath(↓, =) under the regular constraints that can be expressed by DD automata remains decidable in ExpTime. This is a particularly well behaved class of regular properties, since the satisfiability problem of regXPath(↓, =) restricted to regular tree languages is known to have non-primitive recursive complexity. 2On 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 seems to rely on data equality tests, as the corresponding fragment XPath(↓ * ) without unions is shown to be PSpace-complete. We thus prove that the satisfiability problems 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 by showing that satisfiability for XPath(↓, =) is also PSpace-complete. Our results, together with the results of [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF][START_REF] Marx | XPath with conditional axis relations[END_REF]], establish the precise complexity for all downward fragments of XPath with and without data tests (cf. Table IV on page 44).

Related work

The main results of this work first appeared in the conference paper [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF]]. The cited work does not contain a full proof of the decidability of the downward fragment of XPath, but only the main ideas due to a space limitation. Here we give a full and detailed proof by a reduction to a powerful class of automata, and we extend some results. Although the main XPath results of [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF]] are the same as of the present work, the underlying automata model is completely different. There are basically two reasons to adopt a different strategy to show the decidability. First, the automaton introduced here is simpler than the one of [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF]]: it does not require a nested definition between two different kinds of automata as in [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF]]. And second, it is more general: it can express data properties that cannot be expressed in the model of [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF]], and it can test (weak) regular properties on the sequence of children of a node. The larger expressive power of the automata model yields a decidability procedure for the satisfiability of downward-XPath under a subclass of regular properties, something that was out of the scope of [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF]]. The results of this paper also appear in the doctoral dissertation [Figueira 2010b, Chapter 5]. [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] study the satisfiability problem for many XPath logics, mostly fragments without negation or without data equality tests. Also, the fragment XPath(↓, =) is shown to be in NExpTime. We improve this result by providing an optimal PSpace upper bound. It is also known that XPath(↓) is already PSpace-hard3 , and in this work we give a matching upper bound showing PSpace-completeness. Furthermore, [START_REF] Marx | XPath with conditional axis relations[END_REF] proves that XPath(↓, ↓ * ) is 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 study XPath(↓ * , =), a fragment that is not considered in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF], and show that XPath(↓ * , =) is ExpTime-complete while XPath(↓ * ) is PSpace-complete. In this case, data tests do make a real difference in complexity (at least under widelyheld complexity theoretical assumptions).

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 expressiveequivalent to Core-XPath (cf. [START_REF] Marx | First order paths in ordered trees[END_REF]), F O 2 with data equality tests is 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 showed the decidability of a fragment of XPath(↑, ↓, ←, →, =) with sibling and upward axes but restricted to local elements accessible by a 'one-step' relation, i.e., parent, child, previous-sibling, next-sibling. This fragment is restricted to using data formulae of the kind ε = α (or ε = α ) that test whether a data value accessible with a path expression α is equal to the data value of the current point of evaluation (denoted by ε). In contrast, the fragments we treat here disallow upward and sibling axes but allow the descendant ↓ * axis and arbitrary α = α , α = α data test expressions.

In [Figueira 2010a] the fragment XPath(↓, ↓ * , →, → * , =) is treated, denominated 'forward-XPath'. In the cited work, the full set of downward (child, descendant) and rightward (next-sibling, following-sibling) axes are allowed. This logic can express, for example, a key constraint property on a label a (i.e., that all the nodes labeled with a have different data values), which cannot be expressed in downward-XPath. The satisfiability problem for forward-XPath is shown to still be decidable in [Figueira 2010a]. Also, in [START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF], the satisfiability problem for XPath(↓, ↓ * , ↑, ↑ * , =) is shown to be decidable. This fragment is an extension of the downward fragment with the parent (↑) and ancestor (↑ * ) relations, and it is called vertical -XPath. However, these decidability results come at the expense of a huge rise in complexity with respect to the downward fragment. Indeed, the time or space required by the decidability procedure for the satisfiability of the forward or vertical fragments cannot be bounded by any primitive recursive function [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF]. In fact, this non-primitive recursive lower-bound holds for any XPath fragment containing (or being able to express) any of the axes → + , ↑ + , + ← as shown in [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. 4 However, all the downward fragments are below ExpTime, as evidenced in our present work. Meeting these elementary upper bounds requires an altogether different approach from the ones taken in [Figueira 2010a;[START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF].

PRELIMINARIES Notation

We first fix some basic notation. Let N = {1, 2, 3, . . . }, and let [n] := {1, . . . , n} for n ∈ N. By ℘(S) we denote the power set of a set S. We use letters A, B to denote finite alphabets, D to denote a countably infinite domain (e.g., N) and the letters E and F to denote any kind (finite or infinite) of set. In our examples we will consider D = N. We define the composition (f

• 5 a, 2 a, 2 b, 2 b, 9 b, 5 b, 3 a, 2 b, 1 b, 2
• g)(x) = f (g(x)
).

Unranked ordered finite trees

We define Trees(E), the set of finite, ordered and unranked trees over an arbitrary alphabet E.

A position of a tree is an element of N * . The root's position is the empty string and we denote it by . The position of any other node in the tree is the position of its parent appended to a number s + 1 ∈ N, where s is the number of the node's left siblings. We write '•' for the concatenation operator, and we use x, y, z, w, v as variables for positions, and i, j, k, l, m, n as variables for numbers. Thus, for example, x•i is a position which is not the root, that has i -1 siblings to the left, and has x as parent position.

Formally, we define TreesPos ⊆ ℘(N * ) the set of sets of finite tree positions, such that: Given a tree t ∈ Trees(E), pos(t) denotes the domain P and alph(t) the alphabet E of the tree. From now on, we informally refer by 'node' to a position x together with the value t(x). We define the ancestor partial order as the prefix relation x x•y for every x, y, and ≺ as the strict prefix relation x ≺ x•y for |y| > 0. We say that two positions x, y are incomparable if x y and y x. Given a tree t and x ∈ pos(t), t| x denotes the subtree of t at position x. That is, t| x : {y | x•y ∈ pos(t)} → alph(t) is the tree t| x (y) = t(x•y). The notation f | x is generalized to any function f whose domain is in TreesPos. In the context of a tree t, a siblinghood is a maximal sequence of siblings or, in other words, a sequence of positions x•1, . . . , x•l ∈ pos(t) such that x•(l + 1) ∈ pos(t). Given a tree t and a position x, we define #children(t,

P ∈ TreesPos iff (a) P ⊆ N * , |P | < ∞; (b) it is prefix-closed; and (c) if n•(i + 1) ∈ P for i ∈ N, then n•i ∈ P . A
x) = |{x•i | x•i ∈ pos(t)}|.
Given two trees t 1 ∈ Trees(E), t 2 ∈ Trees(F) with the same set of positions P (i.e., pos(t 1 ) = pos(t 2 ) = P ), we define

t 1 ⊗ t 2 : P → (E×F) by (t 1 ⊗ t 2 )(x) = (t 1 (x), t 2 (x)).
The set of data trees over a finite alphabet A and an infinite domain D is defined as Trees(A×D). Note that every tree t ∈ Trees(A×D) can be decomposed into two trees a ∈ Trees(A) and d ∈ Trees(D) such that t = a ⊗ d. Figure 1 shows an example of a data tree. We denote the set of data values used in a data tree with

data(a ⊗ d) := {d(x) | x ∈ pos(d)} .
We freely extend this notation and denote by data(X) all the elements of D contained in X, for whatever object X may be.

Regular properties on branches

One important object of a data tree is that of a 'branch': a succession of nodes that starts at the root and goes downward, ending at any node of the tree. Note that we consider the possibility that a branch may end at an inner node and not necessarily at a leaf. Given two positions x ≺ y in a branch, we define str(x, y) as the string of labels from the finite alphabet contained between x and y, including x and y. All the power of the automata model we will define relies on the ability to test data properties at distant positions of the tree. These positions are end points of branches whose string belongs to a certain regular language. We next define the execution of a nondeterministic finite automaton over a branch of a data tree.

NFAs A = (A, Q, q 1 , δ, F ) are defined as usual, that is, A is a finite alphabet, Q is a finite set of states, q 1 is the initial state, δ ⊆ Q × A × Q is the transition function, and F ⊆ Q is the final set of states. As usual, L(A) denotes the set of strings accepted by A. We write (q, a, q ) ∈ A to denote that there is a transition from q to q in A by reading a.

Let t = a⊗b be a data tree in Trees(A×D). Given a NFA A over the alphabet A, we consider the execution of A on the string contained between a position x ∈ pos(t) and a descendant position x•y ∈ pos(t). For a state q, let A[q] be identical to A with the exception that now q is the initial state.

We note a 'one-step' of the execution as q A -→

x q if (q, a(x), q ) is a transition of A, the data tree being implicit in the notation. And we write

q A -→ x,x•y q iff    q A -→ x q if y = ; q A -→ x p 1 A -→ x•i1 p 2 A -→ x•i1•i2 • • • A -→ x•i1••••in p n+1 = q if y = i 1 • • • • i n .
That is, if we can reach the configuration by reading the letters between x and x•y in a descending way. Note that the automaton's run includes the starting and ending labels. Hence, all runs execute at least one transition. We fix a notation for the data values of those positions selected by some run of A. For a state q of A and a tree t, we write [[A, q]] t to denote the set of data values of all positions x that can be reached starting at the root with state q and ending at x with a final state from F ,

[[A, q]] t = {d(x) | x ∈ pos(t), str( , x) ∈ L(A[q])} . We write [[A]] t for [[A, q 1 ]] t
, where q 1 is the initial state of A.

AUTOMATA MODEL

In this section we define an automata model that runs over data trees. We show that this model has a decidable emptiness problem in Section 4. In Section 6.1 we

• 7

show that XPath(↓ * , ↓, =) formulae can be effectively translated to an equivalent DD automaton, thus obtaining a decidability procedure for its satisfiability problem.

Our model, called Downward Data automaton (or simply DD automaton), has an execution that consists of two steps: (1) the execution of a transducer, and (2) the verification of data properties of the transduced tree.

For a data tree t = a ⊗ d, the first step consists in the translation of a into another tree b. This is done using a nondeterministic letter-to-letter transducer over unranked trees. We adopt a more detailed definition, where the transducer explicitly has as a parameter the class C of regular properties that it can test over a siblinghood at each transition. If we take this parameter to be the set of all regular properties, this automaton is a standard transducer over unranked trees. However, the emptiness problem for Downward Data automata has a very high complexity lower bound unless we restrict C to be a suitable subclass of regular languages (cf. discussion on page 9). This class, defined as the set of extensible languages, will be introduced in the sequel (Definition 3.7).

In the second step, for every subtree of the transduced tree b ⊗ d, a property on the data values of the tree is verified. The letter at the root of the subtree under inspection determines the property to verify. The properties are boolean combinations of tests verifying the existence of data values shared by nodes in the subtree, hanging from branches satisfying some regular expression.

A brief comment on notation. In the definition of these automata there will be two sorts of sets of states, namely the states corresponding to the run of the transducer, and the states corresponding to the run of the verifier. To avoid confusion we consistently write Q, q, q , . . . as symbols for the states of the transducer, and Q, q, q , . . . for the states of the verifier.

Transducer

Let C be a subclass of regular languages C ⊆ REG. We define a bottom-up unranked tree transducer. This definition is parametrized by C in the following sense: At every transition, the automaton can test the siblinghood for membership in some regular language that must be in the class C .

-Q is a finite set of states, -QF ⊆ Q is the set of final states, -C ⊆ REG( Q) is a class of regular languages over the alphabet Q, -δ ⊆ Q × A × B × C is a finite set of transitions. We define a ⊗ b ∈ R iff a ∈ Trees(A), b ∈ Trees(B)
with pos(a) = pos(b) = P , and there exists a state assigment ρ : P → Q, such that -for every leaf x, there exists L ∈ C with ∈ L and (ρ(x), a(x), b(x), L) ∈ δ, -for every siblinghood x•1, . . . , x•l, there is

L ∈ C such that (ρ(x), a(x), b(x), L) ∈ δ and ρ(x•1)• • • • •ρ(x•l) ∈ L.
We call ρ a run of R on a ⊗ b. We say that the run is accepting iff ρ( ) ∈ QF .

We now turn to the second step.

Verifier

Definition 3.2. A verifier V ⊆ Trees(B×D) defines a set of data trees that are valid with respect to some data properties. It is a tuple A 1 , . . . , A K , v of K NFA over the alphabet B, namely A 1 , . . . , A K , and a function v : B → Φ mapping letters of the alphabet to formulae expressing data properties. The idea is that every subtree t| x of the original tree t must verify a property expressed by the formula v(b(x)). A typical property that we can test at a subtree is the existence of two positions with the same data value, such that one is reachable by going downward through a branch whose labelling is in some regular language L 1 , and the other by some other branch with labelling in L 2 .

The properties of Φ are a subset of closed first-order formulae with no quantifier alternation (that is, no ∀∃ or ∃∀ patterns allowed), and K unary relations, one for every automaton A i , namely D 1 , . . . , D K .

Given a set Vars of variables, Φ contains all the formulae φ defined by the grammar

φ ::= ¬ φ | φ ∧ φ | φ ∨ φ | ∃v.ψ ψ ::= ψ ∧ ψ | ψ ∨ ψ | v = v | v = v | D i (v)
where v stands for a set of variables from Vars, v, v ∈ Vars, i ∈ [K], and we restrict φ to have no free variables. The variables are interpreted over the set of data values, and the D i 's as sets of values reachable by the automata A i 's.

Given a data tree t, let I t be the first-order interpretation where each unary relation D i is interpreted as [[A i ]] t , and the interpretation of the domain is D. We say that that ϕ is verified in t if ϕ is true under the interpretation I t . A verifier A 1 , . . . , A K , v accepts a data tree t = a ⊗ d ∈ Trees(B×D) if for every position

x ∈ pos(t) the formula v(a(x)) is verified in the subtree t| x . Example 3.3. Suppose v(a) = ∃ x 1 , x 2 . D 1 (x 1 ) ∧ D 2 (x 2 ) ∧ x 1 = x 2 ,
for a letter a. This means that for every a-rooted subtree we can find two branches in the regular languages recognized by A 1 and A 2 respectively leading to two nodes whose data values are different as depicted in Figure 2. A data tree a ⊗ d is accepted by (R , V ) iff there exists b ∈ Trees(B) such that a ⊗ b ∈ R and b ⊗ d ∈ V , as depicted in Figure 3. When we want to make explicit that the witnessing tree for the acceptance of a ⊗ d is b, we will say equivalently

• 9 ∈ L 1 L 2 = ∈ L 1 L 2 = Fig. 2. If L 1 , L 2
are the languages recognized by A 1 , A 2 , and the marked positions are labeled by

a, then v(a) is verified in both subtrees. a ⊗ d a ⊗ b b ⊗ d ⇐⇒ R V (R , V ) ∈ ∈ ∈ Fig. 3. Acceptance condition of a DD automaton (R , V ). that a ⊗ b ⊗ d is accepted by (R , V ). Also, we say that a ⊗ b ⊗ d has a run if there is a run of R on a ⊗ b, where b ⊗ d ∈ V .
We now give some closure properties of DD automata. We say that a class of languages C is closed under componentwise product, if for every two languages L 1 , L 2 of C and the language

L 1 × c L 2 = {(a 1 , b 1 ) • • • (a n , b n ) | a 1 • • • a n ∈ L 1 , b 1 • • • b n ∈ L 2 } is in C . Note that if L 1 , L 2 are regular, L 1 × c L 2 is regular.
Proposition 3.5. Given a class C of languages closed under componentwise product, the class of languages recognized by C -DD automata is closed under intersection.

The proof of this proposition can be found in the online appendix.

To obtain closure under complementation we need some extra hypothesis. Given an alphabet A and a letter a ∈ A, we call the membership language of a to the language {w•a•w | w, w ∈ A * }. We also say that a class C ⊆ REG is closed under inverse homomorphisms if for every language L ∈ C over an alphabet A and for every homomorphism h :

B → A there is a language L ∈ C over B such that L = {w ∈ B * | h(w) ∈ L}.
Proposition 3.6. Let C a class of languages closed under intersection, complementation, inverse homomorphisms and containing all membership languages. The class of languages recognized by C -DD automata is closed under complementation.

The proof of this proposition can be found in the online appendix.

Complexity of emptiness problem. The emptiness problem for C -Downward Data automata has a non-primitive recursive complexity if we do not impose any restric-• Diego Figueira tion to C . The non-primitive recursive lower bound can be seen as a consequence of the fact that DD automata -can force the model to be linear (i.e., that all nodes have at most one child), and -can capture any downward XPath formula, as we will see in Section 6.1.

It is known that the satisfiability problem for downward XPath on non-branching data trees (called data word ) is non-primitive recursive (see e.g. [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]). Although the emptiness problem for DD automata without any restriction is not discussed here, we believe that it is decidable. Probably, it can be shown to be decidable via the theory of well quasi orderings, by a similar technique as the one used in [Figueira 2010a] in the context of downward alternating register automata.

Nevertheless, when C is restricted to have some good properties, emptiness of DD automata can be tested in 2ExpTime. Further, if the verifier is such that the number of occurrences of the relations D i inside every quantified subformula is bounded by a constant5 , we achieve an ExpTime decision procedure. We will show that downward XPath formulae can be translated in PTime into equivalent DD automata. These automata are restricted to a class of languages C with good properties, and such that the number of occurrences of the D i are always bounded by 2. Then, the decidability in ExpTime of the satisfiability problem for downward-XPath will follow. In the next section we define which is the necessary property that C must have in order to obtain the aforementioned upper bounds.

Extensibility of languages

To have a low complexity in the testing for emptiness of C -DD automata, we need to weaken the kind of regular properties that the transducer can verify. That is, we need to restrict C . The idea is that if a word is in a language, then an extension of the word where more occurrences of each letter may occur must also be in the language. Let us formally define this notion.

Let A = {a 1 , . . . , a n } be an alphabet and p be the Parikh image function. That is, the function p : A * → N n that associates each word with a vector that counts the number of appearances of each letter, p(w)(i) = |{j | w(j) = a i }|, where w(j) denotes the jth letter of the string w, starting at 1. Definition 3.7. We say that a regular language L is extensible if for every m ∈ N and word w ∈ L there exists another word w ∈ L such that for any coordinate

i ∈ [n], if p(w)(i) = 0 then p(w )(i) ≥ m, and if p(w)(i) = 0 then p(w )(i) = 0.
In this case we say that w is an m-extension of w. We write E for the class of all extensible regular languages. Likewise we define a tree language to be extensible if it can be defined by an unranked tree automaton whose transitions only use languages from E to test properties on the siblinghoods. Note that this is a restriction of the • 11 horizontal tests, and that an extensible tree language can still test for any regular property along a branch. By E tree we denote the set of extensible tree languages.

Let us give some examples of extensible classes of languages. As a first example, consider the following class of languages.

∃-class := {L A1,...,An,B | A 1 , . . . , A n and B are a finite alphabets, n ∈ N}, where L A1,...,An,B := {w ∈ (∪ i A i ∪ B) * | w contains at least one letter from each A i } Note that ∃-class is a class of extensible languages, it is closed under intersection, complementation, inverse homomorphisms and contains all membership languages. Therefore, the class of data tree languages accepted by ∃-class-DD automata is closed under complementation. If we also close ∃-class under componentwise product, we still obtain an extensible language. In this case, the class of languages accepted by DD automata is closed by all boolean operaitons. Also note that the class of ∃-class-transducers are those that can only test for the existence or non existence of children with a certain label, but they do not test any condition on the horizontal ordering or on the number of appearances of elements in the siblinghoods. In fact, they can mostly test for vertical properties along branches.

As another example, we define REG * the class of star -regular languages. The property of extensibility is trivially closed under union, but not necessarily under intersection or complementation.

Proposition 3.8. Given two extensible languages L 1 , L 2 , L 1 ∪ L 2 is also extensible. As a counter-example for the intersection, note that (ab) * ∩ a * b * = { , ab} which is not extensible, and for the complementation note also that under the singleton alphabet A = {a}, (a + a) c = { , a}, which is not extensible.

In the sequel, we will show decidability of the emptiness problem for E -DD automata.

THE EMPTINESS PROBLEM

Throughout this section, we fix the transducer to be an E -transducer. The main objective of this section is to prove the following theorem.

Theorem 4.1. The emptiness problem for E -Downward Data automata can be decided in 2ExpTime.

Sketch of the proof

The proof of the main theorem is divided into four parts. In the first part (Section 4.1) we define some decoration or marking of the nodes of a data trees that in some sense witnesses the acceptance of a run of a DD automaton. These decorations of the tree are the main structures with which we will work with in our proof.

The second part (Section 4.2) is dedicated to proving two properties. The first property states that if a DD automaton is nonempty, it accepts a tree decorated with some guidance system that marks the paths to be covered in order to verify the properties imposed by the verifier. In some sense, it decorates the tree as in Figure 2, avoiding having two paths going through the same node. The guidance system is called certificate and this property is called admissibility of correct certificates. The second property states that if a DD automaton is nonempty, then it accepts a tree whose data values are in a certain normal form, as follows. Every pair of subtrees rooted at two different children of a node, have a disjoint set of data values, with the exception of some polynomially bounded many (this is called the disjoint values property).

The third part (Section 4.3) is centered around proving that DD automata have the exponential width model property. That is, if a DD automaton has a nonempty language, then it accepts a tree whose width is exponentially bounded in the size of the automaton.

In the fourth part (Section 4.4) we give the algorithm for testing emptiness of DD automata, which is based on the bound on the width and the two previous properties: the disjoint values property and the admissibility of correct certificates.

Parameters

We first fix some parameters that we will need in the complexity analysis. We fix, once and for all, that the verifier V contains K NFA: A 1 , . . . , A K . We write Aut to denote the se of these automata, Aut = {A 1 , . . . , A K }. We assume without any loss of generality that all A 1 , . . . , A K share the same set of states Q := {q 1 , . . . , q N }, and have q 1 as initial state. Also, for each i we write Q Ai F for the set of final states of A i . By |A| we denote the number of transitions of A, and Aut stands

for |A 1 | + • • • + |A K |.
Let Vars be the set of variables used by the formulae of the verifier, and let |Vars| = V. We write R for the maximum number of relations admitted under a quantification. In other words, for any formula of the verifier and for any quantified subformula ∃x.ψ, there are at most R different relations used in ψ from the K available. The worst case would be when

R = K, as in the formula v(b) = ∃x.D 1 (x)∧• • •∧D K (x) for some b ∈ B.
This is an important parameter, since we will later see that the subclass of E -DD automata with R fixed has an ExpTime emptiness problem, while the general class has a 2ExpTime emptiness problem. In Section 6.1 we will argue that downward XPath expressions can be translated into E -DD automata where R = 2, and from this fact it will follow that its satisfiability is in ExpTime. Intuitively, the class of properties that do not have a bounded R are of the form there is a data value d accessible by n downward paths in the regular languages L 1 , . . . , L n but not by any path in the languages L 1 , . . . , L m , where n and m are parameters. To verify these properties with our approach would require double exponential time in n, m.

Finally, we fix Q to denote the set of states of the transducer. In addition, we use NFA to represent the regular language L for every transition ( q, a, b, L) ∈ δ. We will • 13 usually use the symbol B to denote such an automaton. We will assume without any loss of generality that all automata used in the transitions of the transducer share the same set of states Q = {q 0 , q1 , . . . } and that all automata have the same initial state q0 . |R | stands for the number of transitions of R , and we assume that | Q| is at most |R |. By |V | we denote K + N + R + V + Aut. Summing up, our complexity analysis will be based on the parameters:

K, N, R, V, | Q|, | Q|, |R |, Aut, |V |.

Decorations of trees

In order to bound the width of the tree, we need a more fine grained notion of runs of a transducer. We label the nodes of the tree with the run of the automaton recognizing the regular language on the siblinghood used at the transition of the transducer's run. This will enable us to state a pumping argument on siblinghoods of the data tree.

Detailed run

Consider, for any extensible language L ∈ E over Q, a NFA B L with initial state q0 . Remember that every B L used in the transducer uses the same set Q of states.

Definition 4.2. A detailed run of a transducer R on a tree a ⊗ b : P → A×B consists of a 3-uple (τ, ρ, ρ h ).
-ρ is a run, that in this context we call a vertical run.

-τ is the transition assignment τ : P → δ specifying which choice of transitions are needed for the run ρ. It verifies, for every position x with l children,

τ (x) = (ρ(x), a(x), b(x), L) where ρ(x•1) • • • ρ(x•l) ∈ L.
We abbreviate B x to denote the NFA B L of the regular language L defined in the transition τ (x) of the transducer's run.

-Finally, ρ h is an assignment from the set of positions P to the set of states of the automaton B that corresponds to the regular language that needs to be checked in order to apply the transition.

ρ h : P → Q .
We call ρ h the horizontal run. It verifies the following conditions (in short, that it is a run of a NFA on the siblinghood).

For every leftmost sibling

x•1 ∈ P , (q 0 , ρ(x•1), ρ h (x•1)) is a transition of B x .

For every pair of consecutive siblings

x•i, x•(i + 1) ∈ P , (ρ h (x•i), ρ(x•(i + 1)), ρ h (x•(i + 1))) is a transition of B x . 3. For every rightmost sibling x•l, ρ h (x•l) is a final state of B x .
This completes the definition of a detailed run.

We also need to be able to precisely describe the behavior of the data values at a position of a data tree.

Description of data

Next we introduce sets of data simultaneously accessible by R automata (remember that this is the maximum number of simultaneous relations D i 's used by the verifier V ). For each one of these sets of data values, we preserve at most V elements (this is a bound on the maximum number of variables used by V ).

Observe that the verifier can test properties of the set of the cardinality of the sets [[A i ]], or a boolean combination of them. More precisely, the verifier can only test the (in)existence of a number of data values that are in some intersection set

[[A i1 ]] ∩ • • • ∩ [[A it ]].
Here, A i1 , . . . , A it range over Aut, and t ≤ R. The tests boil down to checking whether -the intersection contains at least 1, 2, . . . , V different elements, or -the intersection contains at most 0, 1, . . . , V -1 different elements.

Note that we cannot test, for example, that the set contains exactly V elements, since we would need a formula with V + 1 variables. We annotate the tree with this information. Since later we will need to check that this information is consistent between a parent position and its children, we need to also consider the states of the automata A i . Next, we define the set of intersections of at most R relations

[[A i1 , q j1 ]] ∩ • • • ∩ [[A i R , q j R ]]. Inters := ℘ ≤R (Aut × Q) ,
where ℘ ≤R denotes the set of subsets of at most R elements. The following holds by definition.

|Inters| ≤ (K • N) R (1)
Given a data tree t and an intersection we extend the [[ ]] t notation by taking the intersection of the R sets. That is,

[[I]] t = {[[A, q]] t | (A, q) ∈ I} , for I ∈ Inters.
Definition 4.3. The data profile is a function that assigns the number of elements present at each I ∈ Inters to every data tree as follows.

d-profile :

Trees(A × D) → Inters → [0..V] d-profile(t) = {I → min(|[[I]] t |, V) | I ∈ Inters}
Observe that since V is the number of variables in Φ, it is enough to count up to V.

A tree's profile carries sufficient information to evaluate at the root any formula ϕ ∈ Φ used by the verifier. We write

f |= ϕ if f is a function f : Inters → [0..V] and ϕ is a formula of the verifier v(b) = ϕ such that ϕ holds in a tree t if f = d-profile(t).
We formally define this relation in Table I. Thus, for any data tree t, position x, and ϕ ∈ Φ, d-profile(t| x ) |= ϕ iff ϕ holds at t| x .

A profile summarizes information about a position in terms of data values in its subtrees. In addition, we also define the description of a data value in terms of the different ways by which it can be obtained.

• 15 f |= ψ ∧ ψ iff f |= ψ and f |= ψ f |= ¬ψ iff f |= ψ f |= ∃v1, . . . , vt.ψ iff I, g, h |= ψ for some I ∈ Inters, g : {v1, . . . , vt} → {1, . . . , t} and h : {1, . . . , t} → ℘(I) s.t. |h -1 (I )| ≤ f (I ) for all I ⊆ I I, g, h |= ψ ∧ ψ iff I, g, h |= ψ and I, g, h |= ψ I, g, h |= v = v iff g(v) = g(v ) I, g, h |= ψ ∨ ψ iff I, g, h |= ψ or I, g, h |= ψ I, g, h |= v = v iff g(v) = g(v ) I, g, h |= Di(v) iff (Ai, q1) ∈ h(g(v)) Table I. The relation f |= ϕ given f : Inters → [0..V].
Definition 4.4. The description of a data value is the set of states of the automata that can access the data value and it is defined as

desc t (d) := {(A, q) ∈ Aut × Q | d ∈ [[A, q]] t } ∈ Descriptions, where Descriptions := ℘(Aut × Q).

Certificates

For any intersection I, we want to keep track of which data values are in [[I]], and how to access them in the subtree in order to verify that they belong to every [[A, q]] in I. How do we decorate the tree in order to have this information at all times? Suppose t is a data tree and x a position in it. We will develop some branch marking system. For d ∈ [[I]] t , we mark several downward paths starting in x and ending at a lower positions y x with d(y) = d. We do this in such a way that for every (A, q) ∈ I there is a marked path between x and y such that d(y) = d and q A -→

x,y q f with q f a final state. We will mark every element of this path with the data value 'd' to which it leads. We call this marking a certificate. However, markings of paths should not overlap. That we can always have such non-overlapping certificates is not obvious, and it will be the matter of Section 4.2.

A certificate of a data tree t = a⊗d is a partial assignment κ : pos(t) data(t). If κ is undefined for a position x, we write κ(x) = ⊥, and we extend the desc t function with desc t (⊥) := ∅ for convenience in the proofs. A certificate κ is said to be correct if it has the properties of being valid and inductive that we will define next.

The validity property for a position x ensures that the certificate takes into account all the necessary data values to witness every intersection. That is, that for every intersection I the data values of [[I]] t|x are contained either in κ(x) or in some κ(x•i) for a child position x•i of x. Since the verifier has only V variables, it is actually sufficient to verify the existence of certificates for up to V data values from [[I]] t|x . This property, when combined with the inductive property results in each of these data values having a path of certificates that witness each of the elements of I. every variable i ∈ [k] and (A, q) ∈ I, there exists (q, b curr , q ) ∈ A and

-q ∈ Q A F and d curr = d cert = d i , or -there is (d i , Desc) ∈ C, with (A, q ) ∈ Desc.
The inductivity property states that for every position x such that κ

(x) = d = ⊥, if d is in some [[A, q]],
then there must exist a child position x•i with certificate In this context we say that Ĉx is a valid and inductive subset of children positions of x.

d such that d is in [[A, q ]] t|x•i for some q in the transition relation of A. Definition 4.6. Given Desc cert ∈ Descriptions, then inductive( Desc cert , (b curr , d curr , d cert ), C ) holds iff for every (A, q) ∈ Desc cert , there is (q, b curr , q ) ∈ A such that -q ∈ Q A F and d cert = d curr , or -there is (d curr , Desc) ∈ C with (A, q ) ∈ Desc. Definition 4.7. A certificate κ is correct if for every position x ∈ pos(t) there exists a subset of children C x ⊆ {x•i | x•i ∈ pos(t)} such that inductive( desc t|x (κ(x)), (b(x), d(x), κ(x)), Ĉx )
Take any x and (A, q) ∈ I ∈ Inters with k = min(V, [[I]] t|x ). The correctness condition implies that -there are d 1 , . . . , d k different data values and x 1 , . . . , x k ∈ pos(t) below x such that for all i:

d(x i ) = d i ; -for all x ≺ y x i , κ(y) = d i ; and -q A -→ x,xi q f for some q f ∈ Q A F .
Note that not every data tree accepted by a E -DD automaton has a correct certificate. (Think for instance in a tree with branching width 1, in which in order to verify the root's property, two different data values are needed.) Indeed, admissibility of correct certificates is a property shared only by some of the trees recognized by a E -DD automaton. However, in Section 4.2 we will show that every nonempty E -DD automaton accepts a tree which admits a correct certificate. Even more, we show that it accepts a tree where additionally the data values have a particular property, that we define as the disjoint values property.

• 17

Correct certificates and disjoint values

This section is dedicated to proving two central properties that are essential to obtain a decidability procedure for the DD automata emptiness problem. These properties state that every nonempty DD automaton accepts a tree that (1) admits a correct certificate, and (2) has the disjoint values property -a property that we will define in Section 4.2.2. Firstly, in Section 4.2.1 we attack the question of whether we can always assume that we have a correct certificate, which is a property that is not shared by all runs. The next section is devoted to showing that for any tree t accepted by a DD automaton there exists a transformation of this tree t obtained by duplicating some subtrees, that is also accepted by the automaton.

Secondly, Section 4.2.2 treats the question of whether we can always assume that the run and certificate satisfy the disjoint values property. We will show that given a correctly certified data tree, we can always rearrange the data values in order to meet this property, while preserving the run and the certificate.

We define the function κ by

κ(x) := {κ(x•i) | x•i ∈ pos(t)} ∪ {κ(x)},
that is, κ assigns to every position x, the set of data values of the certificates of the children of x, as well as of x.

The next two sections will show that the following theorem holds.

Theorem 4.8. For every E -DD automaton (R , V ) that accepts a non-empty language, there is a tree t and a correct certificate of t with the disjoint values property such that t is accepted by (R , V ).

Correct certificates.

In this section we exploit the particular property of extensibility (Definition 3.7) that we imposed to the regular languages used by E -transducers.

As in previous sections, we have that every verifier we consider has a maximum number of relations inside a quantified subformula bounded by R, maximum number of variables bounded by V, the number of automata is K, and the number of states in any automaton is bounded by N.

Our first observation is that if we duplicate a subtree of a data tree as in Figure 4, the values of the certificates do not change, and either both trees are accepted or both rejected by any verifier. The following easy proposition is given without a proof.

Proposition 4.9. Given a data tree t, and given a position x•i ∈ pos(t) consider the last index l such that x•l ∈ pos(t). Let t be the follwing data tree that results from duplicating the subtree t| x•i in t. We define t := (t • f x ), where f x is the following surjective function.

f x : pos(t) ∪ {x•(l + 1)•y | x•i•y ∈ pos(t)} → pos(t) f x (z) = z if z x•(l + 1) x•i•y if z = x•(l + 1)•y
Then, for every z ∈ pos(t ), and

d ∈ D, desc t |z (d) = desc t| fx (z) (d).
This can be also extended to R -transducer runs, always by replicating subtrees.

Here, the extensibility of the regular languages of R will be of utmost importance.

Proposition 4.10. If we have

-a E -DD automaton (R , V ), -a data tree t = a ⊗ b ⊗ d, -a position x ∈ pos(t) with l = #children(t, x), -a run ρ of R on t -a regular language L such that (ρ(x), a(x), b(x), L) ∈ δ and ρ(x•1) • • • ρ(x•l) ∈ L -an extension q1 • • • qn ∈ L of ρ(x•1) • • • ρ(x•l) (where of course n > l),

and any

surjective function h

x : [n] → [l] such that qi = ρ(x•h x (i)) for every i ∈ [n],
-a data tree defined as t := (t • f x ), whose set of positions is

P = {x•j•y | x•h x (j)•y ∈ pos(t)} ∪ {z | z ∈ pos(t), x ≺ z}
and where f x is as follows.

f x : P → pos(t) f x (y) = y if x ≺ y x•h x (j)•y if y = x•j•y
Then:

(1) For every position y ∈ pos(t ) and data value d, desc t |y (d) = desc t| fx (y) (d).

(2) ρ • f x is a run of R on t .

The proof for this Proposition can be found in the online appendix.

Remark 4.11. Note that Proposition 4.10 implies that if t is accepted by a verifier, then t is also accepted, and idem for the transducer. Now we can show that we can always restrict to correct certificates. Proposition 4.12. Every nonempty E -DD automaton accepts some data tree with a correct certificate.

Proof. Let us fix a DD automaton (R , V ). We will show the following statement.

Claim 4.13. Given a data tree t = a ⊗ b ⊗ d, a run ρ on t, and a data value e ∈ data(t) ∪ {⊥} such that t is accepted by V , there exists another tree t with the same height as t, with run ρ and a correct certificate κ such that κ ( ) = e, ρ ( ) = ρ( ) and t is accepted by V according to ρ . Further, for every d ∈ D,

desc t (d) = desc t (d).
• 19 Since (R , V ) is nonempty, there exists a data tree t with an accepting run ρ. If we take e = ⊥, by Claim 4.13 we obtain a data tree t with an accepting run ρ , and a correct certificate κ , proving the statement of the proposition.

Proof of Claim 4.13. We proceed by induction on the height of t. The base case consists in showing that the property holds for a tree t of height 0 consisting of only one position: . In this case it suffices to define t = t, κ ( ) = e and ρ = ρ, and all the properties are trivially met.

For the inductive case, suppose that for all trees of height at most h the statement holds. Let t be of height h + 1 with a run ρ and let e ∈ data(t) ∪ {⊥}. We need to provide a tree t run ρ and certificate κ with the desired properties.

The basic idea is to build t by replicating some subtrees of t to allow to have sufficently non-overlaping paths to generate the correct certificate. To build such tree and certificate, it is useful to have a function that, given a data value d, a NFA A and a state q, returns a position x with data value d such that str( , x) ∈ L(A[q]).

If there is no such witnessing position, (i.e., if d ∈ [[A, q]] t ) it returns an undefined value. We denote by posWitness any such function. It has the next property, for every data value d, automaton A and state q.

-posWitness(d, A, q) ∈ {y ∈ pos(t) | str( , y) ∈ L(A[q]), d(y) = d}, or -posWitness(d, A, q) = ⊥ if {y ∈ pos(t) | str( , y) ∈ L(A[q]), d(y) = d} = ∅.
Remember that the certificate we build κ need to have the data value e at the root. In order to verify the inductivity condition at the root, we will collect every witness position for the data value e. In some sense we want to gather information about which subtrees t| j need to have a certificate with data value e. A = {(e, j) | j posWitness(e, A, q), A ∈ Aut, q ∈ Q, j ∈ pos(t)}

In order to build a valid certificate at the root, we also must take into account the subtrees t| j that are necessary to verify the formulae for every intersection I.

C I = {(d, j) | d ∈ [[I]] t , j posWitness(d, A, q), (A, q) ∈ I, j ∈ pos(t)}
We must then witness all the elements of E = A ∪ {C I | I ∈ Inters}. We build a data tree t , which is the result of duplicating some of the subtrees of t so as to have enough space to fit all the necessary witness certificates required by E. We then need at most |E| replications of trees. This is achieved by the extensibility of the languages corresponding to the transitions of ρ. Let us consider q1 , . . . , qn to be an

|E|-extension of ρ i (1)• • • • •ρ i (l) ∈ L for a language L such that (ρ( ), a( ), b( ), L) ∈ δ.
We define f as in Proposition 4.10, and we define t = t • f , ρ = ρ • f . It follows that ρ is a run on t and by Remark 4.11 t is accepted by V .

To define κ , we must make sure that for each element of E there is a corresponding certificate in some child of the root of t . Of course, there cannot be two certificates in the same child, so we need a way to choose distinct children for distinct elements of E. Let g be a function that chooses, for each element of E, which subtree to use, g : E → {j | j ∈ pos(t )} such that g is injective and f (g(d, j•y)) = j for every (d, j•y) ∈ E.

We are in a good shape to define a certificate κ for t that satisfies the correctness property at the root. But we need κ to be correct also at all subtrees of t . This is given by the inductive hypothesis.

For every subtree t | i of t we apply the inductive hypothesis with the data value d 0 such that g -1 (i) = (d 0 , y) for some y, or with ⊥ otherwise. We thus obtain a tree t i with a correct certificate κ i and run ρ i . Finally we build the following tree t , certificate κ , and run ρ satisfying all the properties.

t (x) = t(x) if x = t i (y) if x = i•y, i ∈ pos(t ), y ∈ pos(t i ) κ (x) = e if x = κ i (y) if x = i•y, i ∈ pos(t ), y ∈ pos(t i ) ρ (x) = ρ(x) if x = ρ i (y) if x = i•y, i ∈ pos(t ), y ∈ pos(t i )
ρ is a run on t since it is composed of runs ρ i from the subtrees and at the root it satisfies the transition (ρ ( ), a( ), b( ), L) ∈ δ. κ is a correct certificate, since the κ i 's are correct certificates for all the subtrees, and κ verifies the inductive and valid conditions at the root. The description of any data value d at the root was not altered since we only applied Proposition 4.10 and the inductive hypothesis that preserve the descriptions. Finally, we can see that V accepts t since it accepts each of its subtrees, and also has the property of the root, since no descriptions of data values were modified.

Disjoint values.

We introduce a property concerning the data values of the tree. The idea is that given two disjoint subtrees t| x , t| y with x y, y x, the only data values they can share, if any, are those of the certificates of their roots κ(x), κ(y), or those of some of their children κ(x•i), κ(y•j). Remember that these last ones constitute all the witness data that are necessary to verify the profile at x and y. All other data values can be assumed to occur in only one of the two subtrees. Here we show that for every nonempty DD automaton there is always a tree that can be certified in such a way that this property holds. Next we formalize the disjoint values property, which will be an essential property in order to prove our main decidability result of Theorem 4.1.

Definition 4.14. Let t = a ⊗ d be a data tree recognized by a DD automaton (R , V ). Let κ be a correct certificate. We say that it has the disjoint values property if, for every pair of incomparable positions x, y ∈ pos(a ⊗ d),

data(t| x ) ∩ data(t| y ) ⊆ κ(x) ∩ κ(y) .
We show here that we can always assume the model to have the disjoint values property. The idea is that once we have a correct certificate κ over a data tree t, we know that at any inner node x ∈ pos(t), all the important data values to verify d-profile(t| x ) shared between subtrees {t| x•i | x•i ∈ pos}, are those contained in the certificates of the children κ(x•i) or κ(x). That is, for every x, the only necessary data values to verify its profile (or an ancestor's profile) is in κ(x). We can then

• 21 ensure that these are the only data values that may be shared by any two t| x•i , t| x•j .

We now state the important proposition of this section.

Proposition 4.15 (Disjointness). Given -a data tree t with a correct certificate κ, and x ∈ pos(t), -a data value

d x ∈ data(t| x ) \ κ(x), d x ∈ data(t), -the bijective function f : D → D such that f (d) = d for all d ∈ data(t) \ {d x } and f (d x ) = d x ,
-the data tree t with pos(t ) = pos(t) and a certificate κ , defined as follows.

t (y) = (a(y), (f • d)(y)) if y x t(y) otherwise κ (y) = (f • κ)(y) if y x κ(y) otherwise
Then, for every position y ∈ pos(t), d-profile(t| y ) = d-profile(t | y ), and κ is a correct certificate for t .

The following trivial lemma will be useful in the sequel.

Lemma 4.16. Given a data tree t, I, I ∈ Inters, and x, y ∈ pos(t), x y, such that for every (A, q) ∈ I there is (A, q ) ∈ I such that q A -→

x,y q , we have that

[[I ]] t|y•i ⊆ [[I]] t|x for every i.
The proof of this Lemma can be found in the online appendix.

Proof of Proposition 4.15. First, suppose that y is such that (1) y x, or (2) x y x.

Then, κ | y is a correct certificate for t | y . This is because in the case (2), t| y = t | y and κ| y = κ | y , and in the case (1), t | y is the result of applying the data bijection f to t| y , and κ | y = f • κ| y .

Suppose then that y ≺ x. We show that for any k ≤ V, and for every (A, q) ∈ I there is (A, q ) ∈ I with q A -→ y,x q , for x = x •i. Hence, Putting together Proposition 4.12 with Corollary 4.17 we hence verify Theorem 4.8 which was the objective of the current Section 4.2. Now we have all the main ingredients to state the horizontal pumping argument.

f -1 (d x ) = d x ∈ [[I ]] t|x . Since d x ∈ κ(x)
In the next section we show that every E -DD automaton accepts a data tree whose width is bounded by a fixed function on the size of the automaton, or it does not accept any data tree at all.

Horizontal pumping

We first bound, for any x, the size of the set of children C x necessary for any correct certificate.

Lemma 4.18. For every correct certificate on a data tree t and every position x ∈ pos(t) there exists a subset C x of children of x that is valid and inductive with respect to the certificate, and

|C x | ≤ L, with L = (K • N) R • p(V, R, K, N) for some fixed polynomial p.
The proof of this Lemma can be found in the online appendix.

Lemma 4.19 (Horizontal pumping). Let -t be a data tree accepted by a DD automaton (R , V ), -(τ, ρ, ρ h ) be a detailed R -run and κ a correct certificate, -x ∈ pos(t) and C x ⊆ {x•1, . . . , x•#children(t, x)} be a valid and inductive subset of children positions of x, -x•i, x•(i + 1), . . . , x•(i + j) be a set of consecutive siblings with the following properties:

-ρ h (x•i) = ρ h (x•j), -none of the positions x•(i + 1), . . . , x•(i + j) is in C x .
Then the data tree t resulting from the deletion of the subtrees t| x•(i+1) , . . . , t| x•(i+j)

t = t • f, f (y) = y if y ∈ pos(t) and ∀t : y x•(i + t) x•(i + t)•z if x•(i + j + t)•z ∈ pos(t)
is also accepted, with the detailed run (τ • f, ρ • f, ρ h • f ) and correct certificate κ • f resulting by the deletion of the positions x•(i + 1), . . . , x•(i + j).

• 23

Proof. Let t = a ⊗ b ⊗ d and l = #children(t, x). The run

ρ h (x•1) • • • ρ h (x•i)ρ h (i + j + 1) • • • ρ h (l)
continues to be an accepting run for the NFA B x corresponding to τ (x) on the string

ρ(x•1) • • • ρ(x•i)ρ(i+j+1) • • • ρ(l)
, and hence τ (x) correctly labels the position with a valid transition. On the other hand, κ continues to be correct since all the necessary elements of C x are preserved after the pruning.

Corollary 4.20. If there exists a data tree recognized by a DD (R , V ) with a correct certificate, then there also exists a tree with bounded width which is also recognized by (R , V ) with a correct certificate. The bound is

(K • N) R • p(V, R, K, N, | Q|)
for some polynomial p.

The proof of this corollary can be found in the online appendix.

Remark 4.21. The bound of Corollary 4.20 also holds for trees with the disjoint values property, since this property is preserved when a subtree is removed.

We just showed how we can bound the width of a tree with a correct certificate. Unfortunately, bounding the height of the tree is not as simple. Here we will need to make use of the properties showed in Section 4.2.

If a run is such that it can be decorated with a correct certificate that has the disjoint values property, we can show that the acceptance or not of the tree can be decided by inspecting only some local conditions between every inner node and its children. This will be the object of the next section, where we will prove that these local properties can be tested in 2ExpTime.

The emptiness algorithm

In this section we show how to label each node of the tree with some finite information (that we call tree configuration). We do this in such a way that testing whether a data tree is accepted or not by a DD automaton amounts to verifying a local property between a node's configuration and the configurations of its children, for every node of the tree. The configuration depends solely on the certificate of the root and its children, and on the state of the run of the transducer. There is a doubly exponential number in the size of the automaton of such configurations. This fact, together with the bounded width of the tree we showed in Corollary 4.20, leads to a decision procedure to test for emptiness. The algorithm runs in 2ExpTime considering R as a parameter, or ExpTime if R is taken as a constant.

By Theorem 4.8, we assume for the rest of this section that we are always working with a data tree t equipped with: an accepting run ρ of R on t, and a correct certificate κ on t, under the disjoint values property.

In the next section we define the configurations that we associate to each node. We will show an algorithm to test if there is a tree with an accepting configuration at the root. This algorithm heavily relies on the fact that the tree is ranked, given by Corollary 4.20. The correctness of this algorithm will be a consequence of the disjoint values property and the admisibility of correct certificates shown in Section 4.2.

Configurations

Next, we define a configuration for a data tree. The idea is that each position x of a data tree t is associated with the configuration for t| x . Let t = a ⊗ b ⊗ d. We describe what a configuration looks like for a A tree configuration contains the state of the transducer's run, the data value of the root, the root's certificate, the children's certificates, and the description of all the data values of the certificates it contains. In the following definition remember that κ(x) denotes the set consisting of κ(x) and all κ(x ) for x a children of x, and that defines partial functions.

TConfigs = Q × D × D × ℘ ≤W (D) × (D ℘(Aut×Q)) tconfig(t, ρ, κ) = ρ( ), d( ), κ( ), κ( ), {d → desc t (d) | d ∈ κ( )}
Although the configurations contain data values, it is not important to know the concrete data values. We are only interested in the classes of equivalence modulo equality contained in the configuration. This is sensible, since the model of automata presented can only test for data equality or inequality. Later on, we will see that this means that we can substitute D with a finite alphabet.

The objective is to prove that if we are given a tree with a run and certificate, we can deduce the configuration of the root by inspecting only the configurations of the immediate subtrees. And vice versa, if we are given a forest of trees with their respective runs and configurations, and a configuration that is compatible with them (in a sense that will be described below), we can then build a witness data tree with the configuration in question.

Given a DD automaton (R , V ), what conditions on the configurations do we need to check? To abstract these conditions we define an entailment relation that checks whether the root configuration can be deduced from the configurations of the children ⊆ (TConfigs) * × TConfigs .

We next give the conditions for M ( q0 , d 0 , c 0 , C 0 , α 0 ) to hold, with ( q0 , d 0 , c 0 , C 0 , α 0 ) the configuration of the root and

M = ( q1 , d 1 , c 1 , C 1 , α 1 ) • • • ( qm , d m , c m , C m , α m )
the configurations of the immediate subtrees.

We define that M ( q0 , d 0 , c 0 , C 0 , α 0 ) holds if the following conditions are satisfied. The conditions, although lengthy, are straightforward. They are necessary and sufficient to have a tree where ( q0 , d 0 , c 0 , C 0 , α 0 ) is the configuration of the root, and M are the configurations of the children of the root. They can be informally described as follows: (i) is consistent with the run of the transducer; (ii) c 0 is a fresh data value (i.e., a data value that is not in M ), or a data value equal to some c i ; (iii) every data value c i is contained in C 0 ; (iv) the c i 's have the validity property for every intersection; (v) c 0 and the c i 's have the inductivity property; (vi) α 0 is obtained from the description at the children configuration α i 's, by applying all possible transitions from any of the automata; (vii) the root satisfies the verifier's formula. In the next definition, we use a function

f : (TConfigs) * → (B×D) → D → ℘(Aut×Q) such that f (M )(b, d 0 )(d) = A if A is the data description of d, deduced from the
(M )(b, d 0 )(d) = {(A, q) | i ∈ [m], d ∈ C i , (A, q ) ∈ α i (d), (q, b, q ) ∈ A} ∪ {(A, q) | d = d 0 , (q, b, q ) ∈ A, q ∈ Q A F } We also use h : (TConfigs) * → (B×D) → Inters → ℘(D)
where h(M)(b, d 0 )(d) is the set of all data values in M that satisfy the intersection

I at the root. h(M)(b, d 0 )(I) = {d | d ∈ {d 0 } ∪ C 1 ∪ • • • ∪ C m , I ⊆ f (M )(b, d 0 )(d)}
The conditions are as follows.

, c 0 ), ∪ i∈[m] {(c i , α i (c i ))}) . (v) The inductive condition (Definition 4.6) holds, inductive(α 0 (c 0 ), (b, d 0 , c 0 ), ∪ i∈[m] {(c i , α i (c i ))}) . (vi) α 0 = {d → f (d) | d ∈ C 0 }. (vii) {I → |h (I)| ≤V } |= v(b)
, where v is the verifier's mapping, and |= is as defined in Table I on page 15.

We remark that in the above definition we do not exclude the case where M = .

In fact, this case corresponds to the configurations of the leaves.

Correctness of

We verify that this is indeed enough to have a decision procedure. Below, the soundness Proposition 4.22 states that, given a sequence of trees with their respective configurations, for any configuration entailed from these we can find a tree that witnesses this configuration. On the other hand, the completeness Proposition 4.25 states that for any tree, the configurations of the immediate subtrees entail the configuration of the tree.

Proposition 4.22 (soundness). Given m data trees with R -runs, correct certificates and the disjoint values property

t 1 , ρ 1 , κ 1 , . . . , t m , ρ m , κ m with t i = a i ⊗ b i ⊗ d i ∈ Trees(A×B×D) such that ρ i is a run for a i ⊗ b i , V accepts b i ⊗ d i , and ∀i = j data(t i ) ∩ data(t j ) ⊆ κi ( ) ∩ κj ( ) .
(2)

If M = ( q1 , d 1 , c 1 , C 1 , α 1 ) • • • ( qm , d m , c m , C m , α m ) T with ( qi , d i , c i , C i , α i ) = tconfig(t i , ρ i , κ i )
for every i, then there exists a tree t 0 ∈ Trees(A×B×D) with run ρ 0 and correct certificate κ 0 with the disjoint values property, such that it is accepted by V , and tconfig(t 0 , ρ 0 , κ 0 ) = T.

Before going into the details of the proof, we need to state some necessary lemmas (4.23, 4.24). Take any tree t 0 with root (a, b, d 0 ) and subtrees t 1 , . . . , t m , such that

either d 0 ∈ C 1 ∪ • • • ∪ C m or d 0 ∈ ∪ i∈[m] data(t i ) .
(3)

Let us fix f = f (M )(b, d 0 ) and h = h(M)(b, d 0 ).
The proof of the following two Lemmas can be found in the online appendix.

Lemma 4.23. For any

d ∈ C 1 ∪ • • • ∪ C m , f (d) = desc t0 (d).
Lemma 4.24. For any intersection

I and k ≤ V, |[[I]] t0 | ≥ k iff |h (I)| ≥ k.
Proof of Proposition 4.22. We show that there exists (a, b, d cert ) ∈ A×B×D such that the tree with (a, b, d cert ) at the root and t 1 , . . . , t m as immediate subtrees has a correct certificate κ 0 with the disjoint values property, and a R -run ρ 0 , such that the configuration of the tree is T .

We first define the run. Let T = ( q0 , d 0 , d cert , C 0 , α 0 ). As we remarked before, we are only interested in the classes of equivalence of T, T 1 , . . . , T m modulo renaming of data values. So that we can always assume that d 0 is such that hypothesis (3) holds: if

d 0 ∈ C 1 ∪ • • • ∪ C m , we simply assume that d 0 is any value not contained in data(t 1 ) ∪ • • • ∪ data(t m ).
By condition (i) of the entailment definition, there is some transition ( q0 , a, b, L)

of R such that ρ 1 ( ) • • • ρ m ( ) ∈ L. Let t 0 ∈ Trees(A×B×D), defined by t 0 ( ) = (a, b, d 0 ) and t 0 (i•x) = t i (x) for i ∈ [m]. Hence the run ρ 0 defined as ρ 0 ( ) = q0 , ρ 0 (i•x) = ρ i (x) is a valid R -run on t 0 .

We now show that T is indeed a configuration that corresponds to t 0 . By condition (ii) either d cert = d 0 for some fresh data value (i.e., not appearing in any subtree, by hypothesis (3)), or d cert = κ i ( ) for some i ∈ [m]. In the first case we trivially have

desc t0 (d) = {(A, q) | (q, b, q ) ∈ A, q ∈ Q A F } = α 0 (d)
by definition of α 0 (condition (vi)) and definition of f (d cert ). In the second case, we have by Lemma 4.23 that f (d cert ) correctly yields the description of d cert at the root and we verify desc t0 (d cert ) = α 0 (d cert ). By condition (iii) and using the same reasoning as before,

κ 1 ( ) ∪ • • • ∪ κ m ( ) = C 0 and for all d ∈ C 0 , α 0 (d) = desc t0 (d).
Then, we have that dconfig(t 0 , ρ 0 , κ 0 ) = T .

We define the certificate κ 0 as κ 0 ( ) = d cert and κ 0 (i•x) = κ i (x). From hypothesis (2) and the fact that t i , κ i have the disjoint values property for every i ∈ [m], we deduce that t 0 , κ 0 also has the disjoint values property.

We show that κ 0 is a correct certificate for t 0 . For the validity condition we first have by Lemma 4.24 that the sets h (I) are good approximations6 of [[I]] t0 . This, together with condition (iv) and Definition 4.5 gives us that κ 0 must be valid, while the inductivity property is a consequence of Definition 4.6 and condition (v).

• 27

Finally, since h (I) has the same cardinality up to V elements as [[I]] t0 , {I → |h | ≤V } |= ϕ iff ϕ holds at t 0 for any ϕ ∈ Φ used in V . Then, by condition (vii), t 0 is accepted by V . Proof. Let t = a ⊗ b ⊗ d. We verify conditions (i) through (vii). Condition (i) is trivially true as ρ is a run on t. Condition (ii) holds, since the κ( ) can be either equal to d( ) or equal to some child certificate κ(i) as a consequence of κ being a correct certificate. Condition (iii) holds because we have all the certificates from the child configurations. The correctness of the descriptions of condition (vi) for the data values {κ(1), . . . , κ(m)} is based on the disjoint values property. As a consequence of this property, we have that for every data value κ(i) and every j ∈ [m], if κ(i) ∈ data(t| j ), then κ(i) ∈ κ(j). This means that we have a complete description of κ(i) for every subtree t| j . For the case of the root's certificate κ( ) we have two cases. If κ( ) equals some κ(i), then we use the same argument as before. Otherwise, we use the inductivity of the certificate κ, knowing that by Definition 4.6 if κ( ) is in some [[A, q]] t , there must be a path of certificates with value κ( ). So, the fact that there are no κ(i) = κ( ) means that desc t (κ( )) can be completely witnessed locally by inspecting only the root. Then, the description obtained by f ' contained in tconfig(t, ρ, κ) is correct. Since condition (vi) holds and b ⊗ d satisfies v(b( )), then it verifies condition (vii). Finally, conditions (iv) and (v) are consequences of the validity and inductivity properties of κ respectively.

Remark 4.26. Observe that Corollary 4.20 with Remark 4.21 gives us a bound on the width of a recognized tree with a correct run and the disjoint values property. We can thus restrict ourselves to relations T 1 • • • T t T with t ≤ W from now on. (Remember that W is the bound on the width of the tree given by Corollary 4.20.) Also, note that the concrete data values of the configuration are not important and can be abstracted away, as soon as they allow to test the conditions of the entailment . For T, T ∈ TConfigs, let us write T ∼ T if there is a bijection of data values f : D → D such that f (T ) = T , where f (T ) stands for the replacement of every datum d by f (d) in T . In every configuration there are at most W + 2 data values (the root's data value, the root's certificate, and at most W corresponding to the certificates of the children). Then, by Remark 4.26, a ' ' test involves not more than W +1 configurations and hence we only need at most (W +1)•(W +2) different data values. Let us define TConfigs to be TConfigs where instead of having D as data domain, we have {1, . . . , (W + 1)

• (W + 2)}. Let D := {1, . . . , (W + 1) • (W + 2)} (4)
and then let TConfigs be defined in terms of the restricted set of data values D ,

TConfigs = Q × D × D × ℘ ≤W (D ) × (D ℘(Aut×Q)) . ( 5
)
We then have the following obvious lemma.

Lemma 4.27. For every T, T 1 , . . . , T n ∈ TConfigs such that T 1 • • • T n T , there exist T , T 1 , . . . , T n ∈ TConfigs with T ∼ T and T i ∼ T i for all i, such that

T 1 • • • T n T .
This means that, since we are only interested in the tree configurations that can be reached by modulo isomorphism of data values, we can simply use the tree configurations of TConfigs . These are doubly exponential in R, or singly exponential if R is fixed. The proof of this Lemma can be found in the online appendix.

As the first step towards an upper bound, we observe that the relation on TConfigs can be checked in polynomial time in Aut, W, |R |.

Lemma 4.29. Given T, T 1 , . . . , T n ∈ TConfigs with n ≤ W, T 1 • • • T n T can be tested in time p(Aut, W, |R |) for some polynomial p.

We now show an algorithm to test whether a tree configuration can be reached by the entailment relation .

Theorem 4.30. The emptiness problem for DD automata is in 2ExpTime. It can be tested in time

(Aut, |R | • V • R • K • N) p(| Q|,V,R)•r(K•N) s(R)
for p, r and s polynomials.

Proof. We consider a standard reachability algorithm by saturation. We start with an initial empty set of configurations C 0 = ∅, and we iterate to make it grow to entailed configurations until, after at most |TConfigs | iterations, the set stabilizes. We then test if some of the reachable tree configurations contains a final state.

The set of initial configurations is C 0 = ∅. At iteration i + 1, for every possible T 0 ∈ TConfigs we test the following conditions -T 0 ∈ C i -There exists a (possibly empty) sequence T 1 , . . . , T t with t ≤ W such that -T 1 , . . . , T t ∈ C i -T 1 , . . . , T t T 0 and we define C i+1 := C i ∪ C , for C the set of all configurations T 0 satisfying the above conditions. If C is empty, we stop and return the subset C i of TConfigs of ( )-reachable configurations. This algorithm clearly gives as a result the set of configurations of all the accepted trees. For every iteration we might need to perform |TConfigs | W+1 tests for the conditions, each one demanding p(Aut, W, |R |) for a polynomial p by Lemma 4.29. Finally, the loop can only be executed |TConfigs | times. We then have that the total time consumed is

|TConfigs | W+2 • p(Aut, W, |R |) .
• 29 By the inequation (7) of Lemma 4.28, and since W is exponential only in R by ( 6), we have that the emptiness problem is bounded by

(Aut • |R | • V • R • K • N) p(| Q|,V,R)•r(K•N) s(R)
for p, r, s polynomials, and we hence have a 2ExpTime decision procedure. We just proved that the problem of whether a DD automaton accepts a tree t with a correct certificate with the disjoint values properties, can be tested in 2ExpTime. Then, by Theorem 4.8 the result follows.

Note that the theorem above implies the Main Theorem 4.1. From the previous proof, we have that the complexity is doubly exponential only in R.

Corollary 4.31. If R is fixed, emptiness of DD automata is in ExpTime. It can be tested in time bounded by

(Aut • |R | • V • K • N) p(| Q|,V,K,N)
for some polynomial p.

Note that the height of a derivation is directly related to the height of the tree. Hence, for trees with a fixed height, we can take advantage of this fact by performing an on-the-fly algorithm.

Definition 4.32. We define the height-h emptiness problem as follows.

Height-h emptiness problem

Input: A DD automaton (R , V ) and a number h ∈ N.

Output: Is there a data tree t of height at most h such that t is accepted by (R , V )?

For the next theorem let us assume that h is coded in unary.

Theorem 4.33. If R is fixed, the height-h emptiness problem of DD automata is in PSpace.

The proof of this Theorem can be found in the online appendix. for some polynomial p.

The purpose of the remark above for discriminating the space needed to perform the entailment condition sp( ) will become clear in Section 6.2.

XPATH

Here we introduce the query language XPath adapted to data trees, though originally it is a language for xml documents. In Section 6.3 we will see that the satisfiability problem on data trees is equivalent to the satisfiability problem on xml documents. We work with a simplification of XPath, stripped of its syntactic sugar. 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 (that we write α, β, γ) and node expressions (ϕ, ψ, η). The fragment XPath(O, =), with O ⊆ {↓, ↓ * } is defined by mutual recursion as follows:

α, β ::= o | α[ϕ] | [ϕ]α | αβ | α ∪ β o ∈ O ∪ {ε} , ϕ, ψ ::= a | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | α | α = β | α = β a ∈ A,
where A is a finite alphabet. 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 α = β or α = β .

There have been efforts to extend this navigational core of XPath in order to have the full expressivity of FO or MSO -for example by adding a least fix-point operator (cf. [ten Cate 2006, 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 the formation of the transitive closure of any path expression. Although in general this is not enough to already capture MSO -as shown by ten Cate and Segoufin [2008], it does give an intuitive language with counting ability. By regXPath(O, =) we refer to the language where path expressions are extended

α, β ::= o | α[ϕ] | [ϕ]α | αβ | α ∪ β | α * o ∈ O
by allowing the Kleene star on any path expression. In terms of expressivity, we have that XPath(↓ * , =)

XPath(↓ * , ↓, =) regXPath(↓, =) = regXPath(↓ * , ↓, =). For example, in regXPath(↓, =) we can express that the tree has a branch of even length. This is a property that does not depend on the data values, and that cannot be expressed in XPath(↓ * , ↓) nor XPath(↓ * , ↓, =).

We formally define the semantics of XPath in Table II. As an example, if t is the data tree depicted by Figure 1

on page 5, [[ ↓ * [ b ∧ ↓ [b] =↓ [b] ] ]] t = {ε, 1, 12}.
Hereinafter, we write t |= ϕ to denote [[ϕ]] t = ∅. In this case we say that t satisfies ϕ. We state the problem we will address, given a fragment P of XPath.

SAT-P Satisfiability problem for P Input: ϕ ∈ P. Output: Is there a tree t such that t |= ϕ ?

• 31

As we are working with downward-looking fragments of XPath, this problem is equivalent to testing if there is a tree in which the formula ϕ is satisfied at the root. Moreover, we can restrict ourselves to the case where ϕ is a node expression, since

[[α]] = ∅ iff [[ α ]] = ∅.
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. Indeed, this is a consequence of considering an xml document as a data tree where the attributes are at leaf positions. This issue will be explained in detail in Section 6.3.

THE SATISFIABILITY PROBLEM

The first part of this section is devoted to the proof of decidability of the satisfiability problem for regXPath(↓, =), the language with the child relation and the Kleene star over path expressions. In later subsections we consider the satisfiability problem of several fragments of this logic, with or without data tests.

Regular-downward XPath

The proof of satisfiability for regXPath(↓, =) is by reduction to the emptiness problem of DD automata. Before embarking on the reduction, we need to fix some standard terminology. Definition 6.1. A subformula of ϕ is a substring of ϕ that is a formula. We say that a set S of formulae is closed under subformulae if: for every ϕ ∈ S and for every subformula ψ of ϕ, we have that ψ ∈ S. S is closed under simple negations if, for every ϕ ∈ S it holds ¬ϕ ∈ S unless ϕ is of the form ¬ψ. We denote the minimal superset of S closed under subformulae and simple negations by S ¬ .

A locally consistent set over S is a maximal subset of H ⊆ S that satisfies the following conditions:

-For all ¬ϕ ∈ S: ¬ϕ ∈ H if and only if ϕ ∈ H.

-For all ϕ ∧ ψ ∈ S: ϕ ∈ H and ψ ∈ H if and only if

ϕ ∧ ψ ∈ H. -For all ϕ ∨ ψ ∈ S: ϕ ∈ H or ψ ∈ H if and only if ϕ ∨ ψ ∈ H.
For the rest of the section, we consider the parameters of the DD automata (K, N, R, V, | Q|, | Q|, |R |, Aut, |V |) as defined in Section 4. Theorem 6.2. Given a formula η ∈ regXPath(↓, =), a DD automaton (R , V ) can be effectively built, such that for any data tree t: t |= η iff (R , V ) accepts t.

Proof. Let η be a formula of regXPath(↓, =). We build the DD automaton (R , V ), where R tags each node with those sub-node expressions of η that hold at each node, and V checks that all the data and path expressions are verified.

Let nsub(η) = {γ | γ a node expression in sub(η)}, where sub(η) is the set of subformulae of η. Let B be the set of all locally consistent sets over {η} ¬ . Let us build R in such a way that at each step it chooses nondeterministically one element from B consistent with the current label and outputs it. That is, if a ∈ A is the letter of the current position then it outputs any element b ∈ B such that ¬a ∈ b. 7 Note that the transducer only needs one (final) state (i.e., Q = { q}) to reflect this behavior. Further, the only regular language used in all its transitions is { q} * . We can represent { q} * with a NFA with a singleton set of states Q.

For every path expression α in sub(η), let A α be a NFA over the alphabet B that recognizes α. For example, if

α = [ϕ] ↓ [ψ], then A α recognizes {b b | b, b ∈ B, ϕ ∈ b, ψ ∈ b }.
It can be built in polynomial time in |α| and |B| (but note that |B| is exponential in |η|). We define the verifier V to contain the set Aut = {A α | α path expression of sub(η)} of automata. The mapping v is defined, for every element b ∈ B, as the formula that tests all the path formulae in b.

v(b) = (¬) α β ∈b ∈{=, =} (¬) ∃v, v . v v ∧ D α (v) ∧ D β (v ) ∧ (¬) α ∈b (¬) ∃v . D α (v)
Intuitively, the only purpose of the transducer R is to guess which subformulae of η are true and which are false. The real work is done by the verifier V , checking that every formula was correctly guessed.

Suppose that t = a ⊗ b ⊗ d is accepted by (R , V ), i.e., a ⊗ b ∈ R , b ⊗ d ∈ V .
For every position x ∈ pos(t) and subformula ψ ∈ sub(η), we show that ψ ∈ b(x) if and only if x ∈ [[ψ]] a⊗d . We proceed by induction on the size of ψ. The base case is when ψ is a test for a label. This is immediate by the definition of R , which preserves the label:

a(x) ∈ b(x) if a(x) ∈ sub(η). Suppose now that ψ = α β with ∈ {=, =}. By definition of v(b(x)), V verifies that there are data values d d such that d ∈ [[A α ]] b⊗d|x and d ∈ [[A β ]] b⊗d|x .
This means that there is a path that starts at x and ends at some position x•y that satisfies α, in the sense that whenever a node expression ξ has to hold in a position x•x (where x y),

(x) = {ψ ∈ {η} ¬ | x ∈ [[ψ]] t }
by using the labels of the descendant positions. For every ψ ∈ {η} ¬ the following can be shown by induction on the size of ψ.

If ψ ∈ b(x) (in other words, if x ∈ [[ψ]] t )
, and ψ is of the form (¬) α β or (¬) α , then the formula of the verifier ψ is true in t| x , where ψ is the translation of ψ according to v(b). This proves that t is accepted by (R , V ).

The result above already gives us a decidability procedure for the satisfiability problem. Let us analyse its upper bound.

Corollary 6.3. The translation of Theorem 6.2 yields an automaton that uses at most R = 2 relations per existential clause and at most V = 2 variables. It can be built in exponential time in η such that K + N ≤ p(|η|) for some polynomial p. The sets of states Q and Q have only one state.

• 33

The proof for the Corollary can be found in the online appendix.

From Theorem 6.2 and Corollary 6.3 we conclude that the satisfiability problem for the full fragment is in ExpTime. Theorem 6.4 (main result). SAT-regXPath(↓, =) is in ExpTime.

Proof. Given a formula η ∈ regXPath(↓, =) we build, in exponential time, a E -DD automaton (R , V ) as in Theorem 6.2. As remarked in Corollary 6.3, R is such that the set of states Q and Q are fixed. V is such that K and N are polynomial in |η|, R = 2, and V = 2.

We run the emptiness algorithm of Theorem 4.30 on (R , V ). Since R is fixed, by Corollary 4.31, the time consumed by this algorithm is bounded by

(Aut • |R | • V • K • N) p(| Q|,V,K,N)
for some polynomial p. Notice that all the variables in the exponent, namely | Q|, V, K, N, are bounded by a polynomial in |η|. The remaining variables can be at most exponential in |η|. Hence, we have an exponential time algorithm for testing the satisfiability of a formula η ∈ regXPath(↓, =).

Lower bound

We next prove the ExpTime-hardness of satisfiability for 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 6.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 of a set T of tiles T = {T 1 , . . . , T s }, a special winning tile T s , the sequence of initial tiles {T 0 1 , . . . , T 0 n } ⊆ T , and the horizontal and vertical tiling relations H, V ⊆ T × T . The game is played on 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 horizontally consecutive tiles must be in the relation H and every pair of vertically 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 or her 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 if during the game the winning tile T s is placed on the board, or if Abelard cannot place any tile. Otherwise, if the game continues indefinitely or if Eloise cannot place any tile, the game is won by Abelard . A partial game is a game that may not have finished. We assume that the tile T s can only appear as the last placed element in the board (and in this case the game is finished). It is known that deciding whether Eloise has a winning strategy is ExpTime-complete.

Abstract representation of a winning strategy. It is easy to see that in this game Eloise has a winning strategy if, and only if, she has a strategy to win before the row s n of the board is reached (s is the number of tiles). (Otherwise, there would be a repeated configuration in two different rows, and the game could be shrunk to one with less than s n rows.) Hence, we represent a partial game as a string of length at most s n • n, containing the plays on the board from left to right, bottom to top, respecting the constraints H and V . We represent a winning strategy for Eloise as a tree of nodes labeled with tiles such that -the root contains T 0 1 , -every node at even depth (e.g., the root) contains as children every tile T such that the path of tiles (from the root to the current node) appended with T is a partial game, -every node at odd depth with a tile T = T s contains at least one children, -all the maximal paths of the tree represent winning games for Eloise.

Concrete representation of a winning strategy. We must now produce a property of XPath(↓ * , =) such that any tree that satisfies it represents a winning strategy for Eloise. We use the coding of a winning strategy as presented before, extended with some extra nodes and labels, which are necessary to make sure that every path contains at most n • s n tiles, and that the nodes verify the H and V restrictions. For simplicity, we assume that n is an even number, and hence that all positions in odd columns are played by Eloise and the others by Abelard . (A similar coding strategy can be used when n is odd.)

Our alphabet consists of -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 ), -the symbols T 1 . . . T s to code the tile placed at each play, -a symbol # to separate rows, and an extra symbol $ whose role will be explained later.

Inside a path, each block of nodes between two consecutive occurrences of # codes the evolution of the game for a particular row. Each node labeled I i has a tile associated, coded as a descendant node with the same data value containing some label T j as label. For example, in Figure 5, 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, which is the number of the current row. This number is coded by the b i elements with the same data value. 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. This is to move from one position of the board to the next one, from the last position to the # delimiter, and from the # to the first position of the next row. Intuitively, between an element I i , i < n, and the element $ with the same data value, only I i+1 may appear. (There may be, however, more than one node with label I i before the appearance of I i+1 , or more than one node I i+1 . This corresponds o the fact that we have a reflexive-transitive relation ↓ * .) This mechanism of coding a very relaxed 'one step' is the building block of our coding. The idea is that since the logic lacks the ↓ axis, we need to restrict the appearance of the next move of the game to a limited fragment of the tree. 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 • 35 Fig. 5. 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).

must appear with

ε = ↓ * [I 3 ]↓ * [$] .
In a similar way we can demand that there is a prefix of I 2 elements, after which all elements have label I 3 , until the occurrence of the label $, as we will see later.

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

Properties of the tree coding a winning strategy. Since the properties expressed by our logic cannot avoid having repeated consecutives labels along a path, the coding will handle groups of nodes with the same label. Let us call an a-group to a maximal connected segment of a path that has the label a. The fact that there could be a sequence of elements with equal label does not cause any problem to the coding. In some sense it is redundant information in the coding.

Following the intuition given before, we spell out the concrete properties of the data tree that encodes a winning strategy for Eloise.

(1) For every i, we demand that there are no data values shared by different I igroups along a path. Likewise for all T i and #-groups.

(2) The nodes labeled by $ are leaves, in the sense that no other symbol may appear as descendant.

(3) Every I i has its corresponding $, i.e., it has a descendant labeled $ with the same data value.

(4) Every I i has a next element, unless it contains the winning tile. That is, there is a I i+1 between I i and its corresponding $ if i < n (and similarly, a # after I 1 , and a I 1 after #).

(5) Each I i has a unique tile: there is a descendant with equal data value and a tile T as label, and all descendants with equal data value carrying a tile, have the tile T .

(6) Every I i inside a step along a branch must have the same tile. (7) Between I i (i < n) and its corresponding $ there can only appear an I i+1 -group.

(The same applies for the labels I n and #, and for # and I 1 .) (8) The tiles match horizontally: the tiles corresponding to any two consecutive nodes labeled I i and I i+1 are in the H relation. Likewise, the tiles match vertically: the tiles corresponding to any two nodes labeled I i separated by exactly one #-group are in the V relation. ( 9) All the elements corresponding to the first row have tiles T 0 1 • • • T 0 n . (10) Every legal move of Abelard is taken into account. For every node I i with i being odd such that there is a tile T k that can be played in the next position (according to H, V and the tiles already placed, as in Figure 6), then it must appear in the next position. Note that this forces a branching in the tree. (11) The data value of a # element is associated to a counter. The least significant bit corresponds to b 0 . A bit 1 at a bit position i is coded as the presence of a descendant node with the same data value labeled b i . The counter starts in 0, and along a path, each time a #-group appears, the counter increments by one. (12) 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.

As already mentioned, we do not avoid having more than one element before the $. As shown in Figure 7, there may be consecutive repetitions of the same label along a path, or subtrees that are duplicated, but this does not spoil the coding. We are actually forcing properties for all branches and all possible extra elements that the tree may contain. Any extra element or branching induces more copies of winning strategies for Eloise.

For every data tree with these properties, one can replace all consecutive appearances of the same label along a path by only one appearance, and strip off all the nodes containing labels which are not tiles. This gives us a winning strategy. Conversely, given a winning strategy for Eloise, we can add data values to the tree and the necessary nodes to transform it into a data tree that satisfies all the aforementioned properties.

Enforcing the properties in XPath(↓ * , =). We first define some predicates that we will use throughout the coding. s k σ (ϕ) evaluates ϕ at a node at k-steps (with our way

• 37 Fig. 8. A bitwise increment of the counter.

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, we define for a ∈ {#, I 1 , . . . , I n },

s 0 a (ϕ) := a ∧ ϕ s k+1 a (ϕ) := a ∧ ε = ↓ * [s k next(a) (ϕ)]↓ * [$]
Similarly, t i checks that the tile of the current node I corresponds to T i ,

t i := ε = ↓ * [T i ]
bit i checks that the i-bit of the counter's binary encoding of a #-node is one (1),

bit i := ε = ↓ * [b i ]
and G forces a property to hold at all nodes of the tree.

G(ϕ) := ¬ ↓ * [¬ϕ]
We now exhibit the XPath formulae for each of the properties just seen.

(1) For every

I i : ¬↓ * [I i ∧ ε = ↓ * [¬I i ]↓ * [I i ] ]
. Likewise for T i and #.

(2) G($ → ¬ ↓ * [¬$] ).

(3) For every

I i : G(I i → ε = ↓ * [$] ). (4) G(I i ∧ ¬t s → s 1 Ii ( )) ∧ G(# → s 1 # ( )).
(5) For every I i and = j: G(¬(t ∧ t j )). For every i: G(I i → j t j ). ( 6) For every i < n and j = k, G(

I i → ¬ ε = ↓ * [I i+1 ∧ t j ]↓ * [I i+1 ∧ t k ]↓ * [$]
). (And a similar condition for # and I 1 .) (7) For every i < n and a

∈ {I i , I i+1 , $}, G(I i → ¬ ε = ↓ * [a]↓ * [$] ), G(I i → ¬ ε = ↓ * [I i+1 ]↓ * [I i ]↓ * [$] ), and
G(I i → ¬ ε = ↓ * [$]↓ * [I i ∨ I i+1 ]↓ * [$] ).
(8) The tiles match horizontally: for every k and T i , T j such that (T i , T

j ) ∈ H, ¬ ↓ * [I k ∧ t i ∧ s 1 I k (t j )] .
The tiles match vertically: for every k and

T i , T j such that (T i , T j ) ∈ V , ¬ ↓ * [I k ∧ t i ∧ s n+1 I k (t j )] . (9) For all i ∈ [1.
.n] and tile T j = T 0 i , s i # (t j ) must hold at the root. (10) For every T i , T j , T k such that (T i , T k ) ∈ V and (T j , T k ) ∈ H :

¬ ↓ * I 2 ∧ t i ∧ s n I 2 I 2 -1 ∧ t j ∧ ¬s 1 I 2 -1 (t k )
(11) It is easy to code that the first # is all-zero. The increment of the counter between two # is coded as in Figure 8, by 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 )) (12) G(# → ¬ i bit i )
This completes the coding. It is easy to see that all the formulae have polynomial size on s and n, and that they express the previous properties. Hence, Eloise has a winning strategy in the two-player corridor tiling game iff the conjunction of the formulae just described is satisfiable. Notice that the above reduction does not use path unions, and this means that even XPath(↓ * , =) stripped of path unions is ExpTime-hard.

PSpace fragments

We now turn to some other downward fragments of XPath. We complete the picture by analysing the complexity of all the possible combinations of downward axes in the presence or absence of data values tests. We first introduce a basic definition that we use throughout the section. Definition 6.6. We say that the logic P has the poly-depth model property if there exists a polynomial p such that for every formula ϕ ∈ P, ϕ is satisfiable if and only if ϕ is satisfied by a data tree of height at most p(|ϕ|).

We can now prove the following statement that we will later use to show PSpacecompleteness for XPath(↓, =). Proposition 6.7. Every fragment P of regXPath(↓, =) that has the poly-depth model property is in PSpace.

The proof of this Proposition can be found in the online appendix.

We use the result above to prove the following proposition, whose proof can be found in the online appendix. Proposition 6.8. SAT-XPath(↓, =) is PSpace-complete. This concludes our analysis of downward fragments of XPath with data tests. Summing up, we showed that the satisfiability problem for regXPath(↓, =), XPath(↓ , ↓ * , =) and XPath(↓ * , =) is ExpTime-complete, while it is PSpace-complete for XPath(↓, =). For the sake of completeness, we now turn to downward fragments where no data tests are available. Corollary 6.9. SAT-XPath(↓) is PSpace-complete.

Proof. The lower bound by [Benedikt et al. 2008, Theorem 5.1] and the upper bound by Proposition 6.8. Proposition 6.10. XPath(↓ * ) is PSpace-hard. The proof goes by reduction from an instance of the QBF (Quantified Boolean Formula [START_REF] Garey | Computers and intractability: a guide to the theory of NPcompleteness. A series of books in mathematical sciences[END_REF]) validity problem to SAT-XPath(↓ * ) and can be found in the online appendix. (like in [ϕ]↓ * ), that is, such that path formulae are defined

α ::= ↓ * | α[ϕ] | αβ | α ∪ β .
Proposition 6.15. SAT-XPath ε (↓ * , =) is PSpace-complete. The proof of the upper-bound goes by showing the poly-depth model property, and can be found in the online appendix.

XML documents vs. data trees

As outlined before, xml documents may have multiple attributes with data values on each element, while data trees can only have one. Here we will show that every result we have stated in terms of data trees also holds on the class of xml documents. Let us consider that the finite set of symbols is partitioned between the names for attributes and the symbols of the xml elements, A attr ∪ A elem .

We define the class of attributes data trees as the trees a ⊗ d where every position carries one label from A elem and many data values indexed by A attr that we call 'attributes', a : P → A elem , d : P → ℘ <∞ (A attr ×D)8 for some P ∈ TreesPos. It follows that any xml document can be seen as an attributes data tree.

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 ∈ A elem and attr1, attr2 ∈ A attr . Let us call this logic attrXPath. This language with the expected semantics over attributes data trees can encode any attrXPath request on an xml document.

SAT-attrXPath(↓, ↓ * , =) is ExpTime-easy As already mentioned, each xml document can be coded in a data tree by adding one child for each attribute with its corresponding value as in Figure 10. We can enforce this property with XPath(↓ * , ↓, =), by stating that all the nodes with a symbol from A attr are leaves,

ϕ struct = ¬ ↓ * [ s∈Aattr s ∧ ↓ ] .
We can interpret any attrXPath formula as an XPath formula by considering an extended alphabet A = A elem ∪ A attr and replacing every appearance of '@attr1' by '↓ [attr1]'. Let us call tr to this translation. automata corresponding to the (extensible) languages from the transitions of R .

The resulting reduction is in ExpTime because the same arguments used to show 6.4 can be applied.

The above Theorem 6.16 implies that the satisfiability of regXPath(↓, =) under certain kind of restrictions is decidable in ExpTime. Note that these restrictions may be specified as DTD, XML Schema, Relax NG, etc. For example, it would mean that this logic is decidable under DTD whose every type is defined under some transitive operator + or * . That is, that the definition of every type is in REG * (as defined in Definition 3.7), like in the example of Table III.

CONCLUDING REMARKS

In Section 3 we introduced an automata model over data trees. Here we explore very briefly two natural extensions that could be added to this automaton. Firstly, the possibility of allowing any alternation free first order formula in the set Φ of properties that the verifier can test, instead of the restricted kind where no negation of a relation may occur. Secondly, what happens if we allow constants in Φ.

Negation of relations

The reader may have noticed in Definition 3.2 that the DD automata model does not allow to have negated appearances of a relation D i under a (positive) existential quantification. This is not by chance, and in effect we can see that if we allow to have arbitrary boolean combinations of D i relations we fall into a much harder emptiness problem. Although the decidability of the resulting model is not clear, it is possible to show that in the case it is decidable, the emptiness problem cannot be solved in primitive recursive complexity.

Consider the simple formula ¬(∃x.¬D

1 (x) ∧ D 2 (x)), such that A 1 recognizes {b b | b ∈ B} and A 2 recognizes {b b b | b ∈ B}.
In other words, A 1 simply goes to any child of the root, and A 2 goes to any grandchild of the root. This kind of property intuitively tests that all the data values appearing at depth l + 1 also appear at depth l. Although we will not enter into detail, it is possible to code a run of a weak version of a n-counters Minsky machine with increment errors (also called gainy counter machine, or incrementing counter automaton, cf. [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]) by using this kind of property. It is known that the emptiness problem for these kind of machines is non-primitive recursive [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF]], and hence the emptiness problem for this extended automaton cannot be primitive recursive.

Constants

Another simple extension that DD automata may allow to have is the fact of having a set of constant data values. This does not change the complexity results. The results and definitions of Sections 4.1, 4.3, 4.2 remain valid. In Section 4.4

• App-1

This document is the online-only appendix to:

Decidability of downward XPath

A. MISSING PROOFS

Proof of Proposition 3.5. First observe that the set of properties Φ of any verifier is closed under conjunction and disjunction, since it is closed under the operators ∧, ∨.

Suppose we have two DD automata

(R 1 , V 1 ) and (R 2 , V 2 ), R i ⊆ Trees(A×B i ), V i ⊆ Trees(B i ×D).
We build the intersection automaton (R , V ) where R ⊆ Trees(A×(B 1 ×B 2 )) is a transducer that tags each position with a pair of letters,

such that a ⊗ b 1 ⊗ b 2 ∈ R if, and only if, a ⊗ b 1 ∈ R 1 and a ⊗ b 2 ∈ R 2 .
This can be done since C is closed under componentwise product, as follows. We define the state space as Q1 × Q2 and the final states as Q1

F × Q2 F . For every transition ( q1 , a, b 1 , L 1 ) of R 1 and ( q2 , a, b 2 , L 2 ) of R 2 we have a transition (( q1 , q2 ), a, (b 1 , b 2 ), L 1 × c L 2 ) in R . On the other hand we build V ⊆ Trees((B 1 ×B 2 )×D) such that b 1 ⊗ b 2 ⊗ d ∈ V iff b 1 ⊗ d ∈ V 1 and b 2 ⊗ d ∈ V 2 . This can be done since Φ is closed under conjunction.
Proof of Proposition 3.6. Let (R , V ) with R ⊆ Trees(A×B), V ⊆ Trees(B×D), where Q is the set of states of R . We build (R c , V c ) the complement of (R , V ). We define R c ⊆ Trees(A×B ) with B = ℘(Z) where Z = Q × B × {below , notyet, here}.

Every node x of the tree t is labeled by a set of tuples ( q, b, i) ∈ Z describing, for each of the possible partial runs of R on t| x , whether there is a node that does not verify a property demanded by V . More precisely, q is the state of the run at the root, b refers to the output letter of the root, and i ∈ {below , notyet, here} is to keep track of whether in the currently described run there is a node falsifying a property demanded by V . The value notyet denotes that all the nodes in the subtree t| x for this run verify the properties of V ; below that there is a node different from x that does not verify the property of V , and here that in the current run x does not verify the property of V . Formally, R c tags every node x of the tree t with the set of tuples ( q, b, i) ∈ Z such that there is a partial run of R on t| x where -the state of the root is q, Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee. c 2000 ACM 1529-3785/2000/0700-0001 $5.00 -the output label of the root is b, and -i = below iff there is a node of t| x different from the root with output label ( q , b , i ) such that i = here.

Further, R c checks that the output label of the root contains only tuples of the form ( q, b, i) where either i = below , i = here or q is not final in R . This ensures that all possible accepting runs of R lead to trees that falsify some demand of V at some node. Notice that if there is a node different from the root with i = here then i = below , and if there is no node different to the root with i = here, then i may be here or notyet. Also, notice that the state at the leaves has i = here or i = notyet (i.e., no below ).

Assuming we can build R c with the described behavior, we define V c ⊆ Trees(B ×D)

with v c : B → Φ its formulae assignment, as

v c ( q, b, i) = true if i ∈ {below , notyet} ¬ v(b) if i = here.
It follows that if a data tree t is accepted by (R c , V c ), then any run of R on t produces an output such that falsifies V at some node, and then t is not accepted by (R , V ). In turn, if t is accepted by (R , V ), there must be an accepting run of R whose output verifies V . In other words, there must be a tuple ( q, b, notyet) with q an accepting state in the root of every output of R applied to t, but this cannot be since R c does not accept such trees. Now let us describe with more care how R c is built from R . Let L 1 , . . . , L s be all the languages from C used in the transitions of R . For every subset S of these languages consider a language L S that tests that a word belongs to all the languages of S, and does not belong to any other language. It follows that L S ∈ C , by closure under finite intersection and complementation.

Let us define the state space of R c as B . Given a language L over Q (the state space of R ), we can build a similar language L over B that tests that we can pick one tuple for each element of the word in such a way that when we project the first component, the word belongs to L. If L is represented as a regular expression, this boils down to replacing every atomic expression q by a big disjunction of all the elements of B containing a tuple with state q. It follows that L ∈ C since it is closed under inverse homomorphisms. Note that we can further check that there is a word of B * in this language containing a tuple ( q, b, i) with i = notyet (or i = below ). This is a consequence of having the membership languages for each tuple with notyet and below .

Then, for every A ⊆ {L 1 , . . . , L s , notyet, below } consider a language L A that tests -that there is a word over B and a tuple for every element such that the projection on Q is accepted by all languages of S and rejected by all others; -if notyet ∈ A that there is an element of the word containing a tuple with notyet; -and if below ∈ A that there is an element of the word containing a tuple with below .

Now, R c is built with the set of all rules of the form (B, a, B, L A ) where A ⊆ {L 1 , . . . , L s , here, below }, a ∈ A, and B ∈ B such that ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

• App-3

for every q ∈ Q, b ∈ B and L ∈ A such that ( q, a, b, L) ∈ δ then either -below ∈ A and there is i ∈ {here, notyet} where ( q, b, i) ∈ B, or -below ∈ A and ( q, b, below ) ∈ B.

Thus, below means that there was a here in the subtree, and here means that it is in that precise point that a formula is falsified. Finally, the accepting states are those whose every tuple with an accepting state contains no notyet flag.

Proof of Proposition 4.10. We first show (1). Note that t is the result of adding some subtrees t| x•i1 , . . . , t| x•i , where = #children(t , x) -#children(t, x), plus some possible reordering of the siblinghood. Let t 0 , t 1 , . . . , t be data trees such that t 0 = t, and t j with j > 0 is the result of adding t| x•ij as a last child of x in t j-1 . Observe that we can apply Proposition 4.9 to each of the pair of trees (t 0 , t 1 ), (t 1 , t 2 ), . . . , (t -1 , t ) obtaining that for every position y ∈ pos(t j ) and j ∈ [ ], desc tj |y (d) = desc tj-1|

g j x (y) (d)
where g j x : pos(t j ) → pos(t j-1 ) is the surjective function given by Proposition 4.9. Then, the function g x = g 1 x • • • • • g x is surjective onto pos(t), and for every position y ∈ pos(t ), desc t |y (d) = desc t| gx(y) (d). Now, note that t and t (and equivalently f x and g x ) differ only in the order of the subtrees of position x. Since, by definition, desc is invariant under reordering of siblings, it follows that (1) holds.

To show (2), first consider any position of the form x•i ∈ pos(t ), and observe that t | x•i has a run (ρ • f x )| x•hx(i) . This is a consequence of t | x•i and t| x•hx(i) being identical, and the automaton being bottom-up. Secondly, we prove that t | x has a run (ρ • f x )| x . This is because ρ(x•h x (1)) • • • ρ(x•h x (n)) ∈ L by hypothesis and hence (ρ

• f x )| x (1) • • • (ρ • f x )| x (n) ∈ L,
where n = #children(t , x). We can then apply the transition (ρ(x), a(x), b(x), L) obtaining ρ(x) at the root. Finally, since x has the same state in ρ and ρ • f x , and the trees t and t are isomorphic except for perhaps the subtree rooted on x, it follows that ρ • f x is a run on t .

Proof of Lemma 4.16. Given (A, q ) ∈ I , (A, q) ∈ I as in the Lemma, and d ∈ [[A, q ]] t|y•i , we show that d ∈ [[A, q]] t|x . Let z be such that d(z) = d and q A -→ y•i,z q f with q f ∈ Q A F . By hypothesis, q A -→

x,y q . Hence, q A -→

x,y Proof of Lemma 4.18. We show that L := (K•N) R •(V•R)+K•N is a good upperbound. This is a direct consequence of the cardinality of Inters and the number of possible pairs (A, q). To verify the validity condition as in Definition 4.5, for every I ∈ Inters out of at most (K • N) R , we might need to add up to V • R certificates in the children to witness I: one for each of the V data values and each (A, q) ∈ I. On the other hand, to verify the inductivity condition on κ(x), we need at most one extra child witness for each automaton and state in desc t|x (κ(x)), which can have no more than K • N elements. For condition (iv), we see that h(M)(b, d 0 )(I) can be built in time polynomial, and that for every possible intersection I and value of h(M)(b, d 0 )(I) a polynomial condition must be checked, hence, since |Inters| is polynomial in W, testing condition (iv) remains polynomial.

Proof of Corollary 6.3. The fact that R = 2 and V = 2 is immediate from the definition of V . As already discussed, the transducer only uses one state, | Q| = 1, and that it only needs to use transitions ( q, a, b, L) with L = ( Q) * . L is represented with a NFA with a set of states | Q| = 1. The translation we presented is not polynomial. Indeed there is an exponential number of transitions both in R and in the automata A α of V , but it contains a polynomial number of automata A α . Further, each A α has a number of states polynomial in |α|, and a number of transitions polynomial in |α| and |B|. This last one is singly exponential in |ϕ|.

Proof of Proposition 6.7. Suppose that if a formula η ∈ P is satisfied by a data tree, then it is satisfied by a tree of height h ≤ p(|η|), where p is a fixed polynomial that does not depend on η.

We make use of the translation of Theorem 6.2, but we avoid storingthe transition relations of R and of the automata Aut of V explicitly. Instead, we use two facts.

First, that testing whether a set S of subformulae of η is a locally consistent set uses polynomial space in |η|, and these sets can then be enumerated in polynomial space. And second, that v(b) can be built in polynomial space, given a locally consistent set b. Thus, the space sp( ) needed for checking T 1 • • • T n T is polynomial. Hence, by Theorem 4.33 with Remark 4.34 we have an emptiness algorithm that uses space p(h, K, N)+sp( ) for some polynomial p. This is a consequence of | Q|, V, R and | Q| being constant, and h, K, N being polynomial in |η| by Corollary 6.3.

Proof of Proposition 6.8. [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] show that XPath(↓, =) is PSpace-hard and NExpTime-easy. Here we show a PSpace upper bound by proving the poly-depth model property. Note that if η is satisfiable in t, then it is satisfiable in t n where n is the maximum number of nested ↓ in η9 , and t n is the submodel of t consisting of all the nodes that are at distance at most n from

Fig. 1 .

 1 Fig. 1. A data tree of Trees(A×D) with A = {a, b} and D = N.

  tree is a mapping from a set of positions to letters of the alphabet Trees(E) := {t : P → E | P ∈ TreesPos} .

  Definition 3.1. A C -transducer defines a relation between trees with the same set of positions. Given a transducer R , we use the same symbol R to denote the relation of the pairs of trees accepted by R with a slight abuse of notation, i.e., R ⊆ Trees(A×B). The idea is that a ∈ Trees(A) and b ∈ Trees(B) are related by R if a ⊗ b ∈ R . Thus, in order to be related by R , the trees a and b need to have the same set of positions. This relation is defined as the set of accepted trees of a nondeterministic bottom-up unranked transducer represented as a tuple C , A, B, Q, QF , δ where -A and B are finite alphabets of letters,

  Definition 3.4. A C -Downward Data automaton (C -DD for short) is a pair (R , V ) made of a C -transducer R ⊆ Trees(A×B) and a verifier V ⊆ Trees(B×D).

  REG * := {L ∈ REG | L is defined by a regular expression whose every symbol is in the scope of at least one * } Thus, for example '((a | b) c * d) * ' is in REG * while 'a * b' is not. The class REG * is trivially extensible.

  Definition 4.5. Given I ∈ Inters, D ⊆ D, C ⊆ D×Descriptions, and given d cert , b curr , d curr ∈ D, then valid ( D, I, (b curr , d curr , d cert ), C ) holds if there are k = min(V, |D|) different data values d 1 , . . . , d k ∈ D such that for

  holds, where Ĉx = {(κ(y), desc t|y (κ(y))) | y ∈ C x }; and for every intersection I ∈ Inters the valid property holds, valid ( [[I]] t|x , I, (b(x), d(x), κ(x)), Ĉx ) .

Fig. 4 .

 4 Fig. 4. Subtree replication.

  (a) if |[[I]] t|y | ≥ k, then there are k distinct data values d 1 , . . . , d k ∈ [[I]] t|y ∩ [[I]] t |y , and (b) if |[[I]] t |y | ≥ k, then there are k distinct data values d 1 , . . . , d k ∈ [[I]] t|y ∩ [[I]] t |y . Note that (a) and (b) imply that the profiles of y are the same in t and t . For (a), suppose |[[I]] t|y | ≥ k. By correctness of κ there are k distinct data values d 1 , . . . , d k ∈ [[I]] t|y and k distinct positions y•i 1 , . . . , y•i k ∈ pos(t) such that there are k downward paths starting at y•i 1 , . . . , y•i k with respective certificates d 1 , . . . , d k . By the choice of d x , if d x ∈ {d 1 , . . . , d k }, it cannot be that any witness position of d x ∈ [[I]] t|y lies within t| x , as it would mean that d x ∈ κ(x). Thus, d 1 , . . . , d k ∈ [[I]] t |y . For (b), assume there are k distinct data values d 1 , . . . , d k ∈ [[I]] t |y . If none of these is d x , then the certificate κ (which is the same as κ for these values) shows the paths to witness these data values in t| y and then d 1 , . . . , d k ∈ [[I]] t|y . If d x ∈ [[I]] t |y , as d x only appears in t| x , there must be an intersection I such that d x ∈ [[I ]] t |x ,

  by hypothesis, this means (by correctness of κ) that d x is not in any 'small' intersection, and thus |[[I ]] t|x | > V, which, by Lemma 4.16, implies that |[[I]] t|y | > V. Since for all other data values d x = d ∈ [[I]] t y we have that d ∈ [[I]] t|y , there must be k data values d 1 , . . . , d k ∈ [[I]] t|y ∩ [[I]] t |y . It follows that the certificate κ is also correct for all positions y of t , since all the intersections I with |[[I]] t|y | ≤ V coincide in t and t . By applying repeatedly Proposition 4.15 we obtain the following result. Corollary 4.17. For any data tree t = b ⊗ d with correct certificate κ, there exists another data tree t = b ⊗ d with correct certificate κ such that for every position x ∈ pos(t), d-profile(t| x ) = d-profile(t | x ) and t has the disjoint values property.

  letter and datum (b, d 0 ), and the configurations of the children positions M .

  f

  (i) There exists ( q0 , a, b, L) ∈ δ with q1 • • • qm ∈ L. For the remaining conditions let us fix f = f (M )(b, d 0 ) and h = h(M)(b, d 0 ). (ii) Either c 0 = c i for some i ∈ [m], or c 0 = d 0 otherwise. (iii) C 0 = {c 0 , c 1 , . . . , c m }. (iv) For every I ∈ Inters, the validity condition (Definition 4.5) holds, valid (h (I), I, (b, d 0

  Proposition 4.25 (completeness). Given a data tree t ∈ Trees(A×B×D) with correct certificate κ, run ρ and the disjoint values property accepted by V , then tconfig(t| 1 , ρ| 1 , κ| 1 )• • • tconfig(t| m , ρ| m , κ| m ) tconfig(t, ρ, κ)for m the maximum index such that m ∈ pos(t).

  Lemma 4.28. The number of elements in TConfigs is exponential in |R | and |V | if R is a constant, or doubly exponential otherwise.

  Remark 4.34. If sp( ) is the space needed to check T 1 • • • T n T , n ≤ W, then the algorithm of Theorem 4.33 uses an amount of space bounded by sp( ) + p(h, log(| Q|), | Q|, K, N, V)

A

  α verifies that ξ ∈ b(x•x ). By inductive hypothesis, we obtain that x ∈ [[ξ]] a⊗d . Hence, (x, x•y) ∈ [[α]] a⊗d , where d = d(x•y). Applying the same reasoning for β and d , we obtain that x ∈ [[ α β ]] a⊗d . The case where ψ = α is only easier. Finally, if ψ is a boolean combination, we simply need to apply the inductive hypothesis and the rules of locally consistent sets.Suppose now that t |= η for some data tree t = a ⊗ d. We show that a ⊗ d is accepted by the automaton that results from the translation above. Let b(x) = {ψ ∈ {η} ¬ | x ∈ [[ψ]] t } for every x ∈ pos(t). It is easy to check that b(x)is a locally consistent set and hence that b(x) ∈ B. Note that a ⊗ b is accepted by the transducer R since ¬a(x) ∈ b(x). The verifier accepts b ⊗ d since every test performed at a position x corresponds basically to testing b

Fig. 6 .

 6 Fig. 6. Every legal move T k of Abelard is played.

Fig. 10 .

 10 Fig. 10. Transformation from an xml to a data tree.

  Cachan, LSV & University of Edinburgh ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000, Pages 1-45.

  q f , and thend ∈ [[A, q]] t|x . Now suppose d ∈ [[I ]] t|y•i .Since for all (A, q) ∈ I there exists (A, q ) ∈ I as before, with d ∈ [[A, q ]] t|y•i , we can apply the same reasoning, obtaining thatd ∈ [[I]] t|x . Thus, [[I ]] t|y•i ⊆ [[I]] t|x .

•

   |D | is polynomial in W, and we then have|TConfigs | ≤ | Q| • (p(W)) q(W) • 2 K•N•r(W) (7)for some polynomials p, q, r. W is exponential only in R, and if R is constant, W is polynomial in |R | and |V | by definition (6). Thus, the lemma follows. Proof of Lemma 4.29. Condition (i) can be tested in polynomial time in |R |, | Q| and n, where | Q| is polynomial in W. The function f (T 1 • • • T n )(b, d 0 )(d) can be computed in polynomial time in Aut and |T 1 |+• • •+|T n | (which is polynomial in W). It follows that the description function α of condition (vi) can be checked in polynomial time in W, since it consists in at most W + 1 applications of f (M )(b, d 0 )(d). Conditions (ii) and (iii) are easily checked in polynomial time in |T |, |T 1 |, . . . , |T n |. Condition (v) can be tested in polynomial time in W and Aut by the above reasons.

Table III .

 III Example of a DTD under which regXPath(↓, =) is decidable in ExpTime.

	<!ELEMENT book_list (book*)>
	<!ELEMENT book ((author, birthdate?)+, chapter+)>
	<!ELEMENT author (#PCDATA)>
	<!ELEMENT birthdate (#PCDATA)>
	<!ELEMENT chapter (#PCDATA)>

ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000, Pages 1-45.

We use the notation XPath(O, =) to refer to the fragment of XPath including all the relations contained in O for navigation, and where the presence of '=' indicates that the language can perform data tests (both for equality and inequality of data values).ACM Transactions on Computational Logic, Vol. 0, No. 0, 00

This is a corollary of[START_REF] Figueira | Future-looking logics on data words and trees[END_REF].

This is a direct consequence of XPath(↓) being able to code any formula from the normal modal logic K, which enjoys the finite-and tree-model properties[START_REF] Blackburn | Modal logic[END_REF], and is PSpacecomplete[START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]].ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

Here, (•) + stands for the non-reflexive version of (•) * .ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

For example, (∃v.D 1 (v)) ∧ ¬(∃v.D 2 (v) ∧ D 3 (v)) is bounded by 2, since there are at most 2 D i 's used in each quantified subformula.ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

They coincide in min([[I]] t 0 , V) elements. ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

Note that if a ∈ sub(η), then ¬a ∈ b and a ∈ b for all b ∈ B. ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

Note that in this model an attribute may be associated with multiple data values.ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

For example, the maximum number of nexted ↓ in the expression↓ [a ∧ ↓↓ [b] ] ↓ [ ↓↓ [a] ] is 4.ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

• 39 Fig. 9. The subtree copy property. Now we focus in finding an upper bound for SAT-XPath(↓ * ). We prove that it is in PSpace by the poly-depth model property. But before doing that, we need to introduce an important property of this logic. The subtree copy property states that if a tree satisfies some XPath(↓ * ) property at the root, then the tree where some subtree was copied at a higher position of the tree (as depicted in Figure 9) also satisfies the property. Lemma 6.11 (subtree copy). Given a tree t, and given two positions x, y ∈ pos(t) with x ≺ y, consider the last index l such that x•l ∈ pos(t). Let t be defined as follows.

Then, for every w ∈ pos(t) and ϕ ∈ XPath(↓ * ), t| w |= ϕ iff t | w |= ϕ. The shapes of t and t are illustrated in Figure 9.

The proof of this Lemma can be found in the online appendix.

Note that the preceding Lemma 6.11 is a stronger property than that of Proposition 4.9, but this one holds only for XPath(↓ * ), a logic with no data tests or ↓ axis. Having stated the subtree copy property, we can now show the following proposition.

Proposition 6.12. SAT-XPath(↓ * ) is in PSpace.

Indeed it can be shown that ϕ ∈ XPath(↓ * ) is satisfiable iff it is satisfied by a tree of height bounded by |ϕ| 2 . The full proof can be found in the online appendix.

We then have as a corollary from Proposition 6.12 and Proposition 6.10 that XPath(↓ * ) is complete for PSpace. Theorem 6.13. SAT-XPath(↓ * ) is PSpace-complete.

So far we have that, in the presence of data values, the presence of the descendant axis ↓ * produces an increase (in the case PSpace = ExpTime) in the complexity from PSpace to ExpTime. However, we argue that it is not the ability to test for data equality of distant elements what produces this increase 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 remove this kind of data tests, the resulting logic is in PSpace, even though the fragment contains the ↓ * axis. Definition 6.14. We denote by XPath ε (↓ * , =) the fragment of XPath(↓ * , =) where ε path formulae are forbidden, and in general where there is no ε-testing on a path

Decidability of downward XPath

• 41

We can then decide the satisfiability of a formula ψ of attrXPath(↓, ↓ * , =) on attributes data trees by testing the satisfiability of 'tr(ψ) ∧ ϕ struct ' on data trees. Since we have that XPath(↓, ↓ * , =) is in ExpTime, we also have an ExpTime decidability procedure for the full downward fragment of attrXPath (as the translation tr is clearly performed in PTime) even with the Kleene star operator.

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

SAT-attrXPath(↓, =) is PSpace-complete

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

where d is the maximum quantity of nested occurrences of ↓ in ψ. 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 that tr(ψ) can access. This is associated with the poly-depth model property of the logic. We then have that attrXPath(↓, =) is PSpace-complete.

In the presence of regular languages

In this section we make some observations on the following problem for L a class of tree languages and P a fragment of XPath.

SAT-P + L Satisfiability problem for P under L

Input: ϕ ∈ P and an automaton representing a language L ∈ L . Output: Is there a tree t ∈ L such that t |= ϕ ?

By [Figueira 2010a] we know that satisfiability of downward XPath under a regular language is decidable. However, the problem has a very big complexity. Even for the fragment containing only the descendant axis, it can be shown that there is no algorithm that solves the satisfiability problem under a regular language in primitive recursive time or space [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. However, if the language to be tested at the siblinghoods is restricted to be extensible, we can translate this problem to the emptiness problem for DD automata obtaining the following result. Theorem 6.16. SAT-regXPath(↓, =) + E tree , that is, the satisfiability problem for regXPath(↓, =) under the class E tree of extensible tree regular languages, is in ExpTime.

Proof. Let ϕ ∈ regXPath(↓, =) and L ∈ E tree , represented as an E -transducer

We first build the DD automaton (R , V ) resulting from the translation of ϕ by Theorem 6.2. We compute the composition R = R L • R such that R (t ⊗ t ) iff R L (t ⊗ t) and R (t ⊗ t ) in polynomial time in R and R L . We then test the emptiness of (R , V ) in exponential time in the number of states | Q| of the • 43 we modify the tree configurations by keeping explicit track of these constants, by adding the description of these constants to the data description mapping α at all configurations, and modifying the conditions of accordingly. This implies that we can verify the satisfiability of regXPath(↓, =) with constants also in ExpTime.

Discussion

We have shown the complexity of various downward fragments of XPath, as summarized in Table IV. The highest complexity class we obtained is ExpTime. In the presence of data equality tests, 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 any sibling axis. Indeed, as soon as any horizontal navigation is allowed in the logic, the problem becomes non-primitive recursive. However, we have shown that we can evaluate some restricted fragment of XML Schema or DTD that cannot limit the quantity of occurrences of nodes of a certain type, but that can verify that there is a certain structure in the siblings of the tree. For example, we can express that the children of every node with label book form a sequence of labels in the language (author (chapter) * ) + (since it is an extensible language). Also, by solving the satisfiability problem we are also able to solve the containment and equivalence problems of node expressions for free, since we work with logics closed under boolean operators. 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 Downward Data automata that capture all the expressivity of regXPath(↓, =). This automata model is more expressive than XPath. It can test properties like, for example, that there are exactly 7 data values with label book; or that every node labeled book has between 1 and 4 children author with different data value; or that there is a data value that can be simultaneously accessed by three different branches, satisfying the path expressions "↓ *

By the proof of decidability of the DD automata, we conclude that there is a normal form of the model for downward XPath. 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 property is reflected by the fact that the emptiness of the automaton that results from the translation of a downward XPath formula only depends on a polynomial number of data values at every position. 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 its execution.

It would also be interesting to study if the techniques of this work could be used to treat the satisfiability problem of monadic datalog programs [START_REF] Ceri | What you always wanted to know about datalog (and never dared to ask)[END_REF]] extended with equality and inequality of data values.

Finally, a recent result [START_REF] Figueira | A decidable two-way logic on data words[END_REF]] on XPath on data words, suggests that it is plausible that XPath(↓, ↓ * , → * , * ←, =) or even XPath(↓, ↓ * , ↑ * , → * , * ←, =) is decidable in elementary time. This would be an extension of the result of the present work, and in contrast with the fact that XPath(↓, ↓ * , → * , + ←, =) is undecidable and XPath(↓, ↓ * , → + , =) has non-primitive recursive complexity [START_REF] Figueira | Future-looking logics on data words and trees[END_REF].

Proof of Corollary 4.20. We show that it can be bounded by

for some polynomials p, p . Given a maximal sequence of siblings x•1, . . . , x•l, we already established in Lemma 4.18 that a valid and inductive subset C x needs no more than L elements to preserve the correctness of the certificate. Hence, there can be at most L + 1 zones of consecutive positions not in C x , and each one of them must have at most | Q| -1 elements. Should it have more, then there are at least two repeating elements with the same horizontal configuration by the pigeonhole principle, and we can then apply Lemma 4.19 and remove some of the siblings.

Proof of Lemma 4.24. The right-to-left implication is a direct consequence of the definition of h (I). For the left-to-right implication, suppose that

We argue that if d appears in some κi ( ), then it is in h (I). This is because all the subtrees t i with d ∈ data(t i ) must have d ∈ C i , as a consequence of the hypothesis (2). Hence we have a complete description of d at every subtree, and f yields the correct description of d at the root by Lemma 4.23, which implies that d ∈ h (I) by definition of h.

Suppose on the other hand that d is not in κi ( ) for any i. Since every κ i is correct, this means that d does not appear in any small intersection [[I ]] of fewer than V data values. Hence, in particular |[[I]] t0 | ≥ V. By hypothesis (2), we know that d can appear in at most one tree t i , or at the root. We consider both cases.

If d appears only at the root, it means that d = d 0 , and for every (A, q) ∈ I there is q ∈ Q A F with (q, b, q ) ∈ A and this is taken into account by the definition of h (I). Hence, d ∈ h (I).

If d appears only in t i , this means that there is an intersection I such that d ∈ [[I ]] ti and for every (A, q) ∈ I there is (A, q ) ∈ I with (q, b, q Proof of Lemma 4.28. Now we have at most |D | data values, and the function of each configuration is restricted to the data values (at most W) of the configuration. We then have the following bounds by definition of TConfigs (5). the root: t n = {x → t(x) | x ∈ pos(t), |x| ≤ n}. Hence, by Proposition 6.7, XPath(↓, =) is in PSpace.

Proof of Proposition 6.10. The proof goes by reduction from an instance of the QBF (Quantified Boolean Formula [START_REF] Garey | Computers and intractability: a guide to the theory of NPcompleteness. A series of books in mathematical sciences[END_REF]) validity problem to SAT-XPath(↓ * ).

Let

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 . The tree's alphabet is A = {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. After this marking we build the tree that satisfies ψ by choosing a witness atom for every disjunctive clause. Finally, we check that there are no inconsistencies with respect to its valuation. For example, in Figure 11 we depict a possible tree that is forced by a formula.

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 . We specify formulae f 1 , . . . , f n depending on Q 1 , . . . , Q n , where G is defined as in the proof of Theorem 6.5.

-ϕ X forces that the label X always appears once the valuation for all propositions has been defined.

-For all X we build a formula for ψ = C 1 ∧ . . . ∧ C l where C i = t 1 ∨ . . . ∨ t m and each t j is either p k or pk for some k. That is,

and this must hold for all X-valued nodes,

ACM Transactions on Computational Logic, Vol. 0, No. 0, 00 2000.

Decidability of downward XPath

• App-7

-Finally, we must check that there are no inconsistencies between the p i along a branch.

The final formula is then

Suppose that ϕ is valid. We can build a tree that satisfies ϕ F as follows. Let's assume that Q 1 = ∃ (the other case is similar). Note that

is valid, (where this is interpreted as the result of replacing p i by true or false in the formula according to v(p i )). Conversely,

are valid. Now, we build the tree as follows. We first take the witnessing valuation of p 1 for the validity of ϕ and put it as the root. Then we iterate adding leaves in the tree until obtaining a tree whose every leaf is at depth n -1 in the following way. Suppose we are adding the children of a leaf at depth i with i < n -1. Let v be the valuation of p 1 . . . p i that corresponds to the labels that appear in the path that leads to the current leaf. Consider ϕ as the result of replacing every p j by true or false corresponding to v(p j ) for every

and note that ϕ must be valid. If Q i+1 = ∃ we just add one child with the witnessing valuation v(p i+1 ) that makes ϕ [p i+1 → v(p i+1 )] valid. If Q i+1 = ∀ we add two children with labels p i+1 and pi+1 . Once we do this with all the quantifiers, we append a node with label X to all leaves, and put the witness of the satisfaction of ψ which must be a choice between the valuations that occurred along the path, which gives us a tree whose every leaf is at depth n + 1, as in Figure 11. Note that it cannot be that there is a p i and pi along a path. Indeed, this tree satisfies ϕ F .

On the other hand, if ϕ F is satisfied by a tree, then we can produce witness for every ∃ quantifier of the formula, always making sure that the valuation chosen for one propositional variable p i will not change, since we disallow having p i nad pi in the same path. This shows that ϕ is in fact valid.

Then we have that ϕ is QBF-valid if and only if ϕ F is satisfiable. Note that this reduction does not use path unions. Then, this lower bound holds even in the absence of path unions.

Proof of Lemma 6.11. All path formulae that hold at the root of t, hold also in t as it is an extension of the tree. On the other hand, any path formula that is satisfied at the root by a succession of nodes in a branch in t , can also be found in t , as we only count with the ↓ * axis. This is true not only for the root but for any position of t. In other words, the logic XPath(↓ * ) is closed under subtree copy.

Proof of Proposition 6.12. We prove that ϕ ∈ XPath(↓ * ) is satisfiable iff it is satisfied by a tree of height bounded by |ϕ| 2 .

For the proof of this statement we first define, for a path expression, the set of possible sequences of node tests that it must satisfy, that we note with 'nseq' (Table V). The idea is that if for instance {ψ, ϕ}•{ϕ}•{ψ, η} ∈ nseq(α) for a path for every j.

Note that in particular |wit t (x, α)| ≤ |S| for some S ∈ nseq(α), and we hence have

In the sequel, given ϕ ∈ XPath(↓ * ) we write nesting(ϕ) for the maximum number of nested node tests (that is, of nested '[ ]') that are in the formula ϕ.

We can make use of Lemma 6.11 to make sure that we can always assume wit t to be in a normal form where all its elements are chained with the parent/child relation. That is, that given wit t (x, α) = {x 1 ≺ • • • ≺ x n }, then for all i x i+1 = x i •j for some j .

(9)

We are now in a position to explain the main argument. Let ϕ ∈ XPath(↓ * ) and n = nesting(ϕ), and suppose we have a tree t that satisfies ϕ. Next, we describe a procedure to 'mark' the important nodes in the tree. We start by marking the root with the label 'n'. Then, for every position x marked with t ≥ 0 and for every path expression β ∈ sub(ϕ) such that nesting(β) ≤ t and t| x |= β, we mark all positions y ∈ wit t (x, β) with 't -1'.

Note that all the positions marked with {-1, 0, . . . , n} form one connected component by ( 9), and that they are all at a distance from the root of at most nesting(ϕ) • |ϕ| by (8). Let t be the tree resulting from eliminating all the positions with no marking. We then have that t |= ϕ iff t |= ϕ, and hence that XPath(↓ * ) has the poly-depth model property. We conclude by Proposition 6.7 that XPath(↓ * ) is in PSpace.

Proof of Proposition 6.15. The proof of the upper-bound goes by showing the poly-depth model property. Let t = a ⊗ d be a data tree. The key observation is that any XPath ε (↓ * , =) expression of the form α , α = β or α = β that is satisfied at a node x of a tree, is also satisfied in any ancestor of x. This is because all path expressions start with a ↓ * axis. In other words, for any pair of positions x, x such that x

x , the set of formulae of the aforementioned type

Decidability of downward XPath

• App-9 that are satisfied in x is a subset of those that are satisfied in x. Given a branch = x 0 ≺ • • • ≺ x n of t where x i+1 is a child of x i for all i, and given a formula ϕ, consider for every i ∈ [n]

We then have C 0 ⊇ • • • ⊇ C n , and there is only a polynomial number of different sets. Take any two C i = C j such that a(x i ) = a(x j ). Then, the tree which results from replacing the subtree at x i by the subtree at x j preserves the satisfaction of ϕ at the root. Hence, the logic has the poly-depth model property and by Proposition 6.7 its satisfiability problem is in PSpace.

The lower-bound comes from the proof of Proposition 6.10, whose encoding is in XPath ε (↓ * , =).

Proof of Theorem 4.33. Given the previous algoritm of Theorem 4.30, note that all the configurations corresponding to derivations of height i are present once the ith iteration has been executed. Also, note that the height of the derivation and the height of the tree are related in this sense: any tree of height h can be witnessed by a derivation of height h. We can then build a top-down NPSpace algorithm as follows.

Let us denote by g(T, l) the following procedure for T ∈ TConfigs , l ∈ [0..h]. First, g(T, 0) yields 'ok' iff T , otherwise it fails. g(T, l + 1) performs the following tasks. Guesses the tree configurations T 1 , . . . , T n with 0 ≤ n ≤ W. Checks T 1 • • • T n T in PSpace, and recursively tests that g(T 1 , l), . . . , g(T n , l) succeed. Consider now the main algorithm that guesses a root configuration T ∈ TConfigs and checks both that it contains a final state q ∈ QF and that g(T, h) succeeds. This algorithm correctly answers whether there exists a derivation of height at most h that has T at the root.

Notice that the space needed to store the data description function α of a configuration T is bounded by sp for some polynomial p. This is a consequence of (4) and ( 6), and the fact that R is fixed. If we perform a DFS evaluation strategy of g we only need to store simultaneously at most (W + 1) • h configurations and hence the algorithm takes a space polynomial in the size of the automata R , V considering R is fixed. It is then immediate that this is a NPSpace procedure for any configuration and l.

Thus, as NPSpace = PSpace the theorem follows.