Pierre Genev

Nabil Layaïda

Alan Schmitt

Pierre Genevès
email: pierre.geneves@cnrs.fr.

Nils Gesbert

A Efficiently Deciding µ-calculus with Converse over Finite Trees

Keywords: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-modal logic, F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages-decision problems, E.1 [Data Structures]: Trees Algorithms, languages, theory, verification Modal logic, satisfiability, implementation ACM Reference Format:

We present a sound and complete satisfiability-testing algorithm and its effective implementation for an alternation-free modal µ-calculus with converse, where formulas are cycle-free and are interpreted over finite ordered trees. The time complexity of the satisfiability-testing algorithm is 2 O(n) in terms of formula size n. The algorithm is implemented using symbolic techniques (BDD). We present crucial implementation techniques and heuristics that we used to make the algorithm as fast as possible in practice. Our implementation is available online, and can be used to solve logical formulas of significant size and practical value. We illustrate this in the setting of XML trees.

INTRODUCTION

This paper introduces a logic for reasoning over finite trees, a sound and complete decision procedure for checking the satisfiability of a formula of the logic, and an effective implementation of the decision procedure. The logic is a variant of µ-calculus adapted for finite trees and equipped with backward modalities and nominals. Specifically, the logic is an alternation-free modal µ-calculus with converse, where formulas are cycle-free and are interpreted over finite ordered trees. The time complexity of the satisfiability-testing algorithm is optimal1 : 2 O(n) in terms of formula size n. We present crucial implementation techniques like the use of symbolic techniques (BDD) and heuristics to make the algorithm as fast as possible in practice. Our implementation is available online, and can be used to solve logical formulas of significant size.

Related Work and Motivations

The propositional µ-calculus was introduced as a logic for describing properties of graphs with labeled edges. It was invented by Dana Scott and Jaco de Bakker, and further developed by V. R. [START_REF] Pratt | A decidable mu-calculus: Preliminary report[END_REF] and then Dexter [START_REF] Kozen | Results on the propositional µ-calculus[END_REF] into the version mostly used nowadays. Several modal logics can be encoded in the µ-calculus, including linear temporal logic, computational tree logic [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF], CTL*, and propositional dynamic logic [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. In contrast with the importance and large applicative spectrum of the µ-calculus satisfiability problem, only very few actual effective implementations have been reported in the literature. One implementation for the full µ-calculus (without converse modalities) and some variants is MLSolver [START_REF] Friedmann | A solver for modal fixpoint logics[END_REF], a generic tool which implements the satisfiability problem for several fixpoint logics by reducing it to the problem of solving a parity game, which is then solved using the solver PGSolver [START_REF] Friedmann | The pgsolver collection of parity game solvers[END_REF].

A large number of variants of the µ-calculus have been studied, but as pointed out by [START_REF] Tanabe | A decision procedure for the alternation-free two-way modal µ-calculus[END_REF]: "the satisfiability testing problem for the µ-calculus is known to be decidable for a variety of extensions and subfragments, but effective implementation has not necessarily been developed for all such logics".

We review below the works on variants that are most closely related to ours in terms of supported logical features (e.g., backward modalities, nominals), models of the logic (trees), or from the point-of-view of the approach oriented toward an effective implementation (effective algorithmics). For instance, the work of [START_REF] Pan | BDD-based decision procedures for the modal logic K[END_REF] pursues a goal similar to ours for the modal logic K. The approach yields effective BDD-based decision procedures for K, usable in practice. However, K is strictly less expressive than the µ-calculus since it lacks recursion (no fixpoint) and backward modalities.

Backward Modalities. In applications, we often need to follow edges not only in the forward direction but also in the backward direction. Therefore, researchers have been focusing on temporal logics that can handle both directions, or modalities, in order to reason about both the "past" and the "future". Although converse modalities do not, in the case of finite trees, add expressive power, they provide an advance in terms of succinctness as they offer a notation for otherwise exponentially larger formulas. Succinctness is a crucial matter when considering the combined complexity of the decision procedure. The satisfiability problem for the general µ-calculus with converse modalities (MC) is known to be EXPTIME-complete [START_REF] Vardi | Reasoning about the past with two-way automata[END_REF]]. The decision procedure is constructed by converting the problem into the emptiness problem of the language recognized by a certain alternating tree automaton on infinite trees. In order to solve this emptiness problem, complex operations are required including determinization of parity automata [START_REF] Safra | On the complexity of omega -automata[END_REF]]; it can be done in 2 O(n 4 •log n) , where n is the size of the formula [START_REF] Gr Ädel | Automata logics, and infinite games: a guide to current research[END_REF].

The works of [START_REF] Tanabe | A decision procedure for the alternation-free two-way modal µ-calculus[END_REF]2008] provide an implementation of a decision procedure for the alternation-free fragment of the µ-calculus with converse (AFMC), whose time complexity is 2 O(n•log n) . As expected, the decision procedure for the AFMC is less complex than the one for the MC. The alternation-free restriction makes much sense since the expressive power of AFMC exactly corresponds to the one of weak monadic-second order logic [START_REF] Kupferman | The weakness of self-complementation[END_REF].

Trees. Applications of the satisfiability-checking problem often restrict the allowed models to sets of finite trees (see, e.g., [START_REF] Zee | Full functional verification of linked data structures[END_REF]). Therefore, even if the AFMC lacks the finite model property (which is lost due to the addition of converse modalities), it makes sense to search for finite trees satisfying a given logical formula.

In this line of research, the work of [START_REF] Afanasiev | PDL for ordered trees[END_REF] presents a special version of Propositional Dynamic Logic (PDL) for reasoning about finite sibling-ordered trees. However, the precise expressive power of the logic is still an open problem, although the logic is subsumed by the AFMC.

In the works of [START_REF] Tanabe | A decision procedure for the alternation-free two-way modal µ-calculus[END_REF]2008], models of the logic are Kripke structures (infinite graphs). Models can be restricted to be binary-branching finite trees through an additional logical formula that forbids the existence of infinite branches. However, the authors notice that the performance of the decision procedure may not be very attractive in this setting. They do not give further details, but our research has given us some insights. Specifically, a first source of inefficiency of this approach comes from the fact that the decision procedure requires expensive cycle-detection for rejecting infinite derivation paths for least fixpoint formulas. A second and even more fundamental source of inefficiency is that the decision procedure of [START_REF] Tanabe | A decision procedure for the alternation-free two-way modal µ-calculus[END_REF] must compute a greatest fixpoint: it starts from all possible (graph) nodes and progressively removes all inconsistent nodes until a fixpoint is reached. Then the formula is judged as satisfiable if the fixpoint contains a satisfying (tree) structure. As a consequence, and 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. The resulting performance of our decision procedure, whose time complexity is 2 O(n) , is much more attractive.

In an earlier work, 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.

The connection with Automata. In our extended abstract [Genevès et al. 2007], we showed the decidability in time 2 O(n) of the cycle-free fragment of the AFMC for finite trees. Since then, alternative and closely related approaches based on tree automata have been proposed with similar or higher complexity, but without implementation [START_REF] Calvanese | Regular XPath: Constraints, query containment and view-based answering for xml documents[END_REF][START_REF] Libkin | Reasoning about xml with temporal logics and automata[END_REF][START_REF] Calvanese | An automata-theoretic approach to regular XPath[END_REF][START_REF] Libkin | Reasoning about xml with temporal logics and automata[END_REF][START_REF] Calvanese | Node selection query languages for trees[END_REF].

Approaches based on alternating two-way tree automata (2ATA) for infinite trees have resisted implementation, as noticed by [START_REF] Calvanese | An automata-theoretic approach to regular XPath[END_REF], mainly because of complex determinization (see also [START_REF] Calvanese | Regular XPath: Constraints, query containment and view-based answering for xml documents[END_REF]); the authors also mention that it is practically infeasible to apply the symbolic approach in the infinite tree setting.

A simpler and more appropriate automata-based approach for finite trees is the technique based on weak alternating two-way tree automata (2WATA). However, they require a conversion to non-deterministic finite tree automata (NFTA) for testing nonemptiness. The translation given by [START_REF] Calvanese | Node selection query languages for trees[END_REF] yields an automaton with 2 O(n 2 ) states in terms of the number n of states of the original 2WATA.

As mentioned before, none of the works cited above provides an implementation. In fact, [START_REF] Calvanese | Regular XPath: Constraints, query containment and view-based answering for xml documents[END_REF] remark that a naive implementation of their technique would result in a blow-up in complexity, requiring the use of more elaborate techniques very similar to what we have done. The approach of [START_REF] Libkin | Reasoning about xml with temporal logics and automata[END_REF] is an alternative version of our previous work [Genevès et al. 2007] that allows the shortening of some proofs but does not simplify the implementation. The present work can thus be regarded as the only efficient implementation of the logic or, alternatively, of the 2WATA framework.

For the sake of simplicity and uniformity between the satisfiability algorithm, the proofs, and the implementation techniques, we focus in this paper on the native modal logic. This also emphasizes the fact that bottom-up construction of the finite tree model and cycle-freeness come naturally and shows exactly why the whole approach is efficient.

Contributions

Our main result is a satisfiability-testing algorithm for a logic for finite trees whose time complexity is optimal: 2 O(n) in terms of the formula size n, together with its effective implementation through BDD techniques.

The essence of our results lives in a sub-logic of the AFMC, with a syntactic restriction-cycle-freeness-on formulas, and whose models are finite trees. Such restrictions are interesting from a theoretical point of view: we prove that, under these conditions, the least and greatest fixpoint operators collapse into a single fixpoint operator. This makes our logic closed under negation and provides many opportunities to derive an efficient implementation.

The decision procedure is implemented and an online demonstration is publicly available, as detailed in §5.5.

An extended abstract of this work was presented at the ACM Conference on Programming Language Design and Implementation (PLDI), [START_REF] Voss | Wikipedia dtd[END_REF][Genevès et al. 2007]. The new material included in this article comprises the following. The notion of cyclefreeness, a fundamental aspect of our logic, and its formalization are much more detailed. Proofs have been added. A detailed run of the algorithm is described. Implementation techniques and the optimizations used to obtain a satisfiability-testing algorithm that performs well in practice are also discussed.

Outline

The paper is organized as follows. We first present our data model, trees with focus, in §2. We then introduce the logic in §3.

Our satisfiability algorithm is introduced and proven correct in §4. Crucial implementation techniques are discussed in §5. Applications such as regular language equivalence and query analysis are reviewed in §6. We conclude in §7.

TREES WITH FOCUS

Our data model is based on binary trees. Note that it is possible and straightforward to use binary trees to represent unranked n-ary trees where the children of a node are ordered-we use this, for instance, to apply our work to the analysis of XPath queries in Section 6.

In order to represent 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 parent, its parent's other subtree, and its parent's context recursively. Exploring such a structure has the advantage to preserve all the information, which is quite useful when considering forward and backward navigation.

Formally, we assume an alphabet Λ of labels, ranged over by α, β, . . .. Each node of the trees bears a finite number of labels; we use L to range over finite sets of labels. The syntax of our data model is as follows. A focused tree τ c is a pair consisting of a tree τ and its context c. The context describes what is above the tree. It is either Top, meaning the current tree is actually at the root, (L, [], st) c , meaning that the current tree is the left child of a node labeled L whose right child is st and whose context is c , or symmetrically (L, st, []) c , meaning that the current tree is the right child of a node labeled L whose left child is st and whose context is c .

We write F for the set of finite focused trees, i.e., the language generated by the above grammar.

We now describe how to navigate focused trees. There are four directions, or modalities, that can be followed: for a focused tree ft, ft 1 changes the focus to the left (first) child of the current tree, ft 2 changes the focus to the right (second) child of the current tree, ft 1 changes the focus to the parent of the tree if the current tree is a left child, otherwise it is undefined, and ft 2 changes the focus to the parent of the tree if the current tree is a right child and is undefined otherwise.

Formally, we have:

(L, τ, st) c 1 def = τ (L,[],st)c (L, st, τ ) c 2 def = τ (L,st,[])c τ (L,[],st)c 1 def = (L, τ, st) c τ (L,st,[])c 2 def = (L, st, τ ) c
When the focused tree does not have the required shape, these operations are not defined. These navigation operations can be combined and iterated to move from any node of a tree to any other node; a sequence of navigation steps forms a path in a tree. Since the steps have inverses, it makes sense to define the set of paths as a free group rather than as just a set of sequences.

Definition 2.1 (Paths). We define the set P of paths as the free group generated by 1 and 2. We denote the inverse with an overline bar, the neutral element with ε and the composition law with a dot •.

The navigation operation on trees defined above for elementary paths is extended to arbitrary paths p ∈ P in the obvious way.

The path navigation operation has the following interesting properties:

-if ft p is defined and p = ε, then ft p = ft (this represents the fact that a tree has no cycles); -if ft p is defined, then either ft p • q and ft p q are both undefined, or they are both defined and are equal; -the equivalence relation ∼ between focused trees defined by ft ∼ ft ⇔ ∃p ∈ P, ft = ft p is the relation "be nodes of the same tree". Its classes are finite since we only consider finite trees.

This last property holds because we are considering focused trees: such trees make explicit their set of nodes, even those in the context, and the relation between these nodes.

We can also remark that some paths p are such that ft p is undefined for all ft, e.g., the path 1 • 2. Again, this is due to the topological restrictions of trees.

In the following, we will often use navigation operations on whole sets of trees; we introduce the following notation.

Notation 2.2. If E is a set of focused trees and p a path, we define: Remark 2.3. Note that because the navigation operation is partial, we do not have, in general, E p q = E p • q , but only E p q ⊆ E p • q . More precisely: E p q = E p • q ∩ F p q . This remark holds in particular for q = p and implies that, in the logic that we now define, the formulas ϕ and 1 1 ϕ are not equivalent (but the second one implies the first). Indeed, the second formula additionally asserts that the selected tree node has a 1 child.

E p def = {ft p | ft ∈ E ∧ ft p defined}. A:6 Pierre Genev ès et al. ϕ, ψ ::= formula | ⊥ true, false | α | ¬α atomic proposition (negated) | X variable | ϕ ∨ ψ disjunction | ϕ ∧ ψ conjunction | a ϕ | ¬ a existential modality (negated) | µ(X i = ϕ i ) i∈I in ψ least polyadic fixpoint | ν(X i = ϕ i ) i∈I in ψ greatest polyadic fixpoint

THE LOGIC

We introduce the logic as 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 this restriction and this interpretation make the greatest and smallest fixpoint collapse, yielding a logic that is closed under negation without requiring a greatest fixpoint.

Formulas

In the following, we denote tuples of unknown size using parentheses and an indexing set, e.g., (X i = ϕ i ) i∈{1...n} means (X 1 = ϕ 1 ; X 2 = ϕ 2 ; . . . ; X n = ϕ n ). It is implicitly assumed that the indexing set is always finite.

In the definitions, a ∈ {1, 2, 1, 2} are programs. Atomic propositions α correspond to labels from Λ. Formulas, defined in Fig. 1, include the truth and falsehood predicates, atomic propositions (indicating the tree at focus should bear the corresponding label), disjunction and conjunction of formulas, formulas under an existential modality (denoting the existence of a subtree satisfying the sub-formula), and least and greatest polyadic fixpoints. We chose to include a polyadic 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. When there is no need to distinguish between least and greatest fixpoints, we write ι for either µ or ν. In the following, we write "ιX.ϕ" for "ι(X = ϕ) in X".

We consider µ and ν as binders for the variables and define the notions of free and bound variables and of open and closed formulas as usual. The language L µ we consider is the set of closed formulas.

In general, ¬ϕ is not part of the syntax. It is defined, for closed formulas, as an abbreviation in Fig. 2. This definition uses an auxiliary function neg(•) which is defined inductively on possibly open formulas, but neg(ϕ) is in general not the negation of ϕ if ϕ is open (in particular, neg(X) = X).

Efficiently Deciding µ-calculus with Converse over Finite Trees A:7

¬ϕ def = neg(ϕ) if ϕ is closed and ϕ = a neg( ) def = ⊥ neg(α) def = ¬α neg(⊥) def = neg(X) def = X neg(ϕ ∨ ψ) def = neg(ϕ) ∧ neg(ψ) neg(¬ϕ) def = ϕ neg(ϕ ∧ ψ) def = neg(ϕ) ∨ neg(ψ) neg( a ϕ) def = ¬ a ∨ a neg(ϕ) neg(µ(X i = ϕ i ) i∈I in ψ) def = ν(X i = neg(ϕ i )) i∈I in neg(ψ) neg(ν(X i = ϕ i ) i∈I in ψ) def = µ(X i = neg(ϕ i )) i∈I in neg(ψ)
Fig. 2. Negation of closed formulas, defined as syntactic sugar.

V def = F α V def = {(L, st 1 , st 2 ) c ∈ F | α ∈ L} ⊥ V def = ∅ ¬α V def = {(L, st 1 , st 2 ) c ∈ F | α ∈ L} X V def = V (X) a ϕ V def = ϕ V a ϕ ∨ ψ V def = ϕ V ∪ ψ V ¬ a V def = F \ (F a ) ϕ ∧ ψ V def = ϕ V ∩ ψ V µ(X i = ϕ i ) i∈I in ψ V def = ψ V [Xi →Ui]
where the U i are defined as follows:

let S = {(T i ) ∈ P(F) I | ∀j ∈ I, ϕ j V [Xi →Ti] ⊆ T j }
and for all j ∈ I, let

U j = (Ti)∈S T j ν(X i = ϕ i ) i∈I in ψ V def = ψ V [Xi →U i ]
where the U i are defined as follows:

let S = {(T i ) ∈ P(F) I | ∀j ∈ I, T j ⊆ ϕ j V [Xi →Ti] }
and for all j ∈ I, let U j = (Ti)∈S T j

Fig. 3. Interpretation of formulas

For ϕ = (ι(X i = ϕ i ) i∈I in ψ) we define unfold(ϕ) def = ψ{( ι(Xi=ϕi) i∈I in ϕ k / X k ) k∈I }, which denotes the formula ψ in which every occurrence of an X k is replaced by (ι(X i = ϕ i ) i∈I in ϕ k ).

Model

We define in Fig. 3 an interpretation of our formulas as subsets of F, the set of finite focused trees. For formulas containing free variables, this interpretation is parameterized by a valuation, i.e., a mapping V from variables to subsets of F. We use square brackets and an overline bar to denote a modified mapping, as follows:

V [X i → T i ](X) def = T k if X = X k V (X) otherwise.
A:8 Pierre Genev ès et al.

We now comment on the interpretation of polyadic fixpoints. Let ϕ = ι(X i = ϕ i ) i∈I in ψ with ι = µ or ν. We write P(F) I for the set of I-indexed tuples of subsets of F; it represents the set of all possible valuations for the tuple of variables (X i ) i∈I . We give to this set the partial ordering defined by componentwise inclusion, i.e., (T

i ) (T i ) iff ∀i ∈ I, T i ⊆ T i .
The interpretation of the tuple of formulas (ϕ i ) parameterized by the valuation of the tuple of variables X i defines a function from P(F) I to P(F) I . The final valuation used to define the interpretation of ϕ is a fixpoint of this function, the least one if ι = µ and the greatest one if ι = ν, with respect to the ordering defined above. We now show that this corresponds to the definitions in Fig. 3. LEMMA 3.1. Let (X i = ϕ i ) i∈I be a tuple of bindings and ψ a formula, and let V be a valuation.

Let F : P(F) I → P(F) I be the function defined by F ((T i ) i∈I ) = ( ϕ j V [Xi →Ti] ) j∈I . Let (U j ) j∈I and (U j ) j∈I be as defined in Fig. 3. Then (U j ) j∈I is the least fixpoint of F and (U j ) j∈I is its greatest fixpoint.

To prove this, we use the following auxiliary lemma: LEMMA 3.2. Let ϕ be a formula, X a variable, V a valuation. Let A = V (X) and

A ⊆ B. Then ϕ V ⊆ ϕ V [X →B] .
PROOF OF LEMMA 3.2. We prove the lemma by structural induction on ϕ, for any valuation V , variable X, and sets of focused trees A and B. Almost all cases are straightforward (note that X cannot appear under a negation, which is the key point). We only detail the cases of µ and ν:

-ϕ = µ(X i = ϕ i ) i∈I in ψ. If X is one of the X i , we immediately have ϕ V = ϕ V [X →B] .
We thus assume X is different from every X i and we let them commute freely in the valuation. Let

(T i ) i∈I ∈ S B = {(T i ) ∈ P(F) I | ∀j ∈ I, ϕ j V [X →B][Xi →Ti] ⊆ T j }. By induction hypothesis, for any j ∈ I, we have ϕ j V [Xi →Ti] ⊆ ϕ j V [Xi →Ti][X →B] , thus (T i ) i∈I ∈ S A = {(T i ) ∈ P(F) I | ∀j ∈ I, ϕ j V [Xi →Ti] ⊆ T j },
which implies that S B ⊆ S A . Let j ∈ I and t ∈ U A j = (Ti)∈S A T j , we thus have t ∈ T j for every (T i ) ∈ S A . As S B ⊆ S A , we have t ∈ T j for every (T i ) ∈ S B . Thus t ∈ U B j = (Ti)∈S B T j , and U A j ⊆ U B j . We conclude by the following computation, applying the induction hypothesis each time:

ψ V [Xi →U A i ] ⊆ ψ V [Xi →U A i ][X1 →U B 1 ] ⊆ . . . ⊆ ψ V [Xi →U A i ][Xi →U B i ] = ψ V [Xi →U B i ] ⊆ ψ V [Xi →U B i ][X →B] -ϕ = ν(X i = ϕ i ) i∈I in ψ.
As in the previous case, we use the induction hypothesis to deduce that

T j ⊆ ϕ j V [Xi →Ti] ⊆ ϕ j V [Xi →Ti][X →B] , thus S A ⊆ S B .
As we now define U as the union of the tuples in S , we thus have for every j, U A j ⊆ U B J . We conclude as above.

PROOF OF LEMMA 3.1. First of all, we deduce from the auxiliary lemma 3.2 that the function F is increasing (with respect to the ordering defined by componentwise inclusion, as explained above), i.e., T T implies F (T ) F (T ). The result is then a consequence of the Knaster-Tarski fixpoint theorem; it is also easy to prove directly, as we now show.

Efficiently Deciding µ-calculus with Converse over Finite Trees A:9 -For the least fixpoint: the set S defined in Fig. 3 is the set of tuples T such that F (T )

T . This set is preserved by F : since F is increasing, F (T ) T implies F (F (T )) F (T ). Let U = (U j ) j∈I . For all T in S, we have U T , hence F (U ) F (T ) since F is increasing, and thus F (U ) T for every T ∈ S. This implies F (U ) U (since U is the intersection of every T in S). We thus have U ∈ S, and therefore F (U ) ∈ S (because S is preserved by F ), from which we conclude U F (U ) (because U is a lower bound), and finally F (U ) = U . This fixpoint is clearly the least one, since S contains by definition all fixpoints of S and all its elements are greater than U .

-For the greatest fixpoint: the reasoning is the dual of the above.

For closed formulas, the interpretation is clearly independent from the initial V , thus we omit it when considering only closed formulas. Furthermore, we can check by a straightforward induction that ¬ϕ = F \ ϕ for any closed formula ϕ, as expected.

A corollary of the fixpoint lemma 3.1 is that for any fixpoint formula ϕ we have unfold(ϕ) = ϕ .

To illustrate the interpretation of fixpoints, consider the two closed formulas ϕ = µX. 1 X ∨ 1 X and ψ = νX. 1 X ∨ 1 X. Following the definition, the interpretation of ϕ is X X →U = U where U is the intersection of all sets in S. Straightforwardly we have ∅ ∈ S :

1 X ∨ 1 X X →∅ = ∅ ⊆ ∅.
Thus U = ∅ and ϕ = ∅. 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 ft 1 = (a, (b, nil, nil), nil) Top . Let ft 2 = ft 1 1 , that is the tree (b, nil, nil) (a,[],nil) Top . We thus have ft 2 1 = ft 1 . Finally, let V be the mapping [X → {ft 1 , ft 2 }]. We compute as follows:

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} = {ft 1 } ∪ {ft 2 } thus V (X) ⊆ 1 X ∨ 1 X V , hence {ft 1 , ft 2 } ∈ S,
and thus {ft 1 , ft 2 } ⊆ U . We have indeed ft 1 ∈ ψ .

Cycle-Free Formulas

As shown in §3.2, the smallest and greatest fixpoints do not coincide. This fact can be linked to a result from [START_REF] Mateescu | Local model-checking of modal µ-calculus on acyclic labeled transition systems[END_REF]: the two fixpoint operators coincide2 on a given Kripke structure if and only if the structure is acyclic. Although our structures are trees, they are not acyclic Kripke structures since these trees are navigable in both directions. However, the fact they are trees means that the only possible simple cycles are paths which go one way and back the exact same way (ft p = ft if and only if p = ε). This allows us to introduce a syntactic restriction on formulas, which we call cycle-freeness, making the two fixpoints collapse on our semantic domain.

To define this notion formally, we first define the syntactic graph of a formula, where we label the edges with tree paths from P (see Def. 2.1). Formally, we consider an oriented graph whose vertices are all formulas and whose edges are as follows:

A:10 Pierre Genev ès et al.

-

ϕ 1 ∧ ϕ 2 ε -→ ϕ 1 , ϕ 1 ∧ ϕ 2 ε -→ ϕ 2 -ϕ 1 ∨ ϕ 2 ε -→ ϕ 1 , ϕ 1 ∨ ϕ 2 ε -→ ϕ 2 -a ϕ a -→ ϕ -ι(X i = ϕ i ) i∈I in ψ ε -→ unfold(ι(X i = ϕ i ) i∈I in ψ)
-Formulas which are not of one of the forms above have no outgoing edges. This graph has the property that the formulas reachable from a closed formula are all closed, thanks to the 'exp' operation.

Definition 3.3. The Fischer-Ladner closure cl(ψ) of a normalised (all bound variables have different names) closed formula ψ is the set of formulas reachable from ψ in the graph defined above, including ψ itself. This set is finite. Indeed, most of the edges go from a formula to a subformula; the only exception is the fixpoint. When a fixpoint formula is expanded, all the new fixpoint formulas which appear have the form ι(X i = ϕ i ) i∈I in ϕ k with k ∈ I. But the total number of such formulas is bounded by the number of variables in the whole initial formula, which is finite.

However, the subgraph corresponding to the closure typically contains cycles. What we want to ensure is that the cycles in the syntactic graph do not correspond to cycles in models of the formula. Intuitively, whether a subformula holds at a given node of a tree may depend on whether the same subformula holds at another node of that tree, but should not depend on itself (the same subformula holding at the same node) if we want the two fixpoints to coincide.

We call walk a sequence of consecutive formulas and edges in the syntactic graph. The definition below relates walks in the syntactic graph and paths in the trees.

Definition 3.4 (Trace of a walk). Let w = ϕ 1 p1 -→ ϕ 2 p2 -→ • • • pn -→ ϕ n+1 be a walk in the syntactic graph. The trace of w is the path tr(w) = p 1 • p 2 • • • • • p n , where • is the composition law from Def. 2.1
We can now define cycle-freeness.

Definition 3.5 (Cycle-free formula). We say that a formula ϕ is cycle-free if, in the syntactic graph of its closure, no nonempty walk from a formula to itself has trace ε.

Note that cycle-freeness implies the more usual property of guardedness, which here could be defined as the absence of cycles whose edges are all labelled ε.

For instance, the formulas ϕ and ψ described at the end of §3.2 are not cycle-free. Indeed, looking at the syntactic graph of e.g. ψ, illustrated by Fig. 4, we can see that starting from the top vertex and going first along the right loop then along the left one, we obtain a cyclic walk with trace ε

• ε • 1 • ε • ε • 1 = ε.
As a more elaborate example, the formula

χ = µ(X = 2 Y ∨ 2 Y ∨ 1 X, Y = 1 X) in X
is not cycle-free. Indeed, its graph has 3 simple cycles from the same starting point unfold(χ), with traces respectively p 1 = 2 • 1, p 2 = 2 • 1 and p 3 = 1, and we can see that

p 2 • p 3 • p 1 • p 3 = ε.
We further comment on the automated detection of cycle-free formulas in Appendix C.

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: the interpretation of a cycle-free formula is equal to its finite interpretation, defined in Fig. 5. The finite interpretation is identical to the normal inter-Efficiently Deciding µ-calculus with Converse over Finite Trees A:11

νX. 1 X ∨ 1 X 1 (νX. 1 X ∨ 1 X) ∨ 1 (νX. 1 X ∨ 1 X) 1 (νX. 1 X ∨ 1 X) 1 (νX. 1 X ∨ 1 X) ε ε ε 1 1 Fig. 4. Syntactic graph of ψ = νX. 1 X ∨ 1 X ϕ ∨ ψ V def = ϕ V ∪ ψ V ϕ ∧ ψ V def = ϕ V ∩ ψ V a ϕ V def = ϕ V a ι(X i = ϕ i ) i∈I in ψ V def = ψ V [Xi →Ui]
where the U i are defined as follows:

let F : P(F) I → P(F) I (T i ) i∈I → ( ϕ j V [Xi →Ti] ) j∈I
and for all j ∈ I, let pretation for all formulas but fixpoints; for fixpoints, the valuation of the variables is obtained by iterating the function F starting from an empty valuation. We know from Lemma 3.1 and its proof that F is an increasing function with at least one fixpoint; given this, it is straightforward to see that iterating F starting from the smallest possible tuple, i. e. (∅ • • • ∅), gives an approximation of its least fixpoint from below. Therefore for any closed ϕ we have ϕ ⊆ ϕ . We now prove that for cycle-free formulas, the converse inclusion also holds.

U j = n∈N (F n (∅, . . . , ∅))(j) ϕ V = ϕ V in all other cases.
Notice that the following Lemma 3.6 is not necessary to prove the correctness of our decision procedure (Theorem 4.4). The fact that the least and the greatest fixpoints coincide is an implication of Theorem 4.4. We nevertheless present a direct proof of Lemma 3.6, since we believe that it is also interesting independently in itself.

LEMMA 3.6. Let ϕ be a cycle-free formula. Then ϕ V = ϕ V for any V .

We organise the proof in auxiliary lemmas: first we show in Lemma 3.7 that ϕ V can always be put into a sort of normal form, with constant parts and parts which depend on V , where the variable parts are of the form V (X) p , with p the trace of a walk from ϕ to X in the syntactic graph.

Then in Lemma 3.8 we show that for a fixpoint formula, by iterating that property, F n (U ) can be put into a normal form where the variable parts are of the form U i p 1 • • • p n , with the p k traces of walks going from one to another binding of the fixpoint in the syntactic graph.

Finally, we conclude by noticing that the number of tree nodes visited by the sequences of paths p 1 • • • p n is unbounded if the formula is cycle-free. This implies that any given focused tree which belongs to F n (U ) for all n, as is the case if U is a fixpoint of F , must fall in the constant part of the normal form for n large enough, which means it also belongs to F n (∅, . . . ∅).

We now present the main proof formally. The proofs of Lemmas 3.7 and 3.8 are in Appendix B.

LEMMA 3.7. Let ϕ be a formula with free variables

{X i | i ∈ I}. Then ϕ V is of the form k∈K A k ∩ l∈L k V (X j l ) p l , where :
-K, the A k , the L k , the j l and the p l do not depend on V , and the L k are finite. We also assume the L k are all disjoint. -for each l, there is a (possibly empty) walk w l from ϕ to X j l such that tr(w l ) = p l .

We do not require K to be finite, and we consider an empty intersection to be equal to F and an empty union to ∅.

LEMMA 3.8. Let ϕ = ι(X i = ϕ i ) i∈I in ψ be a fixpoint formula and let F be the function defined in Fig. 5. For each j ∈ I, we write

ψ j def = ι(X i = ϕ i ) i∈I in ϕ j .
For each pair (i, j) ∈ I 2 , we consider the set of nonempty walks, in the syntactic graph of formulas, which go from ψ i to ψ j , and we write P j i for the corresponding set of traces. Then for any n ∈ N and for any

U = (U j ) j∈I ∈ P(F) I , F n (U ) is of the form : k∈Ki A k ∩ l∈L k U j l q l 1 q l 2 • • • q l n i∈I
where :

-the K i , the A k , the L k and the q l m do not depend on U ; -for each l, there is a sequence of indices (i l 0 , . . . , i l n ) ∈ I n+1 , with i l 0 = j l and i l n = i, such that for all m between 1 and n, q l m ∈ P

i l m-1 i l m .
PROOF OF LEMMA 3.6. We can now prove our main lemma. We do it by structural induction on ϕ. All cases are completely straightforward except the fixpoints, since the definitions of ϕ V and ϕ V only differ for them. Thus we assume that ϕ is of the form ι(X i = ϕ i ) i∈I in ψ with ι = µ or ν and that the property is true for ψ and the ϕ i . The fact that it is true for the ϕ i means that the function F defined in Fig. 5 is the same as the one defined in Lemma 3.1. This lemma furthermore tells us that we have

ϕ V = ψ V [Xi →Ui] where (U i ) i∈I is a fixpoint of F , either the least or the greatest. By induction hypothesis, we have ψ V [X i →U i ] = ψ V [X i →U i ] . What remains to prove is that for all i ∈ I such that X i appears free in ψ we have U i = n∈N (F n (∅, . . . , ∅))(i).
(This is not necessarily true for all i ∈ I because it is possible that some of the ψ i are unreachable from ϕ in the syntactic graph, if the fixpoint formula contains unused bindings, in which case the constraint that ϕ is cycle-free does not impact the corresponding variables.)

As remarked earlier, the inclusion from right to left is easy. Since F is increasing, (U i ) is a fixpoint and (∅, . . . , ∅) (U i ), by a straightforward induction we have F n (∅, . . . , ∅) (U i ) for any n.

We now have to prove that U i ⊆ n∈N (F n (∅, . . . , ∅))(i), or in other words, that for all ft ∈ U i , there exists n such that ft ∈ (F n (∅, . . . , ∅))(i). So, let ft ∈ U i . It is a finite tree, with m > 0 nodes. This means that there are no more than m different tree paths p in P such that ft p is defined. Let n = m(Card I). Since (U i ) is a fixpoint of F , we have ft ∈ (F n (U ))(i). From Lemma 3.8, we have both:

-(F n (U ))(i) = k∈Ki A k ∩ l∈L k U j l q l 1 q l 2 • • • q l n
where the q l m have the properties described in the lemma, and

-(F n (∅, . . . , ∅))(i) = k∈Ki|L k =∅ A k .
Indeed, ∅ q is always empty and the only nonempty intersection of empty sets is the empty intersection.

Thus, to show that ft ∈ (F n (∅, . . . , ∅))(i), it suffices to prove that for any l, ft ∈

U j l q l 1 q l 2 • • • q l n . Suppose we do in fact have ft ∈ U j l q l 1 q l 2 • • • q l n
for some l. We prove that in that case, ϕ is not cycle-free. For h between 0 and n, let p h = q l h+1 • q l h+2 • • • q l n (we adopt the convention that p n = ε). Then for any h, ft p h must be defined. Let (i l 0 , . . . , i l n ) be the sequence of indices associated to the q l h as per Lemma 3.8. The length of this sequence is n + 1. Since there are only Card I possible indices and n = m(Card I), at least one of the indices, say j, appears m + 1 times in the sequence, say at h 0 . . . h m in increasing order. Since all the ft p h are defined and ft has only m nodes, two of the p hx must be equal (since there are m + 1 of them). Suppose they are p hx and p hy with x < y. We have

p hx = q l hx+1 • q l hx+2 • • • q l hy • p hy ; therefore q l hx+1 • q l hx+2 • • • q l hy = ε.
But this path is the trace of a nonempty (since x < y) walk from ψ j to ψ j , so ψ j is not cycle-free. Furthermore, ψ j is reachable, in the syntactic graph, from ψ i since it appears in the sequence, and ψ i is reachable from ϕ since we assumed X i appeared free in ψ. Thus ϕ is not cycle-free either.

An important consequence of Lemma 3.6 is that the negation of a cycle-free least fixpoint formula is itself a least fixpoint, so that the subset of the logic consisting of closed cycle-free formulas with only least fixpoints is closed under negation. In the rest of the paper, we only consider this subset.

SATISFIABILITY-TESTING ALGORITHM

In this section, we present an algorithm to test the satisfiability of a cycle-free closed formula of L µ . To simplify the approach, we restrict ourselves to checking whether a formula is satisfiable by a focused tree whose context is Top. This can be done without loss of generality, as the following lemma shows. LEMMA 4.1. Let ϕ be a cycle-free closed formula. Let ψ = µX.ϕ ∨ 1 X ∨ 2 X. Then ϕ = ∅ if and only if there exists a focused tree τ Top ∈ ψ .

PROOF. Suppose ϕ is unsatisfiable (i.e. ϕ = ∅). Then ∅ is a fixpoint of the function

F associated to ψ, hence ψ = ∅.
Conversely, suppose ϕ is satisfiable. By definition of ψ , we have: ϕ ⊆ ψ , and ∀ft ∈ ψ , (ft

1 defined ⇒ ft 1 ∈ ψ ) ∧ (ft 2 defined ⇒ ft 2 ∈ ψ ). Since ϕ is sat- isfiable, ψ is not empty. Let ft ∈ ψ .
Because of the structure of focused trees, either the context of ft is Top, or one of ft 1 or ft 2 is defined, which means ψ contains an In the rest of this section, we always assume ψ to be the 'plunged formula' built in this way from the formula ϕ whose satisfiability we want to decide. The algorithm only looks for models of ψ whose context is Top.

⇐= (∅, ∅) ϕ ∈ Lean(ψ) ϕ ⇐= ({ϕ}, ∅) ϕ 1 ⇐= (T 1 , F 1 ) ϕ 2 ⇐= (T 2 , F 2 ) ϕ 1 ∧ ϕ 2 ⇐= (T 1 ∪ T 2 , F 1 ∪ F 2 ) ϕ 1 ⇐= (T 1 , F 1 ) ϕ 1 ∨ ϕ 2 ⇐= (T 1 , F 1 ) ϕ 2 ⇐= (T 2 , F 2 ) ϕ 1 ∨ ϕ 2 ⇐= (T 2 , F 2 ) ϕ ∈ Lean(ψ) ¬ϕ ⇐= (∅, {ϕ}) unfold(µ(X i = ϕ i ) in ψ) ⇐= (T, F ) µ(X i = ϕ i ) in ψ ⇐= (T, F )

Preliminary Definitions

We call Σ(ψ) the set of atomic propositions α used in ψ.

We consider the Fischer-Ladner closure of ψ, cl(ψ) (see Def. 3.3). 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 define it as follows:

Lean(ψ) = { a | a ∈ {1, 2, 1, 2}} ∪ Σ(ψ) ∪ { a ϕ | a ϕ ∈ cl(ψ)}
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).

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

A type intuitively represents the conjunction of all formulas in t together with the negations of all formulas in its complement (however this conjunction formula is never built or even considered as such in the algorithm: only the sets are manipulated).

Fig. 6 gives derivation rules defining a binary relation between formulas ϕ ∈ cl(ψ) and pairs (T, F ) of subsets of Lean(ψ). The meaning of ϕ ⇐= (T, F ) is that whenever all formulas in T are true and all formulas in F are false, ϕ is true.

Because we have restricted ourselves to cycle-free formulas, the derivations in Fig. 6 are finite. Indeed, the formulas in the premises are always reachable from the formula in the conclusion following an ε-labelled edge in the syntactic graph. It can therefore not loop, and we know that cl(ψ) is finite. Definition 4.2. Let ϕ ∈ cl(ψ), and let t ∈ Types(ψ). We say that ϕ is true at type t or that t implies ϕ, written ϕ ∈ t, if there exist (T, F ) such that ϕ ⇐= (T, F ) and

T ⊆ t ⊆ Lean(ψ) \ F .
ϕ ∈ t means that whenever all formulas in t are true and all formulas in its complement are false, ϕ is true.

We next define a compatibility relation between types to state that two types are related according to a modality.

Efficiently Deciding µ-calculus with Converse over Finite Trees A:15

T 3 | | | T 2 | | | T 1 | | |
a ∈ {1, 2, 1, 2}, written ∆ a (t, t ), iff ∀ a ϕ ∈ Lean(ψ), a ϕ ∈ t ⇔ ϕ ∈ t ∀ a ϕ ∈ Lean(ψ), a ϕ ∈ t ⇔ ϕ ∈ t
Note that we have ∆ a (t, t ) ⇔ ∆ a (t , t). Only ∆ 1 and ∆ 2 are used in the algorithm.

The Algorithm

4.2.1. General idea.
Recall that the models of formulas are focused trees consisting of a tree and a context. We say that a formula is 'partially satisfied' by a tree if, informally, the tree would satisfy the formula provided an appropriate context is added (such a context may however not exist).

The algorithm works by enumerating all partially satisfiable ψ-types, in a bottom-up order: it first considers all types which are partially satisfied by leaves, then incrementally uses the already known partially satisfiable types and the compatibility relation ∆ to find types which require a deeper tree to be partially satisfied, as illustrated by Fig. 7.

Whenever a type that does not contain 2 nor 1 is found to be partially satisfiable, then it is actually satisfiable (by adding Top as the context). If such a type furthermore implies ψ (ψ ∈ t), then ψ is satisfied by at least a focused tree with context Top, which is what we want.

If no such type is found, the algorithm stops when it has enumerated all partially satisfiable types and concludes that ψ does not have a model of the form τ Top .

4.2.2. Formal description. The main iteration is as follows:

X ← ∅ repeat X ← X X ← Upd(X ) if FinalCheck(X) then return "ψ is satisfiable" until X = X return "ψ is unsatisfiable"
where X is the set of partially satisfiable types found so far and the update operation Upd(•) and success check operation FinalCheck(•) are defined as follows.

Upd(X) def = X ∪ t ∈ Types(ψ) 1 ∈ t ⇒ ∃t 1 ∈ X, ∆ 1 (t, t 1 ) ∧ 2 ∈ t ⇒ ∃t 2 ∈ X, ∆ 2 (t, t 2 ) FinalCheck(X) def = ∃t ∈ X, ψ ∈ t ∧ 1 / ∈ t ∧ 2 / ∈ t
The update operation constructs new types from the existing ones, using the ∆ relations. At each step of the algorithm, FinalCheck(X) 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 call X i the set X after i iterations, and T i the set of types added to X at the ith iteration (so T i = X i \X i-1 ). Remark that the types in T i can only be partially satisfied by trees of depth at least i (otherwise they would have been added earlier).

Example Run of the Algorithm.

To illustrate the algorithm, imagine we want to test the satisfiability of the formula:

ϕ = 1 α ∧ ¬ 1 α ∧ 1 µZ.α ∨ 2 Z.
We write η for the subformula µZ.α ∨ 2 Z. First, ¬ 1 α is converted into the core syntax and the plunged formula ψ is computed:

ψ = µX. 1 X ∨ 2 X ∨ ( 1 α ∧ ( 1 ¬α ∨ ¬ 1 ) ∧ 1 η).
Then Lean(ψ) is computed:

Lean(ψ) = { 1 , 2 , 1 , 2 , α, 1 ψ, 2 ψ, 1 α, 1 ¬α, 1 η, 2 η}
We then enter the main iteration with an initially empty set X 0 : Upd(X 0 ):

The types added during the first pass are all those which do not contain 1 nor 2 . Because we only consider types and not arbitrary subsets of the lean, they also do not contain any formula starting with 1 or 2 ; furthermore, a type cannot contain 1 α without 1 , and cannot contain both 1 and 2 . Given all this, we can find 8 types that are partially satisfied by leaves:

X 1 = {∅, {α}, { 1 }, { 2 }, {α, 1 }, {α, 2 }, { 1 α, 1 }, {α, 1 α, 1 }}
FinalCheck(X 1 ): We have:

ψ ∈ t iff either    1 ψ ∈ t or 2 ψ ∈ t or 1 α ∈ t and 1 η ∈ t and [either] 1 ¬α ∈ t [or 1 / ∈ t]
3 Given this, we can see that there are no types t in X 1 such that ψ ∈ t, so we continue iterating.

Upd(X 1 ):

Since X is not empty anymore, we now need to compute the ∆ relations. We have:

η ∈ t iff either α ∈ t or 2 η ∈ t
As remarked before, no types in X 1 are such that ψ ∈ t. However there are types such that η ∈ t: they are exactly all the types containing α.

One example of type in

T 2 is t 2 = { 2 , 2 α, 2 η, 1 }. Indeed, t 1 = {α, 2 } is such that ∆ 2 (t 2 , t 1 ) holds.
FinalCheck(X 2 ): X 2 is too big to write here, but from what we remarked about X 1 , we know that no type in X 2 can contain 1 ψ or 2 ψ or both 1 η and 1 ¬α; hence there is still no type in X 2 such that ψ ∈ t.

Upd(X 2 ): At the third iteration, one of the types which will be added is

t 3 = { 1 , 1 ¬α, 1 η, 1 , 1 α}. Indeed, we have ∆ 1 (t 3 , t 2 ).
FinalCheck(X 3 ): We can check that ψ ∈ t 3 ; however, t 3 contains a pending backward modality 1 , so we cannot conclude yet. Since ψ was not true at any type in X 2 , there are no types in X 3 which contain either 1 ψ or 2 ψ, so FinalCheck still fails.

Upd(X 3 ): Finally, at the fourth iteration, the type t 4 = {α, 1 , 1 ψ} will be added since ∆ 1 (t 4 , t 3 ) holds. This type has now been proved partially satisfiable, and since it has no pending backward modalities, it is satisfiable.

FinalCheck(X 4 ): We also have ψ ∈ t 4 and therefore the algorithm now concludes that ψ is satisfiable, and thus the initial formula ϕ as well.

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 4.4 (CORRECTNESS). The algorithm decides satisfiability of cycle-free closed L µ formulas over finite focused trees.

4.3.1. Termination. For ψ ∈ L µ , since cl(ψ) is a finite set, Lean(ψ) and P(Lean(ψ)) are also finite. Furthermore, Upd(•) is monotonic and X ⊆ P(Lean(ψ)), therefore the algorithm terminates.

To finish the proof, it thus suffices to prove that: whenever the algorithm answers SAT, the formula is indeed satisfiable (soundness); and whenever the formula is satisfiable, the algorithm correctly answers SAT (completeness). Remark 4.6. Whenever ϕ ⇐= (T, F ) holds, F does not contain any formula of the form a χ with χ = ; indeed, it would imply that ϕ contains a subformula of the form ¬ a χ, which is not part of the core syntax (it is only defined as syntactic sugar).

We call 'negatable' the formulas in Lean(ψ) which are not of this form, i.e. the for-

mulas in { a | a ∈ {1, 2, 1, 2}} ∪ Σ(ψ).
We now define two structures, trees of types and dependency graphs, which will allow us to reason about the sets of types the algorithm builds, by making explicit the links between the types induced by the ∆ relations.

A forward path is a path that only mentions forward modalities. We define a tree of types T as a binary tree whose nodes are types. We write T (•) for the type at the root of the tree; T 1 and T 2 are respectively the left and right subtrees if they exist, and more generally, for a forward path p, T p is the subtree reached by navigating in T from the root following path p. A tree of types is consistent iff for every forward path p and every program a ∈ {1, 2, 1, 2}:

a ∈ T p (•) implies that T p • a is defined, and -if T p and T p • a are both defined then ∆ a (T p (•), T p • a (•)) holds.

The first condition notably implies that if T is consistent, then its root node T (•) contains neither 1 nor 2 . This structure is related to the result of the algorithm in the following way: LEMMA 4.7. Let t ∈ X n such that 1 / ∈ t and 2 / ∈ t. Then there exists a consistent tree of types T such that T (•) = t.

PROOF. We can show by a straightforward induction on n the slightly different property that for all t ∈ X n , there exists a tree of types T , such that T (•) = t, which satisfies all the consistency conditions except possibly, at the root node and for a ∈ {1, 2}, the one which says T a must exist if a ∈ T (•). This corresponds to the possible 'pending backward modalities'.

Then we just have to notice that the hypotheses 1 / ∈ t and 2 / ∈ t make that last consistency condition satisfied.

Given a consistent tree of types T , we define a dependency graph whose nodes are all pairs (p, ϕ) where p is a path such that T p is defined and ϕ is either a formula in t = T p (•) or the negation of a negatable formula in the complement of t. The directed edges of the graph are labelled with modalities consistent with the tree. For every (p, ϕ) in the nodes we build the following outgoing edges:

-ϕ ∈ Σ(ψ) ∪ ¬Σ(ψ) ∪ { a , ¬ a }: no edge -ϕ = a ϕ , with ϕ = : let t = T p (•). We have a ϕ ∈ t and t is a type, therefore a ∈ t; thus, since T is consistent, T p • a is defined: let t = T p • a (•).
We have ∆ a (t, t ), which implies ϕ ∈ t , hence there exist T, F such that ϕ ⇐= (T, F ) with T a subset of t , and F a set of negatable formulas not in t . For every ϕ T ∈ T we add an a-labelled edge to (p • a, ϕ T ), and for every ϕ F ∈ F we add an a-labelled edge to (p • a, ¬ϕ F ).

LEMMA 4.8. The dependency graph of a consistent tree of ψ-types (where ψ is cyclefree) is cycle-free.

PROOF. First notice that whenever we have ϕ ⇐= (T, F ), all the formulas in T and all the ¬χ for χ ∈ F are reachable from ϕ, in the syntactic graph, following only εlabelled edges. Thus any walk in the dependency graph corresponds to a walk with the same trace in the syntactic graph.

Furthermore, whenever there is a walk in the dependency graph from (ϕ, p) to (ϕ , p ), its trace is p • p (straightforward induction).

Thus if there were a cycle in the dependency graph, i.e. a nonempty walk from (ϕ, p) to (ϕ, p), then there would be a nonempty walk in the syntactic graph from ϕ to ϕ with trace ε, thus ϕ would not be cycle-free. But all ϕ in the dependency graph belong to cl(ψ) and ψ is cycle-free, hence they must be cycle-free as well; thus there cannot be a cycle in the dependency graph. LEMMA 4.9. Let T be a consistent tree of ψ-types. Then there exists a focused tree ft whose context is Top and such that, for all nodes (p, ϕ) in the dependency graph of T , ft p is defined and ft p ∈ ϕ .

Efficiently Deciding µ-calculus with Converse over Finite Trees A:19 PROOF. We first describe how ft is built: first, inductively, we associate a tree to each node of T , starting from the leaves. The tree associated with T p is (L, st 1 , st 2 ), where:

-L = T p (•) ∩ Λ st a is either the tree associated with T p • a if it is defined or nil if it is not.

We then add context Top to the tree associated with T to obtain our focused tree ft.

We now show that this ft satisfies the condition we want, by induction on the dependency graph, which we know is finite and has no cycles. More precisely, we show by a case analysis on ϕ that if the property is true of all nodes directly reachable from (p, ϕ), then it is true of (p, ϕ) as well: LEMMA 4.10 (SOUNDNESS). If there exists t in X n such that ψ ∈ t, 1 / ∈ t and 2 / ∈ t, then there exists a focused tree ft, whose context is Top, such that ft ∈ ψ .

-ϕ = α. In this case, α ∈ T p (•) ∩ Λ,
PROOF. We know from Lemma 4.7 that there exists a consistent tree of ψ-types T such that T (•) = t. Furthermore, we know from Lemma 4.9 that there exists a focused tree ft whose context is Top and such that for all nodes (p, ϕ) in the dependency graph of T , ft p ∈ ϕ . We consider the particular case p = ε: there are nodes (ε, ϕ) for all ϕ in t and for the negations of all negatable formulas in Lean(ψ) \ t, and for all these nodes we have ft ∈ ϕ . Since we have ψ ∈ t, we can conclude from Proposition 4.5.

Completeness

LEMMA 4.11 (COMPLETENESS). If there exists a tree τ such that τ Top ∈ ψ , then there exists n such that FinalCheck(X n ) holds.

PROOF. Let N = {τ Top p | p ∈ P }, the set of nodes in τ . For all ft in N , we define type(ft) def ={ϕ ∈ Lean(ψ) | ft ∈ ϕ }. Straightforwardly, type(ft) is a type. We call depth of a focused tree ft the length of the longest forward path p such that ft p is defined. We prove the lemma in several steps:

(1) We first show that for all ϕ ∈ cl(ψ) and all ft ∈ N , if ft ∈ ϕ then ϕ ∈ type(ft). For this, we consider the syntactic graph of ψ and remove all edges not labelled ε (i.e. which leave a formula of the form a ϕ). The resulting graph is typically no longer connected, but has no cycles since ψ is cycle-free, hence we can reason by induction, showing that the property is true for a formula if it is true for all formulas directly reachable from it in this subgraph. We reason by cases on ϕ: -if ϕ = , the result is immediate since ϕ ∈ t is always true.

-if ϕ = ⊥, the result is trivially true since there is no ft ∈ ϕ .

-if ϕ is an atomic proposition or of the form a ϕ , then ϕ ∈ Lean(ψ), by definition of Lean(ψ). Then ft ∈ ϕ implies ϕ ∈ type(ft), by definition of this set, and we also have ϕ ⇐= ({ϕ}, ∅), thus ϕ ∈ type(ft).

-if ϕ = ¬ϕ , with ϕ either an atomic proposition or of the form a , then ϕ ∈ Lean(ψ) and ϕ ⇐= (∅, {ϕ }). If ft / ∈ ϕ , we have ϕ / ∈ type(ft), thus ϕ ∈ type(ft).

-the other cases are straightforward from the induction hypothesis.

(2) We then show that for all ft ∈ N and a ∈ {1, 2}, if ft a is defined then ∆ a (type(ft), type(ft a )) holds. Because of the symmetric way ∆ is defined, it is equivalent to show that for all ft ∈ N and all a ∈ {1, 2, 1, 2}, if ft a is defined then: ∀ a ϕ ∈ Lean(ψ), a ϕ ∈ type(ft) ⇔ ϕ ∈ type(ft a ). We prove the two directions of the equivalence: -If a ϕ ∈ type(ft), then ft ∈ a ϕ . Therefore, ft a ∈ ϕ . From step (1) we then conclude ϕ ∈ type(ft a ). -If ϕ ∈ type(ft a ), then let (T, F ) be such that ϕ ⇐= (T, F ) and T ⊆ type(ft a ) ⊆ Lean(ψ) \ F . By definition of type(ft a ), we have ft a ∈ χ for all χ in T and ft a / ∈ χ for all χ in F . From this, Proposition 4.5 allows us to deduce ft a ∈ ϕ , which implies ft ∈ a ϕ , which in turn implies a ϕ ∈ type(ft) since a ϕ ∈ Lean(ψ).

(3) We now show by induction on n that all ft ∈ N of depth strictly less than n are such that type(ft) ∈ X n . This property is trivially true for n = 0. Suppose now that it is true of n and let ft ∈ N be of depth n (or less). Then for a ∈ {1, 2}, either ft a is undefined or it has depth strictly less than n. In the first case, we have ft / ∈ a , thus type(ft) does not contain a and therefore trivially satisfies the condition relative to a in Upd(X n ). In the second case, by induction hypothesis we have type(ft a ) ∈ X n , and by step (2) above we have ∆ a (type(ft), type(ft a )), so the condition is fulfilled as well. This is true for both as, so in the end we have type(ft) ∈ Upd(X n ) = X n+1 .

(4) Finally, if n is the depth of τ plus one and t = type(τ Top ), we have t ∈ X n . Since both τ Top 1 and τ Top 2 are undefined, t contains neither 1 nor 2 . Furthermore, since τ Top ∈ ψ , we have from step (1) that ψ ∈ t. Therefore FinalCheck(X n ) holds.

4.3.4. Complexity. We now present one of the main contributions of this paper: the complexity of our algorithm is 2 O(n) where n is the formula size. It is well-known that cl(ψ) is a finite set and its size is linear with respect to the size of ψ (i.e., the number of operators and propositional variables appearing in ψ) [START_REF] Kozen | Results on the propositional µ-calculus[END_REF]]. Therefore |Lean(ψ)| is also trivially linear with respect to the size of ψ. THEOREM 4.12 (COMPLEXITY). For ψ ∈ L µ , closed and cycle-free, the satisfiability problem ψ ∅ = ∅ is decidable in time 2 O(n) where n = |Lean(ψ)|.

PROOF. |Types(ψ)

| is bounded by |P(Lean(ψ))| which is 2 O(n) . During each iteration, the algorithm adds at least one new type (otherwise it terminates), thus 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

* 2 O(n) * 2 O(n) = 2 O(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 ϕ ∈ t are simple inclusion and disjunction tests. The FinalCheck condition tests at most 2 O(n) ψ-types and each test takes at most 2 O(n) . 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. Our implementation is publicly available and usable through a web interface [Genevès et al. 2014].

Efficiently Deciding µ-calculus with Converse over Finite Trees A:21

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

We introduce a bit-vector representation of ψ-types: 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 ⊆ P(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 =                  1 if ϕ = 0 if ϕ = ⊥ t i if ϕ ∈ Lean(ψ) status ϕ ( t) ∧ status ϕ ( t) if ϕ = ϕ ∧ ϕ status ϕ ( t) ∨ status ϕ ( t) if ϕ = ϕ ∨ ϕ ¬status ϕ ( t) if ϕ = ¬ϕ status unfold(ϕ) ( t) if ϕ = µ(X i = χ i ) in ξ
We use a → b to denote the implication and a ↔ b to denote the equivalence of two Boolean formulas a and b over bit vectors. 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 [ χ T ( y) ∧ ∆ a ( x, 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 either the satisfiability condition is met or a fixpoint is reached. The satisfiability condition is met if ψ is present in a ψ-type of T 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.

Conjunctive Partitioning and Early Quantification

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

∃ y [ χ T ( 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 χ T ( 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) = ∃ χ T ( 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 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.

Online Implementation

The system has been implemented as a web application. Interaction with the system is offered through a user interface in a web browser. The tool is available online from:

http://wam.inrialpes.fr/websolver/ Table I indicates how the syntax used in this paper translates into the syntax understood by our solver, which we also use in some examples in the next section.

EXAMPLES AND EXPERIMENTS

In this section we report on practical experiments that we have made using the solver implementation. These experiments can be tried with the online implementation described above.

A:24

Pierre Genev ès et al. We already defined as syntactic sugar the negation of an arbitrary closed formula, in Section 3. We add equivalence ⇔, implication ⇒ and the universal modalities [a] as follows:

ϕ ⇒ ψ def = ¬ϕ ∨ ψ ϕ ⇔ ψ def = (¬ϕ ∨ ψ) ∧ (ϕ ∨ ¬ψ) [a] ϕ def = ¬ a ∨ a ϕ 6.1.2. Node names.
A very common constraint in tree-like data models is that each node should be named, i.e. bear exactly one name σ from some set Σ. In order to state properties of such structures, we need atomic propositions corresponding to these names: σ, meaning the name of the current node is σ. These name-propositions behave like label-propositions except for the additional constraint that exactly one of them must be true for each node; because any given formula contains only a finite number of name-propositions, it is possible to encode this additional constraint as a formula. When checking the satisfiability of a formula containing such name-propositions, we can thus generate the formula corresponding to this labeling constraint, conjunct it with the plunged formula and then treat all atomic propositions in the same way in the satisfiability-checking algorithm. This is implemented as follows: given ϕ, let names(ϕ) be the set of all names appearing in ϕ, plus an additional atomic proposition σ x not in ϕ, to represent all other possible names. The labelling-requirement formula is defined as follows:

lab-req(ϕ) def = σ∈names(ϕ)   σ ∧ σ ∈names(ϕ)\{σ} ¬σ  
The formula fed to the main algorithm is then:

ψ def = (µX.ϕ ∨ 1 X ∨ 2 X) ∧ (µY.lab-req(ϕ) ∧ [1] Y ∧ [2] Y ).
Note that the cost of this additional constraint on the size of the lean is only 3. Indeed, lab-req(ϕ) contains no modality and the only atomic proposition it contains which is not already in ϕ is σ x ; then two modalities are added in the final formula. Thus names are not more expensive to use than regular atomic propositions.

6.1.3. Node identifiers (a.k.a. nominals). Another useful kind of constrained proposition is nominals, which must be true at exactly one node of any given tree. They typically allow relating formulas by constraining two nodes reached in different ways to be the same one. Similarly to node names, nominals can be implemented as regular atomic propositions provided the plunged formula is conjuncted with a global constraint stating unicity4 . Given a nominal n, we define the following formulas:

nowhere(n) def = µX.¬n ∧ [1] X ∧ [2] X here(n) def = n ∧ [1] nowhere(n) ∧ [2] nowhere(n) somewhere(n) def = µY.here(n) ∨ (¬n ∧ (( 1 Y ∧ [2] nowhere(n)) ∨ ([1] nowhere(n) ∧ 2 Y )))
To enforce the constraint, it is sufficient to conjunct the formula ψ (defined in Sec. 6.1.2 above) with the formula somewhere(n) for each nominal n appearing in ϕ. This increases the size of the lean by 4 for each nominal (four modalities corresponding to the two 'nowhere's and the two 'somewhere's), thus is significantly more costly than simple atomic propositions. It is however still linear in terms of the original formula, so this extension does not modify the order of complexity of the algorithm.

Regular Language Equivalence

As a first, simple, application, we show how we can use our solver to decide the equivalence of regular languages. To this end, we translate regular expressions in formulas of our tree logic. The translation presented here is similar to the one described by [START_REF] Lange | Weak automata for the linear time µ-calculus[END_REF]; the actual translation used in the online implementation (using the reg exp keyword) contains additional optimizations for conciseness.

As illustrated in Section 2, our model does not allow the empty tree. To translate regular expressions which may recognize the empty word, we add a final letter e at the end of the expression. We also need to be careful with the repetition of regular expressions, of the form R * , if R is nullable (it accepts the empty word ε). A direct translation in this case would result in a recursion variable appearing naked (i.e., without a surrounding modality). We thus extract the non-null part of R, written R ε , and translate R * as R * ε . We first recall how to naively extract from a regular expression R its nullable part (either ε or ∅), written R ε , and its non-null part.

ε ε = ε ε ε = ∅ a ε = ∅ a ε = a (R.R ) ε = R ε .R ε (R.R ) ε = R ε .R ε ∨ R ε .R ε ∨ R ε .R ε (R * ) ε = ε (R * ) ε = (R ε ) + (R ∨ R ) ε = R ε ∨ R ε (R ∨ R ) ε = R ε ∨ R ε
The translation of a regular expression R with a continuation c is written R c and is defined as follows.

a c = a ∧ 1 c ε c = c R.R c = R R c R * c = µx.c ∨ R ε x if R ε = ∅ R * c = c if R ε = ∅ R ∨ R c = R c ∨ R c
Given a regular expression R, we translate it into our logic as the formula R e . To check the equivalence of two regular expressions R 1 and R 2 , we need to check the validity of the formula ( R 1 e ⇐⇒ R 2 e ) (i.e. we want this equivalence to hold for all focused trees). Since our solver is a satisfiability solver, we ask it the question ¬( R 1 e ⇐⇒ R 2 e ). If the formula is unsatisfiable, the languages are equivalent. If it is satisfiable, the solver will return a model of this formula, i.e. a tree representing a word in one language and not the other.

We illustrate this translation with an example. To show that the languages (ab) * a and a(ba) * are equivalent, we run the following query in the solver. (This code may be copied and pasted directly in the online demo.)

( let $X = (a & <1>e) | a & <1>(b & <1> $X) in $X) <=> (a & <1> (let $X = e | b & <1>(a & <1> $X) in $X))
We now extend our simple translation to study the equivalence of languages of Kleene Algebra with Test (KAT) [START_REF] Genev | Kleene algebra with tests[END_REF]].

We extend our translation with a case for boolean propositions α:

α c = α ∧ c ¬α c = ¬α ∧ c
Note that, unlike the translation for letters, we do not move to the next letter. One may thus specify several propositions that must concurrently be true.

As an example, consider the usual encoding of a while loop in KAT.

(αa) * ¬α e = µx.(¬α ∧ e) ∨ (α ∧ a ∧ 1 x)

We can thus use the solver to test for language equality or inequality. In the solver, boolean propositions α are represented by identifiers starting with an underscore. For instance, one may show that βq * is different from (βq) * as follows.

(_b & (let $X = e | q & <1>$X in $X) <=> let $X = e | _b & q & <1>$X in $X)
The satisfying word found is e ~_b, which is the empty word annotated with the negation of _b: it belongs to the second language but not to the first.

Applications to the analysis of XPath queries

Another natural application of the tree logic consists in the static analysis of programs that manipulate XML documents seen as trees. Backward modalities naturally capture XPath expressions that navigate upward in the tree in a succinct manner. The translations of XPath and XML type expressions into the logic are recalled from Genevès [START_REF] Genev Ès | A system for the static analysis of XPath[END_REF] in an appendix to make the article self-contained. We also give the semantics of XPath in terms of focused trees, and prove that the generated formulas are cycle-free. Owing to these translations, we can formulate several decision problems involving XPath expressions e 1 , ..., e n and XML type expressions T 1 , ..., T n , for which the solver provides a decision procedure. In particular, the following basic problems are of special interest:

-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 -Static type checking of an annotated XPath expression:

E → e 1 T1 ∧ ¬ T 2 (if 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 expression has to change as well.)

We carried out extensive tests with the implementation [Genevès et al. 2014], 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 Fig. 8 (where "//" is used as a shorthand for "/desc-or-self::*/") and XML types shown on Table II. Table III 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 µ .

The first XPath containment instance was first formulated by [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.

CONCLUSION

We showed that the collapsing of the least and greatest fixpoints on acyclic structures [START_REF] Mateescu | Local model-checking of modal µ-calculus on acyclic labeled transition systems[END_REF]] could be extended to trees with converse modalities by restricting the language to cycle-free formulas. We were able to leverage this property to obtain an efficient implementation.

We also emphasize that the fact that the algorithm is implemented as a least fixpoint construction makes it possible to check for satisfiable formulas as soon as possible, often not requiring the full fixpoint to be computed, as opposed to algorithms based on greatest fixpoint computations that must eliminate all contradictions and therefore complete the computation of the fixpoint all the time. The main result of our paper is a sound and complete satisfiability-testing algorithm for a sub-logic of the alternation-free modal µ-calculus with converse for finite trees. The algorithm operates in time complexity 2 O(n) in the size n of a formula. It has been implemented and is available online.

As a direction for future work, we plan to study the extension of the logic with counting operators. We have started this investigation for a restricted form of counting and interleaving [START_REF] Barcenas | Query reasoning on trees with types, interleaving and counting[END_REF]], which we want to extend to the full logic. As another perspective, notice that it is possible to configure the solver such that, instead of computing one satisfying tree for a satisfiable formula, it computes a regular tree type representation of the set of all satisfying trees. Such a representation could be used in the setting of rich type systems for programming and query languages such as XQuery [START_REF] Boag | XQuery 1.0: An XML query language[END_REF] and CDuce [START_REF] Benzaken | CDuce: An XML-centric general-purpose language[END_REF]].

Efficiently Deciding µ-calculus with Converse over Finite Trees A:29

A. XPATH AND REGULAR TREE LANGUAGES

A.1. XPath

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 toplevel "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.

For the practical experiments, we consider an XPath fragment covering all major features of the XPath 1.0 recommendation [START_REF] Clark | XML path language (XPath) version 1.0, W3C recommendation[END_REF] with the exception of counting and comparisons between data values.

Fig. 9 gives the syntax of XPath expressions.

L qualified path | a::σ step with node test | a:: * step Qualif q ::= 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

A.2. Focused Tree Interpretation of XPath

XML documents have the structure of unranked n-ary trees where the children of a node are ordered. This structure can be represented by a binary tree if we relate a node directly only to its first child and its next sibling, if any. To formalise this, we give below a syntax for n-ary trees: The translation of a single n-ary tree t can then be defined as: bintree(t) def = bintree(t :: ε).

Note that this is not a bijection since the root of the resulting binary tree never has a right child.

We now describe how XPath expressions can be interpreted in terms of focused trees. XPath expressions can be absolute, starting from the root of the document, or relative, starting from a set of nodes called context nodes. In order to solve the query containment problem for relative XPath expressions, we mark all the context nodes with a distinguished label which we call the 'start mark'. This start mark allows us to compare XPath expressions from a common initial set of context nodes (so that we obtain in logical terms that the XPath expression "descendant:: * " is not contained in the XPath "child:: * ", which we would not find if we replaced the start mark by the formula " "). The precise data domain we consider is thus the set F * of focused trees whose root has no right child, where each node has exactly one name σ from Σ5 , and where at least one node bears the start mark in addition. For a focused tree ft = (L, st 1 , st 2 ) c , we write name(ft) for the unique σ ∈ L ∩ Σ.

Fig. 10 gives the interpretation of XPath expressions as functions between sets of such focused trees.

A.3. 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 Fig. 11. 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.

S p p 1 /p 2 F def = S p p 2 (Sp p1 F ) S p p[q] F def = {ft ∈ S p p F | S q q ft } S p a::σ F def = {ft ∈ S a a F | name(ft) = σ} S p a:: * F def = S a a F S q • • : Qualif → F * → {true, false}
S q q 1 and q 2 ft def = S q q 1 ft ∧ S q q 2 ft S q q 1 or q 2 ft def = S q q 1 ft ∨ S q q 2 ft S q not q ft Logical Interpretation of Expressions. Fig. 12 gives the translation of XPath expressions into L µ . The translation function "E → e χ " takes an XPath expression e and a L µ formula χ as input, and returns the corresponding L µ translation. The translation of a relative XPath expression marks the initial context with . The translation of an absolute XPath takes as initial context a formula saying that we are at the root (¬ 1 ∧ ¬ 2 ) and that the previous context ( ∧ χ) can be anywhere below. The parameter χ in the translation allows straightforward composition of XPath expressions. For the whole expression, the initial χ is the formula µZ.(¬ 1 ∧¬ 2 ∧ ¬ 2 ) ∨ 1 Z ∨ 2 Z, which states that the root has no right child, as required by our interpretation domain F * . Fig. 13 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.

def = ¬ S q q ft S q p ft def = S p p {ft} = ∅ S a • • : Axis → P(F * ) → P(F * ) S a a ∅ def = ∅ S a self F def = F S a child F def = F 1 ∪ S a foll-sibling F 1 S a foll-sibling F def = F 2 ∪ S a foll-sibling F 2 S a prec-sibling F def = F 2 ∪ S a prec-sibling F 2 S a parent F def = F 1 ∪ S a parent F 2 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 ) ) root(∅) def = ∅ root(F ) def = {τ Top ∈ F } ∪ root(F 2 ) ∪ root(F 1 )
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 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 χ
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. The fact that the L µ logic is equipped with both forward and converse programs is important for supporting XPath6 . 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.

Efficiently Deciding µ-calculus with Converse over Finite Trees A:33 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 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 Fig. 14, 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 χ.

E → • • : L XPath → L µ → L µ E → /p χ def = P → p ((¬ 1 ∧¬ 2 )∧(µ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 χ
∧ (µX. 1 (χ ∧ ) ∨ 2 X) ϕ ∧ 1 µY.b ∨ 2 Y ψ χ 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.

A:34 Pierre Genev ès et al. The translation of paths inside qualifiers is also given in Fig. 14. 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).

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) χ
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 A.4 where we show that every regular tree language may be translated to an L µ formula. PROPOSITION A.1 (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 ϕ 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. Fig. 15 illustrates this on an typical example. Finally, formal translations do not duplicate any subformula of arbitrary length.

A.4. 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 types into L µ . Regular tree types gather most of the schemas occuring in practice [Murata et al. 2005] 7 . 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:

L BT T ::= tree type expression ∅ empty set | ε leaf | T 1 T 2 union | L(X 1 , X 2 ) label | let X i .T i in T binder
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 → L µ T def = ⊥ for T = ∅, ε T 1 T 2 def = T 1 ∨ T 2 L(X 1 , X 2 ) def = L ∧ succ 1 (X 1 ) ∧ succ 2 (X 2 ) let X i .T i in T def = µ(X i = T i ) in T
where 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, Fig. 17 gives the translation of a DTD fragment of the Wikipedia encyclopedia [START_REF] Voss | Wikipedia dtd[END_REF]] shown on Fig. 16.

let $X11=(interwiki & ~<1>T & (~<2>T | <2>($X11 | (history & ~<2>T & <1>$X6)))), $X6=(edit & (~<1>T | <1>(status & ~<1>T & (~<2>T | <2>($X8 | (text & ~<1>T & ~<2>T) | (redirect & ~<1>T & ~<2>T))))) & (~<2>T | <2>$X6)), $X8=(interwiki & ~<1>T & (~<2>T | <2>($X8 | (text & ~<1>T & ~<2>T) | (redirect & ~<1>T & ~<2>T)))) in (article & <1>(meta & <1>(title & ~<1>T & (~<2>T | <2>($X11 | (history & ~<2>T & <1>$X6) | (status & ~<1>T & (~<2>T | <2>($X11 | (history & ~<2>T & <1>$X6))))))) & <2>((text & ~<1>T & ~<2>T) | (redirect & ~<1>T & ~<2>T))))
Fig. 17. The Lµ Formula for the DTD of Fig. 16.

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

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.

B. PROOFS OF AUXILIARY LEMMAS FROM SEC. ??

PROOF OF LEMMA 3.7. By structural induction on ϕ.

-If ϕ = , α, ¬α or ¬ a , then ϕ V does not depend on V , so the result is immediate.

-If ϕ = X then X is one of the X i , and ϕ and X are the same vertex in the syntactic graph, so X is reachable from ϕ by following the empty walk. We have ϕ V = V (X) ε , so the result is again immediate.

-If ϕ = ϕ 1 ∨ϕ 2 , the induction hypothesis tells us that ϕ 1 V and ϕ 2 V are of the appropriate union of intersections form. The union of these two unions is a larger union, of the form k∈K1∪K2 A k ∩ l∈L k V (X j l ) p l where for each l there exists a walk w l which starts either at ϕ 1 or at ϕ 2 , which terminates at X j l , and whose trace is p l . Since there are edges labelled ε from ϕ to both ϕ 1 and ϕ 2 , by following the appropriate one and then w l we obtain, for each l, a walk from ϕ to X j l whose trace is ε • p l = p l .

-If ϕ = ϕ 1 ∧ ϕ 2 , we use the induction hypothesis again and use distributivity to get ϕ V as a union of intersections again: we get ϕ V = (k,k )∈K1×K2 A k ∩ A k ∩ l∈L k ∪L k V (X j l ) p l . It is thus of the appropriate form and the reasoning on walks is then the same as in the previous case.

-If ϕ = a ψ, then there is an edge from ϕ to ψ labelled a. By induction hypothesis we have ψ V = k∈K A k ∩ l∈L k V (X j l ) p l where the p l are traces of walks from ψ to X j l . This yields ϕ V = ψ V a = k∈K A k a ∩ l∈L k V (X j l ) p l a . We conclude by remarking that : -V (X j l ) p l a = V (X j l ) p l • a ∩ F * p l a (see Remark 2.3).

-The sets F * p l a do not depend on V , nor do the A k a . We can define A k = A k a ∩ l∈L k F * p l a . p l • a = a • p l and a • p l is the trace of a walk from ϕ to X j l .

-If ϕ = ι(Y i = ϕ i ) i∈J in ψ, we consider, for all i ∈ J, the formulas ψ i = ι(Y j = ϕ j ) j∈J in ϕ i . They have the following property: unfold(ψ i ) = ϕ i {( ψ k / Y k ) k∈J }. Thus, each walk from ϕ i to an X k straightfowardly translates into a walk from unfold(ψ i ) to X k , and each walk from ϕ i to an Y k straightforwardly translates into a walk from unfold(ψ i ) to ψ k . Furthermore, there is an ε-labelled edge from ψ i to unfold(ψ i ), so these walks can be prolongated to start from ψ i while keeping the same trace. We now proceed in several steps.

(1) We first apply the induction hypothesis to all the ϕ i . The Y i are free in these subformulas, so we get :

ϕ i V = k∈Ki A k ∩ l∈L k V (X j l ) p l ∩ m∈M k V (Y jm ) q m
where for every i ∈ J and every k ∈ K i there is: -for every l ∈ L k , a walk from ϕ i to X j l , and hence also a walk from ψ i to X j l , whose trace is p l ; -for every m ∈ M k , a walk from ϕ i to Y jm and hence also a walk from ψ i to ψ jm , whose trace is q m . (2) We then show by induction on n that for all i ∈ J, (F n (∅, . . . , ∅))(i) is of the form

k ∈K n i C k ∩ h∈H k V (X j h ) r i,h
, where each r i,h is the trace of a walk from ψ i to X j h : For n = 0, we just take K 0 i = ∅ (the empty union yields the empty set). We now suppose that the property is true for n and for all i and pick j ∈ J. By definition, (F n+1 (∅, . . . , ∅))(j) = ϕ j V [Yi →(F n (∅,...,∅))(i)] . Combining step (1) with the induction hypothesis on n, we have that this set is of the form:

k∈Kj   A k ∩ l∈L k V (X j l ) p l ∩ m∈M k k ∈K n jm   C k q m ∩ h∈H k V (X j h ) r jm,h q m    
where: -for each k ∈ K j and l ∈ L k , there is a walk w l from ψ j to X j l such that tr(w l ) = p l ; -for each k ∈ K j and m ∈ M k , there is a walk v m from ψ j to ψ jm such that tr(v m ) = q m ; Efficiently Deciding µ-calculus with Converse over Finite Trees A:39

Using now the induction hypothesis, we get:

k∈K   A k ∩ l∈L k k ∈K j l   A k p l ∩ l ∈L k U j l q l 1 q l 2 • • • q l n p l    
with, for all l , i l 0 = j l and i l n = j l (with the i l m defined as in the lemma's statement). We use distributivity to put this expression in the correct form: for each k ∈ K, let K k = l∈L k K j l ; for a tuple k ∈ K k , let k (l) be its component whose index is l. We obtain that F n+1 (U )(j) is:

k∈K∧k ∈K k A k ∩ l∈L k A k (l) p l ∩ l∈L k ∧l ∈L k (l) U j l q l 1 q l 2 • • • q l n p l
The big intersections are now indexed by pairs (l, l ) such that l ∈ L k and l ∈ L k (l) . We have to check that the property on paths is true for each such pair. Let k ∈ K and let l ∈ L k ; k (l) is an element of K j l , thus for l ∈ K k (l) we have i l n = j l ; we also know that, for m n, q l m ∈ P i l m-1 i l m , and that i l 0 = j l , which is what we want. The last component, p l , has to belong to P i l n j . We know from what precedes that i l n = j l and that p l ∈ P j l j , so we can conclude the induction.

C. DETECTING CYCLE-FREE FORMULAS

Every formula generated from XPath queries or from regular types is cycle-free by construction.

Detecting whether an arbitrary formula is cycle-free or not is not straightforward. However, an approximate detection, that only checks a sufficient condition for the formula to be cycle-free, can be useful and easily implemented in practice.

Let ψ be a formula, and let us consider the set of cyclic walks in the syntactic graph of its closure. We can easily see that any such walk goes through at least one formula of the form ψ j = ι(X i = ϕ i ) i∈I in ϕ j with j ∈ I; so without loss of generality, we can consider only cyclic walks which start and end at such a formula. What we want to know is whether there exists one such walk whose trace reduces to ε. The difficulty is that the shortest such walk may actually be quite long and step several times through the starting point, as illustrated by our example on p. 10 where ε is only reached after following 4 simple cycles. We can however give the following necessary condition for the existence of such a walk:

-either there is a walk from ψ j to ψ j which follows only edges labelled ε, -or there is a walk from ψ j to ψ j , which steps at most once through ψ j in between, in which an edge labelled a and an edge labelled a occur separated only by edges labelled ε.

In other words, either there is a simple cycle which already has trace ε, or a reduction can occur by composing the traces of two simple cycles. If it is not the case, then it is impossible to obtain trace ε by composing simple cycles, thus the formula is cycle-free. This criterion has the advantage that checking it only requires unfolding recursion once.

Although some cycle-free formulas do not meet this criterion, like e.g. µX.(α ∨ 1 X ∨ 1 2 X), the class of formulas which do meet it is large enough for practical purposes. For example, the former formula can be rewritten:

µX.(α ∨ 1 X ∨ ( 1 ∧ 2 X)) ∨ 1 2 µX.(α ∨ 1 X ∨ ( 1 ∧ 2 X)).
∆ Γ R I ϕ ∆ Γ R I ϕ ∆ Γ R I ψ ∆ Γ R I ϕ ∨ ψ ∆ Γ R I ϕ ∆ Γ R I ψ ∆ Γ R I ϕ ∧ ψ ∆ Γ R I ¬ a ∆ (Γ ¡ a) R I ϕ ∆ Γ R I a ϕ ∀j ∈ I. (∆ + X i : ϕ i ) (Γ + X i : ) R\Xi I\Xi ϕ j ∆ Γ R\Xi I∪Xi ψ ∆ Γ R I ι(X i = ϕ i ) 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
Fig. 18. Detecting Cycle-free Formulas Indeed, 2 1 ϕ is equivalent to ⊥ and 1 1 ϕ is equivalent to 1 ∧ ϕ. In Figure 18, we present an inductive relation that detects when a formula does not meet this cycle-freeness criterion. In the judgement ∆ Γ R I ϕ of Figure 18, ∆ 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 { , ⊥, 1, 2, 1, 2}. means that no modality has been encountered yet since the variable was bound; ⊥ means that two converse modalities have been followed in a row; a means that the last modality followed was a and that no two converse modalities have been followed in a row up to now. A formula is rejected if an occurrence of a variable under a fixpoint operator is either not under a modality (in this case Γ(X) = ), or is under a modality sequence containing a a for some a (Γ(X) = ⊥). The following auxiliary operator is used to detect invalid modality sequences:

Γ ¡ a def = {X : (Γ(X) ¡ a)} 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 ) 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 formulas 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 = ∅.

τ

  ::= (L, st, st) binary tree st ::= τ | nil subtree c ::= context Top root of the tree | (L, [], st) c | (L, st, []) c context node ft ::= τ c focused tree Efficiently Deciding µ-calculus with Converse over Finite Trees A:5

Fig. 1 .

 1 Fig. 1. Logic formulas

Fig. 5 .

 5 Fig. 5. Finite interpretation of formulas

Fig. 6 .

 6 Fig. 6. Truth assignment of a formula element with a strictly smaller context than ft. By induction, since contexts are finite, ψ contains at least one element with context Top.

Fig. 7 .

 7 Fig. 7. Algorithm's principle: progressive bottom-up reasoning.

  4.3.2. Soundness. We first relate formally the ⇐= relation to our semantics. PROPOSITION 4.5. For ϕ ∈ cl(ψ), if ϕ ⇐= (T, F ), then we have χ∈T χ \ χ∈F χ ⊆ ϕ . PROOF. Immediate by induction on the derivation yielding ϕ ⇐= (T, F ).

  thus by construction of ft we have ft p ∈ α . ϕ = ¬α. In this case, α / ∈ T p (•) ∩ Λ, thus again by construction we have ft p / ∈ α . ϕ = a (resp. ϕ = ¬ a ). Then by consistency of T , T p • a exists (resp. does not exist), and by construction of ft, so does ft p • a . ϕ = a ϕ . Then T p (•) must contain aas well, and by the argument above T p • a and ft p • a exist. We know from the construction of the dependency graph that there exist T and F such that ϕ ⇐= (T, F ) and that (p, ϕ) has edges going to all nodes (p • a, χ) for χ ∈ T and all nodes (p • a, ¬χ) for χ ∈ F . By induction hypothesis, for all χ in T we have ft p • a ∈ χ , and for all χ in F we have ft p • a / ∈ χ . By Proposition 4.5, this implies ft p • a ∈ ϕ , hence ft p ∈ ϕ .

e 1

 1 Fig. 8. XPath Expressions Used in Experiments.

Fig. 9 .

 9 Fig. 9. XPath Abstract Syntax.

  = (L, tl ) n-ary tree We now define the bintree translation from tree lists tl to subtrees st, and notice that the translation of a nonempty list is always a nonempty subtree: bintree(ε) def = nil bintree((L, tl 1 ) :: tl 2 ) def = (L, bintree(tl 1 ), bintree(tl 2 ))

Efficiently

  Deciding µ-calculus with Converse over Finite Trees A:31 S e • • : L XPath → P(F * ) → P(F * ) S e /p F def = S p p root(F ) S e p F def = S p p {(L,st1,st2) c ∈F | ∈L} 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 → P(F * ) → P(F * )

Fig. 10 .

 10 Fig. 10. Interpretation of XPath Expressions as Functions Between Sets of Focused Trees.

Fig. 11 .

 11 Fig. 11. Translation of XPath Axes.

Fig. 12 .

 12 Fig. 12. Translation of Expressions and Paths.

Fig. 13 .

 13 Fig. 13. XPath Translation Example.

Fig. 14 .

 14 Fig. 14. Translation of Qualifiers.

Fig. 15 .

 15 Fig. 15. Example of Back and Forth -Yet Cycle-Free -XPath Navigation.

  et al. ϕ = , ⊥, α or ¬α

Table I .

 I Concrete syntax used in the online solver

		abstract syntax	concrete syntax
	Atomic proposition	α	_a
	Node name	σ	a
	Variable	X	$X
	True, False	, ⊥	T, F
	Disjunction	ϕ ∨ ψ	ϕ | ψ
	Conjunction	ϕ ∧ ψ	ϕ & ψ
	Negation	¬ϕ	~ϕ
	Backward modality	a ϕ	<-a>ϕ
	Fixpoint	µ(X = ϕ, Y = ψ) in χ	let $X=ϕ, $Y=ψ in χ
	6.1. Syntax Extensions
	6.1.1. Standard Syntactic Sugar.

Table II .

 II Types Used in Experiments.

	Efficiently Deciding µ-calculus with Converse over Finite Trees	A:27
	DTD	Symbols	Binary Type Variables
	SMIL 1.0	19	11
	XHTML 1.0 Strict	77	325

Table III .

 III Results with Some Decision Problems.

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

  Fig. 16. A Fragment of the DTD of the Wikipedia Encyclopedia.

	<!ELEMENT article (meta, (text | redirect))>
	<!ELEMENT meta (title, status?, interwiki*, history?)>
	<!ELEMENT title (#PCDATA)>
	<!ELEMENT interwiki (#PCDATA)>
	<!ELEMENT status (#PCDATA)>
	<!ELEMENT history (edit)+>
	<!ELEMENT edit (status?, interwiki*, (text | redirect)?)>
	<!ELEMENT redirect EMPTY>
	<!ELEMENT text (#PCDATA)>

Here 'optimal' means that we cannot expect a decision procedure with lower time complexity. This is easy to show because the logic can encode the containment problem for finite tree automata.

ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

By 'coincide' on a structure we mean formally: for any ϕ, the sets of nodes of that structure where µX.ϕ holds and where νX.ϕ holds are identical.ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

the case between square brackets is actually incompatible with 1 η ∈ t since t is a type. ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

It might look surprising that we manage to axiomatize nominals in the modal µ-calculus because the hybrid µ-calculus (ie. modal µ-calculus with nominals) has different model-theoretic properties. So how is this possible, in particular since the use of nominals breaks bisimulation-invariance? The answer is: the class of models we consider is not bisimulation-closed because every node has at most one 1-and one 2successor. In fact, nominals are already present in the logic over this class in a hidden form: every node in a tree can be reached by a unique simple path. Thus, the trace of such a simple path in fact acts like the nominal for this node already.ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

We describe how this constraint is implemented in Sec.

6.1.2

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].ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

Notice, however, that we do not consider counting nor interleaving features that can be found in e.g. XML Schemas. These features are beyond the scope of this paper: see B árcenas et al.[2009] for a preliminary work on how to integrate counting constraints in such a logic. ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

ACKNOWLEDGMENTS

We thank the anonymous referees of TOCL for their valuable remarks and suggestions that significantly contributed to improving the presentation of the results described in this publication.

A:38

Pierre Genev ès et al.

-for each i ∈ J, k ∈ K n i and h ∈ H k , there is a walk u i,h from ψ i to X j h such that tr(u i,h ) = r i,h . Similarly to the case of the modality formula above, we use the equality V (X j h ) r jm,h q m = V (X j h ) q m • r jm,h ∩ F * r jm,h q m . We do some distributivity work. For k ∈ K j , we define K k,n = m∈M k K n jm . For a tuple k ∈ K k,n , we write k (m) for its component whose index is m, and we define B k = m∈M k C k (m) q m ∩ h∈H k (m) F * r jm,h q m . We obtain that (F n+1 (∅, . . . , ∅))(j) is of the correct form:

Furthermore, for each l we know that p l = tr(w l ) where w l is a walk from ψ j to X j l , and for each pair (m, h) we can obtain a walk from ψ j to X j h whose trace is q m • r jm,h by concatenating v m and u jm,h . This concludes the induction on n.

(3) We conclude from this induction that the tuple (U j ) j∈J as defined in Fig. 5 is such that each U j is of the form k∈Kj C k ∩ h∈H k V (X j h ) r j,h , with r j,h the trace of a walk from ψ j to X j h (by setting K j = n∈N K n j ). ( 4) We now apply the main induction hypothesis to ψ, to obtain:

By applying the definition of • for a fixpoint formula, we obtain that ϕ V is:

To conclude, we apply distributivity exactly as in step 2 above, noticing that: -in the syntactic graph, there is an edge labelled ε from ϕ to ψ{( ψi / Yi ) i∈J }. Therefore, for each m, since there is a walk from ψ to Y jm with trace q m , there is also a walk w m from ϕ to ψ jm with trace q m ; -for each pair (m, h), concatenating this walk w m with a walk from ψ jm to X j h whose trace is r jm,h yields a walk from ϕ to X j h whose trace is q m • r jm,h ; -similarly, for each l, the walk from ψ to X j l with trace p l yields a walk from ϕ to X j l with the same trace p l .

PROOF OF LEMMA 3.8. We prove the result by induction on n.

For n = 0, we have F 0 (U ) = U , which can be written (F * ∩ U i ) i∈I .

We now suppose the result true for n and show it for n + 1. Let j ∈ I. We have F n+1 (U )(j) = ϕ j Xi →F n (U )(i) . Using Lemma 3.7, we have that this set is of the form k∈K A k ∩ l∈L k F n (U )(j l ) p l , with p l the trace of a possibly empty walk w l from ϕ j to X j l , which translates straightforwardly into a walk w l from ϕ j {( ψi / Xi ) i∈I } to ψ j l . Since there is an ε-labelled edge, in the syntactic graph, which goes from ψ j to ϕ j {( ψi / Xi ) i∈I } , we can construct a nonempty walk w l from ψ j to ψ j l by taking this edge first and then following w l , and this walk still has trace p l ; hence p l ∈ P j l j .