Introduction

XML reasoning tasks have been addressed in many recent papers. Typical problems include consistency of type declarations and constraints [1,2,16], or of schema specifications and navigational properties [3,11] or containment of XPath expressions [4,5,10,18,26]. Static analysis tasks are often addressed using logic and automata-based techniques [6]. Thus, due to the well-known correspondences between XML formalisms and logics and automata on trees, it is natural to apply logic and automata techniques to reasoning about XML.

Indeed, several attempts have been made to find generic logic/automata tools applicable in a variety of XML reasoning tasks. The idea of such approaches is roughly as follows. Suppose the task at hand is the well-known XPath containment problem under DTDs: given a DTD d and two XPath expressions e 1 and e 2 , is it true that d |= e 1 ⊆ e 2 ? In other words, is it true that for each XML tree T that conforms to d, the expression e 1 selects a subset of nodes selected by e 2 ? Suppose we can somehow capture by an automaton A e the set of nodes selected by the expression e 1 ∧ ¬e 2 , i.e., counterexamples to containment. Schemas such as DTDs, Relax NG, and others, are easily translated into tree automata (in fact most designs of schemas for XML are based on tree automata). So assume that we have an automaton A d that accepts trees that conform to d. Then to see whether d |= e 1 ⊆ e 2 one simply checks whether

L(A d × A e ) = ∅

since a tree in L(A d × A e ) is a counterexample to d |= e 1 ⊆ e 2 . Throughout the paper, L(A) is the language accepted by automaton A.

This is essentially the same as the main idea of automata-based verification [6], whose goal is to check whether a program P satisfies a specification ϕ. One views an abstraction of P as an automaton A P , constructs an automaton A ¬ϕ capturing counterexamples to the specification (i.e., program executions that do not satisfy ϕ), and checks for nonemptiness of L(A P × A ¬ϕ ). If the language is nonempty, it contains counterexamples to the specification, i.e., bugs in P .

In the verification context, one most commonly deals with automata over ωwords, as they properly capture traces of program behavior and specifications. In the XML context, we deal with queries on finite trees, and finite (unranked) tree automata. The idea of adapting verification techniques to static analysis of XML is therefore very natural and it has been explored in a number of papers [5,7,10,11,13,15,18].

In the classical verification scenario, the specification logic is most often LTL (linear temporal logic), which happens to have the same expressive power as first-order logic (FO). In our context, we deal with XPath, whose navigational capabilities are expressible in FO and which, with an addition of a certain conditional construct, captures FO [19]. If we want to adapt existing LTL-to-automata translations, there are two main approaches to it: translating formulae into nondeterministic, or alternating automata [30,29]. The difference between these approaches is where the complexity lies -in the translation itself, or in checking nonemptiness of languages defined by automata: P P P P P P P P Task

Automata

Nondeterministic Alternating Translation exponential polynomial Nonemptiness checking polynomial exponential

Both techniques have their advantages; the choice is really about the task to which algorithmic and optimization techniques will be applied. In the XML context, there are at least two reasons to seriously consider translating into nondeterministic automata. First, most schema formalisms come from nondeterministic tree automata, so these translations appear to be better suited for reasoning tasks involving schemas. Second, one may hope to use a rich arsenal of optimization tools developed for the original Vardi-Wolper translation [30] of LTL into nondeterministic Büchi automata [8,30,12] and adapt it for XML reasoning tasks.

Both approaches have been explored in the XML context. In [5], a direct translation from XPath to a certain type of alternating automata on unranked trees is given. In [15], translations into nondeterministic automata are explored, but the logic used for translation is not XPath, but rather an LTL-like logic on trees, first introduced in [25] and used later in [19]. While the translation is single-exponential, this is not satisfactory since the translation from XPath into that logic is single-exponential itself! Curiously enough, this does not make the whole translation from XPath into automata double-exponential, but showing this requires a careful analysis of the structure of subformulas of formulas which are translations of XPath queries. However, this intermediate step, with its exponential blowup, seems to preclude any possibility of providing efficient implementations of XPath-to-nondeterministic automata translations, as very little of the original XPath query can still be seen and used in its translation.

Thus, we would like to have a direct translation from XPath queries into nondeterministic tree automata. This is the goal of this paper. We provide such a translation; in fact, we do a bit more. Since XPath node queries select nodes from documents, we provide a translation into query automata [20,22] which not only accept or reject trees, but also select nodes from them. For example, for the task of checking containment of queries, this will give us not just a yes/no answer, but a concise description of all counterexamples to containment.

The translation will be single-exponential: in case of nondeterministic automata, one cannot do better than this, as LTL fragments requiring this complexity are easily coded in XPath. As the exact language, we use Conditional XPath of [19], which is FO-complete; it extends the standard XPath with an analog of the temporal 'until' operator.

The translation follows the spirit of the Vardi-Wolper translation, and thus one can expect that optimization techniques developed for the latter (e.g., those in [8,30,12]) can be adapted for our construction.

Organization In Section 2 we describe XML documents (unranked trees), automata for them, and query automata. In Section 3 we give the syntax and semantics of (conditional) XPath. The translation from XPath to query automata is given in Section 4. Its correctness is shown in Section 5.

Preliminaries

XML documents as unranked trees XML documents are normally abstracted as labeled unranked trees [21,14,27]. Nodes in unranked trees are elements of N * , i.e. strings of natural numbers. We write s • s ′ for the concatenation of strings, and ε for the empty string. The basic binary relations on N * are:

-the child relation: s ≺ ch s ′ if s ′ = s • i, for some i ∈ N, and -the next-sibling relation: s ′ ≺ ns s ′′ if s ′ = s • i and s ′′ = s • (i + 1) for some s ∈ N * and i ∈ N.

The descendant relation ≺ * ch and the younger sibling relation ≺ * ns are the reflexive-transitive closures of ≺ ch and ≺ ns .

An unranked tree domain D is a finite prefix-closed subset of N * such that s

• i ∈ D implies s • j ∈ D for all j < i. If Σ is a finite alphabet, a Σ-labeled unranked tree is a pair T = (D, λ)

, where D is a tree domain and λ is a labeling function λ : D → Σ.

Unranked tree automata A nondeterministic unranked tree automaton (cf. [21,27]) over Σ-labeled trees is a triple A = (Q, F, δ) where Q is a finite set of states, F ⊆ Q is the set of final states, and δ is a mapping Q × Σ → 2 Q * such that each δ(q, a) is a regular language over Q. We assume that each δ(q, a) is given as an NFA (nondeterministic finite automaton). A run of A on a tree

T = (D, λ) is a function ρ A : D → Q such that if s ∈ D is a node with n children, and λ(s) = a, then the string ρ A (s • 0) • • • ρ A (s • (n − 1)) is in δ(ρ A (s), a). Thus, if s is a leaf labeled a, then ρ A (s) = q implies that ε ∈ δ(q, a). A run is accepting if ρ A (ε) ∈ F ,

and a tree is accepted by A if an accepting run exists. Sets of trees accepted by automata A are called regular and denoted by L(A).

Unranked tree automata are relevant in the context of schemas for XML document. There are multiple notions of schemas. What is common for such notions is that their structural aspects are subsumed by unranked tree automata, see [17] for several examples. More, translations from various schema formalisms into automata are usually very effective [17], and thus automata are naturally viewed as an abstraction of schemas in the XML literature. So when we speak of XML schemas, we shall assume that they are given by unranked tree automata.

Query automata It is well known that automata capture the expressiveness of MSO (monadic second order logic) sentences over finite and infinite strings and trees [28]. The model of query automata [22] captures the expressiveness of MSO formulae ϕ(x) with one free first-order variable -that is, MSO-definable unary queries. We present here a nondeterministic version, as in [20,9].

A query automaton (QA) for Σ-labeled unranked trees is a tuple QA = (Q, F, Q s , δ), where (Q, F, δ) is a nondeterministic unranked tree automaton, and Q s ⊆ Q is the set of selecting states. The runs of QA on a tree T are defined as the runs of (Q, F, δ) on T . Each run ρ of QA on a tree T = (D, λ) defines the set S ρ (T ) = {s ∈ D | ρ(s) ∈ Q s } of nodes assigned to a selecting state. The unary query defined by QA is then, under the existential semantics,

QA ∃ (T ) = {S ρ (T ) | ρ is an accepting run of QA on T }.

Alternatively, one can define QA ∀ (T ) under the universal semantics as {S ρ (T ) | ρ is an accepting run of QA on T }. Both semantics capture the class of unary MSO queries [20].

To eliminate the need to choose the semantics, and problems related to it (for example, the most natural constructing for the complement of a QA under the existential semantics produces a QA under the universal semantics), one can use single-run query automata. Such QA satisfy the conditions that for every tree T , and every two accepting runs ρ 1 and ρ 2 on T , we have S ρ1 (T ) = S ρ2 (T ). For such QAs, we can unambiguously define the set of selected nodes as QA(T ) = S ρ (T ), where ρ is an arbitrarily chosen accepting run. This is not a restriction in terms of the expressiveness, as the following result is known: [9,23,24,15]) For every query automaton there exists an equivalent single-run query automaton.

Proposition 1. (see

It is known that nonemptiness problem for QAs (single-run, or under the existential semantics) is solvable in polynomial time. Single-run QAs are easily closed under intersection: the usual product construction works. Moreover, if one takes a product A × QA of a tree automaton and a single-run QA (where selecting states are pairs containing a selecting state of QA), the result is a single-run QA, and the nonemptiness problem for it is solvable in polynomial time too. This makes single-run QAs convenient for reasoning tasks, as outlined in the introduction.

Conditional XPath queries

We present a first-order complete extension of XPath, called conditional XPath, or CXPath [19]. To keep notations in translations manageable, we introduce very minor modifications to the syntax: we use an existential quantifier E instead of the usual XPath node test brackets [ ], and we use symbols for the main XPath axes, rather then their verbose analogs.

The node formulae α and path formulae β of CXPath are given by:

α, α ′ := a | ¬α | α ∨ α ′ | Eβ β, β ′ := ?α | step | step * | (step/?α) * | β/β ′ | β ∨ β ′ where step ∈ {≺ ch , ≺ − ch , ≺ ns , ≺ − ns }.

Given a tree T = (D, λ), the semantics of a node formula is a set of nodes [[α]] T ⊆ D, and the semantics of a path formula is a binary relation [[β]] T ⊆ D×D given by the following rules. We use R * to denote the reflexive-transitive closure of the relation R, and π 1 (R) to denote its first projection. The semantics is formally defined as follow:

[[a]] T = {s ∈ D | λ(s) = a} [[?α]] T = {(s, s) | s ∈ [[α]] T } [[¬α]] T = D − [[α]] T [[step]] T = {(s, s ′ ) | s, s ′ ∈ D and (s, s ′ ) ∈ step} [[α ∨ α ′ ]] T = [[α]] T ∪ [[α ′ ]] T [[β ∨ β ′ ]] T = [[β]] T ∪ [[β ′ ]] T [[Eβ]] T = π 1 ([[β]] T ) [[step * ]] T = [[step]] * T [[β/β ′ ]] T = [[β]] T • [[β ′ ]] T [[(step/?α) * ]] T = [[(step/?α)]] * T

CXPath node formulae α define unary queries: such a query selects the set [[α]] T from a tree T . It is known that these capture precisely unary FO queries on trees [19]. Hence, they can be translated into query automata, although the standard translation from FO into automata necessarily involves non-elementary blowup. The following was shown in [15]: Theorem 1. Every CXPath node formula α can be translated, in exponential time, into an equivalent single-run query automaton (of exponential size).

The translation went in two steps:

1. First, CXPath node formulae were translated, in single-exponential time, into formulae of a temporal logic TL tree . Those formulae could be of size exponential in the size of the original CXPath formula. 2. TL tree formulae were translated, again in single-exponential time, into exponential-size QAs.

While this appears to give a double-exponential algorithm, a careful analysis of the translations showed that it did not occur, i.e., the state-space of the resulting QA was always single-exponential in the size of the original CXPath formula.

Still, as we explained before, it is undesirable to have such a two-stage translation, as it practically eliminates any chance of adapting algorithmic techniques that have been developed for the LTL-to-automata translation. So now we provide a direct translation for CXPath to automata.

CXPath-to-query automata translation

The direct translation from CXPath α queries into single-run QAs (Q, δ, F, Q s ) is done in the following steps:

1. First, we define the set sub(α) of subformulae of α (analog of the Fischer-Ladner closure). 2. Then we let the set Q be a subset of 2 sub(α) satisfying certain properties. 3. Then we define the set of final states. 4. Selection states are those states q ⊆ sub(α) that contain α. 5. Finally, we define the transition function: this is the most involved part of the translation.

Intuitively the automaton is such that there is exactly one accepting run for each tree which labels each node by the sets of all subformula from sub(α) it satisfies.

Subformulae of a CXP formula As standard in translations from logic to automata, we push all the negations down the formula in a way that they are all in front of either an atom (a) or a path formula (Eβ), so we assume all formulae are in such a form (we push negations inside subformulae as well).

We define, for a given node formula α, its subformulae sub(α) as follows:

sub(a) = {a} sub(α ∧ α ′ ) = {α ∧ α ′ } ∪ sub(α) ∪ sub(α ′ ) sub(¬α) = {¬α} ∪ sub(α) sub(α ∨ α ′ ) = {α ∨ α ′ } ∪ sub(α) ∪ sub(α ′ ) sub(step) = {step} sub(β ∨ β ′ ) = {β ∨ β ′ } ∪ sub(β) ∪ sub(β ′ ) sub(step * ) = {step * } sub(β/β ′ ) = {β/β ′ } ∪ sub(β) ∪ sub(β ′ ) sub(?α) = {?α} ∪ sub(α) sub((step/?α) * ) = {(step/?α) * } ∪ sub(α) sub(Eβ) = {Eβ} ∪ sub(β)

In the following, we refer to step, step * , and (step/?α) * as navigational connectives.

States Now fix a node formula α 0 . The set of states of the query automaton QA α0 is Q ⊂ 2 sub(α0) where each q ∈ Q satisfies the following conditions for each formula γ ∈ sub(α 0 ):

-If γ = α 1 ∨ α 2 , then γ ∈ q iff either α 1 ∈ q or α 2 ∈ q. -If γ = α 1 ∧ α 2 , then γ ∈ q iff both α 1 ∈ q and α 2 ∈ q. -If γ = β 1 ∨ β 2 , then γ ∈ q iff either β 1 ∈ q or β 2 ∈ q. -If γ =?α, then γ ∈ q iff α ∈ q. -If γ = Eβ, then γ ∈ q iff β ∈ q. -If γ = β 1 /β 2 , where β 1 does not contain any navigational connectives, then γ ∈ q iff β 1 ∈ q and β 2 ∈ q. -If γ is a node formula of the form a or Eβ, then γ ∈ q iff ¬γ / ∈ q. -If γ = β 2 /β 1 where β 2 is step * or (step/?α) * , then β 1 ∈ q implies β 2 /β 1 ∈ q. -If γ = step * or γ = (step/?α) * then γ ∈ q.

-Each state q contains exactly one formula of the form a.

Final states The set of final states F ⊂ Q is the set of states q such that for any step ∈ {≺ ns , ≺ − ns , ≺ − ch }: -q does not contain any formula of the form step or step/β.

-If q contains a formula of the form β ′ /β, where β ′ is of the form step * or (step/?α) * then q also contains β.

Selecting states

The selecting states Q s are simply the states containing α 0 .

In general, we denote by Q u the set of states containing a certain path or node formula u.

Thus Q s = Q α0 .

Transition function The transition function δ is defined as follows, for each q ∈ Q and a ∈ Σ :

δ(q, a) = L ns ∩ L up (q) ∩ L down (q, a)

where the languages L down (q, a), L up (q), and L ns are to be defined shortly.

Intuitively the language L ns checks horizontal constraints. It is independent from q and a and describes valid sequences of siblings w.r.t. the formula α 0 . The language L up (q) is used to check upward conditions. It ensures that every child of a node assigned to q is assigned to a state such that its upward formula are compatible with q. Finally, the language L down (q, a) is used to check local and downward constraints. For each node labeled by a and assigned to a state q it ensures that the labelling of its children is compatible with the downward formula of q. It also checks that a is compatible with q.

The language L ns of horizontal conditions L ns is the set of words from q 0 q 1 • • • q n−1 q n for n ∈ N which respects the following constraints.

-Conditions for the leftmost state q 0 • q 0 does not contain any formula of the form

≺ − ns /β • From each formula β ′ /β ∈ sub(α 0 ) where β ′ is either ≺ − * ns or (≺ − ns /?α) * , β ∈ q 0 iff β ′ /β ∈ q 0 .

-Conditions for the rightmost state q n • q n does not contain any formula of the form ≺ ns /β • From each formula β ′ /β ∈ sub(α 0 ) where β ′ is either ≺ * ns or (≺ ns /?α) * , β ∈ q n iff β ′ /β ∈ q n . -Conditions for two consecutive states q i , q i+1 .

• For any path formula

β in q i * If β =≺ ns /β ′ then β ′ ∈ q i+1 . * If β =≺ * ns /β ′ then either β ′ ∈ q i or ≺ * ns /β ′ ∈ q i+1 . * If β = (≺ ns /?α) * /β ′ then either β ′ ∈ q i or (≺ ns /?α) * /β ′ ∈ q i+1

and α ∈ q i+1 . • For any path formula

β in q i+1 * If β =≺ − ns /β ′ then β ′ ∈ q i . * If β =≺ − * ns /β ′ then either β ′ ∈ q i+1 or ≺ − * ns /β ′ ∈ q i . * If β = (≺ −

ns /?α) * /β ′ then either β ′ ∈ q i+1 or (≺ − ns /?α) * /β ′ ∈ q i and α ∈ q i . • The set sub(α 0 ) − q i does not contains any formula of the form ≺ ns or ≺ * ns or (≺ ns /?α) * .

• For any formula β in sub(α 0 ) − q i * If β =≺ ns /β ′ then β ′ / ∈ q i+1 . * If β =≺ * ns /β ′ then β ′ / ∈ q i and ≺ * ns /β ′ / ∈ q i+1 . * If β = (≺ ns /?α) * /β ′ then β ′ /

∈ q i and either (≺ ns /?α) * /β ′ / ∈ q i+1 or α / ∈ q i+1 . • The set sub(α 0 ) − q i+1 does not contains any formula of the form ≺ − ns or ≺ − * ns or (≺ − ns /?α) * .

• For any formula β in sub(α 0 ) − q i+1 * If β =≺ − ns /β ′ then β ′ / ∈ q i . * If β =≺ − * ns /β ′ then β ′ / ∈ q i+1 and ≺ − * ns /β ′ / ∈ q i . * If β = (≺ −

ns /?α) * /β ′ then β ′ / ∈ q i+1 and either (≺ − ns /?α) * /β ′ / ∈ q i or α / ∈ q i .

It is easy to build a DFA that checks all the conditions and thus recognises L ns .

The language L up (q) of upward conditions We define L up (q) = Q up (q) * , where Q up (q) is the set of states that are legal children of q wrt formulae of the form β or β/β ′ where β is ≺ − ch , ≺ − * ch or (≺ − ch /?α) * . Formally, a state q ′ belongs to Q up (q) if it satisfies the following conditions:

-For each path formula β in q ′ • If β =≺ − ch /β ′ then β ′ ∈ q. • If β =≺ − * ch /β ′ then either β ′ ∈ q ′ or ≺ − * ch /β ′ ∈ q. • If β = (≺ − ch /?α) * /β ′ then either β ′ ∈ q ′ or (≺ − ch /?α) * /β ′ ∈ q and α ∈ q. -The set sub(α 0 ) − q ′ does not contains any formula of the form ≺ − ch or ≺ − * ch or (≺ − ch /?α) * . -For each path formula β in sub(α 0 ) − q ′ • If β =≺ − ch /β ′ then β ′ / ∈ q. • If β =≺ − * ch /β ′ then β ′ / ∈ q ′ and ≺ − * ch /β ′ / ∈ q. • If β = (≺ − ch /?α) * /β ′ then β ′ / ∈ q ′ and either (≺ − ch /?α) * /β ′ / ∈ q or α / ∈ q.

The language L down (q, a) of local and downward conditions Let sub down (α 0 ) be is the set of formulae from sub(α 0 ) of the form either β or β/β ′ where β is ≺ ch , ≺ * ch or (≺ ch /?α) * . We define L down (q, a) = L(a, q, a)∩ u∈sub down (α0) L(u, q, a) where each L(u, q, a) is defined as follows:

-Propositional letters • L(a, q, a) = Q * if a ∈ q and ∅ otherwise. -Path conditions when u ∈ q • If u =≺ ch then L(u, q, a) = Q + . • If u =≺ * ch or u = (≺ ch /?α) * then L(u, q, a) = Q * . • If u =≺ ch /β ′ then L(u, q, a) = Q * Q β ′ Q * . • If u =≺ * ch /β ′ then either β ′ ∈ q or L(u, q, a) = Q * Q ≺ * ch /β ′ Q * . • If u = (≺ ch /?α) * /β ′ then either β ′ ∈ q or L(u, q, a) = Q * (Q (≺ ch /?α) * /β ′ ∩ Q α )Q * . -Path conditions when u / ∈ q • If u =≺ ch then L(u, q, a) = ǫ. • If u =≺ * ch or u = (≺ ch /?α) * then L(u, q, a) = ∅. • If u =≺ ch /β ′ then L(u, q, a) = Q * Q β ′ Q * . • If u =≺ * ch /β ′ then either β ′ ∈ q and L(u, q, a) = ∅, or β ′ / ∈ q and L(u, q, a) = Q * Q ≺ * ch /β ′ Q * . • If u = (≺ ch /?α) * /β ′ then either β ′ ∈ q and L(u, q, a) = ∅, or β ′ / ∈ q and L(u, q, a) = Q * (Q (≺ ch /?α) * /β ′ ∩ Q α )Q * .

Correctness of the construction

In this section, we prove that the correctness of our construction. Theorem 2. Let α 0 be a CXPath node formula.

1. The automaton QA α0 is a single-run query automaton such that [[α 0 ]] T = QA α0 (T ) for every tree T .

2. The automaton QA α0 is of size exponential in the size of α 0 and can be constructed in single-exponential time

The second point of the theorem follows directly from the construction given in the previous section. The first point of Theorem 2 follows from two propositions, presented below.

Consistency and Maximality

We show that an accepting run of the automaton labels each node of the input tree by a state which represents exactly all subformulae of the original formula which are true at the node. As an immediate corollary, the automaton has at most one accepting run per tree, and that those accepting runs select the same nodes as the CXPath formula.

First, we show that each accepting run of the automaton is both consistent and maximal in the following sense. Recall that our trees are of the form T = (D, λ), where D is the domain, and λ is the labelling function. Throughout the section, we fix a node CXPath formula α 0 . Definition 1 (Consistency). Let ρ be a labelling function D → 2 sub(α0) , for a given tree T (D, λ) and a given node formula α 0 . We say that ρ is consistent if, for each node s ∈ D, the following is true:

-for each node formula α ∈ ρ(s), we have s ∈ [[α]] T ; -for each path formula β ∈ ρ(s), there is at least one pair (s, s ′ ) in [[β]] T . Definition 2 (Maximality). Let ρ be a labelling function D → 2 sub(α0) , for a given tree T (D, λ) and a given node formula α 0 . We say that ρ is maximal if, for each node s ∈ D, the following is true:

-for each node formula α ∈ sub(α 0 ), if s ∈ [[α]] T , then α ∈ ρ(s); -for each path formula β ∈ sub(α 0 ), if [[β]] T contains at least one pair of the form (s, s ′ ), then β ∈ ρ(s).

Proposition 2 (Consistency and maximality). If ρ is an accepting run of QA α0 on a given tree T and for a given node formula α 0 , then ρ is both consistent and maximal.