Luca Alberucci

Alessandro Facchini
email: alessandro.facchini@unil.ch

THE MODAL µ-CALCULUS HIERARCHY OVER RESTRICTED CLASSES OF TRANSITION SYSTEMS

We study the strictness of the modal µ-calculus hierarchy over some restricted classes of transition systems. First, we prove that over transitive systems the hierarchy collapses to the alternation-free fragment. In order to do this the finite model theorem for transitive transition systems is proved. Further, we verify that if symmetry is added to transitivity the hierarchy collapses to the purely modal fragment. Finally, we show that the hierarchy is strict over reflexive frames. By proving the finite model theorem for reflexive systems the same results holds for finite models.

.

§1. Introduction. The modal µ-calculus is an extension of modal logics, with least and greatest fixpoint operators. The term "µ-calculus" and the idea of extending modal logic with fixpoints appeared for the first time in the paper of Scott and De Bakker [START_REF] Scott | A theory of programs[END_REF] and was further developed by others. Nowadays, the term "modal µ-calculus" stands for the formal system introduced by Kozen [START_REF] Kozen | Results on the propositional mu-calculus[END_REF]. It is a powerful logic of programs subsuming dynamic and temporal logics like PDL, PLTL, CTL and CTL * . Hence, it provides us with the capability of expressing and reasoning about assertions concerning "temporal" properties of dynamic (reactive and parallel) systems with potentially infinite behavior. We refer to Bradfield and Stirling's tutorial article [START_REF] Bradfield | Modal logic and mu-calculi[END_REF] or Stirling's book [START_REF] Stirling | Modal and Temporal Properties of Processes[END_REF] for a thorough introduction to this system.

The standard semantics of the modal µ-calculus is given by transition systems. As usual, formulae are interpreted as subsets of a system, the set of states where the property expressed by the formula holds. Many natural properties such as "there is an infinite path" can be expressed by a modal µ-formula. Further, most such properties are given by formulae with alternation depth two, where the alternation depth is the number of non-trivial nestings of least and greatest fixpoints. Nevertheless, it is mathematically interesting to see whether the expressive power of the modal µ-calculus increases with the alternation depth. If this is the case then we have a strict hierarchy otherwise we have a collapse at some point.

By a result of Bradfield [START_REF] Bradfield | The Modal µ-calculus Alternation Hierarchy is Strict[END_REF][START_REF] Bradfield | Simplifying the Modal µ-Calculus Alternation Hierarchy[END_REF] the hierarchy over arbitrary transition systems is strict, a result independently proved by Lenzi in [START_REF] Lenzi | A Hierarchy Theorem for the µ-Calculus[END_REF] but only for the positive fragment. Subsequently, Arnold showed in [START_REF] Arnold | The µ-Calculus Alternation-Depth Hierarchy is Strict on Binary Trees[END_REF] that the hierarchy is also strict over binary trees by using the Banach-Cacciopoli fixpoint theorem. His proof Luca Alberucci's research is supported by the Hasler Foundation (Project-Nr.: 2192) Alessandro Facchini's research is supported by a grant from the Swiss National Science Foundation (Project n. 200021-116508: "Topological Complexity, Games, Logic and Automata") 1 has been naturally extended to the class of all models by one of the authors in [START_REF] Alberucci | Strictness of the Modal µ-Calculus Hierarchy[END_REF].

Having seen the strictness over arbitrary transition systems, it can be asked whether the alternation hierarchy remains strict for restricted classes of transition systems such as those that are reflexive or those that are transitive. In the case of transitive systems, to our knowledge, the first attempt to answer this question is presented by Lenzi in [START_REF] Lenzi | The Transitive µ-Calculus is Büchi-definable[END_REF]. There, he shows that on transitive frames every Büchi automaton is equivalent to a co-Büchi automaton, and conversely 1 . This implies that over transitive frames the modal µ-calculus collapses to the level of Büchi automata (and to co-Büchi automata). Because, for example, well-foundedness is not definable in the modal fragment, the hierarchy is non trivial. Thus, since over arbitrary graphs the intersection of Büchi and co-Büchi automata corresponds to the alternation-free fragment, Lenzi conjectured that the full modal µ-calculus collapses to the alternation-free fragment ( [START_REF] Lenzi | Personal Communication[END_REF]). It is interesting to note that Visser has shown in [START_REF] Visser | Uniform interpolation and layered bisimulation[END_REF] that in the case of reflexive and transitive models, where well-foundedness is false and therefore can be expressed by a modal formula, the non-triviality of the fixpoint hierarchy is testified by the formula stating the existence of an infinite path alternately labelled with p, ¬p, p, ¬p, etc.

In this paper we answer positively Lenzi's conjecture for the class of all transitive systems by giving an explicit syntactical translation of the full modal µ-calculus into the alternation-free fragment. This result is first showed for finite transition systems and then generalized, by proving a finite model theorem, to all transitive systems. We also verify, again by giving an explicit syntactical translation, that if we add symmetry to transitivity all collapses to the purely modal fragment. Further, by adapting Arnold's proof for the general case, we show that the hierarchy remains strict over reflexive frames. By proving a finite model theorem for reflexive transition systems the corresponding result holds even on finite models.

In the next section we introduce the modal µ-calculus and some additional, not standard, notions. In Section 3 we introduce evaluation games and show their relevance for the modal µ-calculus. In Section 4 some finite model theorems are proved. In Sections 5 and 6 the collapse of the hierarchy over transitivesymmetric and over transitive systems are proved. In Section 7 we prove the strictness of the hierarchy over reflexive transition systems.

Related work. The question whether the modal µ-calculus hierarchy collapses on special classes of transition systems has been addressed in various other works. A prominent subclass, coming from Gödel-Löb logic, is the class of transitive upward well-founded frames. As shown by Visser in [START_REF] Visser | Löb's Logic Meets the µ-Calculus[END_REF] and van Benthem in [START_REF] Van Benthem | Modal Frame Correspondences and Fixed-Points[END_REF] by using the de Jongh-Sambin fixpoint Theorem, the modal µcalculus collapses to its modal fragment. A direct proof of this result without using de Jongh-Sambin Theorem is given by the authors in [START_REF] Alberucci | On Modal µ-calculus and Gödel-Löb Logic[END_REF]. In [START_REF] Ten Cate | Some Modal Aspects of XPath[END_REF] ten Cate, Fontaine and Litak show that on the class of finite trees with the descendant relation the modal µ-calculus collapses to the modal fragment. Concerning the hierarchy on transitive frames d'Agostino and Lenzi in [START_REF] D'agostino | On the µ-calculus over Transitive and Finite Transitive Frames[END_REF] propose a different proof which uses Theorem 6.5 of this paper. Further, Dawar and Otto in [START_REF] Dawar | Modal Characterisation Theorems over Special Classes of Frames[END_REF] give a characterization of the bisimulation invariant fragment of Monadic Second Order Logic over transitive frames. From their result, by using the Finite Model Theorem for transitive frames (Theorem 4.4), the collapse of the modal µ-calculus follows, too. §2. The propositional modal µ-calculus. In this section we introduce syntax, semantics of the modal µ-calculus and the alternation depth hierarchy.

2.1. Syntax. The language of the modal µ-calculus, L µ , results by adding greatest and least fixpoint operators to propositional modal logic. More precisely, given a set P of propositional variables, the collection L µ of modal µ-formulae (or simply µ-formulae) is defined as follows:

ϕ ::= p | ∼ p | ⊤ | ⊥ | (ϕ ∧ ϕ) | (ϕ ∨ ϕ) | 3ϕ | ϕ | µx.ϕ | νx.ϕ
where p, x ∈ P and x occurs only positively in ηx.ϕ (η = ν, µ), that is, ∼ x is not a subformula of ϕ. L M denotes the pure modal fragment of L µ .

The fixpoint operators µ and ν can be viewed as quantifiers. Therefore we use the standard terminology and notations as for quantifiers and, for instance, free(ϕ) denotes the set of all propositional variables occurring free in ϕ and bound(ϕ) those occurring bound. Further, we define var(ϕ) = free(ϕ)∪bound(ϕ). If ψ is a subformula of ϕ, we write ψ ≤ ϕ. We write ψ < ϕ when ψ is a proper subformula. sub(ϕ) is the set of all subformulae of ϕ.

Let ϕ(x) and ψ be two µ-formulae. The substitution of all occurrences of x with ψ in ϕ is denoted by ϕ[x/ψ] or sometimes simply ϕ(ψ). Simultaneous substitution of all x i by ψ i (i ∈ {1, . . . , n}) is denoted by ϕ[x 1 /ψ 1 , . . . , x n /ψ n ]. For serial substitution such as (ϕ[x 1 /ψ 1 ])[x 2 /ψ 2 ] we often omit the parentheses and write ϕ[

x 1 /ψ 1 ][x 2 /ψ 2 ].
Remark 2.1. Note, that if ϕ(x), ψ ∈ L µ then ϕ[x/ψ] need not be a µ-formula, for example, if we set ϕ ≡ µy.x and ψ ≡∼ y then we have ϕ[x/ψ] ≡ µy. ∼ y ∈ L µ . Nevertheless, in this paper, if nothing else mentionned, an expression like ϕ[x/ψ] will denote well defined µ-formula. For a formal introduction of substitution we refer to Alberucci [START_REF] Alberucci | A Syntactical Treatment of Simultaneous Fixpoints in the Modal µ-Calculus[END_REF].

The negation ¬ϕ of a µ-formula ϕ is defined inductively such that ¬p ≡∼ p and ¬(∼ p) ≡ p, by using de Morgan dualities for boolean connectives and the usual modal dualities for 3 and . For µ, ν we define

¬µx.ϕ(x) ≡ νx.¬ϕ(x)[x/¬x] and ¬νx.ϕ(x) ≡ µx.¬ϕ(x)[x/¬x].
As usual, we introduce implication ϕ → ψ as ¬ϕ ∨ ψ and equivalence ϕ ↔ ψ as

(ϕ → ψ) ∧ (ϕ → ψ).
We say that a variable x ∈ bound(ϕ) is well-bounded in ϕ if no two distinct occurrences of fixpoint operators in ϕ bind x, and x occurs only once in ϕ. A propositional variable p is guarded in a formula ϕ ∈ L µ if every occurrence of p in ϕ is in the scope of a modal operator. A formula ϕ of L µ is said to be guarded if and only if for every subformula of ϕ of the form ηx.δ, x is guarded in δ. A formula ϕ of L µ is said to be well-named if it is guarded and every

x ∈ bound(ϕ) is well-bounded in ϕ. For all well-named ϕ, if x is bound in ϕ then there is exactly one subformula ηx.δ ≤ ϕ which bounds x, this formula is denoted by ϕ x . In the subsection of the semantics, by Lemma 2.3 we will see that any µ-formula ϕ is equivalent to a well-named formula wn(ϕ), therefore, if nothing else mentionned, we assume that all formulae are well-named.

If x ∈ bound(ϕ) and x is in the scope of a 3 operator in ϕ x , resp. operator, then we say that x is weakly existential in ϕ, resp. weakly universal in ϕ. If x ∈ bound(ϕ) and x is in the scope only of 3 operators in ϕ x , resp. operators, then we say that x is existential in ϕ, resp. universal in ϕ. Let ϕ(x) be a µformula. If x is free and occurs only positively in ϕ, then we define ϕ n (x) for all n inductively such that ϕ 1 (x) = ϕ(x) and such that

ϕ k+1 (x) ≡ ϕ[x/ϕ k (x)].
We define ϕ n (⊤) = ϕ n [x/⊤], and analogously for ϕ n (⊥).

The rank, rank(ϕ), of a formula ϕ is an ordinal number defined inductively as follows:

• rank(p) = rank(∼ p) = 1 • rank(△ α) = rank(α) + 1 where △∈ { , 3} • rank(α • β) = max{rank(α), rank(β)} + 1 where • ∈ {∧, ∨} • rank(ηx.α) = sup{rank(α n (x)) + 1 ; n ∈ N} where η ∈ {ν, µ}.
The fact that the definition of rank terminates is shown in the joint work with Krähenbühl [START_REF] Alberucci | Justifying Induction on Modal µ-Formulae[END_REF] (see also [START_REF] Alberucci | A Syntactical Treatment of Simultaneous Fixpoints in the Modal µ-Calculus[END_REF]). It is an easy exercise to show that for all formulae ϕ we have that rank(ϕ) = rank(¬ϕ).

The next lemma shows that wellnaming iterated formulae which are already well-named does not affect the rank. It follows by the fact that since ϕ is wellnamed the equivalent well-named formula for ϕ n (⊤) is given by simply renaming bound variables. Lemma 2.2. For all well-named formulae ϕ such that x appears only positively and all n ∈ N we have that rank(ϕ n (⊤)) = rank(wn(ϕ n (⊤))).

Similarly for ⊥.

Given a µ-formula ϕ, for all set of bound variables X ⊆ bound(ϕ), the formula ϕ free(X) is obtained from ϕ by eliminating all fixpoint operators binding a variable x ∈ X but leaving the previously bound variables x as a free occurrences. Further, if X = {x i , . . . , x n } ⊆ bound(ϕ) then we define

ϕ -X ≡ ϕ free(X) [x 1 /⊥, . . . , x n /⊥].
2.2. Semantics. The semantics of modal µ-calculus is given by transition systems. A transition system T is of the form (S, → T , λ T ) where S is a set of states → T is a binary relation on S called the accessibility relation and the function λ : P → ℘(S) is a valuation for all propositional variables. A transition system T with a distinguished state s is called a pointed transition system and denoted by (T , s). T denotes the class of all pointed transition systems. Given any property P , by T P we denote the subclass of pointed transition systems satisfying the property P . In particular T r denotes all pointed reflexive transition systems, T st all pointed symmetric and transitive transition systems, T t all pointed transitive transition systems and T rst denotes all pointed transition systems where the accessibility relation is an equivalence relation, that is, it denotes the class of all S5 models. Given any property P , with T P f we denote the subclass of finite pointed transition systems satisfying the property P . For example, T tf denotes all finite pointed transition systems where the accessibility relation is transitive.

Let λ be a valuation, p a propositional variable and S ′ a subset of states S; we set for all propositional variables

p ′ λ[p → S ′ ](p ′ ) = S ′ if p ′ = p, λ(p ′ ) otherwise.
Given a transition system T = (S, → T , λ T ), then T [p → S ′ ] denotes the transition system (S, → T , λ T [p → S ′ ]). This notions are generalized straightforwardly to λ[x 1 → S 1 , . . . , x n → S n ] and T [x 1 → S 1 , . . . , x n → S n ]. Given a transition system T , the denotation of ϕ in T , ϕ T , that is, the set of states satisfying a formula ϕ is defined inductively on the structure of ϕ. Simultaneously for all transition systems we set

• p T = λ(p) and ∼ p T = Sλ(p) for all p ∈ P,

• α ∧ β T = α T ∩ β T , • α ∨ β T = α T ∪ β T , • α T = {s ∈ S | ∀t((s → T t) ⇒ t ∈ α T )}, • 3α T = {s ∈ S | ∃t((s → T t) ∧ t ∈ α T )}, • νx.α T = {S ′ ⊆ S | S ′ ⊆ α(x) T [x →S ′ ] }, and • µx.α T = {S ′ ⊆ S | α(x) T [x →S ′ ] ⊆ S ′ }.
We say that a pointed transition system (T , s) is a model of a µ-formula if and only if s ∈ ϕ T . By ϕ we denote the class of all models of ϕ and by ϕ P the class of all models of ϕ with property P . For a formula ϕ(x) and set of states S ′ ⊆ S we sometimes write ϕ(S ′ ) T instead of ϕ(x) T [x →S ′ ] . When clear from the context we use ϕ(x) T for the function

ϕ(x) T : ℘(S) → ℘(S) S ′ → ϕ(S ′ ) T .
By Tarski-Knaster Theorem, c.f. [28], νx.α(x) T is the greatest fixpoint and µx.α(x) T the least fixpoint of the operator α(x) T .

The next two lemmas state some basic properties of denotations. Their proofs are left to the reader. Lemma 2.3. For all transition systems T = (S, → T , λ T ) and all formulae ϕ we have that 1. ¬ϕ T = Sϕ T , 2. ηx.ηy.ϕ(x, y) T = ηx.ϕ(x, x) T , where η ∈ {µ, ν}, 3. νx.ϕ(x) T = ϕ(⊤) T , if all occurrences of x are not guarded, 4. µx.ϕ(x) T = ϕ(⊥) T , if all occurrences of x are not guarded. 5. There is a well-named formula wn(ϕ) such that ϕ T = wn(ϕ) T .

Lemma 2.4. Let ϕ, α, α i , β, β i , ψ, ψ i ∈ L µ be well-named µ-formulae, where i ∈ {1, . . . , k}. For all transition systems T the following holds:

1. If free(ψ i ) ∩ bound(ϕ) = ∅ for all i ∈ {1, . . . , k} then

ϕ[x 1 /ψ 1 , . . . , x k /ψ k ] T = ϕ T [x1 → ψ1 T ,...,x k → ψ k T ] .
2. If ψ ≤ ϕ and x i ∈ free(ψ) ∩ bound(ϕ), with i = 1, . . . , k, then

ψ[x 1 /ϕ x1 , . . . , x k /ϕ x k ] T = ψ T [x1 → ϕx 1 T ,...,x k → ϕx k T ] . 3. If free(ψ i ) ∩ bound(α) = free(ψ i ) ∩ bound(β) = ∅ and x i ∈ free(α) ∩ free(β)
for all i ∈ {1, . . . , k} and for every transition system T we have that

α T = β T
then, for every transition system T we have that

α[x 1 /ψ 1 , . . . , x k /ψ k ] T = β[x 1 /ψ 1 , . . . , x k /ψ k ] T .
4. Let free(α i ) ∩ bound(ϕ) = free(β i ) ∩ bound(ϕ) = ∅ and let x i ∈ free(ϕ) occur positively in ϕ, where i = 1, . . . , k. If for every transition system T we have that

α i T ⊆ β i T , for every i ∈ {1, . . . , k}, then we have that ϕ[x 1 /α 1 , . . . , x k /α k ] T ⊆ ϕ[x 1 /β 1 , . . . , x k /β k ] T .
Let T = (S, → T , λ) be a transition system and s, s ′ two states in S. A sequence s 0 , s 1 , . . . , s n such that s i → T s i+1 , s 0 = s and s n = s ′ is a path of length n connecting s to s ′ . We say that s ′ is reachable from s. A subset S ′ ⊆ S of the set of states is called a strongly connected component if for all s, s ′ ∈ S ′ we have that s ′ is reachable from s. For each s by scc(s) we denote the greatest strongly connected component which contains s if there is one and scc(s) = ∅ if s is not contained in any strongly connected component. Note, that the notion scc(s) is well-defined. Given a pointed transition system (T , s) and a state s ′ in it, we define the depth of s ′ , dp(s ′ ), to be the length of the shortest path from s to s ′ . Since parts which are non connected to the point s will be irrelevant in the sequel we assume that all transition system are connected and, therefore, that dp(s ′ ) is defined for all s ′ .

2.3. The alternation depth hierarchy. Let Φ ⊆ L µ . For η ∈ {ν, µ}, η(Φ) is the smallest class of formulae such that:

• Φ, ¬Φ ⊂ η(Φ);

• If ψ(x) ∈ η(Φ) and x occurs only positively, then ηx.ψ ∈ η(Φ);

• If ψ, ϕ ∈ η(Φ), then ψ ∧ ϕ, ψ ∨ ϕ, 3ψ, ψ ∈ η(Φ); • If ψ, ϕ ∈ η(Φ) and free(ψ) ∩ bound(ϕ) = ∅ then ϕ[x/ψ] ∈ η(Φ)
With the help of this definition, we introduce the syntactical hierarchy for the modal µ-calculus. For all n ∈ N, we define the class of µ-formulae Σ µ n and Π µ n inductively as follows:

• Σ µ 0 := Π µ 0 := L M ; • Σ µ n+1 = µ(Π µ n ); • Π µ n+1 = ν(Σ µ n ). ∆ µ n := Σ µ n ∩ Π µ n
The fixpoint alternation depth, ad, of a formula is the number of non-trivial nestings of alternating least and greatest fixpoints. Formally, the alternation depth of ϕ ∈ L µ is given by ad(ϕ) := inf{k : ϕ ∈ ∆ µ k+1 }. All Σ µ n and Π µ n form the syntactical modal µ-calculus hierarchy, which is strict. The fixpoint alternation free fragment corresponds to the class ∆ µ 2 . Lemma 2.5. For all µ-formulae ϕ there is a well-named formula wn(ϕ) such that for all T we have ϕ T = wn(ϕ) T and ad(ϕ) = ad(wn(ϕ)).

Proof. We have just to verify that the construction of wn(ϕ) given by parts 2 to 4 of Lemma 2.3 does not increase the alternation depth of the formula. But this is straightforward. ⊣ Given Lemma 2.2 and Lemma 2.5, we can assume that wn is a function associating to every formula ϕ a well-named formula wn(ϕ) which has the same alternation depth and the same denotation in every transition system and such that, if ϕ is well-named, it also preserves the rank of ϕ n (⊤) and ϕ n (⊥), for every n.

The semantical modal µ-calculus hierarchy over T consists of all Σ µT n and Π µT n , which are classes of pointed transition systems defined inductively as follows:

Σ µT n = { ϕ : ϕ ∈ Σ µ n } Π µT n = { ϕ : ϕ ∈ Π µ n }
As usual, the ambiguous classes are defined by ∆ µT n := Σ µT n ∩ Π µT n . The semantical modal µ-calculus hierarchy over T P , for any property P , is defined analogously.

Theorem 2.6 ( [START_REF] Bradfield | The Modal µ-calculus Alternation Hierarchy is Strict[END_REF][START_REF] Bradfield | Simplifying the Modal µ-Calculus Alternation Hierarchy[END_REF]). The semantical modal µ-calculus hierarchy over T is strict.

From now on, when we write about the modal µ-calculus hierarchy, we always mean the semantical modal µ-calculus hierarchy.

Example 2.7. It is instructive to have a look at two typical µ-formulae. The first formula express the property of "always eventually p" νx.(µy.(p ∨ 3y)) ∧ x).

Indeed, it says that from any node of a model, we can reach a node where p holds. Since this formula is in Π µ 1 , this kind of property can be expressed without any alternation. Moreover, it can be shown that cannot be reduced to a purely modal formula. The second formula defines the property of "there is a path where p holds infinitely often" νx.µy.((p ∨ 3y)) ∧ 3x).

It can be verified that the alternation is really needed, that is, that the class of models of this formula is in Π µT 2 \ Σ µT 2 . §3. Evaluation games for the modal µ-calculus. Evaluation games are a very important tool in the modal µ-calculus and will play a crucial role in the sequel. After introducing some general notions for infinite games we define the evaluation games. The last subsection is about the concept of game formula.

3.1. Parity games. Let V be a set. By V * we denote the set of finite sequences on V , and by V + we denote the set of nonempty sequences. Finally, by V ω we denote the set of infinite sequences over V .

A game G is defined in terms of an arena A and a winning condition W . In our case an arena is simply a bi-partite graph

A = V 0 , V 1 , E , where V 0 ∩ V 1 = ∅ and the edge relation, or set of moves, is E ⊆ (V 0 ∪ V 1 ) × (V 0 ∪ V 1 ). Let V = V 1 ∪ V 2
be the set of vertices, or positions, of the arena. Given two vertices a, b ∈ V , we say that b is a successor of a, if (a, b) ∈ E. The set of all successors of a is sometimes denoted by aE or E(a). We say that b is reachable from a if there are a 1 , . . . , a n ∈ V such that a 1 = a, a n = b and for every 0

< i < n, a i+1 ∈ a i E.
A play in the arena A can be finite or infinite. In the former case, the play is a non empty finite path π = a 1 . . . a n ∈ V + such that for every 0 < i < n, a i+1 ∈ a i E and a n E = ∅. In the last case, the play consists in an infinite path π = a 1 . . . a n • • • ∈ V ω with a i+1 ∈ a i E for every i > 0. Thus a finite or infinite play in a game can be seen as the trace of a token moved on the arena by two Players, Player 0 and Player 1, in such a way that if the token is in position a ∈ V i , then Player i has to choose a successor of a where to move the token.

The set of winning conditions W is a subset of V ω . Thus, given a game G = (A, W ) a play π is winning for Player 0 iff 1. if π is finite, then the last position a n of the play is in V 1 , 2. if π is infinite, then it must be a member of W .

A play is winning for Player 1 if it is not winning for Player 0. In this framework we are interested in what is called a parity winning condition. That is, given a set of vertices V , we assume a coloring or ranking function Ω : V → ω such that Ω[V ] is bounded. Then, the set W of winning conditions is defined as the set of all infinite sequences π such that the greatest priority appearing infinitely often in Ω(π) is even.

Let A be an arena. A strategy for Player i is simply a function σ i : V * V i → V , with i = 1, 2. A prefix a 1 . . . a n of a play is said to be compatible or consistent with σ i iff for every j with 1 ≤ j < n and a j ∈ V i , it holds that σ i (a 1 . . . a j ) = a j+1 . A finite or infinite play is compatible or consistent with σ i if each of its prefix which is in V * V i is compatible with σ i . The strategy σ i is said to be a winning strategy for Player i on W if every play consistent with σ i is winning for Player i. A position a ∈ V is winning for Player i in the parity game G iff there is a strategy σ for Player i such that every play compatible with σ which starts from a is winning for Player i. A winning strategy σ is called

memoryless if σ(a 1 . . . a n ) = σ(b 1 . . . b n ), when a n = b n .
For parity games we have a memoryless determinacy result. Theorem 3.1 ( [START_REF] Emerson | Tree Automata, µ-Calculus and Determinacy (Extended Abstract)[END_REF][START_REF] Mostowski | Games with forbidden position[END_REF]). In a parity game, one of the Players has a memoryless winning strategy from each vertex.

Having in mind this theorem, in the sequel we assume that all winning strategies are memoryless, that is, a winning strategy in a parity games for Player 0 is a function σ : V 0 → V , analogously for Player 1.

3.2. Evaluation games for the modal µ-calculus. In this subsection we will see, given ϕ ∈ L µ and a pointed transition system (T , s 0 ), how to determine the corresponding parity game E(ϕ, (T , s 0 )), called also the evaluation game of ϕ over (T , s 0 ).

Remember that T = (S, → T , λ T ). The arena of E(ϕ, (T , s 0 )) is the triple

V 0 , V 1 , E which is defined recursively such that ϕ, s 0 ∈ V (remember that V = V 0 ∪ V 1 )
and such that if ψ, s ∈ V then we distinguish the following cases:

• If ψ ≡ (¬)p and p ∈ free(ϕ). In this case we set E ψ, s = ∅ and

ψ, s ∈ V 1 iff s ∈ λ T (ψ) if ψ ≡ p s ∈ λ T (ψ) if ψ ≡ ¬p.
• If ψ ≡ x and x ∈ bound(ϕ). In this case we set

( ψ, s , ϕ x , s ) ∈ E and we have ψ, s ∈ V 0 iff x is a µ-variable. • If ψ ≡ α ∧ β then we have ψ, s ∈ V 1 , and if ψ ≡ α ∨ β then we have ψ, s ∈ V 0 .
In both cases it holds that ( ψ, s , α, s ) ∈ E and ( ψ, s , β, s ) ∈ E

• If ψ ≡ α then we have ψ, s ∈ V 1 , and if ψ ≡ 3α then we have ψ, s ∈ V 0 .

In both cases it holds that ( ψ, s , α, s ′ ) ∈ E for all s ′ such that s → T s ′ .

• If ψ ≡ νx.α then we have ψ, s ∈ V 1 , and if ψ ≡ µx.α then we have ψ, s ∈ V 0 . In both cases it holds that ( ψ, s , α, s ) ∈ E.

We complete the definition of the parity game E(ϕ, (T , s 0 )) by defining the (partial) priority function Ω : V → ω. The function is first defined on states of the form ηx.δ, s ∈ V , where η ∈ {µ, ν}. In this case we have that:

Ω( ψ, s ) =        ad(ηx.δ) if η = µ and ad(ηx.δ) is odd, or η = ν and ad(ηx.δ) is even; ad(ηx.δ) -1 if η = µ and ad(ηx.δ) is even, or η = ν and ad(ηx.δ) is odd.
For a state of the form x, s , where x ∈ bound(ϕ), we set Ω( x, s ) := Ω( ϕ x , s ).

s {p} 1 || | | | | | | s {p} 2 J J / / s 3 Figure 1
For all the other states α, s we distinguish two cases. If there is a least formula ηx.δ ∈ sub(ϕ) such that ηx.δ > α we set Ω( α, s ) := Ω( ηx.δ, s ).

If there is no such formula then we set

Ω( α, s ) = min{Ω(ηx.δ) : ηx.δ ≤ ϕ} if ϕ ∈ ∆ µ n , n > 1 1 if ϕ ∈ ∆ µ 1 .
It can easily be seen that if there is a formula ηx.δ > α then there is also a least one. Therefore, the second case refers to subformulae α of ϕ which can not be regenerated by a fixpoint application in a parity game. In the following we simply write min Ω and max Ω instead of min{Ω( α, s ) : α, s ∈ V } and of max{Ω( α, s ) : α, s ∈ V }.

Remember that if the play π is finite, Player 0 wins iff the last vertex of the play belongs to V 1 , and if the play π is infinite, Player 0 wins iff the greatest priority appearing infinitely often even. This result can be seen as the "game-theoretical version" of what is usually called the Fundamental Theorem of the semantic of the modal µ-calculus. The proofs of the following Lemma is by unwinding the definitions of winning strategy. Lemma 3.3. Let T = (S, → T , λ T ) be a transition system and ϕ(x 1 , . . . , x k ) be a formula where all x i occurs positively. Let σ be a strategy for Player 0 in E(ϕ(x 1 , . . . , x k ), (T , s)). Suppose that for all vertices of the form x i , s ′ which are reachable by σ we have that s ′ ∈ A i ⊆ S, with i = 1, . . . , k. Then σ can be converted into a winning strategy for Player 0 in the evaluation game

E(ϕ(x 1 , . . . , x k ), (T [x 1 → A 1 , . . . , x k → A k ], s)). Example 3.4. Evaluation game E(νx. ((p ∨ ⊥) ∧ x), (T , s 1 )).
T is as in Figure 1, that is, it has states {s 1 , s 2 , s 3 } and p holds in s 1 and s 2 , and the accessibility relation is as depicted in Figure 1.

In Figure 2, you find the arena of E(νx. ((p ∨ ⊥) ∧ x), (T , s 1 )). In order to simplify the picture we identified vertices of the form νx. ((p∨ ⊥)∧x), s with the vertices of the form ((p ∨ ⊥) ∧ x), s . Note, that this does not change essentially the evaluation game. Further, the graph given by the non-dotted edges represents the part of the arena which can be reached by a play given the strategy of Player 0 where he chooses, if there is the possibility, the non-dotted instead of the dotted move. Note, that it is a winning strategy. It is left as an

((p ∨ ⊥) ∧ x), s 1 ' ' O O O O O O O O O O O O (p ∨ ⊥) ∧ x, s 3
x x q q q q q q q q q q

(p ∨ ⊥) ∧ x, s 2 * * U U U U U U U U U U U U U U U U U p ∨ ⊥, s 3 } } x, s 3 ν (p ∨ ⊥), s 2 $ $ x, s 2 ν p, s 3 ⊥, s 3 ((p ∨ ⊥) ∧ x), s 3 p, s 2 ⊥, s 2 ((p ∨ ⊥) ∧ x), s 2 a a W W Figure 2
exercise to verify that νx. ((p ∨ ⊥) ∧ x) is valid if for all reachable states in a transition system we have that either, the state is terminal, or, p holds in the state. E(ϕ,(T ,s)) for a formula ϕ we define the pointed game transition system T (E(ϕ, (T , s))) = ((S, → T , λ T ), s 0 ) such that the states S are the vertices V and the distinguished state s 0 = ϕ, s , and such that the transition relation → T is the edge relation E of the parity game. If ad(ϕ) = n then the valuation λ T is specified for the new propositional variables

Game formulae. Given a parity game

{c i : 0 ≤ i ≤ n} ∪ {d i : 0 ≤ i ≤ n}.
For all ψ ∈ sub(ϕ) we define our valuation for these propositional variables such that λ T (d i ) = { ψ, s : ψ, s ∈ V 0 and Ω( ψ, s ) = i} and

λ T (c i ) = { ψ, s : ψ, s ∈ V 1 and Ω( ψ, s ) = i}.
In the following we introduce the game formulae and show that with them it is possible to test the existence of a winning strategy for Player 0 in an evaluation game. Definition 3.5. For all n ≥ 1 we define the Σ µ n game formula W Σ µ n such that:

W Σ µ n :≡ µx n-1 .νx n-2 . . . . νx 0 n-1 i=0 (d i ∧ 3x i ) ∨ n-1 i=0 (c i ∧ x i ) n even µx n .νx n-1 . . . . µx 1 n i=1 (d i ∧ 3x i ) ∨ n i=1 (c i ∧ x i ) n odd
The Π µ n game formula W Π µ n is defined such that:

W Π µ n :≡ νx n .µx n-1 . . . . µx 1 n i=1 (d i ∧ 3x i ) ∨ n i=1 (c i ∧ x i ) n even νx n-1 .µx n-2 . . . . νx 0 n-1 i=0 (d i ∧ 3x i ) ∨ n-1 i=0 (c i ∧ x i ) n odd For n = 0 we define W Σ µ 0 :≡ W Π µ 0 :≡ W Σ µ 1 . It is clear from definition that for all n ≥ 1 we have that W Σ µ n ∈ Σ µ n and W Π µ n ∈ Π µ n .
Proposition 3.6 ( [START_REF] Emerson | Tree Automata, µ-Calculus and Determinacy (Extended Abstract)[END_REF][START_REF] Walukiewicz | Monadic second-order logic on tree-like structures[END_REF]). Let G an arbitrary parity game. Assume that min Ω ∈ {0, 1} and max Ω = n. We have that if n is even (resp. odd): (a) if min Ω = 0 then Player 0 has a winning strategy for G if and only if

T (G) ∈ W Π µ n+1 (resp. T (G) ∈ W Σ µ n+1
), (b) if min Ω = 1 then Player 0 has a winning strategy for G if and only if

T (G) ∈ W Π µ n (resp. T (G) ∈ W Σ µ n ) From Proposition 3.
6 and the definition of an evaluation game, it follows immediately that: Corollary 3.7. Let ϕ be a Π µ n -formula (resp. a Σ µ n -formula) and let (T , s) be an arbitrary pointed transition system. We have that Player 0 has a winning strategy for E(ϕ, (T , s)) if and only if

T (E(ϕ, (T , s))) ∈ W Π µ n (resp. if and only if (T , s) ∈ W Σ µ n ).
Therefore, by applying Proposition 3.2 and Corollary 3.7, we have the following result:

Corollary 3.8. Let ϕ be a Π µ n -formula (resp. Σ µ n -formula) and let (T , s) be an arbitrary pointed transition system. We have that (T , s) ∈ ϕ if and only if T (E(ϕ, (T , s))) ∈ W Πn (resp. (T , s) ∈ W Σn ). §4. Finite model theorems. In this section we prove finite model theorems for the modal µ-calculus over the class of all reflexive and over the class of all transitive transition systems. Let us first state the well-known finite model theorem for general transition systems. Theorem 4.1 ([18, 25]). For all modal µ-formulae ϕ for which there is a transition system T and a state s in T such that s ∈ ϕ T there is a finite transition system T F and a state s F such that s F ∈ ϕ T F .

4.1. Finite model theorem for reflexive transition systems. Let ϕ be a µ-formula. By induction on the structure of ϕ we define the formula ϕ ref as follows:

• (∼)p ref ≡ (∼)p, • (α • β) ref = α ref • β ref where • ∈ {∧, ∨}, • ( α) ref = α ref ∧ α ref , • (3α) ref = 3α ref ∨ α ref , and • (ηx.α) ref = ηx.α ref where η ∈ {µ, ν}.
The next Lemma is by induction on the structure of the formula.

Lemma 4.2. Let T be a finite transition system and let T ref be its reflexive closure. For all µ-formulae ϕ the following holds

s ∈ ϕ ref T if and only if s ∈ ϕ T ref .
With the help of this lemma we can easily prove the finite model property for reflexive transition systems.

Theorem 4.3. For all modal µ-formulae ϕ for which there is a reflexive transition system T and a state s in T such that s ∈ ϕ T there is a finite reflexive transition system T F and a state s F such that s F ∈ ϕ T F .

Proof. Let ϕ be a µ-formula and T a reflexive transition system with a state s such that s ∈ ϕ T . Since T is reflexive we have that T = T ref and therefore by Lemma 4.2 we have that

s ∈ ϕ ref T .
By the general Finite Model Theorem 4.1 we get that there is a finite transition system T F and a state s F such that

s F ∈ ϕ ref T F .
If we define T F ref to be the reflexive closure of T F by applying again Lemma 4.2 we get s F ∈ ϕ T F ref and we have found the finite reflexive model and a state in it satisfying ϕ. ⊣ 4.2. Finite model theorem for transitive transition systems. Let ϕ be a µ-formula. By induction on the structure of ϕ we define the formula ϕ tr as follows: As in the reflexive case, the next Lemma is proved by induction on the structure of the formula. Lemma 4.4. Let T be a finite transition system and let T tr be its transitive closure. For all µ-formulae ϕ the following holds s ∈ ϕ tr T if and only if s ∈ ϕ T tr . By using Lemma 4.4, mutatis mutandis, the proof of the finite model property for transitive transition systems is exactly the same as for Theorem 4.3.

• (∼)p tr ≡ (∼)p, • (α • β) tr = α tr • β tr where • ∈ {∧, ∨}, • ( α) tr = νx. (α tr ∧ x), • (
Theorem 4.5. For all modal µ-formulae ϕ for which there is a transitive transition system T and a state s in T such that s ∈ ϕ T there is a finite transitive transition system T F and a state s F such that s F ∈ ϕ T F . §5. The hierarchy on transitive and symmetric transition systems. In this section, we prove the collapse of the semantical modal µ-calculus hierarchy over T st to the purely modal fragment. Let us begin with the following easy lemma.

Lemma 5.1. Let T be a transitive transition system and let s ′ ∈ scc(s). For all µ-formulae ϕ we have that

s ∈ △ ϕ T if and only if s ′ ∈ △ ϕ T
where △∈ { , 3}.

Proof. Suppose that s ∈ ϕ T . This is equivalent to the fact that for all s ′′ such that s → T s ′′ we have that s ′′ ∈ ϕ T . On the other hand by definition of scc we have for all s ′ ∈ scc(s) that s → T s ′ and s ′ → T s. Therefore, for an arbitrary state s ′′ by transitivity we have s → T s ′′ if and only if s ′ → T s ′′ . This implies that s ∈ ϕ T if and only if for all s ′′ such that s ′ → T s ′′ we have that s ′′ ∈ ϕ T which itself is equivalent to s ′ ∈ ϕ T . The case for 3 is proved similarly. ⊣ Theorem 5.2. Let T be a transitive and symmetric transition system. We have that

νx.ϕ(x) T = ϕ(ϕ(⊤)) T .
Proof. The ⊆ inclusion is clear. For the ⊇ inclusion, define A = ϕ(ϕ(⊤)) T ; by definition of greatest fixpoint it is enough to show that we have

A ⊆ ϕ(A) T . (1)
First recall that we assume that νx.ϕ(x) is well-named. This means that in the formula ϕ(x) the variable x is in the scope of a modal operator and occurs only once in ϕ. Therefore, we can assume that ϕ is of the form β(△ α(x)) where △∈ {3, }. Moreover x we have that △ α(x) and △ α(ϕ(x)) occur only once in the formula tree of ϕ(ϕ(x)). Let s ∈ A, by Proposition 3.7 there is a winning strategy σ for Player 0 in the evaluation game E(ϕ(ϕ(x)), (T [x → S], s)). Let π be an arbitrary play consistent with σ. If π reaches a vertex of the form △ α(x), s ′ then the same play reaches a vertex of the form △ α(ϕ(x)), s ′′ . Since σ is a winning strategy for Player 0 by Proposition 3.7 we have that

s ′′ ∈ △ α(ϕ(x)) T [x →S] and s ′ ∈ △ α(x) T [x →S] .
Since T is transitive and symmetric it clearly holds that s ′′ ∈ scc(s ′ ) and, by applying Lemma 5.1, we have

s ′ ∈ △ α(ϕ(x)) T [x →S] .
Hence, we have shown that for all plays π consistent with σ, if π reaches a vertex of the form △ α(x), s ′ then, by Theorem 3.2, there is a winning strategy for Player 0 in the evaluation game E(△ α(ϕ(x)), (T [x → S], s ′ )). A fortiori, this implies that if π reaches a vertex of the form △ α(x), s ′ then there is a winning strategy σ △α(x),s ′ for Player 0 in E(△ α(x), (T [x → ϕ(x) T [x →S] ], s ′ )). Therefore, since ϕ(x) T [x →S] ⊆ S, the strategy σ * given by following σ but switching to the corresponding σ △α(x),s ′ when a position of the form △ α(x), s ′ is reached, is winning for Player 0 in the parity game

E(ϕ(ϕ(x)), (T [x → S], s)). Let B := ϕ(x) T [x →S]
. By construction of σ * we have that for all vertices of the form x, v which are reachable by σ * it holds that v ∈ B. Then, by applying Lemma 3.3, σ * can be converted into a winning strategy for Player 0 in the evaluation game E(ϕ(ϕ(x), (T [x → B], s)). By Theorem 3.2, we have that s ∈ ϕ(ϕ(B)) T which can be reformulated as s ∈ ϕ(ϕ(ϕ(⊤))) T or s ∈ ϕ(A) T . Therefore, we have proved Equation 1 and completed the proof. ⊣ Definition 5.3. The syntactical translation ( ) t : L µ → L M is defined recursively on the structure of the formula such that p t = p, ⊥ t = ⊥ and ⊤ t = ⊤, such that it distributes over boolean and modal connectives, and such that (µx.ϕ) t = wn(ϕ(ϕ(⊥)))

t and (νx.ϕ) t = wn(ϕ(ϕ(⊤))) t .

Note that (ϕ) t is defined via an application of ( ) t either to a strict subformula ψ of ϕ, or to a formula whose rank, by Lemma 2.2, is strictly smaller than the rank of ϕ. Thus ( ) t terminates and is well-defined.

The next corollary proves that on transitive and symmetric models, the semantical hierarchy of the µ-calculus collapses to the class ∆ µT st 1 . Its proof goes by induction on the rank of a formula and uses Theorem 5.2.

Corollary 5.4. On transitive and symmetric transition systems we have that

ϕ T = ϕ t T .
Example 5.5. If we look at our example from Section 2, for "always eventually p", we have that

νx.(µy.(p ∨ 3y)) ∧ x) T st = (p ∨ 3p) ∧ (p ∨ 3p) T st
and for "there is a path where p holds infinitely often", we have that

νx.µy.((p ∨ 3y)) ∧ 3x) T st = p ∨ 3(p ∧ 3((p ∨ 3(p ∧ 3⊤)) ∧ 3⊤) ∧ 3((p ∨ 3(p ∧ 3⊤)) ∧ 3⊤) T st .
Remark 5.6. Because the previous proof applies to any S5 model, that is, for every T ∈ T rst we have that:

ϕ T = ϕ t T
The fact that the modal µ-calculus hierarchy for S5-models collapses to the pure modal fragment is indeed not surprising since for a S5-formula ϕ there are only finitely many formulae with the same propositional variables which are not equivalent over T rst and, therefore, it can easily be shown that for all νx.ϕ(x) ∈ L µ there is a n ∈ N such that ϕ n (⊤) T rst = νx.ϕ T rst . The existence of only finitely many non equivalent formulae follows from the fact that for all S5-formulae ϕ there is a conjunctive modal normal form ψ such that ψ ≡ δ 1 ∧ δ 2 ∧ .. ∧ δ n where δ ≡ α ∨ β 1 ∨ β 2 ∨ ... β n ∨ 3γ 1 ∨ 3γ 2 ∨ .. ∨ 3γ m and α, β i and γ j are propositional formulae 2 . §6. The hierarchy on transitive transition systems. We show that the modal µ-calculus hierarchy over T t collapses to the alternation-free fragment. This is done in four parts starting from subsection two. First, any modal µformula is reduced to a semantically equivalent formula τ (ϕ) such that normalized strategies on evaluation games, which will be introduced in the third subsection, have certain nice properties. Then, we encode such normalized winning strategies in modal µ-formulae and, finally, we show the collapse for finite transitive transition system and, by using the previously proved finite model theorem, generalize it to all transitive transition systems.

In the next subsection some technical notions like the one of unfolding a formula in a model are introduced and some properties are proved.

6.1. Some technical preliminaries. Remember that we suppose all µformulae well-named. First we introduce the unfolding of a formula which generalizes the one of closure of a formula, introduced by Kozen in [START_REF] Kozen | Results on the propositional mu-calculus[END_REF]. In order to do this, let ϕ and ψ be any µ-formulae such that {x 1 , . . . , x n } = X ⊆ bound(ϕ). The unfolding of ψ in ϕ over X, unf X ϕ (ψ), is the formula defined recursively such that unf ∅ ϕ (ψ) ≡ ψ and such that if X is of the form {x 1 , . . . , x n } then

unf X ϕ (ψ) ≡ ψ[x 1 /unf X -1 ϕ (ϕ x1 ), . . . , x n /unf X -n ϕ (ϕ xn )]
where X -i = {x 1 , . . . , x i-1 , x i+1 , . . . , x n }. It can easy be seen that we have X ∩ free(unf X ϕ (ψ)) = ∅. In order to explain semantically the unfolding of a formula we introduce for each transition system T the transition system induced by ϕ, T ϕ . For every variable x ∈ bound(ϕ) we define a natural number l(x) recursively such that l(x) = 0 if free(ϕ x ) ∩ bound(ϕ) = ∅ and such that l(x) = max{l(x i ) :

x i ∈ free(ϕ x ) ∩ bound(ϕ)} + 1
in the opposite case. For all transition systems T with valuation λ and for all 0 ≤ i ≤ max{l(x) : x ∈ bound(ϕ)} =: N we define new valuations λ i and transition systems T i such that λ 0 = λ and T 0 = T , and such that T k+1 is identical to T k except for the valuation λ k+1 which is defined as follows:

• λ k+1 | P\bound(ϕ) = λ k | P\bound(ϕ) ; • if x ∈ bound(ϕ): λ k+1 (x) = λ k (x) if l(x) = k + 1 ϕ x T k if l(x) = k + 1.
We define T ϕ to be T N and λ ϕ = λ N . Note, that if we have a formula ψ such that free(ψ) ∩ bound(ϕ) is empty then, since the denotation of ϕ is independent of the valuation of the bound variables, we have ψ T = ψ T ϕ . In particular, we have ϕ T = ϕ T ϕ . Moreover note that for all x i ∈ bound(ϕ) it holds that λ ϕ (x i ) = ϕ xi T ϕ . Lemma 6.1. For all formulae ϕ, all subformulae ψ ≤ ϕ, all X ⊆ bound(ϕ), and all transition systems T we have that

ψ T ϕ = unf X ϕ (ψ) T ϕ . Proof.
By induction on the size of X. If X is empty, then by definition of unfolding we have that unf X ϕ (ψ) ≡ ψ and the claim is trivial. For the inductive step, suppose that X ∩ free(ψ) is the set {x 1 , . . . , x m }. Hence, by definition we have

unf X ϕ (ψ) ≡ ψ[x 1 /unf X -1 ϕ (ϕ x1 ), . . . , x m /unf X -m ϕ (ϕ xm )].
Since bound(ψ) ∩ free(ϕ xi ) = ∅ and free(unf X -1 ϕ (ϕ xi )) ⊆ free(ϕ xi ) for all i we get that bound(ψ) ∩ free((unf X -1 ϕ (ϕ xi )) = ∅. Therefore, by induction hypothesis and Lemma 2.4.1 we get

unf X ϕ (ψ) T ϕ = ψ T ϕ [x1 → ϕx 1 T ϕ ,... ,xm → ϕx m T ϕ ] . Since for all x i we have that λ ϕ (x i ) = ϕ xi T ϕ we get unf X ϕ (ψ) T ϕ = ψ T ϕ .
⊣ The previous lemma tells us that on the transition system induced by ϕ the denotation of any subformula of ϕ and the denotation of any of its unfolding over ϕ are the same.

Other usefull properties of T ϕ are summarized in the next lemma.

Lemma 6.2. Let T = (S, → T , λ T ) be a transition system, ϕ any µ-formula and ψ ≤ ϕ.Then:

1. For every X ⊆ bound(ϕ) we have

ψ free(X) T ϕ = ψ T ϕ . 2. For every X 1 , X 2 ⊆ bound(ϕ), where X 1 ∩ X 2 = ∅, we have unf X2 ϕ free(X 1 ) ψ free(X1) T ϕ = ψ T ϕ . 3. For every X 1 , X 2 ⊆ bound(ϕ), where X 1 ∩ X 2 = ∅, we have unf X2 ϕ ψ free(X1) T ϕ = ψ T ϕ .
Proof. Part 1. By Lemma 2.4.2 and since ϕ x T ϕ = λ T ϕ (x) for every variable x ∈ bound(ϕ) we get ψ free(X)

T ϕ = ψ free(X) [x 1 /ϕ x1 , . . . , x n /ϕ xn ] T ϕ . The proof ends with a straightforward induction on the structure of ψ proving that for all transition systems T we have

ψ T ϕ = ψ free(X) [x 1 /ϕ x1 , . . . , x n /ϕ xn ] T ϕ .
The only non trivial step is the one where ψ is of the form ηx.α (η ∈ {µ, ν}). In this case, note that if any x i appears free in α then x appears only bound in ϕ xi .

Part 2. We prove the equation by induction on the size of X 2 . If X 2 is empty, the equation holds by the previous point. For the inductive step, given {x i1 , . . . , x i k } = X 2 ∩free(ψ free(X1) ), we have that by definition of unf the formula unf X2 ϕ free(X 1 ) ψ free(X1) T ϕ is equal to

ψ free(X1) [x i1 /unf X -i 1 2 ϕ free(X 1 ) (ϕ free(X1) ) xi 1 , . . . , x i k /unf X -i k 2 ϕ free(X 1 ) (ϕ free(X1) ) xi k ] T ϕ .
Since free(unf

X -i 1 2
ϕ free(X 1 ) (ϕ free(X1) ) xi 1 ) ⊆ free(ϕ free(X1) ) xi 1 ) and since we have that free(ϕ free(X1) ) xi 1 ) ∩ bound(ψ free(X1) ) = ∅ we get free(unf

X -i 1 2 ϕ free(X 1 ) (ϕ free(X1) ) xi 1 ) ∩ bound(ψ free(X1) ) = ∅.
With Lemma 2.4.1 we get the equality with

ψ free(X1) T ϕ [xi 1 → unf X -i 1 2 ϕ free(X 1 ) (ϕ free(X 1 ) )x i 1 T ϕ ,...,xi k → unf X -i k 2 ϕ free(X 1 ) (ϕ free(X 1 ) )x i k T ϕ ]
and by induction hypothesis this expression is equal to

ψ free(X1) T ϕ [xi 1 → ϕx i 1 T ϕ ,...,xi k → ϕx i k T ϕ ] .
Since in T ϕ we have that λ(x ij ) = ϕ xi j T ϕ the last expression is equal to

ψ free(X1) T ϕ . Part 3. Suppose {x i1 , . . . , x i k } = X 2 ∩ free(ψ free(X1)
). Following the same argumentation as in part 2 we get that unf X2 ϕ ψ free(X1) T ϕ is equal to

ψ free(X1) T ϕ [xi 1 → unf X -i 1 2 ϕ ϕx i 1 T ϕ ,...,xi k → unf X -i k 2 ϕ ϕx i k T ϕ ]
.

With Lemma 6.1 we get the equality with

ψ free(X1) T ϕ [xi 1 → ϕx i 1 T ϕ ,...,xi k → ϕx i k T ϕ ] ,
and because in T ϕ we have that λ(x ij ) = ϕ xi j T ϕ the last expression is equal to ψ free(X1) T ϕ which by part 1 is equal to ψ T ϕ . ⊣ Lemma 6.3. Let ϕ be a µ-formula and T = (S, → T , λ T ) be a transition system. For all X ⊆ bound(ϕ), all x k ∈ X = bound(ϕ) \ X, all ψ ≤ ϕ and all x / ∈ X we have that

1. unf X ϕ -X ψ -X T ⊆ unf X∪{x k } ϕ -X -k ψ -X -k T , 2. unf X ϕ -X ψ -X T ⊆ unf bound(ϕ) ϕ ψ T , 3. unf X ϕ -X (ϕ -X ) x T ϕ ⊆ ϕ x T ϕ , 4. ψ -X T ϕ -X ⊆ ψ T ϕ .
Proof. Suppose σ is a winning strategy for Player 0 in E(unf X ϕ -X ψ -X , (T , s)). By definition, any winning play for Player 0 starting from unf X ϕ -X ψ -X , s and compatible with σ do not reach a position of type ⊥, s ′ . Thus, this strategy determines a winning strategy for Player 0 in E(unf

X∪{x k } ϕ -X -k ψ -X -k
, (T , s)). Part 1 is then obtained by applying Theorem 3.2. Part 2 follows by a finite reiteration of part 1. In order to obtain part 3 just apply Lemma 6.1 to part 2 and note that, since x / ∈ X, (ϕ -X ) x ≡ (ϕ x ) -X . Part 4 is also a consequence of an application of Lemma 6.1 to part 2. ⊣ 6.2. A first reduction. We begin with a Lemma whose proof is standard.

Lemma 6.4. Let T be a transitive transition system and let s, s ′ be two stated such that s → T s ′ . For all µ-formulae ϕ we have that

s ∈ ϕ T =⇒ s ′ ∈ ϕ T and s ′ ∈ 3ϕ T =⇒ s ∈ 3ϕ T .
Theorem 6.5. Let T be a transitive transition system and let νx.ϕ(x) be a formula such that x is weakly universal. We have that νx.ϕ(x) T = ϕ(ϕ(⊤)) T .

Proof. The ⊆ inclusion is clear. For the ⊇ inclusion, define A = ϕ(ϕ(⊤)) T ; by definition of greatest fixpoint it is enough to show that we have

A ⊆ ϕ(A) T . (2)
First, recall that we assume that νx.ϕ(x) is well-named. This means that in the formula ϕ(x) the variable x is in the scope of a modal operator and, therefore, we can assume that ϕ is of the form β( α(x)). Moreover x occurs only once in ϕ. This implies that α(x) and α(ϕ(x)) occur only once in the formula tree of ϕ(ϕ(x)). Let s ∈ A, by Theorem 3.2 there is a winning strategy σ for Player 0 in the evaluation game E(ϕ(ϕ(x)), (T [x → S], s)). Let π be an arbitrary play consistent with σ. If π reaches a vertex of the form α(x), s ′ then the same play reaches a vertex of the form α(ϕ(x)), s ′′ , with α(x) ≤ α(ϕ(x)) and s ′ reachable from s ′′ in T [x → S]. Since σ is a winning strategy for Player 0 by Proposition 3.7 we have that

s ′′ ∈ α(ϕ(x)) T [x →S] and s ′ ∈ α(x) T [x →S] .
Since T [x → S] is transitive we have that s ′′ → T [x →S] s ′ and, by applying Lemma 6.4, we have

s ′ ∈ α(ϕ(x)) T [x →S] .
Hence, we have shown that for all plays π consistent with σ, if π reaches a vertex of the form α(x), s ′ then, by Theorem 3.2, there is a winning strategy for Player 0 in the evaluation game E( α(ϕ(x)), (T [x → S], s ′ )). A fortiori, this implies that if π reaches a vertex of the form α(x), s ′ then there is a winning strategy σ α(x),s ′ for Player 0 in E( α(x), (T [x → ϕ(x) T [x →S] ], s ′ )). Therefore, since ϕ(x) T [x →S] ⊆ S, the strategy σ * given by following σ but switching to the corresponding σ α(x),s ′ when a position of the form α(x), s ′ is reached, is winning for Player 0 in the parity game E(ϕ(ϕ(x)), (T [x → S], s)).

Let B := ϕ(x) T [x →S]
. By construction of σ * we have that for all vertices of the form x, v which are reachable by σ * it holds that v ∈ B. Then, by applying Lemma 3.3, σ * can be converted into a winning strategy for Player 0 in E(ϕ(ϕ(x), (T [x → B], s)). By Theorem 3.2, we have that

s ∈ ϕ(ϕ(B)) T [x →S]
which can be reformulated as s ∈ ϕ(ϕ(ϕ(⊤))) T or s ∈ ϕ(A) T . Therefore, we have proved Equation 2and completed the proof. ⊣ Definition 6.6. The syntactical translation τ : L µ → L µ is defined recursively on the structure of the formula such that τ (p) = p, τ (¬p) = ¬p, τ (⊥) = ⊥ and τ (⊤) = ⊤, such that it distributes over boolean and modal connectives, and such that

• τ (µx.ϕ) = τ wn(ϕ(ϕ(⊥))) , x is weakly existential in ϕ • τ (µx.ϕ) = wn(µx.τ (ϕ)), x is universal in ϕ • τ (νx.ϕ) = τ wn(ϕ(ϕ(⊤))) , x is weakly universal in ϕ • τ (νx.ϕ) = wn(νx.τ (ϕ)), x is existential in ϕ.
First, note that in each defining clause τ (ϕ) is defined via an application of τ to a formula whose rank, by Lemma 2.2, is strictly smaller than the rank of ϕ. Thus τ terminates and is well-defined. Note also, that it can be proved by induction on the structure of ϕ that all variables which are existential (resp. universal) in ϕ are weakly existential (resp. universal) in τ (ϕ) and that therefore for all µx.α ≤ τ (ϕ) we have that x is weakly universal and for all νx.α ≤ τ (ϕ) we have that x is weakly existential. Corollary 6.7. On transitive transition systems we have that

ϕ T = τ (ϕ) T .
Proof. By induction on rank(ϕ). If rank(ϕ) = 1 or rank(ϕ) is a successor ordinal the proof is straightforward. If rank(ϕ) is a limit ordinal then ϕ is of the form ηx.α. We distinguish four cases. If ϕ is of the form νx.α and x is existential in ϕ the induction step is straightforward. Similarly for ϕ of the form µx.α and x is universal in ϕ. If ϕ is of the form νx.α and x is in the scope of a in ϕ the induction step follows from Theorem 6.5 and Lemma 2.5. In the third case, if ϕ is of the form µx.α and x is in the scope of a 3 in ϕ then ¬ϕ is of the form νx.¬α[x/¬x] and x is in the scope of a in ¬ϕ. Since in this case rank(ϕ) = rank(¬ϕ) we can apply the induction step as in the third case. ⊣ 6.3. Normalizing the winning strategies. Let T be a transitive transition system and ϕ a µ-formula. Consider an arbitrary (memoryless) strategy σ for Player 0, not necessarily winning. We define the restriction of E(ϕ, (T , s 0 )) on σ, denoted by E| σ (ϕ, (T , s 0 )), as follows:

• The set of positions V | σ of the restriction is given by all nodes which are the positions of some play compatible with σ starting from position ϕ, s 0 , • The arena of E| σ (ϕ, (T , s 0 )) is the triple

V 0 | σ , V 1 | σ , E| σ where: 1. V 0 | σ = ∅, 2. V 1 | σ = V | σ , 3. if ψ, s ∈ V | σ ∩ V 1 then E| σ ( ψ, s ) = E( ψ, s ), and 4. if ψ, s ∈ V | σ ∩ V 0 then E| σ ( ψ, s ) = {σ( ψ, s )}.
• The ranking function Ω| σ is given by the restriction of Ω on V | σ . Note, that if T is finite then V | σ is finite, too. We have that in E| σ (ϕ, (T , s 0 )) the only Player who can move is Player 1. This can be done because the moves for Player 0 are already completely determined by the (memoryless) strategy σ. Clearly, any play in E| σ (ϕ, (T , s 0 )) is a play in E(ϕ, (T , s 0 )) compatible with σ. We say that a play π in E| σ (ϕ, (T , s 0 )) is winning for Player 0 if and only if the play π is winning for Player 0 in E(ϕ, (T , s 0 )). If σ is a winning strategy for Player 0 then any play in E| σ (ϕ, (T , s 0 )) is winning for Player 0. Example 6.8. Look at the arena depicted in Example 3.4. The non-dotted part of the picture represents the arena of a restricted evaluation game. Definition 6.9. Let T be a finite transitive transition system and ϕ a µformula. Suppose there is a winning strategy σ for Player 0 in the parity game E(ϕ, (T , s 0 )). Then, for every position ψ, s of E| σ (ϕ, (T , s 0 )), we define a measure d( ψ, s ). We distinguish two cases in the definition, depending on whether the strongly connected component scc( ψ, s ) of ψ, s in E| σ (ϕ, (T , s 0 )) is empty or not:

1. scc( ψ, s ) = ∅ :

d( ψ, s ) = 0 if E| σ ( ψ, s ) = ∅ max{d( φ, s ′ ) : φ, s ′ ∈ E| σ ( ψ, s )} + 1 else 2. scc(ψ, s) = ∅ : d( ψ, s ) = 0 if {E| σ ( α, s ) : α, s ∈ scc(ψ, s)} \ scc(ψ, s) = ∅, else d( ψ, s ) = max{d( φ, s ′ ) : φ, s ′ / ∈ scc( ψ, s ) and exists ξ, s ′′ ∈ scc( ψ, s ) with φ, s ′ ∈ E| σ ( ξ, s ′′ )} + 1.
For all finite transition systems d is a well-defined measure. Indeed, if we have a finite transition system we obviously have a finite arena which can be collapsed to a finite and well-founded graph by identifying all vertices in the arena which are in the same strongly connected component. It is clear that on finite and well-founded graphs d is well-defined. By noting that on the original arena the measure of a vertex corresponds to its measure of the collapsed arena we get that d is well-defined. Lemma 6.10. Let T be a finite transitive transition system and ϕ ∈ Σ µ 2 . Suppose there is a winning strategy σ for Player 0 in the parity game E(ϕ, (T , s 0 )). If y ∈ bound(ϕ) is a µ-variable, then for every position y, s ∈ V | σ , we have that scc( y, s ) = ∅.

Proof. If scc( y, s ) = ∅ then Player 1 can determine a play π in the restricted game E| σ (ϕ, (T , s 0 )) where y, s occurs infinitely often, since in E| σ (ϕ, (T , s 0 )) only Player 1 moves and therefore can stay as long as he wants in a strongly connected component. Remember that ϕ ∈ Σ µ 2 . Thus, there is no ν-variable free in ϕ y . Moreover, if y ∈ free(ϕ x ), where x is an arbitrary ν-variable, we have that Ω( y, s ) is strictly greater than the priorities of x and ϕ x positions. Therefore, π is winning for Player 1. But since π is compatible with σ, the play must be winning for Player 0, too. A contradiction.

⊣ Given the restriction of E(ϕ, (T , s 0 )) on a winning strategy σ and the measure d on V | σ we define the normalization of σ, denoted by σ N , as follows:

• For all positions 3β, s ′ ∈ V | σ we have that

σ N ( 3β, s ′ ) = σ( 3β, s ′ ), if d(σ( 3β, s ′ )) is the minimum of the set {d( β, s ) : β, s ∈ E( 3β, s ′ )}, where any β, s ∈ E( 3β, s ′ ) has to be reachable from 3β, s ′ in V | σ . Else σ N ( 3β, s ′ ) = β, s ′′ , where β, s ′′ ∈ E( 3β, s ′ ) is a vertex reachable from 3β, s ′ in V | σ such that d( β, s ′′ ) is the minimum of the set {d( β, s ) : β, s ∈ E( 3β, s ′ )} where any β, s ∈ E( 3β, s ′ ) has to be reachable from 3β, s ′ in V | σ .
• If ψ is not of the form 3β then we simply set σ N ( ψ, s ) = σ( ψ, s ).

Intuitively, given a winning strategy σ for Player 0 on E(ϕ, (T , s 0 )), the normalized strategy σ N for Player 0 is given by adapting σ such that for all vertexes of the form 3β, s ′ Player 0 moves to a vertex β, s ′′ whose measure is the minimal measure of all positions of the type β, s reachable from 3β, s ′ which are still winning in E(ϕ, (T , s 0 )). We have the following lemma.

Lemma 6.11. Let T be a finite transitive transition system. If σ is a winning strategy for Player 0 on E(ϕ, (T , s 0 )) then σ N is a winning strategy for Player 0 on E(ϕ, (T , s 0 )), too.

Proof. First we prove the following claim: Claim : E| σ and E| σ N coincide on every non empty scc of E| σ N (ϕ, (T , s 0 )). The proof of the claim goes as follow. If there is no position of the form 3β, s in a scc of E| σ N (ϕ, (T , s 0 )), the claim is trivially verified. Consider now an arbitrary scc( 3β, s ) of E| σ N (ϕ, (T , s 0 )). Let ψ, t ∈ scc( 3β, s ), in order to prove the claim we have to show that

E| σ N ( ψ, t ) = E| σ ( ψ, t ). (a) If ψ is not of the form 3α, then E| σ N ( ψ, t ) = E| σ ( ψ, t ). (b) For the case where ψ = 3α then suppose that E| σ N ( ψ, t ) = E| σ ( ψ, t ) and that E| σ N ( ψ, t ) = { α, t ′ }. Note, that by construction of σ N the position α, t ′ is the only successor of ψ, t . Since E| σ N ( ψ, t ) = E| σ ( ψ, t ) it must hold that d( α, t ′ ) < d( ψ, t ) (3)
where d is the depth defined on E| σ (ϕ, (T , s 0 )). Since scc( 3α, t ) = ∅ and since α, t ′ is the only position reachable in one step from 3α, t we have that α, t ′ ∈ scc( 3α, t ) and therefore that 3α, t is reachable from α, t ′ in E| σ N (ϕ, (T , s 0 )). Since reachability in E| σ N (ϕ, (T , s 0 )) implies reachability in E| σ (ϕ, (T , s 0 )) we can infer that d( α, t ′ ) ≥ d( 3α, t ), where d is the depth defined on E| σ (ϕ, (T , s 0 )). This is a contradiction to point 3 and therefore the claim is proved.

Consider an arbitrary play π in the graph of E| σ N (ϕ, (T , s 0 )). If π is finite, then by construction of the normalized arena the play is winning for Player 0. If π is infinite then from a certain position, say α, t , we are in a scc of E| σ N (ϕ, (T , s 0 )). But then by the previous claim after α, t the strategies of σ and σ N coincide. Since by construction of σ N the position α, t is winning in E| σ (ϕ, (T , s 0 )) the highest priority appearing infinitely often in π must be even and, therefore π is a winning play in E(ϕ, (T , s 0 )) for Player 0. ⊣

In the next lemma we prove that, when considering Σ µ 2 -formulae, normalized strategies have a nice and very usefull property. Lemma 6.12. Let T be a finite transitive transition system and ϕ ∈ Σ µ 2 such that all ν-variables are weakly existential. Let σ N be a normalized winning strategy for Player 0 on E(ϕ, (T , s 0 )). Consider a position x, s 1 in E| σ N (ϕ, (T , s 0 )) where x ∈ bound(ϕ) is a ν-variable. Then, if there is a position y, s 2 reachable from x, s 1 in V | σ N , where y ∈ bound(ϕ) is a µ-variable, then there is no position x, s 3 reachable from y, s 2 in V | σ N .

Proof. Suppose there is a play π consistent with σ N such that we have the following regenerations: x, s 1 then y, s 2 and then x, s 3 , where x is a νvariable and y a µ-variable. Note that, since ϕ ∈ Σ µ 2 , we have that y ∈ free(ϕ x ), and therefore ϕ x < ϕ y . This implies that in π we must have positions of the form 3(β(x)), s ′ 1 and β(x), s ′′ 1 before x, s 1 , and also positions of the form 3(β(x)), s ′ 3 and β(x), s ′′ 3 before x, s 3 but after y, s 2 . By construction of normalized strategy and by the transitivity of the transition system T it holds that d( β(x), s ′′ 1 ) = d( β(x), s ′′ 3 ) but also that d( β(x), s ′′ 1 ) = d( β(x), s ′′ 3 ) = d( y, s 2 ). This implies that scc( y, s 2 ) = ∅. Because σ N is a winning strategy for Player 0, by Lemma 6.10 we get the desired contradiction. ⊣

We immediately can restate the previous lemma as the following theorem.

Theorem 6.13. Suppose a finite transitive transition system T , a formula ϕ ∈ Σ µ 2 such that all ν-variables are weakly existential and a normalized winning strategy, σ N , of Player 0 in E(ϕ, (T , s)). If in a play π consistent with σ N there is a regeneration of a ν-variable x then either there is no more regeneration of a µ-variable after the first regeneration of x or, if there is such a regeneration of a µ-variable, then after this position there is no more regeneration of x.

6.4. Encoding normalized winning strategies. In Definition 6.14 we define the formulae NS - ϕ (X ′ , y) and NS + ϕ (x, X ′ ) used to encode the main properties of the normalization of winning strategies of ϕ given by Theorem 6.13. Encoding, in this context, will be formalized in the two main Lemmas of the section, Lemmas 6.16 and 6.17. The intuition behind these formulae is the following:

• NS - ϕ (X ′ , y) reflects the fact that we are regenerating y and any ν-variable regenerated afterwards will be an element of X ′ , • NS + ϕ (x, X ′ ) reflects the fact that we are regenerating x and if we regenerate any µ-variable then afterwards any ν-variable regenerated will be an element of X ′ .

In the sequel, in order to ease notation, we write a formula of the form ϕ free(X) y instead of (ϕ free(X) ) y . Definition 6.14. Let ϕ be a Σ µ 2 -formula. Let Y = {y 1 , . . . , y k } be the set of all µ-variables in ϕ and X be the set of all ν-variables in ϕ. For all subsets of X ′ ⊂ X, all ν-variables x such that x ∈ X/X ′ and all µ-variables y we define the formulae NS + ϕ (x, X ′ ) and NS - ϕ (X ′ , y) recursively on the size of X ′ such that

NS - ϕ (∅, y) ≡ unf Y ϕ -X ((ϕ -X ) y
) and, such that

NS + ϕ (x, ∅) ≡ (unf X ϕ free(Y ) ϕ free(Y ) x )[y 1 /NS - ϕ (∅, y 1 ), . . . , y k /NS - ϕ (∅, y k )]. If X ′ = {x i1 , . . . , x i l } and X ′ = X \ X ′ , then NS - ϕ (X ′ , y) ≡ (unf Y (ϕ -X ′ ) free(X ′ ) (ϕ -X ′ ) free(X ′ ) y )[ x i1 /NS + ϕ -X ′ (x i1 , X ′ -i1 ), . . . x i k /NS + ϕ -X ′ (x i l , X ′ -i l )],
and

NS + ϕ (x, X ′ ) ≡ (unf X ′ ϕ free(Y ∪X ′ ) ϕ free(Y ∪X ′ ) x
)[ y 1 /NS - ϕ (X ′ , y 1 ), . . .

y k /NS - ϕ (X ′ , y k ), x i1 /NS + ϕ (x i1 , X ′ -i1
), . . .

x i l /NS + ϕ (x i l , X ′ -i l )
]. Note that by construction we have that for every ν-variable x, every µ-variable y and every set of ν-variables X ′ , free(NS + ϕ (x, X ′ )), free(NS - ϕ (X ′ , y)) ⊆ free(ϕ) and bound(NS + ϕ (x, X ′ )), bound(NS - ϕ (X ′ , y)) ⊆ bound(ϕ). Lemma 6.15. Let ϕ ∈ Σ µ 2 , y be µ-variable in ϕ and X ′ be a proper subset of the set of all ν-variables. Suppose that x i is a ν-variable such that x i ∈ X ′ . We have that

NS - ϕ (X ′ , y), NS + ϕ (x i , X ′ ) ∈ ∆ µ 2 .
Proof. The proof goes by induction on the size of X ′ . If X ′ = ∅ then clearly NS - ϕ (X ′ , Y ) ∈ Σ µ 1 and, by definition of the formula, NS + ϕ (x, X ′ ) ∈ ∆ µ 2 . The induction step follows from the definitions by noting that the class ∆ µ 2 is closed under substitution of ∆ µ 2 formulae if no new variable is bound. ⊣ Lemma 6.16. Let ϕ be a Σ µ 2 -formula and X be the set of all ν-variables in ϕ. Suppose that all x ∈ X are weakly existential. Let (T , s 0 ) be a finite transitive transition system such that there is a normalized winning strategy σ N in the evaluation game E(ϕ, (T , s 0 )). The following holds for every X ′ ⊆ X where X ′ = X/X ′ :

1. If there is a play consistent with σ N which reaches a position y, s (y a µvariable in ϕ) such that on this play before y, s there are positions x, s for all x ∈ X ′ then it holds that s ∈ NS - ϕ (X ′ , y) T ϕ . 2. If there is a play consistent with σ N which reaches for the first time a position x, s (x a ν-variable in ϕ) such that on this play before x, s there are positions x, s for all x ∈ X ′ \ {x} then it holds that s ∈ NS + ϕ (x, X ′ ) T ϕ . Proof. Let Y = {y 1 , . . . , y k } be the set of all µ-variables in ϕ. We prove the two points simultaneously by induction on the size of X

′ . If X ′ = ∅ we have that NS - ϕ (∅, y) ≡ unf Y ϕ -X ((ϕ -X ) y ).
If there is a play consistent with σ N reaching a position of the form y, s whereby for all ν-variables there has been a regeneration in this play before, then, since σ N is a normalized strategy, by Theorem 6.13 there can not be any regeneration of a ν-variable after y, s . Therefore σ N determines a winning strategy in

E(unf Y ϕ -X ((ϕ -X ) y ), (T , s))
and with Theorem 3.2 we get the induction base for part 1. For part 2 remember that

NS + ϕ (x, ∅) ≡ (unf X ϕ free(Y ) ϕ free(Y ) x )[y 1 /NS - ϕ (∅, y 1 ), . . . , y k /NS - ϕ (∅, y k )].
Suppose that there is a play consistent with σ N which reaches for the first time a position x, s (x ∈ X) such that on this play before x, s there are positions x, s for all x ∈ X \ {x}. Then, since σ N is a normalized strategy, by Theorem 6.13 for every play extending this position which is compatible with σ N , either there are only regenerations of ν-variables, or, if there is a regeneration of a y, s , then after this regeneration there is no more regeneration of a ν-variable. Therefore σ N determines a winning strategy in

E((unf X ϕ free(Y ) ϕ free(Y )
x

)[y 1 /NS - ϕ (∅, y 1 ), . . . , y k /NS - ϕ (∅, y k )], (T , s)) and with Theorem 3.2 we get the induction base for part 2.

For the induction step of part 1, let X ′ = {x i1 , . . . , x i l } and let y, s be a position of a play consistent with σ N such that all x ∈ X ′ have been regenerated before. Then, by Theorem 6.13 for all ν-variables x i regenerated afterwards in the play we have x i ∈ X ′ . By construction for such a position x i , s i we will have that all ν-variables in X ′ are regenerated before this position. Define X ′ -i = X ′ \ {x i }. It can easily be seen that x i , s i satisfy the condition of part 2 and, since x i ∈ X ′ , that X ′ -i X ′ . Therefore, we can apply induction hypothesis of part 2 and get

s i ∈ NS + (x i , X ′ -i ) T .
Recapitulating, we have that for all plays consistent with σ N starting from y, s if a ν-variable x i is regenerated by a position x i , s i then s i ∈ NS + (x i , X ′ -i ) T and otherwise we have only regenerations of µ-variables. But by Lemmas 2.4.1 and 3.3 this means that σ N gives us a winning strategy in the evaluation game E(γ, (T , s))

where γ ≡ unf Y (ϕ -X ′ ) free(X ′ ) ((ϕ -X ′ ) free(X ′ ) y )[ x i1 /NS + ϕ -X ′ (x i1 , X ′ -i1 ), . . . x i l /NS + ϕ -X ′ (x i l , X ′ -i l )].
By noting that γ ≡ NS - ϕ (X ′ , y) and using Theorem 3.2 we finish the induction step for part 1.

For the induction step of part 2 let x, s be a position of a play consistent with σ N such that all x ∈ X ′ have been regenerated before. There are only three disjoint classes of winning plays (consistent with σ N ) extending the position x, s and they are obtained by considering all possible regenerations of bound variables after this position:

1. The class of plays in which afterwards we regenerate a x i ∈ X ′ in a position x i , s i , and before this position there was no regeneration of a µ-variable.

In this case we can apply the induction hypothesis for part 2 to the set X ′ -i and get

s i ∈ NS + ϕ (x i , X ′ -i ) T . 2.
The class of plays in which afterwards we regenerate a µ-variable y in a position y, s y , and before this position there was no regeneration of a x i ∈ X ′ . In this case, we can apply part 1, where the induction step is already done, and get s y ∈ NS - ϕ (X ′ , y) T . 3. The class of plays in which there is no regeneration of z ∈ X ′ ∪ Y , but there are eventually only regenerations of x i ∈ X ′ . Because these plays are consistent with σ N , they are winning. Therefore, they are winning in the evaluation game E((unf

X ′ ϕ -(Y ∪X ′ ) ϕ -(Y ∪X ′ ) x
), (T , s)), too. By Lemmas 2.4.1 and 3.3 we have that

s ∈ (unf X ′ ϕ free(Y ∪X ′ ) ϕ free(Y ∪X ′ ) x )[ y 1 /NS - ϕ (X ′ , y 1 ), . . . y k /NS - ϕ (X ′ , y k ), x i1 /NS + ϕ (x i1 , X ′ -i1 ), . . . x i l /NS + ϕ (x i l , X ′ -i l )]
T . and this ends the induction step of part 2 and the proof. ⊣ Lemma 6.17. Let ϕ be a Σ µ 2 -formula and X be the set of all ν-variables in ϕ. Suppose that all ν-variables are weakly existential. Then, for every finite transitive transition system T and for every X ′ ⊆ X it holds that 1. For every y ∈ Y we have NS - ϕ (X ′ , y) T ϕ ⊆ ϕ y T ϕ , and 2. for every x ∈ X ′ =: X/X ′ we have

NS + ϕ (x, X ′ ) T ϕ ⊆ ϕ x T ϕ .
Proof. Let Y = {y 1 , . . . , y k } be the set of all µ-variables. We prove the two points simultaneously by induction on the size of X ′ . Suppose X ′ is empty. Then we have that NS - ϕ (∅, y) ≡ unf Y ϕ -X ((ϕ -X ) y ) and by Lemma 6.3.3 we obtain unf Y ϕ -X ((ϕ -X ) y ) T ϕ ⊆ ϕ y T ϕ . Therefore we complete the base case of the induction for part 1. For part 2 remember that

NS + ϕ (x, ∅) ≡ (unf X ϕ free(Y ) ϕ free(Y ) x )[y 1 /NS - ϕ (∅, y 1 ), . . . , y k /NS - ϕ (∅, y k )]
. Thus, by the induction base of part 1 and by Lemma 2.4.4, we have that

(unf X ϕ free(Y ) ϕ free(Y ) x )[y 1 /NS - ϕ (∅, y 1 ), . . . , y k /NS - ϕ (∅, y k )] T ϕ ⊆ (unf X ϕ free(Y ) ϕ free(Y ) x )[y 1 /ϕ y1 , . . . , y m /ϕ ym ] T ϕ .
But because in T ϕ we have that λ(y) = ϕ y T ϕ and by applying Lemma 2.4.1 and Lemma 6.2.2, it holds that

(unf X ϕ free(Y ) ϕ free(Y ) x )[y 1 /ϕ y1 , . . . , y m /ϕ ym ] T ϕ ⊆ ϕ x T ϕ . Therefore (unf X ϕ free(Y ) ϕ free(Y ) x )[y 1 /NS - ϕ (∅, y 1 ), . . . , y k /NS - ϕ (∅, y k )] T ϕ ⊆ ϕ x T ϕ .
This ends the induction base for both parts 1 and 2. Let X ′ = {x i1 , . . . , x i l }. For the induction step of part 1, remember that

NS - ϕ (X ′ , y) ≡ unf Y (ϕ -X ′ ) free(X ′ ) ((ϕ -X ′ ) free(X ′ ) ) y [ x i1 /NS + ϕ -X ′ (x i1 , X ′ -i1 ), . . . x i l /NS + ϕ -X ′ (x i l , X ′ -i l )].
By induction hypothesis, by Lemma 2.4.4 and because in T ϕ -X ′ the evaluation of a variable x ij ∈ X ′ is equal to (ϕ -X ′ ) xi j T ϕ -X ′ , we obtain

NS - ϕ (X ′ , y) T ϕ = unf Y (ϕ -X ′ ) free(X ′ ) ((ϕ -X ′ )
free(X ′ ) y

) [x i1 /NS + ϕ -X ′ (x i1 , X ′ -i1 ), . . .

x i l /NS + ϕ -X ′ (x i l , X ′ -i l )] T ⊆ unf Y
(ϕ -X ′ ) free(X ′ ) ((ϕ -X ′ ) free(X ′ ) ) y T ϕ -X ′ .

With Lemma 6.2.2 we obtain unf Y (ϕ -X ′ ) free(X ′ ) ((ϕ -X ′ ) free(X ′ ) y ) T ϕ -X ′ = (ϕ -X ′ ) y T ϕ -X ′ .

Finally, because by Lemma 6.3.4 it holds that (ϕ -X ′ ) y T ϕ -X ′ ⊆ ϕ y T ϕ we get NS - ϕ (X ′ , y) T ϕ ⊆ ϕ y T ϕ .

For the induction step of part 2 if X = X \ X ′ , then by induction hypothesis and by part 1 we have for every finite transitive transition system T NS - ϕ (X ′ , y 1 ) T ϕ ⊆ ϕ y1 T ϕ , . . .

NS - ϕ (X ′ , y k )] T ϕ ⊆ ϕ y k T ϕ , NS + ϕ (x i1 X ′ -i1 ) T ϕ ⊆ ϕ xi 1 T ϕ , . . . NS + ϕ (x i l X ′ -i l ) T ϕ ⊆ ϕ xi l T ϕ .
• R(νx.ϕ) = ¬(R(µx.¬ϕ[x/¬x])) Lemma 6.24. For all µ-formula ϕ we have that 1. R(ϕ) is well-defined, and 2. R(ϕ) ∈ ∆ µ 2 . Proof. We prove both parts simultaneously by induction on the structure of ϕ. The induction cases for boolean and modal connectives are trivial. If ϕ is of the form µx.α we have that R(µx.α) = wn ρ(τ (wn(µx.(R(α))))) . Because τ is a well-defined syntactical transformation, and neither wn nor τ increase the alternation depth of a formula, the application of ρ in the clause of R(µx.α) is well-defined by induction hypothesis. Thus, R(ϕ) terminates and therefore it is well-defined too. The fact that R(µx.α) ∈ ∆ µ 2 follows by induction hypothesis, by the fact that, by Remark 6.19, for all Σ µ 2 -formulae ψ we have that ρ(ψ) ∈ ∆ µ 2 , and because we know that τ and wn do not increase the alternation depth. If ϕ is of the form νx.α, on one hand R(νx.α) is well-defined because the clause for this form is defined via a reducing case R(µx.¬ϕ[x/¬x]), and, on the other hand R(ϕ) ∈ ∆ µ 2 because ∆ µ 2 is closed under negation. ⊣ Theorem 6.25. For all ϕ ∈ L µ and all finite transitive transition systems T we have that

and induction hypothesis

If ϕ is of the form νx.α we do a similar induction step like above by using the equivalence νx.α T = ¬µx.¬α[x/¬x] T . ⊣ We conclude by verifying that the syntactical translation R is also an explicit syntactical translation of all modal µ-formulae to the alternation free fragment preserving denotation in every transitive transition systems. The proof goes with similar argument as in Corollary 6.22 and it is left to the reader. Theorem 6.26. For all ϕ ∈ L µ and all transitive transition systems T we have that ϕ T = R(ϕ) T . Remark 6.27. Note, that due to the example of Visser in [START_REF] Visser | Uniform interpolation and layered bisimulation[END_REF] mentioned in the introduction the alternation-free fragment is also the optimal bound if restrict ourselves to transition systems which are transitive and reflexive. Example 6.28. Let's have a look at our example from Section 2. In the case of "always eventually", we have that νx.(µy.(p ∨ 3y)) ∧ x) T t = (p ∨ 3p) ∧ (p ∨ 3p) T t .

For "infinitely often", it holds that νx.µy.((p ∨ 3y)) ∧ 3x) T t = νx.(p ∧ 3x) T t . But, because from footnote 4 of the introduction we know that νx.(p ∧ 3x) cannot be reduced to any purely modal formula, contrary to the transitive and symmetric case, over transitive transition systems "infinitely often" cannot be expressed by a ∆ µ 1 formula. §7. Strictness of the hierarchy for reflexive transition systems. In this section we prove the strictness of the modal µ-calculus hierarchy on reflexive transition systems. In doing this, we follows the argumentation of the proof of the strictness of the hierarchy on all binary transition systems presented in [START_REF] Alberucci | Strictness of the Modal µ-Calculus Hierarchy[END_REF]. First, we adapt the game transition system such that it is reflexive.

Let E(ϕ, (T , s)) be a parity game with priority function Ω and with corresponding pointed game transition system T (E(ϕ, (T , s))). We extend the edge relation E of the parity game to its reflexive closure E r = E ∪{(s, s); s ∈ V 0 ∪V 1 }, and change our priority function Ω to Ω r such that for all vertices ψ, s where ψ ≡ ηx.δ (η ∈ {µ, ν}) we have Ω r ( ψ, s ) = Ω( ψ, s ) + 2 and such that for all other vertices we define:

• if min Ω is even

Ω r ( ψ, s ) = 0 if ψ, s ∈ V 1 1 if ψ, s ∈ V 0 .
• if min Ω is odd

Ω r ( ψ, s ) = 2 if ψ, s ∈ V 1 1 if ψ, s ∈ V 0 .
The new resulting "reflexive" parity game is denoted as E r (ϕ, (T , s)). The following Lemma can be proved by unwinding the definition of winning strategy. Lemma 7.1. Player 0 has a winning strategy for E r (ϕ, (T , s)) iff Player 0 has a winning strategy for E(ϕ, (T , s)).

Given a "reflexive" parity game E r (ϕ, (T , s)) the pointed game transition system T (E r (ϕ, (T , s))) is defined analogously as above. Obviously, the pointed game transition system T (E r (ϕ, (T , s))) is reflexive. We have that Proposition 7.2. Let (T , s) be an arbitrary pointed transition system. For all ϕ ∈ Π µ n we have that T (E r (ϕ, (T , s))) ∈ W Π µ n+2 if and only if T (E(ϕ, (T , s))) ∈ W Π µ n and dually for ϕ ∈ Σ µ n . Proof. This follows directly by the definition of the "reflexive" parity game E r (ϕ, (T , s)) and by applying Proposition 3.6 to Lemma 7.1. ⊣ Theorem 7.6. 1. The modal µ-calculus hierarchy is strict over reflexive transition systems. 2. The modal µ-calculus hierarchy is strict over finite reflexive transition systems.

Proof. Part 1 is a corollary of Theorem 7.5. For Part 2, let ϕ ∈ Σ T r n \ Π T r n . Then, by Part 1 we know that for every ψ ∈ Σ µ n-1 it holds that ¬(ϕ ↔ ψ) has a reflexive model. By Theorem 4.3, this model can be finite. Hence ϕ ∈ Σ µ n is not equivalent to any Σ µ n-1 formula on finite reflexive transition systems. ⊣

Theorem 3 . 2 (

 32 [START_REF] Streett | An automata theoretic decision procedure for the propositional µ-calculus[END_REF]). (T , s) ∈ ϕ iff Player 0 has a winning strategy for E(ϕ, (T , s)).

  3α) tr = µx.3(α tr ∨ x), and • (ηx.α) tr = ηx.α tr where η ∈ {µ, ν}.

ϕ

  T = R(ϕ) T . Proof. We prove the equivalence by induction on rank(ϕ) simultaneously for all finite transitive transition systems T . The induction cases for boolean and modal connectives are trivial. If ϕ is of the form µx.α we have that R(µx.α) T = wn ρ(τ (wn(µx.R(α)))) T by definition of R = wn(µx.R(α)) T τ (wn(µx.R(α))) ∈ Σ µ 2 , and by Lemma 2.5 and Theorem 6.20 = µx.α T by Lemma 2.

Cf. Chapter 5 in[START_REF] Hughes | A New Introduction to Modal Logic[END_REF].

Acknowledgements. We thank Igor Walukiewicz, and especially Giovanna D'Agostino and Giacomo Lenzi for various comments on a preliminary version of this paper. We also thank an anonymous referee for valuable comments.

Therefore, by Lemmas 2.4.4 and 2.4.1, and because for every z ∈ bound(ϕ) we have that λ(z) = ϕ z T ϕ , we get (unf X ′ ϕ free(Y ∪X ′ ) (ϕ free(Y ∪X ′ ) x

))[ y 1 /NS - ϕ (X ′ , y 1 ), . . . y k /NS - ϕ (X ′ , y k ) x i1 /NS + ϕ (x i1 , X ′ -i1 ), . . .

Thus, we can apply Lemma 6.2.2 and obtain (unf

Because this implies that NS + ϕ (x, X ′ ) T ϕ ⊆ ϕ x T ϕ this ends the induction step of part 2 and the proof of the Lemma. ⊣ 6.5. The collapse over transitive models. Everything now is ready to prove the collapse of the µ-hierarchy over finite transitive transition systems.

Remark 6.19. By Lemma 6.15 it can easily be seen that ρ(ϕ) is indeed a ∆ µ 2 -formula.

Theorem 6.20. For all ϕ ∈ Σ µ 2 and all finite transitive transition systems T we have that

Proof. First, we observe that τ (ϕ) ∈ Σ µ 2 and that by Corollary 6.7 we have that ϕ T = τ (ϕ) T . Thus, we can assume that each ν-variable in ϕ ∈ Σ µ 2 is weakly existential and any µ-variable weakly universal. If X = {x 1 , . . . , x m } is the set of all ν-variables in ϕ, by definition of ρ we have to prove that

With Lemma 6.17 and, because all ν-variables appear positively in ϕ, by applying Lemma 2.4.4 we get that

By Lemma 2.4.4 and because in T ϕ we have that λ(x i ) = ϕ xi T ϕ , we obtain

T ϕ . Since by Lemma 6.2.2 we have that ϕ free(X) T ϕ = ϕ T we get this inclusion.

"⊆": Let s ∈ ϕ T . By Theorem 3.2 there is a winning strategy in E(ϕ, (T , s)) and by Theorem 6.13 it can be assumed to be normalized. Let π be any play consistent with the strategy starting from ϕ, s . We have that if there is a (first) regeneration of a ν-variable x i in a position x i , s i then by Lemma 6.16 we have that

where X is the set of all ν-variables in ϕ. Therefore, there is a winning strategy for Player 0 in

and with Lemma 2.4.1 we complete the proof. ⊣ Corollary 6.21. The modal µ-calculus hierarchy on finite transitive systems collapses to ∆ µ 2 .

Proof. By Theorem 6.20, Σ µT tf 2 = ∆ µT tf

2

. By duality, Π µT tf 2 = ∆ µT tf

2

. By this fact it is therefore very easy to verify inductively that for every n > 0, Σ µT tf 2+n = Π µT tf 2+n = ∆ µT tf

2

. ⊣ Corollary 6.22. The modal µ-calculus hierarchy on transitive systems collapses to ∆ µ 2 . Proof. Suppose that the hierarchy does not collapse. Therefore, there is a formula ϕ such that for all formula ψ ∈ ∆ µ 2 there is a transitive system T such that T , s 0 |= ¬(ϕ ↔ ψ). By Theorem 4.5, there is a finite transitive model T f such that T f , s f i |= ¬(ϕ ↔ ψ). But this cannot be the case by Corollary 6.21. ⊣ We end with the definition of a syntactical translation from L µ to ∆ µ 2 preserving equivalence on transitive transition systems.

Corollary 7.3. Let (T , s) be an arbitrary pointed transition system. For all ϕ ∈ Π µ n we have that:

if and only if (T , s) ∈ ϕ .

and dually for ϕ ∈ Σ µ n . Proof. By Proposition 7.2 and Corollary 3.8 we obtain our result.

⊣ For all formulae ϕ we define a function f ϕ (functional class) mapping a pointed transition system (T , s) to a reflexive transition system f ϕ (T , s) such that

The proof of the next Lemma follows similar arguments as the proof of the same result for arbitrary transition systems proved by one of the authors in [START_REF] Alberucci | Strictness of the Modal µ-Calculus Hierarchy[END_REF].

Lemma 7.4. For all formulae ψ ∈ Σ µ n (resp. Π µ n ), n ∈ N, there is an equivalent formula ϕ ∈ Σ µ n (resp. Π µ n ) such that the function f ϕ has a fixpoint in T r , that is, a pointed reflexive transition system (T F , s F ) such that f ϕ (T F , s F ) = (T F , s F ).

Theorem 7.5. For all natural numbers n ∈ N \ {0} we have that

n+1 . Proof. We proof the contrapositive. Assume that we have

we have ¬ϕ ∈ Σ µ n+1 and by assumption ¬ϕ ∈ Σ µ n and therefore ϕ ∈ Π µ n . Therefore, assuming the contrapositive leads to

, by definition, it can be inferred that Π T r n ⊆ Σ T r n , and from Π T r n+1 ⊆ Π T r n , by definition, it can be inferred that Σ T r n ⊆ Π T r n , by assuming the contrapositive we get that Π T r n+1 = Π T r n = Σ T r n+1 = Σ T r n and, obviously, we then have for all k ∈ N that

Since W Σ µ n+2 ∈ Σ µ n+2 we have that ¬W Σ µ n+2 ∈ Π µ n+2 and with equation 4 we get ¬W Σ µ n+2 T r ∈ Σ T r n . By Lemma 7.4 there is a formula ϕ ∈ Σ µ n equivalent to ¬W Σn+2 and a pointed transition system (T F , s F ) such that (T F , s F ) = f ϕ (T F , s F ).

Since f ϕ (T , s) is defined as T (E r (ϕ, (T , s))), by Corollary 7.3, for all pointed transition systems (T , s) we have that f ϕ (T , s) ∈ W Σn+2 if and only if (T , s) ∈ ϕ . Since ϕ is equivalent to ¬W Σn+2 we get that

which is a contradiction. ⊣