Radu Mateescu

Anton Wijs

Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity

Keywords: divergence-sensitive branching bisimulation, labeled transition system, modal µ-calculus, model checking, on-the-fly verification

When analyzing the behavior of finite-state concurrent systems by model checking, one way of fighting state space explosion is to reduce the model as much as possible whilst preserving the properties under verification. We consider the framework of action-based systems, whose behaviors can be represented by labeled transition systems (Ltss), and whose temporal properties of interest can be formulated in modal µ-calculus (L µ ). First, we determine, for any L µ formula, the maximal set of actions that can be hidden in the Lts without changing the interpretation of the formula. Then, we define L dsbr µ , a fragment of L µ which is adequate w.r.t. divergence-sensitive branching bisimilarity. This enables us to apply the maximal hiding and to reduce the Lts on-the-fly using divergence-sensitive τ -confluence during the verification of any L dsbr µ formula. The experiments that we performed on various examples of communication protocols and distributed systems show that this reduction approach can significantly improve the performance of on-the-fly verification 1 .

Introduction

Model checking [START_REF] Clarke | Model Checking[END_REF] is a technique to systematically verify whether a system specification meets a given temporal property. Although successfully applied in many cases, its usefulness in practice is still hampered by the state space explosion phenomenon, which may entail high memory and Cpu requirements in order to carry out the verification.

One way to improve the performance of model checking is to check the property at a higher level of abstraction; by abstracting parts of the system behavior away from the specification, its corresponding state space will be smaller, thereby easier to check. This can either be done globally, i.e., before verifying the property, or on-the-fly, i.e., during verification. However, one needs to be careful not to abstract away any details crucial for the outcome of the check, i.e., relevant for the property. This is known as action abstraction in action-based formalisms, where state spaces are represented by Labeled Transition Systems (Ltss), specifications are written using some flavor of process algebra [START_REF] Baeten | A Brief History of Process Algebra[END_REF], and temporal properties are described using an actionbased temporal logic, such as the modal µ-calculus (L µ ) [START_REF] Kozen | Results on the propositional µ-calculus[END_REF][START_REF] Stirling | Modal and Temporal Properties of Processes[END_REF]. Abstracted behavior is then represented by some predefined action, denoted τ in process algebras. In the past, the main focus in this area has been on devising L µ fragments adequate w.r.t. specific relations, such as Actl\X [START_REF] Nicola | Action versus State Based Logics for Transition Systems[END_REF], which is adequate w.r.t. divergence-sensitive branching bisimilarity [START_REF] Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF][START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF] 2 , or weak L µ [START_REF] Stirling | Modal and Temporal Properties of Processes[END_REF], which is adequate w.r.t. weak bisimilarity [START_REF] Milner | Communication and Concurrency[END_REF]. For such fragments, the minimization of an Lts modulo the specific relation preserves the truth value of all formulas written in the adequate L µ fragment. Other works focused on devising reductions targeted to specific formulas, such as those written in the selective L µ [START_REF] Barbuti | Selective Mu-Calculus and Formula-Based Equivalence of Transition Systems[END_REF]. For each selective L µ formula, it is possible to hide all actions not occurring in the formula, and subsequently minimize the Lts modulo τ * .a bisimilarity [START_REF] Fernandez | On the Fly" Verification of Behavioural Equivalences and Preorders[END_REF] before verifying the formula.

In this article, we propose two enhancements with respect to existing work. Firstly, starting from an arbitrary L µ formula, we determine automatically the maximal set of actions which can be hidden in an Lts without mula; and locally (or on-the-fly), by applying maximal hiding and reduction modulo divergence-sensitive τ -confluence simultaneously with the verification. The experiments we carried out on several examples of protocols and distributed systems, including a recent industrial case-study, show that these optimizations can yield significant performance improvements.

The rest of the article is organized as follows. Section 2 defines the formalisms and equivalence relations considered. Section 3 studies the maximal hiding of actions in an Lts w.r.t. a given L µ formula. Section 4 introduces the L dsbr µ fragment, shows its adequacy with divergence-sensitive branching bisimilarity, and compares its expressiveness with other logics. Section 5 illustrates experimentally the model checking optimizations obtained by applying maximal hiding and reductions for L dsbr µ formulas. Section 6 gives concluding remarks and directions for future work. The proofs of all lemmas and propositions are given in Appendix A.

Background

Labeled transition system. We consider as interpretation model the classical Lts, which underlies process algebras and related action-based description languages. An Lts is a tuple S, A, T, s 0 , where S is the set of states, A is the set of actions (including the invisible action τ ), T ⊆ S × A × S is the transition relation, and s 0 ∈ S is the initial state. The visible actions in A \ {τ } are denoted by a and the actions in A are denoted by b. A transition s 1 , b, s 2 ∈ T (also denoted by s 1 b → s 2 ) means that the system can move from state s 1 to state s 2 by performing action b. The reflexive transitive closure of τ → is denoted by = ⇒ . A finite path is denoted by s 0

b 0 •••b k-1 → s k ,
which is a finite sequence s 0 , s 1 , . . . , s k , such that there exist actions b 0 , . . . , b k-1 with ∀0 ≤ i < k.s i b i → s i+1 . For conciseness, we will sometimes omit existential quantifiers (e.g., we will write s 1 b → s 2 to denote the existence of a transition) when this is clear from the context. We consider only finite Ltss, i.e., containing finite sets of states and actions. In the following, we assume the existence of an Lts M = S, A, T, s 0 on which temporal formulas will be interpreted.

Modal µ-calculus. The variant of L µ that we consider here consists of action formulas (denoted by α) and state formulas (denoted by ϕ), which characterize subsets of Lts actions and states, respectively. The syntax and semantics of these formulas are defined in Figure 1. Action formulas are built over the set of actions by using Boolean connectors in a way similar to Actl (Actionbased Ctl) [START_REF] Nicola | Action versus State Based Logics for Transition Systems[END_REF], which is a slight extension w.r.t. the original definition of L µ [START_REF] Kozen | Results on the propositional µ-calculus[END_REF]. Derived action operators can be defined as usual: true = ¬false, α 1 ∧ α 2 = ¬(¬α 1 ∨ ¬α 2 ), etc. State formulas are built from Boolean connectors, the possibility modality ( ), and the minimal fixed point operator (µ) defined over propositional variables X belonging to a set X . Derived state operators can be defined as usual: true = ¬false, ϕ 1 ∧ ϕ 2 = ¬(¬ϕ 1 ∨ ¬ϕ 2 ), [α] ϕ = ¬ α ¬ϕ is the necessity modality, and νX.ϕ = ¬µX.¬ϕ[¬X/X] is the maximal fixed point operator (ϕ[¬X/X] stands for ϕ in which all free occurrences of X, i.e., not bound by a fixed point operator, have been negated). Syntactically, unary operators (negation, modalities, and fixed points) have higher precedence than binary ones (conjunction and disjunction).

Action formulas:

α ::= b | false | ¬α 1 | α 1 ∨ α 2 [[b]] A = {b} [[false]] A = ∅ [[¬α 1 ]] A = A \ [[α 1 ]] A [[α 1 ∨ α 2 ]] A = [[α 1 ]] A ∪ [[α 2 ]] A State formulas: ϕ ::= false | ¬ϕ 1 | ϕ 1 ∨ ϕ 2 | α ϕ 1 | X | µX.ϕ 1 [[false]] M ρ = ∅ [[¬ϕ 1 ]] M ρ = S \ [[ϕ 1 ]] M ρ [[ϕ 1 ∨ ϕ 2 ]] M ρ = [[ϕ 1 ]] M ρ ∪ [[ϕ 2 ]] M ρ [[ α ϕ 1 ]] M ρ = {s ∈ S | ∃s b → s ′ ∈ T.b ∈ [[α]] A ∧ s ′ ∈ [[ϕ 1 ]] M ρ} [[X]] M ρ = ρ(X) [[µX.ϕ 1 ]] M ρ = {U ⊆ S | [[ϕ 1 ]] M (ρ ⊘ [U/X]) ⊆ U }
b ∈ [[α]] A . A transition s 1 b → s 2 such that b |= A α is called an α-transition. A propositional context ρ : X → 2 S
is a partial function mapping propositional variables to subsets of states. The notation ρ⊘[U/X] stands for a propositional context identical to ρ except for variable X, which is mapped to the state subset U . The interpretation [[ϕ]] M ρ of a state formula on an Lts M and a propositional context ρ (which assigns a set of states to each propositional variable occurring free in ϕ) denotes the subset of states satisfying ϕ in that context. The Boolean connectors are interpreted as usual in terms of set operations. The possibility modality α ϕ 1 (resp. the necessity modality [α] ϕ 1 ) denotes the states for which some (resp. all) of their outgoing α-transitions lead to states satisfying ϕ 1 . The minimal fixed point operator µX.ϕ 1 (resp. the maximal fixed point operator νX.ϕ 1 ) denotes the least (resp. greatest) solution of the equation X = ϕ 1 interpreted over the complete lattice 2 S , ∅, S, ∩, ∪, ⊆ . A state s satisfies a closed formula ϕ, denoted by s |= M ϕ, if and only if s ∈ [[ϕ]] M (the propositional context ρ can be omitted since ϕ does not contain free variables). An Lts M = S, A, T, s 0 satisfies a closed formula ϕ, denoted by M |= ϕ, if and only if s 0 |= M ϕ.

Propositional Dynamic Logic with Looping. In addition to plain L µ operators, we will use the modalities of Pdl-∆ (Propositional Dynamic Logic with Looping) [START_REF] Streett | Propositional Dynamic Logic of Looping and Converse[END_REF], which characterize finite (resp. infinite) sequences of transitions whose concatenated actions form words belonging to regular (resp. ω-regular) languages. The syntax and semantics of Pdl-∆, as well as its translation to L µ [START_REF] Emerson | Efficient model checking in fragments of the propositional mu-calculus[END_REF], are given in Figure 2. Regular formulas (denoted by β) are built from action formulas and the testing (?), concatenation (.), choice (|), and transitive reflexive closure ( * ) operators. Apart from Boolean connectors, state formulas are built from the possibility modality ( ) and the infinite looping operator ( @), both containing regular formulas. Derived state operators are defined as follows: [β] ϕ = ¬ β ¬ϕ is the necessity modality, and [β] ⊣ = ¬ β @ is the saturation operator.

The interpretation ||β|| A of a regular formula on an Lts denotes a relation between the states that are source and target of transition sequences whose concatenated actions form a word belonging to the regular language defined by β. The testing operator makes it possible to specify state formulas that must hold in the intermediate states of a transition sequence. The possibility modality β ϕ 1 (resp. the necessity modality [β] ϕ 1 ) denotes the states for which some (resp. all) of their outgoing transition sequences satisfying β lead to states satisfying ϕ 1 . The infinite looping operator β @ (resp. the saturation operator [β] ⊣) denotes the states having some (resp. no) outgoing transition sequence consisting of an infinite concatenation of sub-sequences satisfying β.

The operators of Pdl-∆ can be freely mixed with those of L µ , and in practice they make possible a much more concise and intuitive description of Regular formulas: properties. For example, the fair reachability [START_REF] Queille | Fairness and related properties in transition systems -a temporal logic to deal with fairness[END_REF] (i.e., by skipping cycles) of a response after each request, can be specified in Pdl as follows:

β ::= α | ϕ? | β 1 .β 2 | β 1 |β 2 | β * 1 ||α|| A = {(s, s ′ ) ∈ S × S | ∃b ∈ A.s b → s ′ ∧ b ∈ [[α]] A } ||ϕ?|| A = {(s, s) ∈ S × S | s ∈ [[ϕ]] M } ||β 1 .β 2 || A = ||β 1 || A • ||β 2 || A ||β 1 |β 2 || A = ||β 1 || A ∪ ||β 2 || A ||β * 1 || A = ||β 1 || * A State formulas: ϕ ::= false | ¬ϕ 1 | ϕ 1 ∨ ϕ 2 | β ϕ 1 | β @ [[false]] M = ∅ [[¬ϕ 1 ]] M = S \ [[ϕ 1 ]] M [[ϕ 1 ∨ ϕ 2 ]] M = [[ϕ 1 ]] M ∪ [[ϕ 2 ]] M [[ β ϕ 1 ]] M = {s ∈ S | ∃s ′ ∈ S.(s, s ′ ) ∈ ||β|| A ∧ s ′ ∈ [[ϕ 1 ]] M } [[ β @]] M = {s ∈ S | ∀k ≥ 0.∃s ′ ∈ S.(s, s ′ ) ∈ ||β|| k A } Encoding in L µ : ϕ ′ ? ϕ = ϕ ′ ∧ ϕ β 1 .β 2 ϕ = β 1 β 2 ϕ β 1 |β 2 ϕ = β 1 ϕ ∨ β 2 ϕ β * ϕ = µX.(ϕ ∨ β X) β @ = νX. β X
[true * .req] true * .resp true whereas in plain L µ a more verbose formula is needed:

νX.([req] µY.( resp true ∨ true Y ) ∧ [true] X)
The variant of L µ extended with Pdl-∆ operators, denoted by L reg µ , has been considered and efficiently implemented in [START_REF] Mateescu | Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus[END_REF] (in fact, the syntax used for Pdl-∆ operators in Fig. 2 is that of L reg µ and not the original one). In the remainder of the article, we will use L reg µ whenever possible for specifying temporal properties.

Divergence-sensitive branching bisimilarity. As equivalence relation between Ltss, we consider divergence-sensitive branching bisimilarity [START_REF] Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF][START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF] 4 , which preserves branching-time properties such as inevitable reachability and also the existence of divergences (τ -cycles), while still making possible substantial reductions of Ltss. This relation is finer than plain branching bisimilarity and weak bisimilarity [START_REF] Milner | Communication and Concurrency[END_REF] (none of which preserves divergences), therefore being a good candidate for comparing the behaviour of concurrent systems.

Definition 1 (Divergence-Sensitive Branching Bisimulation [START_REF] Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF]). A binary relation R on the set of states S is a divergence-sensitive branching bisimulation if R is symmetric and s R t implies that

• if s b → s ′ then -either b = τ with s ′ R t; -or t = ⇒ t b → t ′ with s R t and s ′ R t ′ .
• if there is an infinite sequence of states s 0 , s When expressing certain properties (e.g., inevitable reachability), it is necessary to characterize deadlock states in the Lts, i.e., states from which the execution cannot progress anymore. From the ≈ ds br point of view, deadlock states are precisely those states leading eventually to sink states (i.e., states without successors) after a finite number of τ -transitions. These states can be characterized by the Pdl-∆ formula below:

deadlock = [true * .¬τ ] false ∧ [τ ] ⊣
where the box modality forbids the reachability of visible actions and the saturation operator forbids the presence of divergences.

Maximal Hiding

When checking a state formula ϕ over an Lts, some actions of the Lts can be hidden (i.e., renamed into τ ) without disturbing the interpretation of ϕ.

Definition 2 (Hiding Set). Let α be an action formula interpreted over a set of actions A. The hiding set of α w.r.t. A is defined as follows:

h A (α) = [[α]] A if τ |= A α A \ [[α]] A if τ |= A α
The hiding set of a state formula ϕ w.r.t. A, denoted by h A (ϕ), is defined as the intersection of h A (α) for all action subformulas α of ϕ. Definition 3 (Hiding). Let A be a set of actions and H ⊆ A. The hiding of an action b ∈ A w.r.t. H is defined as follows:

hide H (b) = b if b ∈ H τ if b ∈ H
The hiding of an Lts M = S, A, T, s 0 w.r.t. H is defined as follows:

hide H ( S, A, T, s 0 ) = S, (A \ H) ∪ {τ }, {s

1 hide H (b) → s 2 | s 1 b → s 2 ∈ T }, s 0 .
The following lemma states that, given an action formula α, the fact of hiding an action w.r.t. the hiding set of α does not disturb the interpretation of α on that action. Lemma 1. Let α be an action formula interpreted over a set of actions A. A subset H ⊆ A does not disturb the interpretation of α on the actions of A after hiding them w.r.t. H if the following property holds: (Only if.) Let H ⊆ A satisfying the property in the lemma, and suppose Lemma 1 ensures that, for an action formula α, its hiding set h A (α) is the maximal set of actions that can be hidden in the Lts without disturbing the interpretation of α. To make possible Lts reductions prior to (or simultaneously with) the verification of a state formula ϕ, it is desirable to hide as many actions as possible in the Lts, i.e., all actions in h A (ϕ). The following proposition ensures that this hiding preserves the interpretation of ϕ.

∀b ∈ A.(b |= A α ⇔ hide H (b) |= A α) Then: a subset H ⊆ A satisfies this property iff H ⊆ h A (α). Proof. (If.) Let H ⊆ h A (α)
H \ h A (α) = ∅. Let b ∈ H \ h A (α) such that b |= A α ⇔ hide H (b) |= A α,
Proposition 1 (Maximal Hiding). Let M = S, A, T, s 0 be an Lts, ϕ be a state formula of L µ , and H ⊆ h A (ϕ). Then:

[[ϕ]] M ρ = [[ϕ]] hide H (M ) ρ
for any propositional context ρ.

Proof. We proceed by structural induction on ϕ. We give here the most interesting case ϕ ::= α ϕ 1 , the other cases being straightforward. Since H ⊆ h A ( α ϕ 1 ) by hypothesis and h A ( α ϕ 1 ) = h A (α) ∩ h A (ϕ 1 ) by Definition 2, it follows that H ⊆ h A (α) and H ⊆ h A (ϕ 1 ). Therefore, we can apply the induction hypothesis for ϕ 1 , H and Lemma 1 for α, H, which yields:

[[ α ϕ 1 ]] hide H (M ) ρ = by def. of [[ ]] and hide H (M ) {s ∈ S | ∃s hide H (b) → s ′ .hide H (b) |= A α ∧ s ′ ∈ [[ϕ 1 ]] hide H (M ) ρ}
= by ind. hyp. and Lemma 1

{s ∈ S | ∃s b → s ′ .b |= A α ∧ s ′ ∈ [[ϕ 1 ]] M ρ} = by def. of [[ ]] [[ α ϕ 1 ]] M ρ.
In general, for a given property, there are several µ-calculus formulas ϕ specifying it, with different hiding sets h A (ϕ). To take advantage of Proposition 1, one must choose a formula ϕ with a hiding set as large as possible.

Intuitively, in such well-specified formula ϕ, all action subformulas are relevant for the interpretation of ϕ on an Lts. For example, the following formula is not well-specified:

ϕ = µX.( a 1 true ∨ (([a 2 ] false ∨ a 2 true) ∧ a 3 X))
because its subformula [a 2 ] false∨ a 2 true is a tautology and could be deleted from ϕ without changing its meaning. The presence of this subformula yields the hiding set h A (ϕ) = A \ {a 1 , a 2 , a 3 }, whereas deleting it yields a larger hiding set h A (ϕ) = A \ {a 1 , a 3 }. We do not attempt here to check well-specifiedness automatically, which would require a satisfiability checking procedure on subformulas, and will assume below that state formulas are well-specified, i.e., they contain no redundant information.

For instance, consider the L reg µ formula below, expressing the inevitable reachability5 of a recv action after every send action:

ϕ = [true * .send ] µX.(¬deadlock ∧ [¬recv ] X)

When checking ϕ on an Lts, one can hide all actions in h

A (ϕ) = h A (send ) ∩ h A (¬recv ) = (A \ [[send ]] A ) ∩ [[¬recv ]] A = (A \ {send }) ∩ (A \ {recv }) = A \ {send , recv }, i.
e., all actions other than send and recv, without changing the interpretation of the formula.

Mu-Calculus Fragment Adequate with ≈ ds br

When minimizing an Lts modulo a weak bisimilarity relation, i.e., a relation which abstracts away invisible actions, such as ≈ ds br [START_REF] Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF], the degree of reduction achieved is often directly proportional to the percentage of τtransitions contained in the original Lts. Therefore, Proposition 1 provides, for a given L µ formula, the highest potential for reduction, by enabling as many actions as possible to be hidden in the Lts. However, this proposition does not give any indication about which L µ formulas are preserved by reduction modulo ≈ ds br . In this section, we define and study a fragment of L µ , called L dsbr µ , which is adequate w.r.t. ≈ ds br . Such a fragment can, by definition of standard branching bisimilarity and divergence-sensitive branching bisimilarity, not allow one to express anything about the immediate possibility to do a transition. In branching bisimilarities, no distinction is made between the ability to do a transition directly, and the ability to reach a state where this can be done via confluent τ -transitions, i.e., τ -transitions with bisimilar source and target states. In [START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF], it was shown that ≈ ds br satisfies the stuttering property, which means that if the source and target state of a sequence of τ -transitions are divergence-sensitive branching bisimilar, then all intermediate states are as well. The main contribution of [START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF] is a study of the divergence condition in the standard definition of ≈ ds br (Def. 1), leading to the observation that it can be reformulated in a number of ways. We will use these results in the sequel.

We first prove the adequacy result, which means, on the one hand, the compatibility of L dsbr

Mu-calculus fragment L dsbr µ

The L µ fragment we consider here, called L dsbr µ , is defined in Figure 3. Compared to standard L µ , this fragment differs as follows.

It replaces the strong modalities of L µ by three new weak operators (ϕ 1 ?.α 1 ) * ϕ 2 , (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 , and ϕ 1 ?.α 1 @ expressed in Pdl-∆, where the action formulas α 1 must capture the invisible action, and action formulas α 2 denote visible actions only. The ultra-weak possibility modality (ϕ 1 ?.α 1 ) * ϕ 2 characterizes the states having an outgoing sequence of (0 or more) α 1 -transitions whose intermediate states satisfy ϕ 1 and whose terminal state satisfies ϕ 2 . The weak possibility modality (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 characterizes the states having an outgoing sequence of (0 or more) τ -transitions whose intermediate states satisfy ϕ 1 , leading to a state satisfying ϕ 1 and having an α 2 -transition to a state satisfying ϕ 2 . The weak infinite looping operator ϕ 1 ?.α 1 @ characterizes the states having an infinite outgoing sequence of α 1 -transitions whose intermediate states satisfy ϕ 1 . When the ϕ 1 subformula occurring in a weak operator is true, it can be omitted, because in this case the operator becomes α * 1 ϕ 2 , τ * .α 2 ϕ 2 , or α 1 @. The intuition behind the restriction concerning the use of action formulas α 2 is that reachability of visible transitions will remain in the Lts after maximal hiding and ≈ ds br minimization, whereas reachability of invisible transitions may be removed. In the sequel, we will often use the identity α * 1 .τ * = α * 1 , which holds for α 1 formulas capturing the invisible action (this is an instance of Lemma 4(b) in Appendix A). The deadlock formula defined in Section 2 belongs to L dsbr µ , since it can be rewritten as follows by eliminating the '.' operator:

ϕ ::= (ϕ 1 ?.α 1 ) * ϕ 2 | (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 | ϕ 1 ?.α 1 @ | false | ¬ϕ 1 | ϕ 1 ∨ ϕ 2 | X | µX.ϕ 1 where τ ∈ [[α 1 ]] A and τ ∈ [[α 2 ]] A [[ (ϕ 1 ?.α 1 ) * ϕ 2 ]] M ρ = {s ∈ S | ∃m ≥ 0.s = s 0 ∧ (∀0 ≤ i < m. s i b i+1 → s i+1 ∈ T ∧ b i+1 ∈ [[α 1 ]] A ∧ s i ∈ [[ϕ 1 ]] M ρ) ∧ s m ∈ [[ϕ 2 ]] M ρ} [[ (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 ]] M ρ = {s ∈ S | s ∈ [[ϕ 1 ]] M ρ ∧ ∃m ≥ 0.s = s 0 ∧ (∀0 ≤ i < m.s i τ → s i+1 ∈ T ∧ s i+1 ∈ [[ϕ 1 ]] M ρ) ∧ s m b → s m+1 ∈ T ∧ b ∈ [[α 2 ]] A ∧ s m+1 ∈ [[ϕ 2 ]] M ρ} [[ ϕ 1 ?.α 1 @]] M ρ = {s ∈ S | s = s 0 ∧ ∀i ≥ 0.(s i b i+1 → s i+1 ∈ T ∧ b i+1 ∈ [[α 1 ]] A ∧ s i ∈ [[ϕ 1 ]] M ρ)}
deadlock = [true * .¬τ ] false ∧ [τ ] ⊣ = [true * ] [τ * .¬τ ] false ∧ [τ ] ⊣
Similarly, the response formula given in Section 3 can be reformulated in L dsbr µ as follows:

[true * .send ] µX.(¬deadlock ∧ [¬recv ] X) = [true * ] [τ * .send ] ([(¬recv ) * ] ¬deadlock ∧ [¬recv ] ⊣)
The subformula stating the inevitable reachability of a recv action, initially expressed using a minimal fixed point operator, was replaced by the conjunction of an ultra-weak necessity modality forbidding the occurrence of deadlocks before a recv action has been reached, and a weak saturation operator forbidding the presence of cycles not passing through a recv action.

In [START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF]Corollary 4.4], it was shown that ≈ ds br is an equivalence with the so-called stuttering property: Property 1 (Stuttering). Let M = S, A, T, s 0 be an Lts and let

s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 . If s 1 τ → s 1 1 τ → • • • τ → s m 1 τ → s ′ 1 (m ≥ 0) and s ′ 1 ≈ ds br s 2 , then ∀1 ≤ i ≤ m.s i 1 ≈ ds br s 2 .
Using the stuttering property, we can prove the following lemma.

Lemma 2. Let M = S, A, T, s 0 be an Lts and let A ′ ⊆ A with τ ∈ A ′ and s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 . Then for all m ≥ 0 with s 1 = s 0 1 and

∀0 ≤ i < m.s i 1 b i → s i+1 1 ∈ T ∧ b i ∈ A ′ , there exists k ≥ 0 such that s 2 = s 0 2 and ∀0 ≤ j < k.(s j 2 b ′ j → s j+1 2 ∈ T ∧ b ′ j ∈ A ′ ∧ ∃0 ≤ i < m.s i 1 ≈ ds br s j 2 ), and s m 1 ≈ ds br s k 2 .
Proof. We proceed by induction on m.

1. Base case: m = 0, hence s 1 = s 0 1 = s m 1 . Clearly, we can choose k = 0 and s 2 = s 0 2 = s k 2 . 2. Inductive case: s 0 1 b 1 → s 1 1 • • • s m-1 1 bm → s m 1 b m+1 → s m+1 1
. By the induction hypothesis, there exists k ≥ 0 such that s 2 = s 0 2 and ∀0 ≤ j < k.(s

j 2 b ′ j → s j+1 2 ∈ T ∧ b ′ j ∈ A ′ ∧ ∃0 ≤ i < m.s i 1 ≈ ds br s j 2 )
, and s m 1 ≈ ds br s k 2 . We show that it also holds for m + 1. We distinguish two cases for s m

1 b m+1 → s m+1 1 : (a) b m+1 = τ . Since s m 1 ≈ ds br s k 2 , by Definition 1, also s m+1 1 ≈ ds br s k 2 . (b) b m+1 = τ . Since s m 1 ≈ ds br s k 2 , by Definition 1, s k 2 = ⇒ ŝ2 b m+1 → s ′ 2 , with s m 1 ≈ ds br ŝ2 , and s m+1 1 ≈ ds br s ′ 2 . Say that s k 2 = ⇒ ŝ2 consists of c τ -steps s k 2 τ → s k+1 2 • • • s k+c-1 2 τ → s k+c 2 with s k+c 2 = ŝ2 . By Definition 1, for all k ≤ i ≤ k + c, we have s m 1 ≈ ds br s i 2 .
Hence, there exists a matching sequence from

s 2 of length k + c + 1 with s k+c+1 2 = s ′ 2 . Note that τ ∈ A ′ .
A propositional context ρ : X → 2 S is said to be ≈ ds br -closed if for all states s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 and for any propositional variable X ∈ X , s 1 ∈ ρ(X) ⇔ s 2 ∈ ρ(X). Now we can state the main result about L dsbr µ , namely that this fragment is compatible with the ≈ ds br relation.

Proposition 2 (Compatibility with ≈ ds br ). Let M = S, A, T, s 0 be an Lts and let s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 . Then:

s 1 ∈ [[ϕ]] M ρ ⇔ s 2 ∈ [[ϕ]] M ρ
for any state formula ϕ of L dsbr µ and any ≈ ds br -closed propositional context ρ. Proof. We proceed by structural induction on ϕ. We give here the most interesting cases, the other cases being handled in Appendix A.

Case ϕ ::= (ϕ 1 ?.α 1 ) * ϕ 2 . Let s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 and assume that s 1 ∈ [[ (ϕ 1 ?.α 1 ) * ϕ 2 ]] M ρ, i.e., s 1 ∈ {s ∈ S | ∃m ≥ 0.s = s 0 ∧ (∀0 ≤ i < m.s i b i+1 → s i+1 ∈ T ∧ b i+1 ∈ [[α 1 ]] A ∧ s i ∈ [[ϕ 1 ]] M ρ) ∧ s m ∈ [[ϕ 2 ]] M ρ}. This means that: ∃m ≥ 0.s 1 = s ′ 0 ∧ (∀0 ≤ i < m.s ′ i b i+1 → s ′ i+1 ∈ T (1) ∧ b i+1 ∈ [[α 1 ]] A ∧ s ′ i ∈ [[ϕ 1 ]] M ρ) ∧ s ′ m ∈ [[ϕ 2 ]] M ρ We have to prove that s 2 ∈ [[ (ϕ 1 ?.α 1 ) * ϕ 2 ]] M ρ, which means that: ∃k ≥ 0.s 2 = s ′′ 0 ∧ (∀0 ≤ j < k.s ′′ j b ′ j+1 → s ′′ j+1 ∈ T (2) ∧ b ′ j+1 ∈ [[α 1 ]] A ∧ s ′′ j ∈ [[ϕ 1 ]] M ρ) ∧ s ′′ k ∈ [[ϕ 2 ]] M ρ First, since s 1 ≈ ds br s 2 , τ ∈ [[α 1 ]] A ,

and (1), by Lemma 2 with

A ′ = [[α 1 ]] A , there exists k ≥ 0 with s 2 = s ′′ 0 such that ∀0 ≤ j < k.(s ′′ j b ′ j+1 → s ′′ j+1 ∈ T ∧ b ′ j+1 ∈ [[α 1 ]] A ∧ ∃0 ≤ i < m.s ′ i ≈ ds br s ′′ j ) and s ′ m ≈ ds br s ′′ k .
Furthermore, for all 0 ≤ j < k, since there exists 0 ≤ i < m.s ′ i ≈ ds br s ′′ j and

s ′ i ∈ [[ϕ 1 ]] M ρ, by the induction hypothesis, it follows that s ′′ j ∈ [[ϕ 1 ]] M ρ. Finally, since s ′ m ≈ ds br s ′′ k and s ′ m ∈ [[ϕ 2 ]] M ρ, by the induction hypothesis, s ′′ k ∈ [[ϕ 2 ]] M ρ. Hence, (2) holds.
The converse implication (by considering

s 2 ∈ [[ (ϕ 1 ?.α 1 ) * ϕ 2 ]] M ρ) holds by a symmetric argument. Case ϕ ::= (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 . Let s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 and assume that s 1 ∈ [[ (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 ]] M ρ, i.e., s 1 ∈ {s ∈ S | s ∈ [[ϕ 1 ]] M ρ ∧ ∃m ≥ 0.s = s 0 ∧ (∀0 ≤ i < m.s i τ → s i+1 ∈ T ∧ s i+1 ∈ [[ϕ 1 ]] M ρ) ∧ s m b → s m+1 ∈ T ∧ b ∈ [[α 2 ]] A ∧ s m+1 ∈ [[ϕ 2 ]] M ρ}.
This means that:

s 1 ∈ [[ϕ 1 ]] M ρ ∧ ∃m ≥ 0.s 1 = s ′ 0 ∧ (∀0 ≤ i < m.s ′ i τ → s ′ i+1 ∈ T (3) ∧ s ′ i+1 ∈ [[ϕ 1 ]] M ρ) ∧ s ′ m b → s ′ m+1 ∧ b ∈ [[α 2 ]] A ∧ s ′ m+1 ∈ [[ϕ 2 ]] M ρ
We have to prove that s 2 ∈ [[ (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 ]] M ρ, which means that: Case ϕ ::= ϕ 1 ?.α 1 @. Let s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 and assume that

s 2 ∈ [[ϕ 1 ]] M ρ ∧ ∃k ≥ 0.s 2 = s ′′ 0 ∧ (∀0 ≤ i < k.s ′′ i τ → s ′′ i+1 ∈ T (4) ∧ s ′′ i+1 ∈ [[ϕ 1 ]] M ρ) ∧ s ′′ m c → s ′′ m+1 ∧ c ∈ [[α 2 ]] A ∧ s ′′ m+1 ∈ [[ϕ 2 ]] M ρ First,
s 1 ∈ [[ ϕ 1 ?.α 1 @]] M ρ, i.e., s 1 ∈ {s ∈ S | s = s 0 ∧ ∀i ≥ 0.(s i b i → s i+1 ∧ b i ∈ [[α 1 ]] A ∧ s i ∈ [[ϕ 1 ]] M ρ)}.
This means that:

s 1 = s ′ 0 ∧ ∀i ≥ 0.(s ′ i b i → s ′ i+1 ∧ b i ∈ [[α 1 ]] A ∧ s ′ i ∈ [[ϕ 1 ]] M ρ) (5)
We have to prove that s 2 ∈ [[ ϕ 1 ?.α 1 @]] M ρ, which means that:

s 2 = s ′′ 0 ∧ ∀j ≥ 0.(s ′′ j b ′ j → s ′′ j+1 ∧ b ′ j ∈ [[α 1 ]] A ∧ s ′′ j ∈ [[ϕ 1 ]] M ρ) (6)
Since

s 1 ≈ ds br s 2 , τ ∈ [[α 1 ]
] A , and (5), by Lemma 2 with A ′ = [[α 1 ]] A , for any finite prefix of length m ≥ 0 of the infinite path π from s 1 , there exists a finite path of length k ≥ 0 from s 2 such that

s 2 = s ′′ 0 ∧ ∀0 ≤ j < k.(s ′′ j b ′ j → s ′′ j+1 ∧ b ′ j ∈ [[α 1 ]] A ∧ ∃0 ≤ i < m.s ′ i ≈
]] A \ {τ }.
Then, there exists an ŝ reachable from s 1 such that from ŝ, an infinite τ -path exists. By the earlier reasoning, there exists an ŝ′ reachable from s 2 such that ŝ ≈ ds br ŝ′ and for all states s ′′ j on the path from s 2 to ŝ′ , we have

s ′′ j ∈ [[ϕ 1 ]] M ρ.
Finally, since ŝ ≈ ds br ŝ′ , by the second clause of Definition 1, there also exists an infinite τ -path π ′ from ŝ′ . Finally, by Definition 1 and repeated application of Definition 1, it follows that for all states s ′′ j in π ′ , ŝ ≈ ds br s ′′ j , hence by the induction hypothesis,

s ′′ j ∈ [[ϕ 1 ]] M ρ.
Therefore, (6) holds for s 2 . The converse implication (by considering s 2 ∈ [[ ϕ 1 ?.α 1 @]] M ρ) holds by a symmetric argument.

From Proposition 2, it can be easily deduced that a closed L dsbr µ formula ϕ has the same truth value on two Ltss M 1 = S 1 , A, T 1 , s 01 and M 2 = S 2 , A, T 2 , s 02 that are equivalent modulo ≈ ds br . Indeed, the two Ltss can be merged into a single one by joining the sets of states and transitions, and Proposition 2 can be applied to the initial states s 01 and s 02 . In practice, M 2 can be obtained from M 1 by applying maximal hiding followed by a ≈ ds brpreserving reduction, in particular modulo strong equivalence or divergencepreserving τ -confluence.

Compatibility of ≈ ds br with L dsbr µ

To obtain a complete logical characterization of ≈ ds br , we must show that this relation is compatible with L dsbr µ , meaning that two Ltss satisfying the same set of L dsbr µ formulas are equivalent modulo ≈ ds br . This is stated by the following proposition, whose proof relies upon the fact that the characteristic formula [START_REF] Graf | A Modal Characterization of Observational Congruence on Finite Terms of CCS[END_REF] of ≈ ds br can be expressed in L dsbr µ . Proposition 3 (Compatibility of ≈ ds br with L dsbr µ ). Let M 1 = S 1 , A, T 1 , s 01 and M 2 = S 2 , A, T 2 , s 02 be two Ltss. Then:

(∀ϕ ∈ L dsbr µ .(M 1 |= ϕ ⇔ M 2 |= ϕ)) ⇒ M 1 ≈ ds br M 2 .
Proof Sketch. Let M 1 , M 2 be two Ltss satisfying the statement above, and let ϕ ≈ ds br (M 1 ) be the characteristic formula of M 1 w.r.t. ≈ ds br , meaning that any Lts equivalent to M 1 modulo ≈ ds br must satisfy this formula. If ϕ ≈ ds br (M 1 ) is expressible in L dsbr µ , and since M 1 |= ϕ ≈ ds br (M 1 ) by definition, then also M 2 |= ϕ ≈ ds br (M 1 ), which implies M 1 ≈ ds br M 2 . Thus, to complete the proof, it remains to show that ϕ ≈ ds br (M 1 ) is expressible in L dsbr µ . To carry out this task, we rely upon existing work on constructing characteristic formulas, namely for weak bisimilarity [START_REF] Müller-Olm | Derivation of Characteristic Formulae[END_REF] and for strong and ready bisimilarity (among other relations) [START_REF] Steffen | Characteristic Formulae for Processes with Divergence[END_REF][START_REF] Aceto | Characteristic Formulae for Fixed-Point Semantics: A General Framework[END_REF]. The approach is as follows: if a recursively defined logical formula expresses the definition of a behavioral relation, then the largest interpretation of that formula is the characteristic formula for the derived behavioral relation. For a given Lts M = S, A, T, s 0 , we construct a system of equations expressed using L dsbr µ , that captures the largest divergence-sensitive branching bisimulation that can be constructed over S × S. More precisely, we will define a declaration function D : X → L dsbr µ , providing us with a system of equations over X that decides the meaning of each variable.

It is assumed that X is indexed over S, i.e. {X s | s ∈ S}. Now, the largest fixed point of D over the set of all environments ρ, which we refer to as ρ D ν , gives the characteristic formula for a binary relation R over S if, for all s, t ∈ S: s ∈ ρ D ν (X t ) ⇐⇒ (s, t) ∈ R First of all, we need to define an appropriate propositional context. We define context ρ S as follows:

ρ S (X t ) = {s ∈ S | (s, t) ∈ R}
To construct D, we need to translate the two clauses of Definition 1 and their symmetric versions to construct a characteristic formula. These are: → . . . and t k R s for all k ≥ 0, then there is an infinite sequence of states s 0 , s 1 , s 2 , . . . such that s 0 = s, s 0

1. if s b → s ′ then (1) either b = τ with s ′ R t, or (2) t = ⇒ t b → t ′ with s R t and s ′ R t ′ . 2. if t b → t ′ then (1) either b = τ with s R t ′ , or (2) s = ⇒ ŝ b → s ′ with ŝ R t and s ′ R t ′ . 3. if
τ → s 1 τ → s 2 τ → . . . and t k R s ℓ for all k, ℓ ≥ 0.
Clause 2 can be translated straightforwardly, along the lines of [START_REF] Müller-Olm | Derivation of Characteristic Formulae[END_REF][START_REF] Aceto | Characteristic Formulae for Fixed-Point Semantics: A General Framework[END_REF], as follows:

(ρ S , s) |= M t ′ .t τ →t ′ (X t ?.τ ) * X t ′ ∧ b∈A\{τ },t ′ .t b →t ′ (X t ?.τ ) * .X t ?.b X t ′
Here, (ρ S , s) |= M ϕ expresses that s satisfies ϕ with context ρ S . The first part of the above formula expresses that for all τ -transitions enabled from t leading to a state t ′ , there exists a path from s of (0 or more) τtransitions along intermediate states satisfying X t , i.e. that are divergencesensitive branching bisimilar to t, such that the final state satisfies X t ′ , i.e. is divergence-sensitive branching bisimilar to t ′ . This covers clause 2.1 and 2.2 in the case that b = τ . The second part concerns all actions in A \ {τ }. For all visible b-transitions from t to a state t ′ , there exists a path from s of (0 or more) τ -transitions along states satisfying X t , leading to a state from where a b-transition is enabled to a state satisfying X t ′ . The necessity for these two parts stems from the fact that in the weak possibility modality of L dsbr µ , only visible actions may be used.

For clause 1, note that in L dsbr µ , we cannot reason about visible transitions being enabled in a particular state, for example s b → s ′ . However, we can reason about all visible transitions that are reachable from s via (0 or more) τtransitions. Doing so does not weaken the clause. Therefore, we can translate clause 1 to the following:

(ρ S , s) |= M [(X t ?.τ ) * ] (X t ∨ t.t = ⇒ t ∧ (ρ, t)|= M Xt ( t ′ . t τ →t ′ X t ′ )) ∧ b∈A\{τ } [(X t ?.τ ) * .X t ?.b] t.t = ⇒ t ∧ (ρ, t)|= M Xt ( t ′ . t b →t ′ X t ′ )
Similar to the translation of clause 2, the first part addresses the τtransitions. For any τ -transition, reachable from s via (0 or more) τtransitions, via states satisfying X t , we either have that the end state also satisfies X t , i.e. it is divergence-sensitive branching bisimilar to t (clause 1.1), or it satisfies at least one X t ′ , where t ′ is reachable from t via a state t. State t should be reachable from t via (0 or more) τ -transitions, and satisfy X t , i.e. it should be divergence-sensitive branching bisimilar to t, and hence to s, and t must have an outgoing τ -transition to t ′ . This translates clause 1.2, in the case that b = τ . The second part of the translation covers clause 1.2 for the visible transitions.

Clause 4 can be translated to the following:

(ρ S , s) |= M t ′ .t = ⇒ t ′ [τ ] ⊣ ∨ X t ′ ?.τ @
It expresses that every state t ′ reachable from t via a τ -path is either saturated on τ , i.e. the path cannot be extended to an infinite τ -path, hence the clause is not applicable for this state, or there is an infinite τ -path from s such that all intermediate states satisfy X t ′ . Since for all infinite τ -paths from t, the formula expresses that for all intermediate states t ′ , there must exist an infinite τ -path from s in which the intermediate states are divergencesensitive branching bisimilar to t ′ , this covers that all the states in one path must be divergence-sensitive branching bisimilar to all the states in the other path.

In order to translate clause 3, we must first reformulate it. As explained in [START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF], the requirement that t can diverge, and all states on that infinite τ -path satisfy certain properties, can be replaced by the requirement that a state t ′ satisfying those properties can be reached from t via a single τ -transition. If a binary relation satisfies that, then the divergence of t can be inductively constructed [START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF]. Along these lines, we reformulate clause 3 as follows:

3 ′ . if there is an infinite sequence of states s 0 , s 1 , s 2 , . . . such that s 0 = s, s 0 τ → s 1 τ → s 2 τ
→ . . . and s k R t for all k ≥ 0, then there exists a t ′ such that t τ → t ′ and s k R t ′ for all k ≥ 0. Clause 3 ′ can be translated to the following:

(ρ S , s) |= M [(X t ?.τ ) * ] ([τ ] ⊣ ∨ t ′ .t τ →t ′ X t ′ )
The operator E[ϕ 1 α Uϕ 2 ] (resp. A[ϕ 1 α Uϕ 2 ]) denotes the states from which some (resp. all) outgoing sequences lead, after 0 or more α-transitions (or τ -transitions) whose source states satisfy ϕ 1 , to a state satisfying ϕ 2 . The operator

E[ϕ 1 α 1 U α 2 ϕ 2 ] (resp. A[ϕ 1 α 1 U α 2 ϕ 2 ]
) denotes the states from which some (resp. all) outgoing sequences lead, after 0 or more α 1 -transitions (or τtransitions) whose source states satisfy ϕ 1 , to an α 2 -transition whose source state satisfies ϕ 1 and whose target state satisfies ϕ . The action subformulas α, α 1 , and α 2 denote visible actions only. The lower part of Figure 4 shows the encodings in L µ of the Actl\X temporal operators, as proposed in [START_REF] Fantechi | From ACTL to Mu-Calculus[END_REF]. Actl\X and also its richer version Actl * \X, which captures linear-time properties, were shown to be adequate w.r.t. ≈ ds br [START_REF] Nicola | Action versus State Based Logics for Transition Systems[END_REF]. Moreover, Actl\X was extended in [START_REF] Fantechi | From ACTL to Mu-Calculus[END_REF] with fixed point operators, yielding a fragment of L µ called µ-Actl\X, which subsumes Actl * \X. The temporal operators of Actl\X can be translated in L dsbr µ , as stated by the following proposition (proven in Appendix A).

State formulas: ϕ

::= E[ϕ 1 α Uϕ 2 ] | E[ϕ 1 α 1 U α 2 ϕ 2 ] | A[ϕ 1 α Uϕ 2 ] | A[ϕ 1 α 1 U α 2 ϕ 2 ] [[E[ϕ 1 α Uϕ 2 ]]] M = {s ∈ S | ∃s 1 (= s) b 1 → • • • b i-1 → s i • • • .∃k ≥ 1. ∀1 ≤ j < k.(b j ∈ [[α ∨ τ ]] A ∧ s j ∈ [[ϕ 1 ]] M ) ∧ s k ∈ [[ϕ 2 ]] M } [[E[ϕ 1 α 1 U α 2 ϕ 2 ]]] M = {s ∈ S | ∃s 1 (= s) b 1 → • • • b i-1 → s i • • • .∃k ≥ 1. ∀1 ≤ j < k.(b j ∈ [[α 1 ∨ τ ]] A ∧ s j ∈ [[ϕ 1 ]] M ) ∧ b k ∈ [[α 2 ]] A ∧ s k+1 ∈ [[ϕ 2 ]] M } [[A[ϕ 1 α Uϕ 2 ]]] M = {s ∈ S | ∀s 1 (= s) b 1 → • • • b i-1 → s i • • • .∃k ≥ 1. ∀1 ≤ j < k.(b j ∈ [[α ∨ τ ]] A ∧ s j ∈ [[ϕ 1 ]] M ) ∧ s k ∈ [[ϕ 2 ]] M } [[A[ϕ 1 α 1 U α 2 ϕ 2 ]]] M = {s ∈ S | ∀s 1 (= s) b 1 → • • • b i-1 → s i • • • .∃k ≥ 1. ∀1 ≤ j < k.(b j ∈ [[α 1 ∨ τ ]] A ∧ s j ∈ [[ϕ 1 ]] M ) ∧ b k ∈ [[α 2 ]] A ∧ s k+1 ∈ [[ϕ 2 ]] M } Encoding in L µ : E[ϕ 1 α Uϕ 2 ] = µX.(ϕ 2 ∨ (ϕ 1 ∧ α ∨ τ X)) E[ϕ 1 α 1 U α 2 ϕ 2 ] = µX.(ϕ 1 ∧ ( α 2 ϕ 2 ∨ α 1 ∨ τ X)) A[ϕ 1 α Uϕ 2 ] = µX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)) A[ϕ 1 α 1 U α 2 ϕ 2 ] = µX.(ϕ 1 ∧ ¬deadlock ∧ [¬(α 1 ∨ α 2 ∨ τ )] false ∧ [α 2 ∧ ¬α 1 ] ϕ 2 ∧ [α 1 ∧ α 2 ] (ϕ 2 ∨ X) ∧ [¬α 2 ] X)
Proposition 4 (Translation from Actl\X to L dsbr µ ). The following identities hold in L µ :

µX.(ϕ 2 ∨ (ϕ 1 ∧ α ∨ τ X)) = (ϕ 1 ?.α ∨ τ ) * ϕ 2 µX.(ϕ 1 ∧ ( α 2 ϕ 2 ∨ α 1 ∨ τ X)) = (ϕ 1 ?.α 1 ∨ τ ) * (ϕ 1 ?.τ ) * .α 2 ϕ 2 µX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)) = [(¬ϕ 2 ?.α ∨ τ ) * ] (ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [(¬ϕ 2 ?.τ ) * .¬ϕ 2 ?.¬(α ∨ τ )] false)) ∧ [¬ϕ 2 ?.α ∨ τ ] ⊣ µX.(ϕ 1 ∧ ¬deadlock ∧ [¬(α 1 ∨ α 2 ∨ τ )] false ∧ [α 2 ∧ ¬α 1 ] ϕ 2 ∧ [α 1 ∧ α 2 ] (ϕ 2 ∨ X) ∧ [¬α 2 ] X) = νX. [(¬α 2 ) * ] (ϕ 1 ∧ ¬deadlock ∧ [τ * .¬(α 1 ∨ α 2 ∨ τ )] false ∧ [τ * .α 2 ∧ ¬α 1 ] ϕ 2 ∧ [τ * .α 1 ∧ α 2 ] (ϕ 2 ∨ X) ∧ X) ∧ νX.([¬α 2 ] ⊣ ∧ [(¬α 2 ) * ] [τ * .α 1 ∧ α 2 ] (ϕ 2 ∨ X)) ∧ µX. [(¬α 2 ) * ] [τ * .α 1 ∧ α 2 ] (ϕ 2 ∨ X)
The intuition underlying these identities is the following: the EU operators are translated into Pdl diamond modalities specifying the existence of the desired transition sequences; the A[ϕ 1 α Uϕ 2 ] operator is translated as the conjunction of a Pdl necessity modality expressing that all sequences having a prefix made of α-transitions must also have the right suffix leading to ϕ 2 -states, and a Pdl-∆ saturation operator forbidding the infinite sequences of α-transitions not containing ϕ 2 -states; and the

A[ϕ 1 α 1 U α 2 ϕ 2 ]
operator is translated as the conjunction of three L dsbr µ subformulas, the first one expressing that all sequences having a prefix made of α 1 -transitions (and not of α 2 -transitions) must also have the right suffix leading to ϕ 2 -states, and the two other ones forbidding the infinite sequences not containing α 2transitions or ϕ 2 -states. By applying the translations of Actl\X temporal operators given in Proposition 4, and given that both L dsbr µ and µ-Actl\X have the same boolean and fixed point operators, it follows that µ-Actl\X is subsumed by L dsbr µ . The converse is also true, because the weak and ultra weak modalities of L dsbr µ can be encoded in µ-Actl\X as follows (α 1 denotes visible or invisible actions, whereas α 2 denotes visible actions only):

(ϕ 1 ?.α 1 ) * ϕ 2 = E[ϕ 1 α 1 ∧¬τ Uϕ 2 ] (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 = E[ϕ 1 false U α 2 ϕ 2 ] ϕ 1 ?.α 1 @ = νX.E[ϕ 1 false U α 1 X]
The first two identities can be easily shown by replacing the EU operators with their fixed point counterparts given in Figure 4, and the third one makes use of Lemma 4(c) given in Appendix A. Hence, L dsbr µ and µ-Actl\X are equally expressive. Therefore, the adequacy result of L dsbr µ w.r.t. ≈ ds br shown in Sections 4.1 and 4.2 also implies the adequacy of µ-Actl\X w.r.t. ≈ ds br . This new adequacy result completes the already known adequacy of µ-Actl w.r.t. strong bisimulation [START_REF] Fantechi | Modelling transition systems within an action based logic[END_REF]. Another temporal logic adequate with ≈ ds br was proposed in [START_REF] Glabbeek | Computation Tree Logic with Deadlock Detection[END_REF] by extending Ctl * \X (and hence, Ctl\X) with a path operator expressing the existence of infinite sequences. This logic, which is interpreted on Ltss via the translation from Kripke structures to Ltss defined in [START_REF] Nicola | Action versus State Based Logics for Transition Systems[END_REF], can be translated into µ-Actl\X following the lines of [START_REF] Dam | Ctl * and Ectl * as Fragments of the Modal µ-calculus[END_REF], and therefore is subsumed by L dsbr µ . In practice, for conciseness and efficiency of model checking, we will use the L µ encodings of the Actl\X operators given in Figure 4 instead of the more complex L dsbr µ formulas shown in Proposition 4. The response formula given in Section 3 can also be expressed in Actl\X:

AG true,send A[true true U recv true] where AG α 1 ,α 2 ϕ = ¬EF α 1 ,α 2 ¬ϕ = ¬E[true α 1 U α 2 ¬ϕ] is the Actl counterpart of the AG operator of Ctl.
Subsuming a relevant selective µ-calculus fragment. The selective µcalculus [START_REF] Barbuti | Selective Mu-Calculus and Formula-Based Equivalence of Transition Systems[END_REF] introduces modalities indexed by sets of actions (represented here as action formulas) specifying the reachability of certain actions after sequences of (0 or more) actions not belonging to the indexing set. The syntax and semantics of selective L µ modalities, as well as their encoding in standard L µ , are shown in Figure 5. The selective possibility modality α 1 α 2 ϕ, where α 1 , α 2 denote visible actions only, specifies the states having ϕ :: Selective L µ is adequate w.r.t. the τ * .a bisimilarity [START_REF] Barbuti | Selective Mu-Calculus and Formula-Based Equivalence of Transition Systems[END_REF]: for each selective formula ϕ, one can hide all Lts actions other than those occurring in the modalities of ϕ and their index sets, and then minimize the Lts modulo τ * .a without changing the interpretation of ϕ. Selective L µ was shown to be equivalent to standard L µ , because the strong possibility modality of L µ can be expressed in terms of the selective one: α ϕ = α true ϕ. However, this way of translating would yield no possibility of hiding actions (and hence, reducing the Lts), because the index sets would contain all actions of the Lts. For instance, the response formula given in Section 3 can be reformulated in selective L µ as follows:

= false | ¬ϕ 1 | ϕ 1 ∨ ϕ 2 | α 1 α 2 ϕ 1 | X | µX.ϕ 1 [[ α 1 α 2 ϕ 1 ]] M ρ = {s ∈ S | ∃s 1 (= s) b 1 → • • • b k-1 → s k a → s k+1 . ∀1 ≤ i < k.b i ∈ [[α 1 ∨ α 2 ]] A ∧ a ∈ [[α 1 ]] A ∧ s k+1 ∈ [[ϕ 1 ]] M ρ)} Encoding in L µ : α 1 α 2 ϕ 1 = µX.( α 1 ϕ 1 ∨ ¬(α 1 ∨ α 2 ) X)
[send ] false µX.( true true true ∧ [¬recv ] true X)

The minimal fixed point subformula expressing the inevitable reachability of a recv action cannot be mapped to selective L µ modalities, which forces the use of strong modalities (represented by selective modalities indexed by true). Therefore, the set of actions that can be hidden according to [START_REF] Barbuti | Selective Mu-Calculus and Formula-Based Equivalence of Transition Systems[END_REF] without disturbing the interpretation of this formula is A\({send , recv }∪A) = ∅, i.e., no hiding of actions prior to verification would be possible in that setting.

When α 1 and α 2 do not cover all visible actions of the Lts, i.e., α 1 ∨ α 2 = true, the selective possibility modality can be encoded in L dsbr µ as follows:

α 1 α 2 ϕ 1 = (¬(α 1 ∨ α 2 )) * τ * .α 1 ϕ 1 .
Therefore, L dsbr µ subsumes the selective L µ fragment whose modalities satisfy the condition above, which precisely contains the selective L µ formulas yielding a potential reduction by allowing one to hide some actions in the Lts before verification.

Subsuming weak µ-calculus. The last logic we consider here is the weak (or observational) µ-calculus [START_REF] Stirling | Modal and Temporal Properties of Processes[END_REF], a fragment of L µ adequate w.r.t. weak bisimilarity. It introduces weak modalities specifying the reachability of certain actions preceded and followed by 0 or more τ -transitions. The syntax, semantics, and encoding of the weak L µ modalities in standard L µ are shown in Figure 6. The weak possibility modality α ϕ, where α denotes visible actions only, specifies the states having an outgoing sequence of 0 or more τ -transitions, followed by an α-transition, followed by another sequence of 0 or more τ -transitions, and leading to a state satisfying ϕ. The empty weak possibility modality ϕ denotes the states having an outgoing sequence of 0 or more τ -transitions leading to a state satisfying ϕ. The weak L µ modalities can be encoded in L dsbr µ as follows:

State formulas: ϕ

::= false | ¬ϕ 1 | ϕ 1 ∨ ϕ 2 | α ϕ 1 | ϕ 1 | X | µX.ϕ 1 [[ α ϕ 1 ]] M ρ = {s ∈ S | ∃s ′ , s ′′ , s ′′′ ∈ S.s ⇒ s ′ a → s ′′ ⇒ s ′′′ ∧ a ∈ [[α]] A ∧ s ′′′ ∈ [[ϕ 1 ]] M ρ)} [[ ϕ 1 ]] M ρ = {s ∈ S | ∃s ′ ∈ S.s ⇒ s ′ ∧ s ′ ∈ [[ϕ 1 ]] M ρ)} Encoding in L µ : α ϕ 1 = µX.( α µY.(ϕ 1 ∨ τ Y ) ∨ τ X) ϕ 1 = µX.(ϕ 1 ∨ τ X)
α ϕ 1 = τ * .α τ * ϕ 1 ϕ 1 = τ * ϕ 1
Weak L µ is able to express only weak safety and liveness properties; in particular, it does not capture the inevitable reachability of a given action, and is therefore less expressive than L dsbr µ .

Implementation and Experiments

We have implemented the maximal hiding and associated on-the-fly reduction machinery within the Cadp verification toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. We exper-imented on the effect of these optimizations on the Evaluator [START_REF] Mateescu | Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus[END_REF][START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF] model checker, which evaluates formulas of the alternation-free fragment of L reg µ (without mutually recursive minimal and maximal fixed point operators) on Ltss on-the-fly. The tool works by first translating the L reg µ formulas into plain L µ by eliminating the Pdl regular operators, and then reformulating the verification problem as the resolution of a Boolean equation system (Bes) [START_REF] Andersen | Model Checking and Boolean Graphs[END_REF], which is solved locally using the algorithms of the Caesar Solve library [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF] of Cadp. Evaluator makes it possible to define reusable libraries of derived operators (e.g., those of Actl) and property patterns (e.g., the pattern system of [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF]).

For the sake of efficiency, we focus on L dsbr µ formulas having a lineartime model checking complexity, namely the alternation-free fragment [START_REF] Cleaveland | A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus[END_REF] extended with the infinite looping and saturation operators of Pdl-∆ [START_REF] Streett | Propositional Dynamic Logic of Looping and Converse[END_REF], which can be evaluated in linear time using the algorithms proposed in [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF]. In the formulas below, we use the operators of Pdl and Actl\X, and the L dsbr µ formula inev (a) = [(¬a) * ] ¬deadlock ∧[¬a] ⊣ as a shorthand for expressing the inevitable execution of an action a. For each verification experiment, we applied maximal hiding as stated in Proposition 1, and then carried out Lts reductions either prior to (by minimization modulo equivalence relations), or simultaneously with (by τ -confluence reduction), the verification of the formula.

Strong bisimulation reduction. We considered first global verification, which consists in generating the Lts, applying maximal hiding, minimizing the Lts modulo a bisimilarity relation, and then verifying the properties on the minimized Lts. Ltss are represented as files in the compact Bcg (Binary Coded Graphs) format of Cadp. Hiding and minimization were carried out using the Bcg Labels and Bcg Min tools [START_REF] Coste | Ten Years of Performance Evaluation for Concurrent Systems Using CADP[END_REF], the whole process being automated using Svl [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF] scripts. We first experimented the effect of minimizing modulo strong bisimilarity, which although it handles visible and invisible actions in the same way, can still improve the model checking performance when the percentage of τ -transitions obtained after hiding is important.

We considered the alternating bit protocol, implemented in Lotos (demo 02 of Cadp), and checked the following property, which states that the protocol behaves as a one-place buffer (initially empty) regarding the emission (action put) and reception (action get) of messages:

[true * ] ([τ * .put] (A[true ¬get U τ @] ∧ [(¬get) * ] [τ * .put] false) ∧ [τ * .get] (A[true ¬put U τ @] ∧ [(¬put) * ] [τ * .get] false))
This formula specifies that, after each emission (resp. reception) of a message, a livelock -denoted by the τ @ subformulas -is eventually reachable because of the unreliable communication channels, and no other emission (resp. reception) can occur until that message was received (resp. a new message was emitted). This formula makes possible the hiding of every action other than put and get. The overall time and peak memory needed for verification are shown in Figure 7 for increasingly larger configurations of the protocol. When strong bisimulation minimization is carried out before verification, we observe gains both in speedup and memory (factors 4 and 2 for the Lts corresponding to 1000 messages, having [START_REF] Fantechi | From ACTL to Mu-Calculus[END_REF]196,201 states and 46, 639, 612 transitions), which become larger with the size of the Lts. The lower plots in Figure 7 indicate the time and peak memory consumption for the same protocol configurations when minimizing modulo divergence-sensitive branching bisimulation before performing the verification. On this example, the additional gain w.r.t. strong bisimulation is of 10% in speedup and 5% in memory; this rather low improvement is explained by the large amount of τ -transitions (around 74.5% for each configuration) obtained after maximal hiding, which yields significant reductions modulo strong bisimulation.

We also considered a token ring leader election protocol, implemented in Lotos (experiment 6 in demo 17 of Cadp), and checked the following property, stating that each station i on the ring accesses a shared resource (actions open i and close i ) in mutual exclusion with the other stations and each access is fairly reachable, i.e., from each state of a τ -cycle due to unreliable communication channels, it is possible to reach an open i action:

[true * ] ([τ * .open i ][(¬close i ) * ][τ * .open j ]false ∧ A[true true U ( true * τ * .open i true)?.τ @])
This formula belongs to L dsbr µ (after expanding the A[U] operator) and makes possible the hiding of every action other than open i,j and close i . The " ... @" subformula of A[U] expresses the existence of infinite τ -sequences whose intermediate states enable the potential reachability of an open i action. The overall time and peak memory needed for verification are shown in Figure 8 for increasingly larger configurations of the protocol. When strong bisimulation minimization is carried out before verification, we observe gains both in speedup and memory (factors 2.8 and 2.5 for the Lts corresponding to 7 stations, having 53, 848, 492 states and 214, 528, 176 transitions), which become larger with the size of the Lts.

Divergence-sensitive branching bisimulation reduction. To study the effect of ≈ ds br minimization, we considered the Dynamic Task Dispatcher (Dtd), a complex hardware block dispatching data-intensive applications on a cluster On-the-fly τ -confluence reduction. Lastly, we examined the effect of τconfluence reduction [START_REF] Groote | Confluence for Process Verification[END_REF] carried out on-the-fly during the verification of formulas. This reduction, which preserves branching bisimilarity, consists in identifying confluent τ -transitions (i.e., whose execution does not alter the observable behavior of the system), and giving them priority over their neighbors during the Lts traversal. The detection of confluent τ -transitions is done on-the-fly by reformulating the problem as a Bes resolution [START_REF] Pace | Calculating τ -Confluence Compositionally[END_REF][START_REF] Mateescu | Efficient On-the-Fly Computation of Weak Tau-Confluence[END_REF], which is performed locally using the algorithms of Caesar Solve. In order to make the reduction compatible with ≈ ds br , we enhanced the τ -confluence detection with the bookkeeping of divergence, by exploiting the τ -cycle compression algorithm proposed in [START_REF] Mateescu | On-the-fly State Space Reductions for Weak Equivalences[END_REF]. In practice, this amounts to reduce the Lts by τ -cycle compression, which collapses the strongly connected components made of τ -transitions and replaces them with τ -loops, and then reduce the Lts further by detecting τ -confluent transitions and deleting their neighbors. These two reductions, both carried out on-the-fly, are invoked in a demand-driven way by the model checking algorithms of Evaluator.

We considered the distributed version of Erathosthene's sieve, implemented using Lotos processes and Exp networks of automata (demo 36 of Cadp). We checked the following formula, expressing that each prime number p fed as input to the sieve will be eventually delivered as output and each non-prime number q will be filtered (where inev (a), expressing the inevitable execution of a, was defined at the beginning of this section):

[true * ] ([τ * .gen p ]inev (output p ) ∧ [τ * .gen q ][true * .¬output q ]false) This formula belongs to L dsbr µ (after eliminating the concatenation operators) and makes possible the hiding of every action other than gen p,q and output p,q .

The overall time and peak memory needed for verification are shown in Figure 10 for increasingly larger configurations of the sieve. We observe a substantial increase in speed in the presence of τ -confluence reduction (about one order of magnitude for a sieve with 10 units). The reduction in memory usage becomes apparent once the size of the system becomes sufficiently large, such that the memory overhead induced by the presence of the on-thefly reduction machinery is compensated by the memory required for verifying the formula.

Overall experiment conclusion. From the experiments shown above, and also from other use cases, we noticed that, when the percentage of τ -transitions obtained after maximal hiding is important (e.g., around 75% for the Alternating Bit Protocol), all reductions are likely to improve the performance of verification. This is valid even for strong bisimulation, which has a low computational cost compared to weak equivalences, and is able in some cases to merge large parts of the invisible behaviour.

When the system under analysis contains many interleavings of independent transitions (e.g., for loosely-coupled systems, such as the Erathosthene's sieve), the partial order reductions applied on-the-fly simultaneously with maximal hiding are likely to yield good results.

Finally, for large Ltss that can be constructed explicitly (e.g., the large configurations of the Dtd), a viable strategy seems to minimize them, after applying maximal hiding, modulo divergent-sensitive branching bisimulation using state-of-the art partition refinement algorithms, which have a better complexity than on-the-fly reductions.

Conclusion and Future Work

We have proposed two techniques enabling one to improve automatically the effectiveness of model checking modal µ-calculus (L µ ) formulas on Ltss by applying reductions modulo bisimilarity relations. The first technique, which uses strong bisimilarity, involves the maximal hiding of an Lts w.r.t. a given L µ formula without changing its truth value on that Lts. In this way, the Lts can be minimized modulo strong bisimilarity before carrying out the verification. This technique is not intrusive, meaning that the specifier is not forced to write L µ formulas in a certain way. The second technique, which uses divergence-sensitive branching bisimilarity (≈ ds br ), relies on a L µ fragment, called L dsbr µ (equally expressive to µ-Actl\X), that we proved adequate w.r.t. this relation. After applying maximal hiding w.r.t. a given L dsbr µ formula, the Lts can be reduced modulo ≈ ds br , either globally (i.e., by minimization prior to), or locally (i.e., by on-the-fly reduction simultaneously with) the verification of the formula. Experimental results on several examples of concurrent systems illustrate the effectiveness of these techniques.

As future work, we plan to study which property patterns of the system [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF] can be translated in L dsbr µ , so as to provide useful information about the possible reductions modulo ≈ ds br . We also plan to continue experimenting with maximal hiding and on-the-fly reduction by using weak forms of divergence-sensitive τ -confluence implemented in a distributed setting [START_REF] Mateescu | Sequential and Distributed On-the-Fly Computation of Weak Tau-Confluence[END_REF], by using clusters or grids for Lts reduction and verification. Finally, it is interesting to investigate property-dependent reductions in the context of directed model checking [START_REF] Wijs | What To Do Next?: Analysing and Optimising System Behaviour in Time[END_REF]. To show the equivalence between the last formula above and the translation of A[ϕ 1 α Uϕ 2 ] in L µ given in Figure 4, it remains to show the following equality:

µX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)) = νX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)) ∧ µX.(ϕ 2 ∨ [α ∨ τ ] X)
The "⇒" implication follows immediately by monotonicity. For the converse implication, we consider an Lts M = S, A, T, s 0 and we show the following inequality between the interpretations on M of the formulas in the left-and right-hand sides (note that ϕ 1 , ϕ 2 are closed and therefore there is no need for a propositional context ρ):

[[νX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X))]] M ∩ [[µX.(ϕ 2 ∨ [α ∨ τ ] X)]] M ⊆ [[µX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X))]] M
Let Φ M , Ψ M : 2 S → 2 S the functionals defined below:

Φ M (U ) = [[ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)]] M [U/X] Ψ M (U ) = [[ϕ 2 ∨ [α ∨ τ ] X]] M [U/X]
Using the iterative characterization of fixed point operators [START_REF] Kleene | Introduction to Metamathematics[END_REF], the inequality above can be reformulated in terms of these functionals as follows:

n≥0 Φ n M (S) ∩ n≥0 Ψ n M (∅) ⊆ n≥0 Φ n M (∅) or, equivalently:

k≥0 n≥0 Φ n M (S) ∩ Ψ k M (∅) ⊆ k≥0 Φ k M (∅)

Figure 1 :

 1 Figure 1: Syntax and semantics of L µ The interpretation [[α]] A of an action formula on the set of actions of an Lts denotes the subset of actions satisfying α. An action b satisfies a formula α (also denoted by b |= A α) if and only if b ∈ [[α]] A . A transition s 1

Figure 2 :

 2 Figure 2: Syntax, semantics, and L µ encoding of Pdl-∆

  and let b ∈ A. Two cases are possible. If b ∈ h A (α), then hide h A (α) (b) = b by Definition 3; in this case, no hiding takes place, and the property holds trivially. If b ∈ h A (α), then hide h A (α) (b) = τ by Definition 3. Two subcases are possible. If τ |= A α, then h A (α) = [[α]] A by Definition 2, and therefore b |= A α. If τ |= A α, then h A (α) = A \ [[α]] A by Definition 2, and therefore b |= A α.

  which by Definition 3 becomes b |= A α ⇔ τ |= A α. Two cases are possible, both leading to a contradiction. If τ |= A α, then h A (α) = [[α]] A by Definition 2, and since b ∈ h A (α), this means b |= A α. If τ |= A α, then h A (α) = A \ [[α]] A by Definition 2, and since b ∈ h A (α), this means b |= A α.

µ

  with ≈ ds br (i.e., a L dsbr µ formula has the same truth value on those Ltss equivalent modulo ≈ ds br ) and, on the other hand, the compatibility of ≈ ds br with L dsbr µ (two Ltss satisfying the same set of L dsbr µ formulas are equivalent modulo ≈ ds br ). Adequacy is important in practice when verifying a L dsbr µ formula on an Lts: any ≈ ds br -preserving reduction of the Lts (either minimization modulo ≈ ds br , or another partial reduction preserving this relation) does not change the interpretation of the formula, and moreover may improve drastically the efficiency of verification. Then, we study the relation between the L dsbr µ fragment and several other weak L µ fragments adequate w.r.t. weak bisimilarity relations.

Figure 3 :

 3 Figure 3: Syntax and semantics of the L dsbr µ fragment

Figure 4 :

 4 Figure 4: Syntax, semantics, and L µ encoding of Actl\X temporal operators

Figure 5 :

 5 Figure 5: Syntax, semantics, and L µ encoding of selective µ-calculus modalities

Figure 6 :

 6 Figure 6: Syntax, semantics, and L µ encoding of weak µ-calculus modalities

Figure 7 :

 7 Figure 7: Effect of strong bisimulation minimization (Alternating Bit Protocol)

Figure 8 :

 8 Figure 8: Effect of strong bisimulation minimization (Token Ring Protocol)

P 5 Figure 9 :

 59 Figure 9: Effect of ≈ ds br minimization (Dynamic Task Dispatcher)

Figure 10 :

 10 Figure 10: Effect of on-the-fly τ -confluence reduction (Erathostene's sieve)

  νX.((ϕ2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false)) ∧ [¬ϕ 2 ?] [α ∨ τ ] X) ∧ [¬ϕ 2 ?.α ∨ τ ] ⊣ = by expansion of the ? operator νX.((ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false)) ∧ (ϕ 2 ∨ [α ∨ τ ] X)) ∧ [¬ϕ 2 ?.α ∨ τ ] ⊣ = by propositional calculus νX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)) ∧ [¬ϕ 2 ?.α ∨ τ ] ⊣ = by expansion of [. . .] ⊣ νX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)) ∧ µX. [¬ϕ 2 ?.α ∨ τ ] X = by expansion of the . operator νX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)) ∧ µX. [¬ϕ 2 ?] [α ∨ τ ] X = by expansion of the ? operator νX.(ϕ 2 ∨ (ϕ 1 ∧ ¬deadlock ∧ [¬(α ∨ τ )] false ∧ [α ∨ τ ] X)) ∧ µX.(ϕ 2 ∨ [α ∨ τ ] X).

  → . . . and s k R t for all k ≥ 0, then there is an infinite sequence of states t 0 , t 1 , t 2 , . . . such that t 0 = t, t 0

	s 0	τ → s 1	τ → s 2	τ	1 , s 2 , . . . such that s 0 = s, τ → t 1 τ → t 2 τ → . . . and
	s k R t ℓ for all k, ℓ ≥ 0.
	Two states s and t are divergence-sensitive branching bisimilar, denoted by
	s ≈ ds br t, if there is a divergence-sensitive branching bisimulation R with s R t.

  since s 1 ≈ ds br s 2 and (3), by Lemma 2 with A ′ = {τ }, there exists k ≥ 0 with s 2 = s ′′ 0 such that ∀0 ≤ j < k.(s ′′ ′′ j and s′ i ∈ [[ϕ 1 ]] M ρ (3),by the induction hypothesis, it follows that s ′′ j ∈ [[ϕ 1 ]] M ρ. Finally, we have to show that s ′′ M ρ, by the induction hypothesis, also s ∈ [[ϕ 1 ]] M ρ. But then, we can select a higher k, thereby extending the path s 2 = ⇒ s ′′ The converse implication (by considering s 2 ∈ [[ (ϕ 1 ?.τ ) * .ϕ 1 ?.α 2 ϕ 2 ]] M ρ) holds by a symmetric argument.

	j k . Furthermore, for all 0 ≤ j < k, since there exists 0 ≤ i < τ → s ′′ j+1 ∈ T ∧ ∃0 ≤ i < m.s ′ i ≈ ds br s ′′ j ) br s ′′ m ≈ ds and s ′ m.s ′ i ≈ ds br s k c → s ′′ k+1 , with c ∈ [[α 2 ]] A and
	s ′′ k+1 ∈ [[ϕ 2 ]] M ρ. Since s ′ m ≈ ds br s ′′ k , and by (3), s ′ m can distinguish two cases:	b → s ′ m+1 , with b ∈ [[α 2 ]] A , we
	1. s ′′ k	b → s ′′ k+1 and s ′ m+1 ≈ ds br s ′′ k+1 . Since s ′
	s ′ m+1 ≈ ds br s ′′	k	b → s ′′ k+1 , with s ′ m ≈ ds br	ŝ′′ k and

m+1 ∈ [[ϕ 2 ]] M ρ, by the induction hypothesis, s ′′ k+1 ∈ [[ϕ 2 ]] M ρ. Furthermore, b ∈ [[α 2 ]] A .

Hence, (4) holds. 2. There exists a ŝ′′ k such that s ′′ k = ⇒ ŝ′′ k+1 . By Definition 1, it follows that for all intermediate states s in s ′′ k = ⇒ ŝ′′ k , we have s ′ m ≈ ds br s, and since s ′ m ∈ [[ϕ 1 ]] k to s 2 = ⇒ ŝ′′ k , i.e. we can initially select ŝ′′ k as s ′′ k . If we do this, then since s ′ m+1 ∈ [[ϕ 2 ]] M ρ, by the induction hypothesis, s ′′ k+1 ∈ [[ϕ 2 ]] M ρ. Furthermore, b ∈ [[α 2 ]] A . Hence, (4) holds.

  ds br s ′′ j ) and s ′ m ≈ ds br s ′′ k , hence, by the induction hypothesis, for all 0 ≤ j ≤ k, we have s ′′ j ∈ [[ϕ 1 ]] M ρ. We distinguish two cases: 1. π contains an infinite number of transitions with a label in [[α 1 ]] A \ {τ }. Repeatedly applying the above reasoning for intermediate states in π yields that (6) holds for s 2 . 2. π contains a finite number of transitions with a label in [[α 1

  there is an infinite sequence of states s 0 , s 1 , s 2 , . . . such that s 0 = s, ≥ 0, then there is an infinite sequence of states t 0 , t 1 , t 2 , . . . such that t 0 = t, t 0

			τ → t 1	τ → t 2	τ → . . . and
	s k R t ℓ for all k, ℓ ≥ 0.
	4. if there is an infinite sequence of states t 0 , t 1 , t 2 , . . . such that t 0 = t, t 0 τ → t 1 τ → t 2 τ
	s 0	τ → s 1	τ → s 2

τ → . . . and s k R t for all k

This article is an extended version of the conference article[START_REF] Mateescu | Property-Dependent Reductions for the Modal Mu-Calculus[END_REF]. Email addresses: Radu.Mateescu@inria.fr (Radu Mateescu), A.J.Wijs@tue.nl (Anton Wijs)

In fact, a distinction can be made between divergence-sensitive branching bisimilarity[START_REF] Nicola | Action versus State Based Logics for Transition Systems[END_REF] and branching bisimilarity with explicit divergence[START_REF] Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF][START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF]. Contrary to the former, the latter distinguishes deadlocks and livelocks, and the latter is the coarsest congruence contained in the former. In this paper, we use the latter, but refer to it with the (more classical) name of the former.

See http://cadp.inria.fr

Referred to as branching bisimilarity with explicit divergence in[START_REF] Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF][START_REF] Glabbeek | Branching Bisimilarity with Explicit Divergence[END_REF], see footnote 2.

In the action-based setting, we use the term "inevitable reachability" of an action b to express that all sequences going out from the current state contain a b-transition after a finite number of steps.

See http://www.grid5000.fr

Acknowledgments

We are grateful to the anonymous referees for their insightful comments, which allowed us to correct an error and to improve the text accordingly. We also thank Wendelin Serwe for carrying out the reduction experiments and gracefully providing the results concerning the Dtd case-study. These experiments were carried out using the Grid'5000 experimental testbed 6 built by Inria with support from CNRS, RENATER, several Universities, and other funding bodies.

As explained in [START_REF] Aceto | Characteristic Formulae for Fixed-Point Semantics: A General Framework[END_REF], we can now construct a monotonic function declaration D, by combining the translations of the individual clauses, such that the characteristic formula is given by the largest interpretation of that declaration:

This completes our adequacy result between L dsbr µ and ≈ ds br . In practice, it is desirable to use a temporal logic sufficiently expressive to capture the essential classes of properties (safety, liveness, fairness) of concurrent systems. Thus, the question is whether L dsbr µ subsumes the existing temporal logics adequate w.r.t. weak equivalence relations (such as τ * .a and weak bisimilarities); in the next subsection, we show that this is indeed the case.

Expressiveness of L dsbr µ

We examine here the relation between L dsbr µ and existing µ-calculi adequate w.r.t. weak equivalence relations. We show first that L dsbr µ is equally expressive to µ-Actl\X, and then we show that L dsbr µ subsumes (a relevant fragment of) selective L µ , as well as the weak L µ .

Translating L dsbr µ into µActl\X and back. Actl [START_REF] Nicola | Action versus State Based Logics for Transition Systems[END_REF] is a branching-time logic similar to Ctl [START_REF] Clarke | Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications[END_REF], but interpreted on Ltss. It consists of action formulas (denoted by α) and state formulas (denoted by ϕ) expressing properties about actions and states of an Lts, respectively. The temporal operators of Actl\X, the fragment of the logic without the next-time operators, are defined in Figure 4 (boolean state formulas are omitted for brevity). of processors for parallel execution. We use the Lnt formal model and some of the temporal logic properties of the Dtd given in [START_REF] Lantreibecq | Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP[END_REF].

Property P 2 , expressed by the formula below, requires that, after waking up a processor x (action wakeup x ), the Dtd eventually informs the processor that there is no more work left (action ld rsp none x ):

The formula fair (α 1 , α 2 ), where α 1 denotes visible actions only and α 2 must capture the invisible action, specifies that an α 1 -transition is eventually reached from the current state by avoiding the (spurious) cycles of actions other than α 1 , and by forbidding α 2 -cycles:

In the Dtd model, the cycles of ld rsp wait slave actions correspond to a master processor waiting indefinitely for the slave processes to terminate, which is an unrealistic situation in the real system, each slave process being supposed to terminate its task. The saturation operator [¬ld rsp wait slave] ⊣ forbids the presence of cycles containing actions other than ld rsp wait slave, meaning that only cycles of ld rsp wait slave actions are allowed (and ignored). The formula encoding P 2 belongs to L dsbr µ , enabling one to hide every action other than wakeup x , ld rsp none x , and ld rsp wait slave.

Property P 5 , expressed by the formula below, requires that each duplication operation for processor x, task c, and number n (action st dup x,c,n ) is followed by the correct number of subtask assignments (actions ld rsp y,c,i ) for each 0 ≤ i < n:

[true * ] τ * .st dup x,c,n 0≤i<n fair (ld rsp y,c,i , ¬ld rsp wait slave) This formula also belongs to L dsbr µ , enabling one to hide every action other than st dup x,c,n , ld rsp y,c,i , and ld rsp wait slave.

The overall time and peak memory needed for verification of properties P 2 and P 5 are shown in Figure 9 for increasingly larger configurations of the Dtd. The minimization modulo ≈ ds br induces significant reductions of both execution time (factor 20.6 for P 2 on the Lts with 48, 263, 777 states) and memory consumption (factor 5.4 for P 2 on the same Lts). For property P 5 , the largest three configurations considered (Ltss having more that 36, 865, 661 states), which caused memory exhaustion using the direct approach, could be checked only with the help of ≈ ds br minimization.

Appendix A. Proofs

We provide in this annex the proofs of all lemmas and propositions stated in the main text.

Proposition 2. We proceed by structural induction on ϕ. For brevity, we omit the (straightforward) boolean cases, and prove only the fixed point cases. Case ϕ ::= X. Let s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 and assume that s

Case ϕ ::= µX.ϕ 1 . Since we consider finite Ltss, we can use the alternative characterization of minimal fixed point formulas [START_REF] Kleene | Introduction to Metamathematics[END_REF]:

We show first the following statement by induction on k:

. By the induction hypothesis of (A.1), this is equivalent to s

] is ≈ ds br -closed, we can apply the induction hypothesis of the proposition to s 1 , ϕ, and ρ ⊘ [Φ k M,ρ (∅)/X], and conclude that

holds by a symmetric argument.

Let s 1 , s 2 ∈ S such that s 1 ≈ ds br s 2 and assume

. This means there exists k ≥ 0 such that s 1 ∈ Φ k M,ρ (∅) and by applying (A.1), this is equivalent to

In order to prove Proposition 4, we show first two lemmas. Lemma 3. Let X ∈ X be a propositional variable and let ϕ be a state formula of L µ , which may contain free occurrences of X. Then:

for any regular formula β of Pdl.

Proof. The right-hand side of the identity can be rewritten by applying the Pdl identity

The first occurrence of X can be replaced with true by applying absorption, which yields the identity below:

Consider an Lts M = S, A, T, s 0 and a propositional context ρ. The functionals Φ M,ρ : 2 S → 2 S and Ψ M,ρ : 2 S → 2 S are defined as follows:

Let θ, θ ′ ⊆ S be the maximal fixed points of Φ M,ρ , Ψ M,ρ , respectively. We must show that θ = θ ′ . We show first that θ ⊆ θ ′ by using Tarski's theorem, which requires to check that θ ⊆ Ψ M,ρ (θ). By definition, θ satisfies the fixed point equation

). The semantics of this formula when X is replaced by θ is characterized iteratively as follows [START_REF] Kleene | Introduction to Metamathematics[END_REF]:

To show the desired inclusion, we prove that θ ⊆ Γ k M,ρ⊘[θ/X] (S) by induction on k.

1. Base case: θ ⊆ S = Γ 0 M,ρ⊘[θ/X] (S). 2. Inductive case:

To show that θ ′ ⊆ θ, we check that θ ′ is a fixed point of Φ M,ρ :

Lemma 4. Let β 1 , β 2 be regular formulas of Pdl such that they denote onestep sequences (i.e., β 1 and β 2 are satisfied by transition sequences containing only one transition) and they are disjoint (i.e., no transition can satisfy both β 1 and β 2 ). Then:

Proof. (a). To show the "⇐" implication, we observe that both disjuncts in the right-hand side of the equality are included in the left-hand side term because the ω-regular languages (β * 1 .β 2 ) * .β ω 1 and (β * 1 .β 2 ) ω are both included in (β 1 |β 2 ) ω , which consists of all infinite sequences made from transitions satisfying β 1 or β 2 . For the "⇒" implication, we observe that, since β 1 and β 2 are disjoint, the ω-regular languages (β * 1 .β 2 ) * .β ω 1 and (β * 1 .β 2 ) ω are complementary: they denote the set of infinite sequences containing a finite and an infinite number of occurrences of β 2 , respectively. Therefore, any infinite sequence of the form (β

, and thus satisfies one of the disjuncts in the right-hand side of the equality. (b). The "⇒" implication holds by monotonicity: since

, and then by monotonicity

The "⇒" implication holds by monotonicity: since

The "⇐" implication holds trivially, since β * 1 .β 2 ϕ ⇐ β 2 ϕ for any ϕ.

Proposition 4. Starting from the L dsbr µ formulations of the Actl\X temporal operators stated in the proposition, we expand the weak modalities to obtain plain L µ formulas, and then we show that these formulas are equivalent to the L µ formulas given in Figure 4.

= by expansion of the . operator µX.(ϕ 2 ∨ ϕ 1 ? α ∨ τ X) = by expansion of the ? operator

= by expansion of the * operator µX.((

by expansion of the . operator

To prove this inequality, we first show the relation below by induction on k:

By applying union for all k ≥ 0 on the left-and right-hand sides of (A.3), we obtain the desired inequality.

Operator

To show the equivalence between the last formula above and the translation of A[ϕ 1 α 1 U α 2 ϕ 2 ] in L µ given in Figure 4, it remains to show the equality:

The proof of this last equality is very similar to the proof of the corresponding equality for the A[ϕ 1 α Uϕ 2 ] operator above, and is omitted here.