Since navigational aspects of XPath correspond to first-order definability, it has been proposed to use the analogy with the very successful technique of translating LTL into automata, and produce efficient translations of XPath queries into automata on unranked trees. These translations can then be used for a variety of reasoning tasks such as XPath consistency, or optimization, under XML schema constraints. In the verification scenarios, translations into both nondeterministic and alternating automata are used. But while a direct translation from XPath into alternating automata is known, only an indirect translation into nondeterministic automata - going via intermediate logics - exists. A direct translation is desirable as most XML specifications have particularly nice translations into nondeterministic automata and it is natural to use such automata to reason about XPath and schemas. The goal of the paper is to produce such a direct translation of XPath into nondeterministic automata.
XML reasoning tasks have been addressed in many recent papers. Typical
problems include consistency of type declarations and constraints [
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 e1 and e2, is it true that d |= e1 ⊆ e2? In other words, is it true that for each XML tree T that conforms to d, the expression e1 selects a subset of nodes selected by e2? Suppose we can somehow capture by an automaton Ae the set of nodes selected by the expression e1 ∧ ¬e2, 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 Ad that accepts trees that conform to d. Then to see whether d |= e1 ⊆ e2 one simply checks whether
L(Ad × Ae) 6= ∅ since a tree in L(Ad × Ae) is a counterexample to d |= e1 ⊆ e2. 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
[
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
[
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 [
PPPAPutPomPaPtPa Task Translation Nonemptiness checking
Nondeterministic Alternating exponential polynomial 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 [
Both approaches have been explored in the XML context. In [
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 [
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 [
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 [
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. 2
XML documents as unranked trees XML documents are normally
abstracted as labeled unranked trees [
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. [
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 [
A query automaton (QA) for Σ-labeled unranked trees is a tuple QA = (Q, F, Qs, δ), where (Q, F, δ) is a nondeterministic unranked tree automaton, and Qs ⊆ 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) ∈ Qs} 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
T{Sρ(T ) | ρ is an accepting run of QA on T }. Both semantics capture the class
of unary MSO queries [
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:
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. 3
We present a first-order complete extension of XPath, called conditional XPath,
or CXPath [
The node formulae α and path formulae β of CXPath are given by: α, α′ :=
a | ¬α | α ∨ α′ | β, β′ := ?α | step | step∗ | (step/?α)∗
Eβ | β/β′ | β ∨ β′ − where step ∈ {≺ch, ≺ch, ≺ns, ≺n−s}.
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 = D − [[α]]T [[α ∨ α ]]T = [[α]]T ∪ [[α′]]T
′ [[Eβ]]T = π1([[β]]T ) [[?α]]T = {(s, s) | s ∈ [[α]]T } [[step]]T = {(s, s′) | s, s′ ∈ D and (s, s′) ∈ step} [[β ∨ β′]]T = [[β]]T ∪ [[β′]]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 [
The translation went in two steps: 1. First, CXPath node formulae were translated, in single-exponential time, into formulae of a temporal logic TLtree. Those formulae could be of size exponential in the size of the original CXPath formula. 2. TLtree 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. 4
The direct translation from CXPath α queries into single-run QAs (Q, δ, F, Qs) 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 2sub(α) 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(step) = {step} sub(step∗) = {step∗} sub(?α) = {?α} ∪ sub(α) sub(Eβ) = {Eβ} ∪ sub(β) sub(α ∧ α′) = {α ∧ α′} ∪ sub(α) ∪ sub(α′) sub(α ∨ α′) = {α ∨ α′} ∪ sub(α) ∪ sub(α′) sub(β ∨ β′) = {β ∨ β′} ∪ sub(β) ∪ sub(β′) sub(β/β′) = {β/β′} ∪ sub(β) ∪ sub(β′) sub((step/?α)∗) = {(step/?α)∗} ∪ 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 ⊂ 2sub(α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, ≺n−s, ≺c−h}: – 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 Qs are simply the states containing α0. In general, we denote by Qu the set of states containing a certain path or node formula u. Thus Qs = Qα0.
Transition function The transition function δ is defined as follows, for each q ∈ Q and a ∈ Σ :
δ(q, a) = Lns ∩ Lup(q) ∩ Ldown(q, a) where the languages Ldown(q, a), Lup(q), and Lns are to be defined shortly. Intuitively the language Lns checks horizontal constraints. It is independent from q and a and describes valid sequences of siblings w.r.t. the formula α0. The language Lup(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 Ldown(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 Lns of horizontal conditions Lns is the set of words from q0q1 · · · qn−1qn for n ∈ N which respects the following constraints. – Conditions for the leftmost state q0 • q0 does not contain any formula of the form ≺n−s /β • From each formula β′/β ∈ sub(α0) where β′ is either ≺n−s∗ or (≺n−s /?α)∗, β ∈ q0 iff β′/β ∈ q0. – Conditions for the rightmost state qn • qn does not contain any formula of the form ≺ns /β • From each formula β′/β ∈ sub(α0) where β′ is either ≺∗ns or (≺ns /?α)∗, β ∈ qn iff β′/β ∈ qn. – Conditions for two consecutive states qi, qi+1.
• For any path formula β in qi ∗ If β =≺ns /β′ then β′ ∈ qi+1. ∗ If β =≺∗ns /β′ then either β
′ ∈ qi or ′≺∈∗nsq/iβo′r∈( ≺qin+s1./?α)∗/β′ ∈ qi+1 ∗ If β = (≺ns /?α)∗/β′ then either β
and α ∈ qi+1. • For any path formula β in qi+1 ∗ If β =≺n−s /β′ then β′ ∈ q . ∗ If β =≺n−s∗ /β′ then eitheri β′ ∈ qi+1 or ≺n−s∗ /β′ ∈ qi. ∗ If β = (≺n−s /?α)∗/β′ then either β′ ∈ qi+1 or (≺n−s /?α)∗/β′ ∈ qi and α ∈ qi. • T≺hnse osert(≺sunbs(α/?0α))−∗.qi does not contains any formula of the form ≺ns or ∗ • For any formula β in sub(α0) − qi ∗ If β =≺ns /β′ then β′ ∈/ qi+1. ∗ If β =≺∗ns /β′ then β′ ∈/ qi and ≺∗ns /β′ ∈/ qi+1. ∗ If β = (≺ns /?α)∗/β′ then β′ ∈/ qi and either (≺ns /?α)∗/β′ ∈/ qi+1 or α ∈/ qi+1. • The set sub(α0) − qi+1 does not contains any formula of the form ≺n−s or ≺n−s∗ or (≺n−s /?α)∗. • For any formula β in sub(α0) − qi+1 ∗ If β =≺n−s /β′ then β′ ∈/ qi. ∗ If β =≺n−s∗ /β′ then β′ ∈/ qi+1 and ≺n−s∗ /β′ ∈/ qi. ∗ If β = (≺n−s /?α)∗/β′ then β′ ∈/ qi+1 and either (≺n−s /?α)∗/β′ ∈/ qi or α ∈/ qi.
It is easy to build a DFA that checks all the conditions and thus recognises Lns. The language Lup(q) of upward conditions We define Lup(q) = Qup(q)∗, where Qup(q) is the set of states that are legal children of q wrt formulae of the form β or β/β′ where β is ≺ch, ≺c−h∗ or (≺c−h /?α)∗.
− Formally, a state q′ belongs to Qup(q) if it satisfies the following conditions: – For each path formula β in q′
− • If β =≺c−h∗ /β′ then β′ ∈ q. • If β =≺chc−h//β?′αt)h∗e/nβ′eitthheenr eβi′th∈erq′βo′r∈≺qc−′ho∗r/(β≺′ c−∈h q/.?α)∗/β′ ∈ q and α ∈ q. • If β = (≺ −∗ – The set sub(α0) − q′ does not contains any formula of the form ≺c−h or ≺ch or (≺c−h /?α)∗. – For each path formula β in sub(α0) − q′ • If β =≺c−−h∗ /β′ then β′ ∈/ q.
•• IIff ββ ==≺( ≺chc−h//β?′αt)h∗e/nβ′βt′h∈/enq′βa′n∈/dq≺′ac−hn∗d/eβi′th∈/erq.(≺c−h /?α)∗/β′ ∈/ q or α ∈/ q. The language Ldown(q, a) of local and downward conditions Let subdown(α0) be is the set of formulae from sub(α0) of the form either β or β/β′ where β is ≺ch, ≺ch or (≺ch /?α)∗.
∗ We define Ldown(q, a) = L(a, q, a)∩Tu∈subdown(α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 =≺c∗h or u = (≺ch /?α)∗ then L(u, q, a) = Q∗. • If u =≺ch /β′ then L(u, q, a) = Q∗Qβ′Q∗. • If u =≺c∗h /β′ then either β′ ∈ q or L(u, q, a) = Q∗Q≺c∗h/β′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 ∗ • ILf(uu,=q,(a≺) c=h /Q?∗αQ)∗≺/c∗βh /′βt′hQe∗n. either β′ ∈ q and L(u, q, a) = ∅, or β′ ∈/ q and
L(u, q, a) = Q∗(Q(≺ch/?α)∗/β′ ∩ Qα)Q∗. 5
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 → 2sub(α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 → 2sub(α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.
This proposition is proved by a mutual induction on the structure of node and path formulae occurring in sub(α0). We present a few sample cases below; full details are in the appendix.
Let s be a node of the tree, a its label, α a node formula, and β a path formula. We suppose, in the cases of consistency, that both α and β are in ρ(s), and in the cases of maximality, that both α and β are true at s. In the following we denote by basic constraints, the constraints given in the definition of the states of the automaton in Section 4.
– Consistency: some base cases.
• If α = a′ then a′ = a so α is true at s.(Otherwise, a ∈/ ρ(s) as each states contains at most one propositional letter so L(a, ρ(s), a) is empty, and thus ρ cannot be an accepting run.) • If β =≺ch then L(≺ch, ρ(s), a) = Q+, thus s has a least one child, so β is true at s. • If β =≺c−h then the only case where β might not be true is at the root.
But this cannot happen, as any state containing ≺c−h cannot be final. So β is true at s. – Maximality: some base cases.
• If α = a′ then a′ = a, because α is true at s. If α ∈/ ρ(s) then
L(a, ρ(s), a) = ∅ and ρ cannot be accepting. Thus, α ∈ ρ(s). • If β =≺ch then s is not a leaf. If β ∈/ ρ(s) then L(β, ρ(s), a) = ǫ which contradicts the fact that s is not a leaf. Thus, β ∈ ρ(s).
− • If β =≺ch then s is not the root, which implies that s has a parent s′, labelled by the state ρ(s′). Then, we have ρ(s) ∈ Lup(ρ(s′)), and all states in Lup contain β. Thus, β ∈ ρ(s). – Consistency: some induction cases.
• If α = ¬α′ then, because of basic constraints, α′ ∈/ ρ(s). By the induction hypothesis for maximality, α′ cannot be true at s. So α is true at s. • If α = α1 ∨ α2 then, because of basic constraints, either α1 or α2 is in ρ(s). Then, by the induction hypothesis for consistency, either α1 or α2 is true at s. So α is true at s. • If α = Eβ then, because of basic constraints, β ∈ ρ(s). By the induction hypothesis for consistency, β is true at s, i.e. contains at least one element when evaluated starting from s. So α is true at s. • If β =?α then, because of basic constraints, ?α ∈ ρ(s). By the induction hypothesis for consistency, α is true at s. So the interpretation of β contains at least (s, s), hence β is satisfied at s. – Maximality: some induction cases.
• If α = ¬α′ then, α′ cannot be true at s. By the induction hypothesis for consistency, this means that α′ ∈/ ρ(s). Then, because of basic constraints, α ∈ ρ(s). • If α = α1 ∨ α2 then either α1 or α2 is true at s. By the induction hypothesis for maximality, either α1 or α2 is in ρ(s). So, because of basic constraints, α ∈ ρ(s). • If α = Eβ then the interpretation of β contains (s, s′) for some s′, which means that β is true at s. By the induction hypothesis, β ∈ ρ(s). So, because of basic constraints, α ∈ ρ(s). • If β =?α then the interpretation of β contains (s, s) which means that α is true at s. By the induction hypothesis, α ∈ ρ(s). So, because of basic constraints, β ∈ ρ(s).
Accepting Runs We have proved so far that the accepting runs of the automaton were consistent and maximal labellings, which means that the automaton accepts at most the same trees than the original CXPath formula. We now prove that each consistent and maximal labelling of a tree is an accepting run of the automaton.
Proposition 3 (Accepting Runs). Let ρ be a maximal and consistent labelling of the nodes of a given tree T with respect to a given formula α0. Then ρ is an accepting run of QAα0 .
This shows that the QA we constructed has indeed at most one accepting run per tree, and that during this run, a node gets labelled by a state which contains α0 iff α0 is true at that node. Hence, the automaton selects all the nodes which are also selected by α0, and this concludes the proof of Theorem 2. Acknowledgements Most of this work was done while all three authors were at the University of Edinburgh, supported by EPSRC grant G049165 and FETOpen Project FoX, grant agreement 233599.