Keywords: Mu-calculus, satisfiability, trees, XPath, queries, XML, types, regular tree grammars Mu-calcul, satisfaisabilité, arbres, XPath, requêtes, XML, types, grammaires d'arbres régulières

An extended abstract of this work was presented at the ACM Conference on Programming Language Design and Implementation (PLDI), 2007 [21]. Extensions included in this article notably comprise proof sketches, crucial implementation techniques for building a satisfiability-testing algorithm which performs well in practice, a detailed description of the algorithm, and formal descriptions and explanations about an important property of the logic: cycle-freeness for formulas.

Introduction

This work is motivated by the need of efficient type checkers for XML-based programming languages where XML types and XPath queries are used as first class language constructs. In such settings, XPath decision problems in the presence of XML types such as DTDs or XML Schemas arise naturally. Examples of such decision problems include emptiness test (whether an expression ever selects nodes), containment (whether the results of an expression are always included in the results of another one), overlap (whether two expressions select common nodes), and coverage (whether nodes selected by an expression are always contained in the union of the results selected by several other expressions).

XPath decision problems are not trivial in that they need to be checked on a possibly infinite quantification over a set of trees. Another difficulty arises from the combination of upward and downward navigation on trees with recursion [START_REF] Vardi | Reasoning about the past with two-way automata[END_REF].

The most basic decision problem for XPath is the emptiness test of an expression [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]. This test is important for optimization of host languages implementations: for instance, if one can decide at compile time that a query result is empty then subsequent bound computations can be ignored. Another basic decision problem is the XPath equivalence problem: whether or not two queries always return the same result. It is important for reformulation and optimization of an expression [START_REF] Genevès | Logic-based XPath optimization[END_REF] , which aim at enforcing operational properties while preserving semantic equivalence [START_REF] Levin | Type-based optimization for regular patterns[END_REF]. The most essential problem for type-checking is XPath containment. It is required for the control-flow analysis of XSLT [START_REF] Møller | Static validation of XSL Transformations[END_REF], for checking integrity constraints [START_REF] Fallside | XML Schema part 0: Primer second edition[END_REF], and for XML security [START_REF] Fan | Secure XML querying with security views[END_REF].

The complexity of XPath decision problems heavily depends on the language features. Previous works [START_REF] Schwentick | XPath query containment[END_REF][START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF] showed that including general comparisons of data values from an infinite domain may lead to undecidability. Therefore, we focus on a XPath fragment which covers all features except counting [START_REF] Zilio | A logic you can count on[END_REF] and data values.

In our approach to solve XPath decision problems, two issues need to be addressed. First, we identify the most appropriate logic with sufficient expressiveness to capture both regular tree types and our XPath fragment. Second, we solve efficiently the satisfiability problem which allows to test if a given formula of the logic admits a satisfying finite tree.

The essence of our results lives in a sub-logic of the alternation free modal µ-calculus (AFMC) with converse, some syntactic restrictions on formulas, without greatest fixpoint, and whose models are finite trees. We prove that XPath expressions and regular tree type formulas conform to these syntactic restrictions. Boolean closure is the key property for solving the containment (a logical implication). In order to obtain closure under negation, we prove that the least and greatest fixpoint operators collapse in a single fixpoint operator. Surprisingly, the translations of XML regular tree types and a large XPath fragment does not increase complexity since they are linear in the size of the corresponding formulas in the logic. The combination of these ingredients lead to our main result: a satisfiability algorithm for a logic for finite trees whose time complexity is a simple exponential of the size of a formula.

The decision procedure has been implemented in a system for solving XML decision problems such as XPath emptiness, containment, overlap, and coverage, with or without XML type constraints. The system can be used as a component of static analyzers for programming languages manipulating XPath expressions and XML type annotations for both input and output.

Outline

The paper is organized as follows. We first present our data model, trees with focus, and our logic in §3 and §4. We next present XPath and its translation in our logic in §5. Our satisfiability algorithm is introduced and proven correct in §6, and a few details of the implementation are discussed in §7. Applications for type checking and some experimental results are described in §8. We study related work in §9 and conclude in §10.

Trees with Focus

In order to represent XML trees that are easy to navigate, we use focused trees, inspired by Huet's Zipper data structure [START_REF] Huet | The zipper[END_REF]. Focused trees not only describe a tree but also its context: its previous siblings and its parent, including its parent context recursively. Exploring such a structure has the advantage to preserve all information, which is quite useful when considering languages such as XPath that allow forward and backward axes of navigation.

Formally, we assume an alphabet Σ of labels, ranged over by σ. A focused tree (t, c) is a pair consisting of a tree t and its context c. The context (tl , c[σ], tl ) comprises three components: a list of trees at the left of the current tree in reverse order (the first element of the list is the tree immediately to the left of the current tree), the context above the tree, and a list of trees at the right of the current tree. The context above the tree may be Top if the current tree is at the root, otherwise it is of the form c[σ] where σ is the label of the enclosing element and c is the context in which the enclosing element occurs.

In order to deal with decision problems such as containment, we need to represent in a focused tree the place where the evaluation of a request was started. To this end, we use a start mark, often simply called "mark" in the following. We thus consider focused trees where a single tree or a single context node is marked, as in σ [tl ] or (tl , c[σ ], tl ). When the presence of the mark is unknown, we write it as σ • [tl ]. We write F for the set of finite focused trees containing a single mark. The name of a focused tree is defined as nm(σ • [tl ], c) = σ.

We now describe how to navigate focused trees, in binary style. There are four directions, or modalities, that can be followed: for a focused tree f , f 1

INRIA L µ ϕ, ψ ::= formula true | σ | ¬σ atomic prop (negated) | | ¬ start prop (negated) | X variable | ϕ ∨ ψ disjunction | ϕ ∧ ψ conjunction | a ϕ | ¬ a existential (negated) | µX i = ϕ i in ψ least n-ary fixpoint | νX i = ϕ i in ψ
greatest n-ary fixpoint Figure 1: Logic formulas changes the focus to the children of the current tree, f 2 changes the focus to the next sibling of the current tree, f 1 changes the focus to the parent of the tree if the current tree is a leftmost sibling, and f 2 changes the focus to the previous sibling. Formally, we have:

(σ • [t :: tl ], c) 1 def = (t, ( , c[σ • ], tl )) (t, (tl l , c[σ • ], t :: tl r )) 2 def = (t , (t :: tl l , c[σ • ], tl r )) (t, ( , c[σ • ], tl )) 1 def = (σ • [t :: tl ], c) (t , (t :: tl l , c[σ • ], tl r )) 2 def = (t, (tl l , c[σ • ], t :: tl r ))
When the focused tree does not have the required shape, these operations are not defined.

The Logic

We introduce in this section the logic to which we translate XPath expressions and XML regular tree types. This logic a sub-logic of the alternation free modal µ-calculus with converse. We also introduce a restriction on the formulas we consider and give an interpretation of formulas as sets of finite focused trees. We finally show that the logic has a single fixpoint for these models and that it is closed under negation.

In the following, we use an overline bar to denote tuples. For instance, we write X i = ϕ i for (X 1 = ϕ 1 ; X 2 = ϕ 2 ; . . . ; X n = ϕ n ). Tuples of variables, such as X i , are often identified to sets.

In the following definitions, a ∈ {1, 2, 1, 2} are programs and atomic propositions σ correspond to labels from Σ. We also assume that a = a. Formulas defined in Figure 1 include the truth predicate, atomic propositions (denoting the name of the tree in focus), start propositions (denoting the presence of the start mark), disjunction and conjunction of formulas, formulas under an existential (denoting the existence a subtree satisfying the sub-formula), and least and greatest n-ary fixpoints. We chose to include a n-ary version of fixpoints because regular types are often defined as a set of mutually recursive definitions, making their translation in our logic more direct and succinct. In the following we write "µX.ϕ" for "µX = ϕ in ϕ". We define in Figure 2 an interpretation of our formulas as subsets of F, the set of finite focused trees with a single start mark. The interpretation of the n-ary fixpoints first compute the smallest or largest interpretation for each ϕ i , bind the resulting sets T i to the variables X i , then returns the interpretation of ψ.

V def = F σ V def = {f | nm(f ) = σ} X V def = V (X) ¬σ V def = {f | nm(f ) = σ} ϕ ∨ ψ V def = ϕ V ∪ ψ V V def = f | f = (σ [tl ], c) ϕ ∧ ψ V def = ϕ V ∩ ψ V ¬ V def = {f | f = (σ[tl ], c)} a ϕ V def = {f a | f ∈ ϕ V ∧ f a defined} ¬ a V def = {f | f a undefined} µX i = ϕ i in ψ V def = let T i = T i ⊆ F | ϕ i V [Ti/Xi] ⊆ T i i in ψ V [Ti/Xi] νX i = ϕ i in ψ V def = let T i = T i ⊆ F | T i ⊆ ϕ i V [Ti/Xi] i in ψ V [Ti/Xi]
To illustrate the interpretation of fixpoints, consider the two following formulas ϕ = µX. 1 X ∨ 1 X and ψ = νX. 1 X ∨ 1 X, which respectively expand

to µX = 1 X ∨ 1 X in 1 X ∨ 1 X and νX = 1 X ∨ 1 X in 1 X ∨ 1 X.
The interpretation of ϕ is straightforward: associating the empty set to X, we have 1

X ∨ 1 X ∅/X ⊆ ∅ thus ϕ = ∅.
Intuitively, there is no base case in the formula, hence the smallest fixpoint is the empty one.

The interpretation of ψ is more complex: it is the set of every focused tree with at least two nodes, one being the parent of the other. We now show that the interpretation of ψ includes the focused tree f 1 = (a[b[ ]], T ), where T is the top-level context ( , Top, ). We do not specify the position of the mark as it is not used in the query: it could be anywhere. Let

f 2 = f 1 1 , that is the tree (b[ ], ( , T [a], )). We thus have f 2 1 = f 1 . Finally, let V be the mapping [{f 1 ; f 2 }/X]. We compute as follow: 1 X ∨ 1 X V = 1 X V ∪ 1 X V = f 1 | f ∈ X V ∧ f 1 defined ∪ {f 1 | f ∈ X V ∧ f 1 defined} = {f 1 } ∪ {f 2 } INRIA thus V (X) ⊆ 1 X ∨ 1 X V , hence by definition of the largest fixpoint, we have f 1 ∈ ψ ∅ .
We now restrict the set of valid formulas to cycle-free formulas. To define them, we first need to define the notion of a path in a formula. Given a formula ϕ, the set of its paths P(ϕ) is the set of sequential chains of modalities contained in the formula. We write for the empty path.

P( a ϕ) = { a p | p ∈ P(ϕ)} P(ϕ ∨ ψ) = P(ϕ) ∪ P(ψ) P(ϕ ∧ ψ) = P(ϕ) ∪ P(ψ) P(ϕ) = otherwise
A modality cycle in a path is a sub-sequence of the form a a . We define cycle-free formulas as formulas that have a bound on the number of modality cycles in every path, independently of the number of unfolding of their fixpoints. For instance, the formula "µX = 1 ( ∨ 1 X) in X" is not cycle free: for any integer n, there is an unfolding of the formula such that a path with n modality cycles exists. Similarly, the formulas ϕ and ψ above are also not cycle free. On the other hand, the formula "µX = 1 (X ∨ Y ), Y = 1 (Y ∨ ) in X" is cycle free: there is at most one modality cycle for each path.

Cycle-free formulas have a very interesting property, which we now describe. To test whether a tree satisfies a formula, one may define a straightforward inductive relation between trees and formulas that only holds when the root of the tree satisfies the formula, unfolding fixpoints if necessary. Given a tree, if a formula ϕ is cycle free, then every node of the tree will be tested a finite number of time against any given subformula of ϕ. The intuition behind this property, which holds a central role in the proof of lemma 4.2, is the following. If a tree node is tested an infinite number of times against a subformula, then there must be a cycle in the navigation in the tree, corresponding to some modalities occurring in the subformula, between one occurrence of the test and the next one. As we consider trees, the cycle implies there is a modality cycle in the formula (as unbalanced cycles of the form 1 2 1 2 cannot occur). Hence the number of modality cycles in any expansion of ϕ is unbounded, thus the formula is not cycle free.

Figure 3 gives an inductive relation that decides whether a formula is cycle free. In the judgement ∆ Γ R I ϕ of Figure 3, ∆ is an environment binding some recursion variables to their formulas, Γ binds variables to modalities, R is a set of variables that have already been expanded (see below), and I is a set of variables already checked.

The environment Γ used to derive the judgement consists of bindings from variables (from enclosing fixpoint operators) to modalities. A modality may be (no information is known about the variable), a (the last modality taken a was consistent), or ⊥ (a cycle has been detected). A formula is not cycle free if an occurrence of a variable under a fixpoint operator is either not under a modality (in this case Γ(X) = ), or is under a cycle (Γ(X) = ⊥). Cycle detection uses an auxiliary operator to detect modality cycles:

Γ a def = {X : (Γ(X) a )} ϕ = , σ, ¬σ, , or ¬ ∆ Γ R I ϕ ∆ Γ R I ϕ ∆ Γ R I ψ ∆ Γ R I ϕ ∨ ψ ∆ Γ R I ϕ ∆ Γ R I ψ ∆ Γ R I ϕ ∧ ψ ∆ Γ R I ¬ a ∆ (Γ a ) R I ϕ ∆ Γ R I a ϕ ∀X j ∈ X i . (∆ + X i : ϕ i ) (Γ + X i : ) R\Xi I\Xi ϕ j ∆ Γ R\Xi I∪Xi ψ ∆ Γ R I µX i = ϕ i in ψ ∀X j ∈ X i . (∆ + X i : ϕ i ) (Γ + X i : ) R\Xi I\Xi ϕ j ∆ Γ R\Xi I∪Xi ψ ∆ Γ R I νX i = ϕ i in ψ NoRec X ∈ R Γ(X) = a ∆ Γ R I X Rec X ∈ R ∆ Γ R∪{X} I ∆(X) ∆ Γ R I X Ign X ∈ I ∆ Γ R I X Figure 3: Cycle-free formulas where • • 1 2 1 2 1 2 1 2 1 1 2 ⊥ 2 2 1 2 1 ⊥ 1 ⊥ 2 1 2 2 1 ⊥ 1 2 ⊥ ⊥ ⊥ ⊥ ⊥
To check that mutually recursive formulas are cycle-free, we proceed the following way. When a mutually recursive formula is encountered, for instance µX i = ϕ i in ψ, we check every recursive binding. Because of mutual recursion, we cannot check formulas independently and we need to expand a variable the first time it is encountered (rule Rec). However there is no need to expand it a second time (rule NoRec). When checking ψ, as the formula bound to the enclosing recursion have been checked to be cycle free, there is no need to further check these variables (rule Ign). To account for shadowing of variables, we make sure that newly bound recursion variables are removed from I and R when checking a recursion. One may easily prove that if ∆ Γ R I ϕ holds, then

I ∩ R = ∅.
This relation decides whether a formula is cycle free because, if it is not, there must be a recursive binding of X i to ϕ i such that ϕ i { ϕi / Xi }{ ϕj / Xj } exhibits a modality cycle above X i , where the X j are recursion variables being defined (either in the recursion defining X i or in an enclosing recursion definition). Cycles are thus detected unfolding every recursive definition once in every formula..

INRIA

Note that our definition of cycle free formulas is strict: a formula such as µX. 1 1 X in contains a cycle even though the variable on which the cycle occurs never needs to be expanded.

We are now ready to show a first result: in the finite focused-tree interpretation, the least and greatest fixpoints coincide for cycle-free formulas. To this end, we prove a stronger result that states that a given focused tree is in the interpretation of a formula if it is in the interpretation of a finite unfolding of the formula. In the base case, we use the formula σ ∧ ¬σ as "false". Definition 4.1 (Finite unfolding) The finite unfolding of a formula ϕ is the set unf (ϕ) inductively defined as

unf (ϕ) def = {ϕ} for ϕ = , σ, ¬σ, , ¬ , X, ¬ a unf (ϕ ∨ ψ) def = {ϕ ∨ ψ | ϕ ∈ unf (ϕ), ψ ∈ unf (ψ)} unf (ϕ ∧ ψ) def = {ϕ ∧ ψ | ϕ ∈ unf (ϕ), ψ ∈ unf (ψ)} unf ( a ϕ) def = { a ϕ | ϕ ∈ unf (ϕ)} unf (µX i = ϕ i in ψ) def = unf (ψ{ µXi=ϕi in ϕi / Xi }) ∪ {σ ∧ ¬σ} unf (νX i = ϕ i in ψ) def = unf (ψ{ νXi=ϕi in ϕi / Xi }) ∪ {σ ∧ ¬σ} Lemma 4.2 Let ϕ a cycle-free formula, then ϕ V = unf (ϕ) V .
The intuition why this lemma holds is the following. Given a tree satisfying ϕ, we deduce from the hypothesis that ϕ is cycle free the fact that every node of the tree will be tested a finite number of times against every subformula of ϕ. As the tree and the number of subformulas are finite, the satisfaction derivation is finite hence only a finite number of unfolding is necessary to prove that the tree satisfies the formula. As least and greatest fixpoints coincide when only a finite number of unfolding is required, this is sufficient to show that they collapse. Note that this would not hold if infinite trees were allowed: the formula µX. 1 X is cycle free, but its interpretation is empty, whereas the interpretation of νX. 1 X includes every tree with an infinite branch of 1 children.

We now illustrate why formulas need to be cycle free for the fixpoints to collapse. Consider the formula µX. 1 1 X. Its interpretation is empty. The interpretation of νX. 1 1 X however contains every focused tree that has one 1 child. Proof:

[sketch of Lemma 4.2] Let f in ϕ V , we show that it is in unf (ϕ) V .
As recursive definitions are never negated, the converse is immediate.

As hinted above, the result is a consequence of the fact that a sub-formula is never confronted twice to the same node of f as there is no cycle in the formula. It is thus possible to annotate occurrences of ν and µ with the direction the formula is exploring for each variable, as in Figure 3, and prove the result by induction on the size of f in this direction.

First, we associate each recursion variable in every µ and ν of the initial formula with a unique identifier. (From now on, we do not distinguish between smallest and largest fixed points, as we handle them identically.) For every recursive formula µX i = ϕ i in ψ, we annotate every modality a ξ in every ϕ j where X i is free in ξ with the variable X i . Note that modalities may be annotated with more than one variable in case of nested recursions.

We then unfold every formula once, to guarantee that the sub-formulas of the shape µX i = ϕ i in ψ are in fact of the shape µX i = ϕ i in ϕ j . We then build a satisfaction derivation maintaining extra information, which we now detail.

• Upon unfolding a recursive formula for the first time, the recursion identifiers are recorded and associated with the direction. Moreover, they are also associated with an integer, the size of the tree f .

• Upon encountering a modality a annotated with identifiers, the direction of the identifiers is updated with the modality according to the • a operator. As the formula is cycle-free, the resulting direction cannot be ⊥.

• Upon unfolding a recursive formula µX i = ϕ i in ϕ j whose identifiers have been already recorded, the integer associated to X j is updated to be the longest path, defined below, of the current focused tree in X j 's direction.

We now define the longest path of a focused tree in a given direction. Given a tree f and a direction a , we define the longest path as the longest cycle-free path of f compatible with the direction, i.e. that does not start in the a direction. By definition of the trees, if a is 1 or 2 , then the path is only made of 1 and 2 steps. If a is 1 or 2 , then the path is a sequence of 1 or 2 steps followed by a sequence of 1 and 2 steps joined by either a 1 2 or a 2 1 sequence. In the case of the unknown direction , the longest path is the size of the tree.

We may now prove the property that f belongs to the finite unfolding of ϕ by induction on the lexical order of:

1. the number of identifiers not yet annotated with a direction and an integer; 2. the sum of the integers of every annotated identifier; 3. the size of the formula.

We proceed by case on the syntax of the formula. The interesting cases are recursive formulas (in every other case, the size of the formula decreases while leaving the other induction metrics unchanged as annotations are updated only when unfolding formulas). In the case of a formula involving unannotated identifiers, they are now all annotated (thus decreasing the number of unannotated identifiers) and associated to the size of the tree. In the case of an annotated formula recursion ϕ = µX i = ϕ i in ϕ j , this formula may only have been produced by a previous expansion where X j was replaced by ϕ. As the formula is cycle-free, at least one modality has been encountered and it was annotated by X j , since X j was free in the formula before the previous expansion. Moreover, every modality encountered since the previous unfolding was also annotated by X j , and as the formula is cycle-free these modalities are all compatible. Thus the longest path of f in X j 's direction has decreased by at least one, and as the other identifiers are unchanged, the sum has decreased and we conclude by induction that f is in a finite expansion of the expansion of ϕ.

In the rest of the paper, we only consider least fixpoints. An important consequence of Lemma 4.2 is that the logic restricted in this way is closed under INRIA negation using De Morgan's dualities, extended to eventualities and fixpoints as follows:

¬ a ϕ def = ¬ a ∨ a ¬ϕ ¬µX i = ϕ i in ψ def = µX i = ¬ϕ i { Xi / ¬Xi } in ¬ψ{ Xi / ¬Xi }

XPath and Regular Tree Languages

XPath [START_REF] Clark | XML path language (XPath) version 1.0, W3C recommendation[END_REF] is a powerful language for navigating in XML documents and selecting sets of nodes matching a predicate. In their simplest form, XPath expressions look like "directory navigation paths". For example, the XPath expression /child::book/child::chapter/child::section navigates from the root of a document (designated by the leading "/") through the top-level "book" node to its "chapter" child nodes and on to its child nodes named "section". The result of the evaluation of the entire expression is the set of all the "section" nodes that can be reached in this manner. The situation becomes more interesting when combined with XPath's capability of searching along "axes" other than "child". For instance, one may use the "preceding-sibling" axis for navigating backward through nodes of the same parent, or the "ancestor" axis for navigating upward recursively. Furthermore, at each step in the navigation the selected nodes can be filtered using qualifiers: boolean expression between brackets that can test the existence or absence of paths.

We consider a large XPath fragment covering all major features of the XPath recommendation [START_REF] Clark | XML path language (XPath) version 1.0, W3C recommendation[END_REF] except counting and comparisons between data values.

Figure 4 gives the syntax of XPath expressions. Figure 5 and Figure 6 give an interpretation of XPath expressions as functions between sets of focused trees.

XPath Embedding

We now explain how an XPath expression can be translated into an equivalent L µ formula that performs navigation in focused trees in binary style.

Logical Interpretation of Axes

The translation of navigational primitives (namely XPath axes) is formally specified in Figure 7. The translation function, noted "A → a χ ", takes an XPath axis a as input, and returns its L µ translation, parameterized by the L µ formula χ given as parameter. This parameter represents the context in which the axis occurs and is needed for formula composition in order to translate path composition. More precisely, the formula A → a χ holds for all nodes that can be accessed through the axis a from some node verifying χ. Let us consider an example. The formula A → child χ , translated as µZ. 1 χ∨ 2 Z, is satisfied by children of the context χ. These nodes consist of the first child and the remaining children. From the first child, the context must be reached immediately by going once upward via 1. From the remaining children, the context is reached by going upward (any number of times) via 2 and finally once via 1.

L Figure 9 illustrates the translation of the XPath expression "child::a[child::b]". This expression selects all "a" child nodes of a given context which have at least one "b" child. The translated L µ formula holds for "a" nodes which are selected by the expression. The first part of the translated formula, ϕ, corresponds to the step "child::a" which selects candidates "a" nodes. The second part, ψ, navigates downward in the subtrees of these candidate nodes to verify that they have at least one immediate "b" child.

::= qualifier q 1 and q 2 conjunction | q 1 or q 2 disjunction | not q negation | p path Axis a ::= tree navigation axis child | self | parent | descendant | desc-or-self | ancestor | anc-or-self | foll-sibling | prec-sibling | following | preceding
Note that without converse programs we would have been unable to differentiate selected nodes from nodes whose existence is tested: we must state properties on both the ancestors and the descendants of the selected node. Equipping the L µ logic with both forward and converse programs is therefore crucial for supporting XPath 1 . Logics without converse programs may only be used for solving XPath emptiness but cannot be used for solving other decision problems such as containment efficiently.

XPath composition construct p 1 /p 2 translates into formula composition in L µ , such that the resulting formula holds for all nodes accessed through p 2 from 1 One may ask whether it is possible to eliminate upward navigation at the XPath level but it is well known that such XPath rewriting techniques cause exponential blow-ups of expression sizes [START_REF] Olteanu | XPath: Looking forward[END_REF].

INRIA S e • • : L XPath → 2 F → 2 F S e /p F def = S p p root(F ) S e p F def = S p p {(σ [tl],c)∈F } S e e 1 e 2 F def = S e e 1 F ∪ S e e 2 F S e e 1 ∩ e 2 F def = S e e 1 F ∩ S e e 2 F S p • • : Path → 2 F → 2 F S p p 1 /p 2 F def = f | f ∈ S p p 2 (Sp p1 F ) S p p[q] F def = {f | f ∈ S p p F ∧ S q q f } S p a::σ F def = {f | f ∈ S a a F ∧ nm(f ) = σ} S p a:: * F def = {f | f ∈ S a a F } S q • • : Qualif → F → {true, false} S q q 1 and q 2 f def = S q q 1 f ∧ S q q 2 f S q q 1 or q 2 f def = S q q 1 f ∨ S q q 2 f S q not q f def = ¬ S q q f S q p f def = S p p {f } = ∅ S a • • : Axis → 2 F → 2 F S a self F def = F S a child F def = fchild(F ) ∪ S a foll-sibling fchild(F ) S a foll-sibling F def = nsibling(F ) ∪ S a foll-sibling nsibling(F ) S a prec-sibling F def = psibling(F ) ∪ S a prec-sibling psibling(F ) S a parent F def = parent(F ) S a descendant F def = S a child F ∪ S a descendant (Sa child F ) S a desc-or-self F def = F ∪ S a descendant F S a ancestor F def = S a parent F ∪ S a ancestor (Sa parent F ) S a anc-or-self F def = F ∪ S a ancestor F S a following F def = S a desc-or-self (Sa foll-sibling (Sa anc-or-self F )) S a preceding F def = S a desc-or-self (Sa prec-sibling (Sa anc-or-self F ))
(F ) def = {f 1 | f ∈ F ∧ f 1 defined} nsibling(F ) def = {f 2 | f ∈ F ∧ f 2 defined} psibling(F ) def = f 2 | f ∈ F ∧ f 2 defined parent(F ) def = {(σ • [rev a(tl l , t :: tl r )], c) | (t, (tl l , c[σ • ], tl r )) ∈ F } rev a( , tl r ) def = tl r rev a(t :: tl l , tl r ) def = rev a(tl l , t :: tl r ) root(F ) def = {(σ [tl ], (tl , Top, tl )) ∈ F } ∪ root(parent(F ))
Figure 6: Auxiliary Functions for XPath Interpretation. those nodes accessed through p 1 from χ. The translation of the branching construct p[q] significantly differs. The resulting formula must hold for all nodes that can be accessed through p and from which q holds. To preserve semantics, the translation of p[q] stops the "selecting navigation" to those nodes reached by p, then filters them depending on whether q holds or not. We express this by introducing a dual formal translation function for XPath qualifiers, noted Q ← q • and defined in Figure 10, that performs "filtering" instead of navigation. Specifically, P → • • can be seen as the "navigational" translating function: the translated formula holds for target nodes of the given path. On the opposite, Q ← • • can be seen as the "filtering" translating function: it states the existence of a path without moving to its result. The translated formula Q ← q χ (respectively P ← p χ ) holds for nodes from which there exists a qualifier q (respectively a path p) leading to a node verifying χ.

A → • • : Axis → L µ → L µ A → self χ def = χ A → child χ def = µZ. 1 χ ∨ 2 Z A → foll-sibling χ def = µZ. 2 χ ∨ 2 Z A → prec-sibling χ def = µZ. 2 χ ∨ 2 Z A → parent χ def = 1 µZ.χ ∨ 2 Z A → descendant χ def = µZ. 1 (χ ∨ Z) ∨ 2 Z A → desc-or-self χ def = µZ.χ ∨ µY. 1 (Y ∨ Z) ∨ 2 Y A → ancestor χ def = 1 µZ.χ ∨ 1 Z ∨ 2 Z A → anc-or-self χ def = µZ.χ ∨ 1 µY.Z ∨ 2 Y A → following χ def = A → desc-or-self η1 A → preceding χ def = A → desc-or-self η2 η 1 def = A → foll-sibling A → anc-or-self χ η 2 def = A → prec-sibling A → anc-or-self χ
INRIA E → • • : L XPath → L µ → L µ E → /p χ def = P → p ((µZ.¬ 1 ∨ 2 Z)∧(µY.χ∧ ∨ 1 Y ∨ 2 Y )) E → p χ def = P → p (χ∧ ) E → e 1 e 2 χ def = E → e 1 χ ∨ E → e 2 χ E → e 1 ∩ e 2 χ def = E → e 1 χ ∧ E → e 2 χ P → • • : Path → L µ → L µ P → p 1 /p 2 χ def = P → p 2 (P → p1 χ ) P → p[q] χ def = P → p χ ∧ Q ← q P → a::σ χ def = σ ∧ A → a χ P → a:: * χ def = A → a χ
a ∧ (µX. ˙1¸( χ ∧ ) ∨ ˙2¸X ) | {z } ϕ ∧ 1 µY.b ∨ 2 Y | {z } ψ χ a ϕ
Q ← • • : Qualif → L µ → L µ Q ← q 1 and q 2 χ def = Q ← q 1 χ ∧ Q ← q 2 χ Q ← q 1 or q 2 χ def = Q ← q 1 χ ∨ Q ← q 2 χ Q ← not q χ def = ¬ Q ← q χ Q ← p χ def = P ← p χ P ← • • : Path → L µ → L µ P ← p 1 /p 2 χ def = P ← p 1 (P ← p2 χ ) P ← p[q] χ def = P ← p (χ∧Q ← q ) P ← a::σ χ def = A ← a (χ∧σ) P ← a:: * χ def = A ← a χ A ← • • : Axis → L µ → L µ A ← a χ def = A → symmetric(a) χ
XPath translation is based on these two translating "modes", the first one being used for paths and the second one for qualifiers. Whenever the "filtering" mode is entered, it will never be left.

The translation of paths inside qualifiers is also given in Figure 10. It uses the translation for axes and is based on XPath symmetry: symmetric(a) denotes the symmetric XPath axis corresponding to the axis a (for instance symmetric(child) = parent).

We may now state that our translation is correct, by relating the interpretation of an XPath formula applied to some set of trees to the interpretation of its translation, by stating that the translation of a formula is cycle-free, and by giving a bound in the size of this translation. We restrict the sets of trees to which an XPath formula may be applied to those that may be denoted by an L µ formula. This restriction will be justified in Section 5.2 where we show that every regular tree language may be translated to an L µ formula. Proof: The proof uses a structural induction that "peels off" the compositional layers of each set of rules over focused trees. The cycle-free part follows from the fact that translated fixpoint formulas are closed and there is no nesting of modalities with converse programs between a fixpoint variable and its binder. Each XPath navigation step is cycle-free, and their composition yields a proper nesting of fixpoint formulas which is also cycle-free. Figure 11 illustrates this on an typical example. Finally, formal translations do not duplicate any subformula of arbitrary length.

Embedding Regular Tree Languages

Several formalisms exist for describing types of XML documents (e.g. DTD, XML Schema, Relax NG). In this paper we embed regular tree languages, which gather all of them [START_REF] Murata | Taxonomy of XML schema languages using formal language theory[END_REF] into L µ . We rely on a straightforward isomorphism between unranked regular tree types and binary regular tree types [START_REF] Hosoya | Regular expression types for XML[END_REF]. Assuming a countably infinite set of type variables ranged over by X, binary regular tree type expressions are defined as follows: We refer the reader to [START_REF] Hosoya | Regular expression types for XML[END_REF] for the denotational semantics of regular tree languages, and directly introduce their translation into L µ :

L BT T ::= tree type expression ∅ empty set | leaf | T 1 T 2 union | σ(X 1 , X 2 ) label | let X i .T i in
• : L BT → L µ T def = σ ∧ ¬σ for T = ∅, T 1 T 2 def = T 1 ∨ T 2 σ(X 1 , X 2 ) def = σ ∧ succ 1 (X 1 ) ∧ succ 2 (X 2 ) let X i .T i in T def = µX i = T i in T
where we use the formula σ ∧ ¬σ as "false", and the function succ • (•) takes care of setting the type frontier:

succ α (X) =    ¬ α if X is bound to ¬ α ∨ α X if nullable(X) α X if not nullable(X)
according to the predicate nullable(X) which indicates whether the type T = bound to X contains the empty tree. For example, Figure 14 gives the translation of a DTD fragment of the Wikipedia encyclopedia [START_REF] Voss | Wikipedia dtd[END_REF] shown on Figure 12. The intermediate binary tree type encoding of the DTD is shown on Figure 13.

Note that the translation of a regular tree type uses only downward modalities since it describes the allowed subtrees at a given context. No additional restriction is imposed on the context from which the type definition starts. In particular, navigation is allowed in the upward direction so that we can support type constraints for which we have only partial knowledge in a given direction. However, when we know the position of the root, conditions similar to those of absolute paths are added in the form of additional formulas describing the INRIA position that need to be satisfied. This is particularly useful when a regular type is used by an XPath expression that starts its navigation at the root (/p) since the path will not go above the root of the type (by adding the restriction µZ.¬ 1 ∨ 2 Z). On the other hand, if the type is compared with another type (typically to check inclusion of the result of an XPath expression in this type), then there is no restriction as to where the root of the type is (our translation does not impose the chosen node to be at the root). This is particularly useful since an XPath expression usually returns a set of nodes deep in the tree which we may compare to this partially defined type.

We are considering as future work a modification of the translation of types such that it imposes the context of a type to also follow the regular tree language definition (stating for instance that the parent of a given node may only be some specific other nodes).

Satisfiability-Testing Algorithm

In this section we present our algorithm, show that it is sound and complete, and prove a time complexity boundary. To check a formula ϕ, our algorithm builds satisfiable formulas out of some subformulas (and their negation) of ϕ, then checks whether ϕ was produced. We first describe how to extract the subformulas from ϕ.

Preliminary Definitions

For ϕ = (µX i = ϕ i in ψ) we define exp(ϕ) def = ψ{ µXi=ϕi in Xi / Xi } which denotes the formula ψ in which every occurrence of a X i is replaced by (µX i = ϕ i in X i ).

We define the Fisher-Ladner closure cl(ψ) of a formula ψ as the set of all subformulas of ψ where fixpoint formulas are additionally unwound once. Specifically, we define the relation → e ⊆ L µ × L µ as the least relation that satisfies the following:

• ϕ 1 ∧ ϕ 2 → e ϕ 1 , ϕ 1 ∧ ϕ 2 → e ϕ 2 • ϕ 1 ∨ ϕ 2 → e ϕ 1 , ϕ 1 ∨ ϕ 2 → e ϕ 2 • a ϕ → e ϕ • µX i = ϕ i in ψ → e exp(µX i = ϕ i in ψ)
The closure cl(ψ) is the smallest set S that contains ψ and closed under the relation → e , i.e. if ϕ 1 ∈ S and ϕ 1 → e ϕ 2 then ϕ 2 ∈ S.

We call Σ(ψ) the set of atomic propositions σ used in ψ along with another name, σ x , that does not occur in ψ to represent atomic propositions not occurring in ψ.

We define cl * (ψ) = cl(ψ) ∪ {¬ϕ | ϕ ∈ cl(ψ)}. Every formula ϕ ∈ cl * (ψ) can be seen as a boolean combination of formulas of a set called the Lean of ψ, inspired from [START_REF] Pan | BDD-based decision procedures for the modal logic K[END_REF]. We note this set Lean(ψ) and define it as follows:

Lean(ψ) = a | a ∈ {1, 2, 1, 2} ∪ Σ(ψ) ∪ { } ∪ { a ϕ | a ϕ ∈ cl(ψ)} INRIA . ∈ t =⇒ (∅, ∅) ϕ ∈ Lean(ψ) ϕ ∈ t ϕ . ∈ t =⇒ ({ϕ}, ∅) ϕ 1 . ∈ t =⇒ (T 1 , F 1 ) ϕ 2 . ∈ t =⇒ (T 2 , F 2 ) ϕ 1 ∧ ϕ 2 . ∈ t =⇒ (T 1 ∪ T 2 , F 1 ∪ F 2 ) ϕ 1 . ∈ t =⇒ (T 1 , F 1 )
ϕ 1 ∨ ϕ 2 . ∈ t =⇒ (T 1 , F 1 ) ϕ 2 . ∈ t =⇒ (T 2 , F 2 ) ϕ 1 ∨ ϕ 2 . ∈ t =⇒ (T 2 , F 2 ) ϕ . / ∈ t =⇒ (T, F ) ¬ϕ . ∈ t =⇒ (T, F ) exp(µX i = ϕ i in ψ)
.

∈ t =⇒ (T, F )

µX i = ϕ i in ψ . ∈ t =⇒ (T, F ) ϕ ∈ Lean(ψ) ϕ ∈ t ϕ . / ∈ t =⇒ (∅, {ϕ}) ϕ 1 . / ∈ t =⇒ (T 1 , F 1 ) ϕ 2 . / ∈ t =⇒ (T 2 , F 2 ) ϕ 1 ∨ ϕ 2 . / ∈ t =⇒ (T 1 ∪ T 2 , F 1 ∪ F 2 ) ϕ 1 . / ∈ t =⇒ (T 1 , F 1 )
ϕ 1 ∧ ϕ 2 . / ∈ t =⇒ (T 1 , F 1 ) ϕ 2 . / ∈ t =⇒ (T 2 , F 2 ) ϕ 1 ∧ ϕ 2 . / ∈ t =⇒ (T 2 , F 2 ) ϕ . ∈ t =⇒ (T, F ) ¬ϕ . / ∈ t =⇒ (T, F ) exp(µX i = ϕ i in ψ) . / ∈ t =⇒ (T, F ) µX i = ϕ i in ψ . / ∈ t =⇒ (T, F )
Figure 15: Truth assignment of a formula A ψ-type (or simply a "type") (Hintikka set in the temporal logic literature) is a set t ⊆ Lean(ψ) such that:

• ∀ a ϕ ∈ Lean(ψ), a ϕ ∈ t ⇒ a ∈ t (modal consistency); • 1 / ∈ t∨ 2 /
∈ t (a tree node cannot be both a first child and a second child);

• exactly one atomic proposition σ ∈ t (XML labeling); we use the function σ(t) to return the atomic proposition of a type t;

• may belong to t.

We call Types(ψ) the set of ψ-types. For a ψ-type t, the complement of t is the set Lean(ψ) \ t.

A type determines a truth assignment of every formula in cl * (ψ) with the relation . ∈ defined in Figure 15. Note that such derivations are finite because the number of naked µX i = ϕ i in ψ (that do not occur under modalities) strictly decreases after each expansion.

We often write ϕ .

∈ t if there are some T, F such that ϕ .

∈ t =⇒ (T, F ). We say that a formula ϕ is true at a type t iff ϕ .

∈ t.

We now relate a formula to the truth assignment of its ψ-types. ∈ t =⇒ (T, F ), then we have T ⊆ t, F ⊆ Lean(ϕ) \ t, and ψ∈T ψ ∧ ψ∈F ¬ψ implies ϕ (every tree in the interpretation of the first formula is in the interpretation of the second). If ϕ . / ∈ t =⇒ (T, F ), then we have T ⊆ t, F ⊆ Lean(ϕ) \ t, and ψ∈T ψ ∧ ψ∈F ¬ψ implies ¬ϕ.

Upd(X) def = X ∪    (t, w 1 (t, X • ), w 2 (t, X • )) | / ∈ t ⊆ Types(ψ) ∧ 1 ∈ t ⇒ w 1 (t, X • ) = ∅ ∧ 2 ∈ t ⇒ w 2 (t, X • ) = ∅    ∪    (t, w 1 (t, X • ), w 2 (t, X • )) | ∈ t ⊆ Types(ψ) ∧ 1 ∈ t ⇒ w 1 (t, X • ) = ∅ ∧ 2 ∈ t ⇒ w 2 (t, X • ) = ∅    ∪    (t, w 1 (t, X ), w 2 (t, X • )) | / ∈ t ⊆ Types(ψ) ∧ 1 ∈ t ⇒ w 1 (t, X ) = ∅ ∧ 2 ∈ t ⇒ w 2 (t, X • ) = ∅    ∪    (t, w 1 (t, X • ), w 2 (t, X )) | / ∈ t ⊆ Types(ψ) ∧ 1 ∈ t ⇒ w 1 (t, X • ) = ∅ ∧ 2 ∈ t ⇒ w 2 (t, X ) = ∅    w a (t, X) def = {type(x) | x ∈ X ∧ a ∈ type(x) ∧ ∆ a (t, type(x))} type((t, w 1 , w 2 )) def = t FinalCheck(ψ, X) def = ∃x ∈ X, dsat(x, ψ) ∧ ∀a ∈ {1, 2}, a / ∈ type(x) dsat((t, w 1 , w 2 ), ψ) def = ψ . ∈ t ∨ ∃x , dsat(x , ψ) ∧ (x ∈ w 1 ∨ x ∈ w 2 ) X def = x ∈ X | x = ( , , )
X • def = {x ∈ X | x = ( , , )}
Proof: Immediate by induction on the derivations.

We next define a compatibility relation between types to state that two types are related according to a modality. Definition 6.2 (Compatibility relation) Two types t and t are compatible under a ∈ {1, 2}, written ∆ a (t, t ), iff

∀ a ϕ ∈ Lean(ψ), a ϕ ∈ t ⇔ ϕ . ∈ t ∀ a ϕ ∈ Lean(ψ), a ϕ ∈ t ⇔ ϕ . ∈ t

The Algorithm

The algorithm works on sets of triples of the form (t, w 1 , w 2 ) where t is a type, and w 1 and w 2 are sets of types which represent every witness for t according to relations ∆ 1 (t, •) and ∆ 2 (t, •).

The algorithm proceeds in a bottom-up approach, repeatedly adding new triples until a satisfying model is found (i.e. a triple whose first component is a type implying the formula), or until no more triple can be added. Each iteration of the algorithm builds types representing deeper trees (in the 1 and 2 direction) with pending backward modalities that will be fulfilled at later iterations. Types with no backward modalities are satisfiable, and if such a type implies the formula being tested, then it is satisfiable. The main iteration is as follows:

INRIA T 3 | | | T 2 | | | T 1 | | |
X ← ∅ repeat X ← X X ← Upd(X ) if FinalCheck(ψ, X) then return "ψ is satisfiable" until X = X return "ψ is unsatisfiable"
where X ⊆ Types(ψ)×2 Types(ψ) ×2 Types(ψ) and the update operation Upd(•) and success check operation FinalCheck(•, •) are defined on Figure 16. The update operation requires four almost identical cases to ensure that the optional mark remains unique. The first case corresponds to the absence of the mark, the second case to the present of the mark at the top level, the third case to the presence of the mark deeper in the first child, and the last case to the presence of the mark deeper in the second child.

At each step of the algorithm, FinalCheck(•, •) verifies whether the tested formula is implied by newly added types without pending (unproved) backward modalities, so that the algorithm may terminate as soon as a satisfying tree is found.

We note X i the set of triples and T i the set of types after i iterations:

T i = type(x) | x ∈ X i . Note that T i+1
is the set of types for which at least one witness belongs to T i .

Example Run of the Algorithm

In a sense, the algorithm performs a kind of progressive bottom-up reasoning while ensuring partial (forward) satisfiability of subformulas, as illustrated by Figure 17.

More specifically, Figure 18 illustrates a run of the algorithm for checking whether the XPath query child::c/preceding-sibling::a[b] is contained in the XPath query child::c[b]. These expressions are first compiled into the logic as explained in section 5.1. For the second translation, the final focus of the tree is a node named c. As we reach it going through a "child" step, formula θ ensures that the parent node is the starting node. Finally, from the final focus of the tree, formula η tests that a child named b is present. As concerns the first formula, the final focus of the tree is on a node named a. We get there by a "preceding-sibling" step from a c node, hence we need to make sure that there is a following sibling named c (this is the recursion on Y). Once this c node has been found, it must be made sure that it was reached by a "child" step from the start of the query, using the same formula θ as before. Finally, going back to the final focus in the tree, we need to check there is a child named b, using again the formula η. Note that the start mark is crucial in this containment case: it ensures that when both formulas are combined, the XPath expressions start from the same context.

From the formulas ϕ 1 and ϕ 2 corresponding to each XPath query, we build a containment formula ψ = ϕ 1 ∧ ¬ϕ 2 (the negated implication). If this formula is unsatisfiable, then the first XPath expression is contained in the second one. Lean(ψ) is then computed, and the fixpoint computation starts: the set of types T 1 contains all possible leaves. Each type added in T i (i ≥ 2) requires at least one witness type found in T i-1 (else it would have been added at some previous step j < i). In this example, a satisfying binary tree of depth 3 is found (as shown on Figure 18), therefore the algorithm stops just after computing T 3 . The first XPath query is not contained in the second one: a counter-example tree is provided to the user (see Figure 18).

Correctness and Complexity

In this section we prove the correctness of the satisfiability testing algorithm, and show that its time complexity is 2 O(|Lean(ψ)|) . Theorem 6.3 (Correctness) The algorithm decides satisfiability of L µ formulas over finite focused trees.

Termination For ψ ∈ L µ , since cl(ψ) is a finite set, Lean(ψ) and 2 Lean(ψ) are also finite. Furthermore, Upd(•) is monotonic and each X i is included in the finite set Types(ψ) × 2 Types(ψ) × 2 Types(ψ) , therefore the algorithm terminates. To finish the proof, it thus suffices to prove soundness and completeness.

Preliminary Definitions for Soundness First, we introduce a notion of partial satisfiability for a formula, where backward modalities are only checked up to a given level. A formula ϕ is partially satisfied iff ϕ 0 V = ∅ as defined in Figure 19.

For a type t, we note ϕ c (t) its most constrained formula, where atoms are taken from Lean(ψ). In the following, • stands for if ∈ t, and for ¬ otherwise.

ϕ c (t) = σ(t) ∧ σ∈Σ,σ / ∈t ¬σ ∧ • ∧ a ϕ∈t a ϕ ∧ a ϕ / ∈t ¬ a ϕ
We now introduce a notion of paths, written ρ which are concatenations of modalities: the empty path is written , and path concatenation is written ρa. Lean(ψ) : Every path may be given a depth:

INRIA 1 η a ∧ ˙1¸ b c T 3 | | | T 2 | | | T 1 | | |
1 2 ˙1¸ ˙2¸ a b c σ 2 c ˙1¸ ... 2 η | {z } topological propositions | {z } atomic propositions in ψ | {z } existential formulas in cl(ψ) ψ = ϕ1 ∧ ¬ϕ2 ϕ1 = E → e1 = a ∧ (µY. 2 (c ∧ θ) ∨ 2 Y ) ∧ 1 η ϕ2 = E → e2 = c ∧ µX. ˙1¸ ∨ ˙2¸X | {z } θ ∧ 1 µZ.b ∨ 2 Z | {z }
e 1 ? ⊆ e 2 . n V def = F X n V def = V (X) ϕ ∨ ψ n V def = ϕ n V ∪ ψ n V p n V def = {f | nm(f ) = p} ϕ ∧ ψ n V def = ϕ n V ∩ ψ n V ¬p n V def = {f | nm(f ) = p} 1 ϕ 0 V def = F n V def = f | f = (σ [tl ], c) 2 ϕ 0 V def = F ¬ n V def = {f | f = (σ[tl ], c)} 1 ϕ n>0 V def = f 1 | f ∈ ϕ n-1 V ∧ f 1 defined 2 ϕ n>0 V def = f 2 | f ∈ ϕ n-1 V ∧ f 2 defined 1 ϕ n V def = f 1 | f ∈ ϕ n+1 V ∧ f 1 defined 2 ϕ n V def = f 2 | f ∈ ϕ n+1 V ∧ f 2 defined ¬ a n V def = {f | f a undefined} µX i = ϕ i in ψ n V def = let T i = T i ⊆ F | ϕ i n V [Ti/Xi] ⊆ T i i in ψ n V [Ti/Xi]
depth( ) def = 0 depth(ρa) def = depth(ρ) + 1 if a ∈ {1, 2} depth(ρa) def = depth(ρ) -1 if a ∈ {1, 2}
A forward path is a path that only mentions forward modalities.

We define a tree of types T as a tree whose nodes are types, T (•) = t, with at most two children, T 1 and T 2 . The navigation in trees of types is trivially extended to forward paths. A tree of types is consistent iff for every forward path ρ and for every child a of T ρ , we have T ρ (•) = t, T ρa (•) = t implies a ∈ t, a ∈ t , and ∆ a (t, t ). Given a consistent tree of types T , we now define a dependency graph whose nodes are pairs of a forward path ρ and a formula in t = T ρ (•) or the negation of a formula in the complement of t. The directed edges of the graph are labeled with modalities consistent with the tree. This graph corresponds to what the algorithm ultimately builds, as every iteration discovers longer forward paths. For every (ρ, ϕ) in the nodes we build the following edges:

• ϕ ∈ Σ(ψ) ∪ ¬Σ(ψ) ∪ { , ¬ , a , ¬ a }: no edge • ρ = and ϕ = a ϕ with a ∈ {1, 2}: no edge • ρ = ρ a and ϕ = a ϕ : let t = T ρ (•).
We first consider the case where a ∈ {1, 2} and let t = T ρa (•). As T is consistent, we have ϕ . ∈ t hence there are T, F such that ϕ . ∈ t =⇒ (T, F ) with T a subset of t , and F a subset of the complement of t . For every ϕ T ∈ T we add an edge a to (ρa , ϕ T ), and for every ϕ F ∈ F we add an edge a to (ρa , ¬ϕ F ).

We now consider the case where a ∈ {1, 2} and first show that we have a = a. As T is consistent, we have a in t. Moreover, as t is a tree type, it must contain a . As a is a backward modality, it must be equal to a as at most one may be present. Hence we have ρ aa = ρ and we let t = T ρ (•). By consistency, we have ϕ . ∈ t , hence ϕ . ∈ t =⇒ (T, F ) and we add edges as in the previous case: to (ρ , ϕ T ) and to (ρ , ¬ϕ F ).

• ρ = ρ a and ϕ = ¬ a ϕ : let t = T ρ (•). If a is not in t then no edge is added. Otherwise, we proceed as in the previous case. For downward modalities, we let t = T ρa (•) and we compute ϕ . / ∈ t =⇒ (T, F ), which we know to hold by consistency. We then add edges to (ρa , ϕ T ) and to (ρa , ¬ϕ F ) as before. For upward modalities, as we have a in t, we must have a = a and we let t = T ρ (•). We compute ϕ . / ∈ t =⇒ (T, F ) and we add the edges to (ρ , ϕ T ) and to (ρ , ¬ϕ F ) as before. Lemma 6.4 The dependency graph of a consistent tree of types of a cycle-free formula is cycle free.

Proof: The proof proceeds by induction on the depth of the cycle, relying on the fact that the dependency graph is consistent with the tree structure (i.e. if a 1 edge reaches a node, no 2 edge may leave this node). The induction case is INRIA trivial: if there is a cycle of depth n, there must be a cycle of depth n -1, a contradiction.

The base case is for a cycle of depth 1. We describe one case, where the cycle is (ρ, 1 ϕ) -→ 1 (ρ1, 1 ψ) -→ 1 (ρ, 1 ϕ). As ϕ must be a subformula of ψ and ψ a subformula of ϕ, they are both recursive formula. An analysis of the shape of ϕ, based on the derivations ϕ . ∈ t =⇒ (T, F ) and ψ . ∈ t =⇒ (T , F ) with 1 ψ ∈ T and 1 ϕ ∈ T then shows that ϕ is not a cycle-free formula, a contradiction. Lemma 6.5 (Soundness) Let T be the result set of the algorithm. For any type t ∈ T and any ϕ such that ϕ . ∈ t, then ϕ 0 ∅ = ∅.

Proof:

The proof proceeds by induction on the number of steps of the algorithm. For every t in T n and every witness tree T rooted at t built from X n , we show that T is a consistent tree type and we build a focused tree f that is rooted (i.e. of the shape (σ • [tl ], ( , Top, tl ))). The tree f is in the partial interpretation of ϕ c (t):

f ρ ∈ ϕ c (T ρ (•)) depth(ρ) ∅
for any path ρ whose depth is 0 or more, and f contains the start mark only if occurs in T . We then show that for all ϕ . ∈ t, we have f ∈ ϕ 0 ∅ . The base case is trivial by the shape of t: it may only contain backward modalities (trivially satisfied at level 0), one atomic proposition, and one start proposition. Moreover there is only one tree of witnesses to consider, the tree whose only node is t. If the atomic proposition is σ, then the focused tree returned is either (σ [ ], ( , Top, )) or (σ[ ], ( , Top, )) depending on the start proposition.

In the inductive case, we consider every witness types for both downward modalities, t 1 and t 2 . For each of them, we consider every tree type T 1 and T 2 and build a tree type rooted at t which is consistent by definition of the algorithm. By induction, we have f 1 and

f 2 such that f 1 ρ ∈ ϕ c (T 1ρ (•)) depth(ρ) ∅ and f 2 ρ ∈ ϕ c (T 2ρ (•)) depth(ρ) ∅
for any path ρ whose depth is 0 or more. If either T 1 or T 2 contains , then f 1 or f 2 contains the start mark by induction. Moreover, by definition of the algorithm, it is the case for only one of them and is not in t.

Let f 1 be (σ • 1 [tl 1 ], ( , Top, tr 1 )) and f 2 be (σ • 2 [tl 2 ], ( , Top, tr 2 )). Let f = (σ(t) • [σ • 1 [tl 1 ] :: tr 1 ], ( , Top, σ • 2 [tl 2 ] :: tr 2 )) where σ(t) • is σ(t) if ∈ t, and σ(t) otherwise. Note that f contains exactly one start mark iff ∈ T . We next show that f 1 ρ ∈ ϕ c (T 1ρ (•)) depth(ρ) ∅ implies f 1ρ ∈ ϕ c (T 1ρ (•)) depth(ρ) ∅
, and the same for the other modality, by induction on the depth of the path, remarking that every backward modality at level 0 is trivially satisfied.

We then proceed to show that f satisfies ϕ c (t) at level 0. To do so, we need a further induction on the dependency tree. Let ρ be a path of the dependency tree and ψ be a formula at that path in the dependency tree, we show that f ρ ∈ ψ depth(ρ) V . To do so, we rely on f ρ ∈ ψ

depth(ρ)-1 V if depth(ρ) = 0.
In the base case at depth 0, the result is by construction as the formula is either a backward modality or an atomic formula. In the base case at another depth, the case is immediate by induction as the formula has to be an atomic formula whose interpretation does not depend on the depth. In the induction case, we conclude by the inductive hypothesis and by definition of partial satisfiability. We conclude the proof by noticing that the final selected type has no backward modality, hence ϕ c (t

f ρ nm(f ) = σ f ρ σ nm(f ) = σ f ρ ¬σ (σ [tl ], c) ρ (σ[tl ], c) ρ ¬ f ρ ϕ f ρ ϕ ∨ ψ f ρ ψ f ρ ϕ ∨ ψ f ρ ϕ f ρ ψ f ρ ϕ ∧ ψ f 1 ρ1 ϕ f ρ 1 ϕ f 2 ρ2 ϕ f ρ 2 ϕ f 1 ρ1 ϕ f ρ 1 ϕ f 2 ρ2 ϕ f ρ 2 ϕ f a undefined f ρ ¬ a f ρ exp(µX i = ϕ i in ψ) f ρ µX i = ϕ i in ψ
) ∅ 0 = ϕ c (t) ∅ .
Lemma 6.6 (Completeness) For a cycle-free closed formula ϕ ∈ L µ , if ϕ ∅ = ∅ then the algorithm terminates with a set of triples X such that FinalCheck(ϕ, X).

Proof: Let f ∈ ϕ ∅ be a smallest focused tree validating the formula such that the names occurring in f are either also occurring in ϕ or are a single other name σ x . By Lemma 4.2, there is a finite unfolding of ϕ such that f belongs to its interpretation. Hence there is a finite satisfiability derivation, defined in Figure 20, of f ϕ. In the satisfiability derivation, we assume the paths are normalized (11 = ). Hence every path is a concatenation of a (possibly empty) backward path ρ b followed by a forward path ρ f . This derivation has the following property, immediate by induction: let f the initial focused tree, then

f ρ ϕ implies f = f ρ . Hence if f 1 ρ ϕ 1 and f 2 ρ ϕ 2 , then f 1 = f 2 .
We next use the satisfiability derivation to construct a run of the algorithm that concludes that ϕ is satisfiable. We first associate each path to a type, which we then saturate (adding formulas that are true even though the satisfiability relation does not mention them at that path). We next show that every formula at a path in the satisfiability relation is implied by the type at that path, and that types are consistent according to the ∆ a (t, t ) relation. We then conclude that the types are created by a run of the algorithm by induction on the paths.

More precisely, we first describe how we build t ρ . Let Φ ρ the set of formulas at path ρ. We first add every formula of Φ ρ that is in Lean(ϕ), then we complete this set to yield a correct type: if a ψ ∈ Φ ρ then we add a ; for every modality a for which f a is defined we add a ; if there is no atomic proposition in Φ ρ then we add nm(f ρ ); finally if f ρ has the start mark we add .

We next saturate the types. For every path t ρ if t ρa exists, if a ψ ∈ Lean(ϕ), and if ψ . ∈ t ρa then we add a ψ to t ρ . This procedure is repeated until it does INRIA not change any type. Termination is a consequence of the finite size of the lean and of the number of paths. The resulting types are satisfiable as they are before saturation (since a focused tree satisfies them) and each formula added during saturation is first checked to be implied by the type.

We next show (*): for any given path ρ, if ϕ ρ ∈ Φ ρ then ϕ ρ .

∈ t ρ , by induction on the satisfiability derivation. Base cases with no negation are immediate by definition of t ρ as these are formulas of the lean. For base cases with negation, we rely on the fact that f ρ satisfies the formula, hence we cannot for instance have σ and ¬σ in Φ ρ . If ¬ a ∈ Φ ρ then we cannot also have a ψ ∈ Φ ρ as ρa is not a valid path, hence a is not in t ρ thus ¬ a .

∈ t ρ . The inductive cases of this induction (disjunction, conjunction, recursion) are immediate as they correspond to the definition of • .

∈ •.

We next show that for every type t ρ and t ρa where a is a forward modality, we have a ∈ t ρa and ∆ a (t ρ , t ρa ). (Note that, by path normalization, the types considered may be t 12 and t 1 for modality 2.) The first condition is immediate by construction of t ρa as f ρa is defined. For the second condition, let a ψ ∈ t ρ . If a ψ ∈ Φ ρ , then it occurs in the satisfiability derivation with an hypothesis f ρa ρa ψ. In this case we have ψ .

∈ t ρa by (*). If a ψ /

∈ Φ ρ then it was added during saturation and the result is immediate by construction. Conversely, if ψ . ∈ t ρa then by saturation we have a ψ ∈ t ρ . We now consider the case a ψ ∈ t ρa . The proof goes exactly as before, distinguishing the case where the formula is in Φ ρa and the case where it was added by saturation.

We now show that there is a run of the algorithm that produces these types. We proceed by induction on the paths in the downward direction: if t ρa has been proven for a partial run for a ∈ {1, 2}, then t ρ is proven for the next step of the algorithm. Moreover, we show that (t ρ , {t ρ1 }, {t ρ2 }) is marked iff a forward subtree of f ρ contains the start mark. The base case is for paths with no descendants, hence no witness is required. The algorithm then adds (t ρ , ∅, ∅) to its set of types, with a mark iff ∈ t ρ , iff f ρ is marked. We now consider the inductive case. By induction, a partial run of the algorithm returns t ρ1 and/or t ρ2 . We first show that t ρ is returned in the next step of the algorithm, taking these two types as witnesses. We first remark that if either witness is marked then the other is not and the mark is not at f ρ , since there is only one start mark in f , and if the mark is at f ρ , then neither witness is marked. For each child a ∈ {1, 2} we have ∆ a (t ρ , t ρa ) and a ∈ t ρa , hence the triple (t ρ , W 1 , W 2 ) with t ρ1 ∈ W 1 and t ρ2 ∈ W 2 is added by the algorithm.

We may now conclude. At the end of the induction, the last path considered, ρ 0 , has no predecessor, hence it is the longest backward only path. Since f ρ 0 is the root of the tree, we have 1 / ∈ t ρ0 and 2 / ∈ t ρ0 . Moreover, as the start mark is somewhere in f , it is in a forward subtree of f ρ 0 , hence the final type is marked. Finally, t is in the witness tree of the final type, and since f ϕ, we have ϕ .

∈ t . Proof: |Types(ψ)| is bounded by 2 Lean(ψ) which is 2 O(n) . During each iteration, the algorithm adds at least one new type (otherwise it terminates), thus

RR n°6590

it performs at most 2 O(n) iterations. We now detail what it does at each iteration. For each type that may be added (there are 2 O(n) of them), there are two traversals of the set of types at the previous step to collect witnesses. Hence there are 2 n) witness tests at each iteration. Each witness test involves a membership test and a ∆ a test. In the implementation these are precomputed: for every formula a ϕ in the lean, the subsets (T, F ) of the lean that must be true and false respectively for ϕ to be true are precomputed, so testing ϕ .

* 2 O(n) * 2 O(n) = 2 O(
∈ t are simple inclusion and disjunction tests. The FinalCheck condition test at most 2 O(n) ψ-types and each test takes at most 2 O(n) (testing the formulas containing against ψ). Therefore, the worst case global time complexity of the algorithm does not exceed 2 O(n) .

Implementation Techniques

This section describes the main techniques used for implementing an effective L µ decision procedure. More details along with an implementation can be found at [START_REF] Genevès | A satisfiability solver for XML and XPath[END_REF].

Implicit Representation of Sets of ψ-Types

Our implementation relies on a symbolic representation and manipulation of sets of ψ-types using Binary Decision Diagrams (BDDs) [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF]. BDDs provide a canonical representation of boolean functions. Experience has shown that this representation is very compact for very large boolean functions. Their effectiveness is notably well known in the area of formal verification of systems [START_REF] Clarke | Model checking[END_REF].

First, we observe that the implementation can avoid keeping track of every possible witnesses of each ψ-type. In fact, for a formula ϕ, we can test ϕ ∅ = ∅ by testing the satisfiability of the (linear-size) "plunging" formula ψ = µX.ϕ ∨ 1 X ∨ 2 X at the root of focused trees. That is, checking ψ 0 ∅ = ∅ while ensuring there is no unfulfilled upward eventuality at top level 0. One advantage of proceeding this way is that the implementation only need to deal with a current set of ψ-types at each step.

We now introduce a bit-vector representation of ψ-types. Types are complete in the sense that either a subformula or its negation must belong to a type. It is thus possible for a formula ϕ ∈ Lean(ψ) to be represented using a single BDD variable. For Lean(ψ) = {ϕ 1 , ..., ϕ m }, we represent a subset t ⊆ Lean(ψ) by a vector t = t 1 , ..., t m ∈ {0, 1} m such that ϕ i ∈ t iff t i = 1. A BDD with m variables is then used to represent a set of such bit vectors.

We define auxiliary predicates for programs a ∈ {1, 2}:

• isparent a ( t) is read " t is a parent for program a" and is true iff the bit for a is true in t

• ischild a ( t) is read " t is a child for program a" and is true iff the bit for a is true in t

For a set T ⊆ 2 Lean(ψ) , we note χ T its corresponding characteristic function. Encoding χ Types(ψ) is straightforward with the previous definitions. We define the equivalent of . ∈ on the bit vector representation:

status ϕ ( t) def =            t i if ϕ ∈ Lean(ψ) status ϕ ( t) ∧ status ϕ ( t) if ϕ = ϕ ∧ ϕ status ϕ ( t) ∨ status ϕ ( t) if ϕ = ϕ ∨ ϕ ¬status ϕ ( t) if ϕ = ¬ϕ status exp(ϕ) ( t) if ϕ = µX i = ϕ i in ψ
We note a → b the implication and a ↔ b the equivalence of two boolean formulas a and b over vector bits. We can now construct the BDD of the relation ∆ a for a ∈ {1, 2}. This BDD relates all pairs ( x, y) that are consistent w.r.t the program a, i.e., such that y supports all of x's a ϕ formulas, and vice-versa x supports all of y's a ϕ formulas:

∆ a ( x, y) def = 1≤i≤m    x i ↔ status ϕ ( y) if ϕ i = a ϕ y i ↔ status ϕ ( x) if ϕ i = a ϕ otherwise
For a ∈ {1, 2}, we define the set of witnessed vectors:

χ Wita(T ) ( x) def = isparent a ( x) → ∃ y [ h( y) ∧ ∆ a ( x, y) ]
where h( y) = χ T ( y) ∧ ischild a ( y).

Then, the BDD of the fixpoint computation is initially set to the false constant, and the main function Upd(•) is implemented as:

χ Upd(T ) ( x) def = χ T ( x) ∨   χ Types(ψ) ( x) ∧ a∈{1,2} χ Wita(T ) ( x)  
Finally, the solver is implemented as iterations over the sets χ Upd(T ) until a fixpoint is reached. The final satisfiability condition consists in checking whether ψ is present in a ψ-type of this fixpoint with no unfulfilled upward eventuality:

∃ t   χ T ( t) ∧ a∈{1,2} ¬ischild a ( t) ∧ status ψ ( t)  

Satisfying Model Reconstruction

The implementation keeps a copy of each intermediate set of types computed by the algorithm, so that whenever a formula is satisfiable, a minimal satisfying model can be extracted. The top-down (re)construction of a satisfying model starts from a root (a ψ-type for which the final satisfiability condition holds), and repeatedly attempts to find successors. In order to minimize model size, only required left and right branches are built. Furthermore, for minimizing the maximal depth of the model, left and right successors of a node are successively searched in the intermediate sets of types, in the order they were computed by the algorithm. For readability purposes, the extracted satisfying model can be enriched by annotating the start mark from which XPath evaluation started and a target node selected by the XPath expression. The annotated model is then provided to the user in XML unranked tree syntax.

Conjunctive Partitioning and Early Quantification

The BDD-based implementation involves computations of relational products of the form:

∃ y [ h( y) ∧ ∆ a ( x, y) ] (1)
It is well-known that such a computation may be quite time and space consuming, because the BDD corresponding to the relation ∆ a may be quite large.

One famous optimization technique is conjunctive partitioning [START_REF] Clarke | Model checking[END_REF] combined with early quantification [START_REF] Pan | BDD-based decision procedures for the modal logic K[END_REF]. The idea is to compute the relational product without ever building the full BDD of the relation ∆ a . This is possible by taking advantage of the form of ∆ a along with properties of existential quantification. By definition, ∆ a is a conjunction of n equivalences relating x and y where n is the number of b ϕ formulas in Lean(ψ) where ϕ = and b ∈ {a, a}:

∆ a ( x, y) = n i=1 R i ( x, y)
If a variable y k does not occur in the clauses R i+1 , ..., R n then the relational product (1) can be rewritten as:

∃ ∃y k h( y) ∧ 1≤j≤i R j ( x, y) ∧ i+1≤l≤n R l ( x, y) y1, ..., y k-1 , y k+1 , ..., ym
This allows to apply existential quantification on intermediate BDDs and thus to compose smaller BDDs. Of course, there are many ways to compose the R i ( x, y). Let ρ be a permutation of {0, ..., n -1} which determines the order in which the partitions R i ( x, y) are combined. For each i, let D i be the set of variables y k with k ∈ {1, ..., m} that R i ( x, y) depends on. We define E i as the set of variables contained in D ρ(i) that are not contained in D ρ(j) for any j larger than i:

E i = D ρ(i) \ n-1 j=i+1 D ρ(j)
The E i are pairwise disjoint and their union contains all the variables. The relational product (1) can be computed by starting from:

h 1 ( x, y) = ∃ h( y) ∧ R ρ(0) ( x, y) y k ∈ E0
and successively computing h p+1 defined as follows:

h p+1 ( x, y) =          ∃ h p ( x, y) ∧ R ρ(p) ( x, y) y k ∈ Ep if E p = ∅ h p ( x, y) ∧ R ρ(p) ( x, y) if E p = ∅
until reaching h n which is the result of the relational product. The ordering ρ determines how early in the computation variables can be quantified out. This directly impact the sizes of BDDs constructed and therefore the global efficiency

INRIA

of the decision procedure. It is thus important to choose ρ carefully. The overall goal is to minimize the size of the largest BDD created during the elimination process. We use a heuristic taken from [START_REF] Clarke | Model checking[END_REF] which seems to provide the best approximation and in practice has the best performance. It defines the cost of eliminating a variable y k as the sum of the sizes of all the D i containing y k :

1≤i≤n,y k ∈Di |D i |
The ordering ρ on the relations R i is then defined in such a way that variables can be eliminated in the order given by a greedy algorithm which repeatedly eliminates the variable of minimum cost.

BDD Variable Ordering

The cost of BDD operations is very sensitive to variable ordering. Finding the optimal variable ordering is known to be NP-complete [START_REF] Hojati | Early quantification and partitioned transition relations[END_REF], however several heuristics are known to perform well in practice [START_REF] Clarke | Model checking[END_REF]. Choosing a good initial order of Lean(ψ) formulas does significantly improve performance. We found out that preserving locality of the initial problem is essential. Experience has shown that the variable order determined by the breadth-first traversal of the formula ψ to solve, which keeps sister subformulas in close proximity, yields better results in practice.

Typing Applications and Experimental Results

For XPath expressions e 1 , ..., e n , we can formulate several decision problems in the presence of XML type expressions T 1 , ..., T n :

• XPath containment: E → e 1 T1 ∧ ¬E → e 2 T2 (if the formula is unsatisfiable then all nodes selected by e 1 under type constraint T 1 are selected by e 2 under type constraint T 2 )

• XPath emptiness: E → e 1 T1

• XPath overlap:

E → e 1 T1 ∧ E → e 2 T2
• XPath coverage:

E → e 1 T1 ∧ 2≤i≤n ¬E → e i Ti
Two problems are of special interest for XML type checking:

• Static type checking of an annotated XPath query: As no third-party implementation we know of addresses reverse axes and recursion, we simply provide evidence that our approach is efficient. We carried out extensive tests2 [START_REF] Genevès | A satisfiability solver for XML and XPath[END_REF] , and present here only a representative sample that includes the most complex language features such as recursive forward and backward axes, intersection, large and very recursive types with a reasonable alphabet size. The tests use XPath expressions shown on Figure 21 (where "//" is used as a shorthand for "/desc-or-self::*/") and XML types shown on Table 1. Table 2 presents some decision problems and corresponding performance results. Times reported in milliseconds correspond to the running time of the satisfiability solver without the (negligible) time spent for parsing and translating into L µ .

E → e 1 T1 ∧ ¬ T 2 (if
The first XPath containment instance was first formulated in [START_REF] Miklau | Containment and equivalence for a fragment of XPath[END_REF] as an example for which the proposed tree pattern homomorphism technique is incomplete. The e 8 example shows that the official XHTML DTD does not syntactically prohibit the nesting of anchors. For the XHTML case, we observe that the time needed is more important, but it remains practically relevant, especially for static analysis operations performed only at compile-time.

Related Work

The XPath containment problem has attracted a lot of research attention in the database community [START_REF] Miklau | Containment and equivalence for a fragment of XPath[END_REF][START_REF] Neven | XPath containment in the presence of disjunction, DTDs, and variables[END_REF][START_REF] Schwentick | XPath query containment[END_REF]. The focus was given to the study of the impact of different XPath features on the containment complexity (see [START_REF] Schwentick | XPath query containment[END_REF] overview). Specifically, [START_REF] Neven | XPath containment in the presence of disjunction, DTDs, and variables[END_REF] proves an EXPTIME upper-bound (in the presence of DTDs) of queries containing the "child" and "descendant" axes, and union of paths. The complexity of XPath satisfiability in the presence of DTDs also is extensively studied in [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]. From these results, we know that XPath containment with or without type constraints ranges from EXPTIME to undecidable. Most formalisms used in the context of XML are related to one of the two logics used for unranked trees: first-order logic (FO), and Monadic Second Order Logic (MSO). FO and relatives are frequently used for query languages since they nicely capture their navigational features [START_REF] Barceló | Temporal logics over unranked trees[END_REF]. For query languages, Computational Tree Logic (CTL) [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF] , which is equivalent to FO over tree structures has been proposed [START_REF] Miklau | Containment and equivalence for a fragment of XPath[END_REF][START_REF] Marx | Conditional XPath, the first order complete XPath dialect[END_REF][START_REF] Barceló | Temporal logics over unranked trees[END_REF]. In a attempt to reach more expressive power, the work found in [START_REF] Afanasiev | PDL for ordered trees[END_REF] proposes a variant of Propositional Dynamic Logic (PDL) [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF] with an EXPTIME complexity. MSO, specifically the weak monadic second-order logic of two successors (WS2S) [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of second-order logic[END_REF][START_REF] Doner | Tree acceptors and some of their applications[END_REF], is one of the most expressive decidable logic used when both regular types and queries [START_REF] Barceló | Temporal logics over unranked trees[END_REF] are under consideration. WS2S satisfiability is known to be non-elementary. A drawback of the WS2S decision procedure is that it requires the full construction and complementation of tree automata. Some temporal and fixpoint logics closely related to MSO have been introduced and allow to avoid explicit automata construction. The propositional modal µ-calculus introduced in [START_REF] Kozen | Results on the propositional µ-calculus[END_REF] has been shown to be as expressive as nondeterministic tree automata [START_REF] Emerson | Tree automata, µ-calculus and determinacy[END_REF]. Since it is trivially closed under negation, it constitutes a good alternative for studying MSO-related problems. Moreover, it has been extended with converse programs in [START_REF] Vardi | Reasoning about the past with two-way automata[END_REF]. The best known complexity for the resulting logic is obtained through reduction to the emptiness problem of alternating tree automaton which is in 2 O(n 4 •log n) , where n corresponds to the length of a formula [START_REF] Grädel | Automata logics, and infinite games: a guide to current research[END_REF]. Unfortunately the logic lacks the finite model property. From [START_REF] Kupferman | The weakness of self-complementation[END_REF], we know that WS2S is exactly as expressive as the alternation-free fragment (AFMC) of the propositional modal µ-calculus. Furthermore, the AFMC subsumes all early logics such as CTL [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF] and PDL [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF] (see [START_REF] Barceló | Temporal logics over unranked trees[END_REF] for a complete survey on tree logics). In [START_REF] Marx | XPath with conditional axis relations[END_REF], the author considers XPath equivalence under DTDs (local tree types) for which satisfiability is shown to be in EXPTIME.

The goal of the research presented so far is limited to establishing new theoretical properties and complexity bounds. Our research differs in that we seek precise complexity bounds, efficient implementation techniques, and concrete design that may be directly applied to the type checking of XPath queries under regular tree types.

In this line of research, some experimental results based on WS2S, through the Mona tool [START_REF] Klarlund | MONA 1.4[END_REF], have recently been reported for XPath containment [START_REF] Genevès | Deciding XPath containment with MSO[END_REF]and even for query evaluation [START_REF] Inaba | MTran[END_REF]. However, for static analysis purposes, the explosiveness of the approach is very difficult to control due to the non-elementary complexity. Closer to our contribution, the recent work found in [START_REF] Tanabe | A decision procedure for the alternation-free two-way modal µ-calculus[END_REF] provides a decision procedure for the AFMC with converse whose time complexity is 2 O(n•log n) . However, models of the logic are Kripke structures (infinite graphs). Enforcing the finite tree model property can be done at the syntactic level [START_REF] Tanabe | A decision procedure for the alternation-free two-way modal µ-calculus[END_REF], and this has been further developed in the XML setting in [START_REF] Genevès | A system for the static analysis of XPath[END_REF]. Nevertheless, the drawback of this approach is that the AFMC decision procedure requires expensive cycle-detection for rejecting infinite derivation paths for least fixpoint formulas. Furthermore, there is a fundamental difference between this approach and the algorithm presented in this article. The algorithm of [START_REF] Tanabe | A decision procedure for the alternation-free two-way modal µ-calculus[END_REF] used in [START_REF] Genevès | A system for the static analysis of XPath[END_REF] actually computes a greatest fixpoint: it starts from all possible (graph) nodes and progressively removes all inconsistent nodes until a fixpoint is reached. Finally, if the fixpoint contains a satisfying (tree) structure then the formula is satisfiable. As a consequence, unlike the algorithm presented in this article, (1) the algorithm must always explore all nodes, and (2) it cannot terminate until full completion of the fixpoint computation (otherwise inconsistencies may remain). The present work shows how this can be avoided for finite trees. As a consequence, the resulting performance is much more attractive. In an earlier work on XML type checking, a logic for finite trees was presented [START_REF] Tozawa | On binary tree logic for XML and its satisfiability test[END_REF], but the logic is not closed under negation.

In [START_REF] Colazzo | Static analysis for path correctness of XML queries[END_REF], a technique is presented for statically ensuring correctness of paths. The approach only deals with emptiness of XPath expressions without reverse axes, whereas our approach solves the more general problem of containment, including reverse axes.

The work [START_REF] Møller | The design space of type checkers for XML transformation languages[END_REF] presents an approximated technique that is able to statically detect errors in XSLT stylesheets. Their approach could certainly benefit from using our exact algorithm instead of their conservative approximation. The XDuce [START_REF] Hosoya | XDuce: A statically typed XML processing language[END_REF], CDuce [START_REF] Benzaken | CDuce: An XML-centric generalpurpose language[END_REF], and XStatic [START_REF] Gapeyev | Regular object types[END_REF] languages support pattern-matching through regular expression types but not XPath. Although some recent work shows how to translate XPath into Xtatic [17], the XPath fragment considered does not include reverse axes nor negation in qualifiers. A survey on existing research on statically type checking XML transformations can be found in [START_REF] Møller | Static validation of XSL Transformations[END_REF].

Conclusion

The main result of our paper is a sound and complete algorithm for the satisfiability of decision problems involving regular tree types and XPath queries with a tighter 2 O(n) complexity in the length of a formula. Our approach is based on a sub-logic of the alternation-free modal µ-calculus with converse for finite trees.

Our proof method reveals deep connections between this logic and XPath decision problems. First, the translations of XML regular tree types and a large XPath fragment are cycle-free and linear in the size of the corresponding formulas in the logic. Second, on finite trees, since both operators are equivalent, the logic with a single fixpoint operator is closed under negation. This allows to INRIA address key XPath decision problems such as containment. The current solver can also support conditional XPath proposed in [START_REF] Marx | XPath with conditional axis relations[END_REF].

Finally, there are a number of interesting directions for further research that build on ideas developed here: extending XPath to restricted data values comparisons that preserves this complexity, for instance data values on a finite domain, and integrating related work on counting [START_REF] Zilio | A logic you can count on[END_REF] to our logic. We also plan on continuing to improve the performance of our implementation.

t

  ::= σ[tl ] tree tl ::= list of trees empty list | t :: tl cons cell c ::= context (tl , Top, tl ) root of the tree | (tl , c[σ], tl ) context node f ::= (t, c) focused tree

Figure 2 :

 2 Figure 2: Interpretation of formulas

Figure 4 :

 4 Figure 4: XPath Abstract Syntax.

Figure 5 :

 5 Figure 5: Interpretation of XPath Expressions as Functions Between Sets of Focused Trees.

  fchild

Figure 7 :

 7 Figure 7: Translation of XPath Axes.

Figure 8 :

 8 Figure 8: Translation of Expressions and Paths.

Figure 9 :

 9 Figure 9: XPath Translation Example.

Figure 10 :

 10 Figure 10: Translation of Qualifiers.

Figure 11 :

 11 Figure 11: Example of Back and Forth -Yet Cycle-Free -XPath Navigation.

Proposition 5 . 1 (

 51 Translation Correctness) The following hold for an XPath expression e and a L µ formula ϕ denoting a set of focused trees, with ψ = E → e ϕ : 1. ψ ∅ = S e e ϕ ∅ 2. ψ is cycle-free 3. the size of ψ is linear in the size of e and ϕ

Figure 12 :

 12 Figure 12: A Fragment of the DTD of the Wikipedia Encyclopedia.

Figure 16 :Proposition 6 . 1

 1661 Figure 16: Operations used by the Algorithm.

Figure 17 :

 17 Figure 17: Algorithm's principle: progressive bottom-up reasoning.

η

  e1 = child::c/preceding-sibling::a[child::b] e2 = child::c[child::b]

Figure 18 :

 18 Figure 18: Run of the algorithm for a sample XPath containment problem:

Figure 19 :

 19 Figure 19: Partial satisfiability

Figure 20 :

 20 Figure 20: Satisfiability relation

Lemma 6 . 7 (

 67 Complexity) For ψ ∈ L µ the satisfiability problem ψ ∅ = ∅ is decidable in time 2O(n) where n = |Lean(ψ)|.

Table 1 :

 1 the formula is unsatisfiable then all nodes selected by e 1 under type constraint T 1 are included in the type T 2 .)• XPath equivalence under type constraints:E → e 1 T1 ∧ ¬E → e 2 T2 and ¬E → e 1 T1 ∧ E → e 2 T2 (This test can be used to check that the nodes selected after a modification of a type T 1 by T 2 and an XPath expression e 1 by e 2 are the same, typically when an input type changes and the corresponding XPath query has to change as well.) Types Used in Experiments.

	e 1 /a[.//b[c/*//d]/b[c//d]/b[c/d]]
	e 2 /a[.//b[c/*//d]/b[c/d]]
	e 3 a/b//c/foll-sibling::d/e
	e 4 a/b//d[prec-sibling::c]/e
	e 5 a/c/following::d/e
	e 6 a/b[//c]/following::d/e ∩ a/d[preceding::c]/e
	e 7 *//switch[ancestor::head]//seq//audio[prec-sibling::video]
	e 8 descendant::a[ancestor::a]
	e 9 /descendant::*
	e 10 html/(head body)
	e 11 html/head/descendant::*
	e 12 html/body/descendant::*
	Figure 21: XPath Expressions Used in Experiments.
	DTD	Symbols Binary Type Variables
	SMIL 1.0	19	11
	XHTML 1.0 Strict	77	325

Table 2 :

 2 for an XPath Decision Problem XML Type Time (ms) e 1 ⊆ e 2 and e 2 ⊆ e 1 none 353 e 4 ⊆ e 3 and e 4 ⊆ e 3 none 45 e 6 ⊆ e 5 and e 5 ⊆ e 6 Some Decision Problems and Corresponding Results.

		none	41
	e 7 is satisfiable	SMIL 1.0	157
	e 8 is satisfiable	XHTML 1.0	2630
	e 9 ⊆ (e 10 ∪ e 11 ∪ e 12 )	XHTML 1.0	2872

RR n°6590

Experiments have been conducted with a JAVA implementation running on a Pentium 4,

Ghz, with 512Mb of RAM with Windows XP.INRIA