Frédéric Lang
email: frederic.lang@inria.fr

Radu Mateescu
email: radu.mateescu@inria.fr

Franco Mazzanti
email: franco.mazzanti@isti.cnr.it

Compositional Verification of Concurrent Systems by Combining Bisimulations

Keywords: Concurrency theory, labelled transition system, modal mu-calculus, model checking, state space reduction, temporal logic

One approach to verify a property expressed as a modal µ-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the L dbr µ fragment of the µ-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or divbranching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend L dbr µ with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by divbranching bisimulation.

Introduction

We consider the problem of verifying a temporal logic property ϕ on a concurrent system P 1 || ... || P n consisting of n processes composed in parallel. We work in the action-based setting, the property ϕ being specified as a formula of the modal µcalculus (L µ ) [START_REF] Kozen | Results on the propositional µ-calculus[END_REF] and the processes P i being described in a language with process algebraic flavour. A well-known problem is the state-space explosion that happens when the system state space exceeds the available computer memory.

Compositional verification is a set of techniques and tools that have proven efficient to palliate state-space explosion in many situations [START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF]. These techniques may be either independent of the property, i.e., focus only on the construction of the system state space, such as compositional state space construction [START_REF] Malhotra | A Tool for Hierarchical Design and Simulation of Concurrent Systems[END_REF][START_REF] Krishan | An Algorithmic Procedure for Checking Safety Properties of Protocols[END_REF][START_REF] Kuo | Hierarchy-Based Incremental Reachability Analysis of Communication Protocols[END_REF][START_REF] Kuo | An Incremental Approach to Reachability Analysis of Distributed Programs[END_REF][START_REF] Graf | Compositional Minimization of Finite State Systems[END_REF][START_REF] Valmari | Compositional State Space Generation[END_REF][START_REF] Krimm | Compositional State Space Generation from LOTOS Programs[END_REF]. Alternatively, they may depend on the property, e.g., verification of the property on the full system is decomposed in the verification of properties on (expectedly smaller) sub-systems, such as in compositional reachability analysis [START_REF] Wei | Compositional Reachability Analysis Using Process Algebra[END_REF][START_REF] Cheung | Enhancing Compositional Reachability Analysis with Context Constraints[END_REF], assume-guarantee reasoning [START_REF] Pnueli | In transition from global to modular temporal reasoning about programs[END_REF], or partial model checking [START_REF] Reif | Partial model checking[END_REF].

Nevertheless, the frontier between property-independent and property-dependent techniques is blurred. In compositional state space construction, to be able to reduce the system size, a set of actions is selected and a suitable equivalence relation (e.g., strong bisimulation, branching bisimulation, or divergence-preserving branching bisimulation 1 -divbranching for short) is chosen, restricting the set of properties preserved after hiding the selected actions and reducing the system w.r.t. the selected relation. Therefore, there is still a dependency between the state space construction and the set of properties that can be verified. Given a formula ϕ of L µ to be verified on the system, Mateescu & Wijs [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] have pushed this idea and shown how to extract a maximal hiding set of actions and an equivalence relation (either strong or divbranching bisimulation) automatically from ϕ, thus inviting the compositional state space construction technique to the table of property-dependent reductions. To select the equivalence relation from the formula, they have identified an L µ fragment named L dbr µ , which is adequate 2 with divbranching bisimulation [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF]. This fragment consists of L µ restricted to weak modalities, which match visible actions preceded by arbitrary sequences of hidden actions, as opposed to traditional strong modalities �α� ϕ 0 and [α] ϕ 0 , which match only a single action satisfying α. If ϕ belongs to L dbr µ , then the system can be reduced for divbranching bisimulation; otherwise, it can be reduced for strong bisimulation, the weakest equivalence relation preserving full L µ .

In this paper, we revisit and refine this approach to accommodate L µ formulas containing both strong and weak modalities. To do so, we define a logic named the processes containing strong actions are reduced modulo strong bisimulation and the other ones modulo divbranching bisimulation. We also provide guidelines for extracting the set A s from particular L µ formulas encoding the operators of widely-used temporal logics, such as CTL [START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF], ACTL [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF], PDL [START_REF] Michael | Propositional dynamic logic of regular programs[END_REF], and PDL-Δ [START_REF] Streett | Propositional dynamic logic of looping and converse is elementarily decidable[END_REF]. This combined use of bisimulations to reduce different parts of the same system makes possible to fine-tune the compositional state space construction by going smoothly from strong bisimulation (when all modalities are strong) to divbranching bisimulation (when A s is empty, as in the previous approach based on L dbr µ ). We implemented this approach on top of the CADP verification toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], and demonstrated how it improves the capabilities of compositional verification on two realistic case studies, namely the TFTP plane-ground communication protocol specified in [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF] and the parallel CTL benchmarks of the RERS'2018 and RERS'2019 challenges.

This paper is an extended version of a previous paper [START_REF] Lang | Compositional verification of concurrent systems by combining bisimulations[END_REF]. Besides new examples and informal explanations, it incorporates the full proofs of all lemmas and theorems, a new section about the automatic extraction of a set of strong actions from a (test-free) PDL formula, a new theorem about the complexity of extracting a minimal set of strong actions from an arbitrary L µ formula, more details on the TFTP case study, a new section on the RERS'2019 parallel challenge (which was not addressed in the short version), and a new related work section.

The paper is organized as follows. Section 2 recalls some definitions. Section 3 defines L strong µ (A s ) and proves the main result of its adequacy with the combined use of strong and divbranching bisimulations. Section 4 deals with the problem of extracting sets of strong actions in the general case of L µ formulas and in particular fragments. Section 5 presents the experimental results obtained on the case studies. Section 6 discusses the relation between the compositional verification approach presented in this paper and two other approaches, namely partial model checking and partial order reductions. Finally, Section 7 contains concluding remarks and directions of future work. The case studies are available at http://doi.org/10. 5281/zenodo.2634148.

Background

LTS compositions and reductions

We consider systems whose behavioural semantics can be represented using an LTS (Labelled Transition System).

Definition 1 (LTS) Let A denote an infinite set of actions, including the invisible action τ , which denotes internal behaviour. All actions in A \ {τ } are called visible actions. An LTS is a tuple (Σ, A, -→, p init ), where Σ is a set of states, A ⊆ A is a set of actions, -→ ⊆ Σ × A × Σ is the (labelled) transition relation, and p init ∈ Σ is the initial state. Note that A may be empty only in the pathological case where -→ is empty, whereas Σ has at least one element p init . We write p a -→ p � if (p, a, p � ) ∈ -→ and p τ * -→ p � if there is a (possibly empty) sequence of τ -transitions from p to p � , i.e., states p 0 , . . . , p n (n ≥ 0) such that p = p 0 , p � = p n , and p i τ -→ p i+1 for i = 0, . . . , n -1.

LTS can be composed in parallel and their actions can be abstracted away using the parallel composition and hiding operators defined below. Prior to hiding, an action mapping operator is also introduced for the generality of the approach.

Definition 2 (Parallel composition of LTS) Let P = (Σ P , A P , -→ P , p init ), Q = (Σ Q , A Q , -→ Q , q init ), and A sync ⊆ A \ {τ }. The parallel composition of P and Q with synchronization on A sync , written "P |[A sync ]| Q", is defined as the LTS (Σ P × Σ Q , A P ∪ A Q , -→, (p init , q init )), where (p, q) a -→ (p � , q � ) if and only if either:

-p a -→ P p � , q � = q, and a / ∈ A sync , or -p � = p, q a -→ Q q � , and a / ∈ A sync , or -p a -→ P p � , q a -→ Q q � , and a ∈ A sync .

To alleviate notations, we generally omit the curly braces delimiting elements of the set A sync , e.g., writing respectively Definition 3 (Action mapping) Consider an LTS P = (Σ P , A P , -→ P , p init ) and a total function ρ : A P → [A] <ω (where [A] <ω denotes the set of finite subsets of A) called action mapping. By abuse of notation, we write ρ(A P ) for the image set of ρ, defined as � a∈A P ρ(a), and ρ(P ) for the action mapping ρ applied to P , defined as (Σ P , ρ(A P ), -→, p init ), where -→ = {(p 1 , a � , p 2 ) | (∃a ∈ A P ) p 1 a -→ P p 2 ∧a � ∈ ρ(a)}.

An action mapping ρ is admissible if

τ ∈ A P ⇒ ρ(τ ) = {τ }.
Action mapping enables a single action a to be mapped onto the empty set of actions, onto a single action a � , or onto more than one (but finitely many) actions a � 0 , . . . , a � n+1 (n ≥ 0). In the first case, every transition labelled by a is removed. In the second case, a is renamed into a � . In the third case, every transition labelled by a is replaced by n + 2 transitions with same source and target states, labelled by a � 0 , . . . , a � n+1 . Action hiding is a special case of admissible action mapping.

Definition 4 (Action hiding) Let P = (Σ P , A P , -→ P , p init ) and A ⊆ A \ {τ }. We write "hide A in P " for the LTS ρ(P ), where ρ is the admissible action mapping defined by (∀a ∈ A P ∩ A) ρ(a) = {τ } and (∀a

∈ A P \ A) ρ(a) = {a}.
Parallel composition and admissible action mapping subsume all abstraction and composition operators encodable as networks of LTS [START_REF] Frédéric | OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF][START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF][START_REF] Sander De Putter | Compositional model checking is lively -extended version[END_REF], such as the parallel composition, hiding, renaming, and cut (or restriction) operators of the process languages CCS [START_REF] Milner | Communication and Concurrency[END_REF], CSP [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF], µCRL [START_REF] Friso | The Syntax and Semantics of µCRL[END_REF], mCRL2 [START_REF] Friso | Modeling and Analysis of Communicating Systems[END_REF], LOTOS [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF], E-LOTOS [START_REF]ternational Organization for Standardization -Information Technology[END_REF], and LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF], as well as synchronization vectors. The ability to map a single action onto a set of actions is essential to attain such a generality. For instance, the composition of P and Q using synchronization vectors a||b → a 1 and a||c → a 2 (where action a of P synchronizes with either action b or c of Q), can be written e.g., as ρ 2 (ρ

1 (P ) |[b, c]| Q),
where ρ 1 maps a onto {b, c} and ρ 2 maps b onto {a 1 } and c onto {a 2 }.

In the sequel, we write P 1 || . . . || P n for any expression composing P 1 , . . . , P n using any combination of parallel composition and action mapping. Given any partition of P 1 , . . . , P n into arbitrary subsets P 1 and P 2 , it is always possible to rewrite P 1 || . . . || P n in the form (|| P i ∈P 1 P i ) || (|| P j ∈P 2 P j ) using appropriate action mappings, even for non-associative parallel composition operators. For instance, the parallel composition operator |[. . .]| is not associative, as

P 1 |[a]| (P 2 |[]| P 3 ) is not equal (in terms of LTS) to (P 1 |[a]| P 2 ) |[]| P 3 . However, the former parallel composition expression is equal to ρ 0 ((ρ 1 (P 1 ) |[a 1 ]| ρ 2 (P 2 )) |[a 2 ]| ρ 3 (P 3 ))
, where ρ 1 maps a onto {a 1 , a 2 }, ρ 2 renames a into a 1 , ρ 3 renames a into a 2 , and ρ 0 renames a 1 and a 2 into a.

LTS can be compared and reduced with respect to well-known bisimilarity relations. In this paper, we consider strong bisimulation [START_REF] Park | Concurrency and Automata on Infinite Sequences[END_REF] and divbranching bisimulation, which itself derives from branching bisimulation [START_REF] Van Glabbeek | Branching-Time and Abstraction in Bisimulation Semantics[END_REF][START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF].

Definition 5 (Strong bisimulation) A strong bisimulation is a symmetric rela- tion R ⊆ Σ × Σ such that if (p 1 , p 2 ) ∈ R then for all p 1 a -→ p � 1 , there exists p � 2 such that p 2 a -→ p � 2 and (p � 1 , p � 2 ) ∈ R. Definition 6 (Branching bisimulation) A branching bisimulation is a symmetric relation R ⊆ Σ × Σ such that if (p 1 , p 2 ) ∈ R then for all p 1 a -→ p � 1 , either: -a = τ and (p � 1 , p 2 ) ∈ R, or -there exists a sequence p 2 τ * -→ p � 2 a -→ p �� 2 such that (p 1 , p � 2 ) ∈ R and (p � 1 , p �� 2 ) ∈ R.
Definition 7 (Divbranching bisimulation) A divergence-preserving branching bisimulation (divbranching bisimulation for short) is a branching bisimulation R such that if (p 0 1 , p 0

2 ) ∈ R and there exists an infinite sequence

p 0 1 τ -→ p 1 1 τ -→ p 2 1 τ -→ . . . with (p i 1 , p 0
2 ) ∈ R for all i ≥ 0, then there exists an infinite sequence

p 0 2 τ -→ p 1 2 τ -→ p 2 2 τ -→ . . . such that (p i 1 , p j 2 ) ∈ R for all i, j ≥ 0.
Definition 8 (Strong, branching, divbranching bisimilarity) Two states p 1 and p 2 are strongly (resp. branching, divbranching) bisimilar, written p 1 ∼ p 2 (resp. p 1 ∼ br p 2 , p 1 ∼ dbr p 2 ), if there exists a strong (resp. branching, divbranching) bisimulation R such that (p 1 , p 2 ) ∈ R. Two LTS P 1 and P 2 are strongly (resp. branching, divbranching) bisimilar, written P 1 ∼ P 2 (resp. P 1 ∼ br P 2 , P 1 ∼ dbr P 2 ), if their initial states are strongly (resp. branching, divbranching) bisimilar.

Reduction with respect to (div)branching bisimulation usually yields much smaller LTS than reduction with respect to strong bisimulation when the LTS contains transitions labelled by τ . In particular, (div)branching bisimulation reduction compresses the so-called inert τ -transitions, which are the transitions labelled by τ , whose source and target state are (div)branching bisimilar. An effective way to fight against state explosion therefore consists in hiding as many labels as possible and then applying (div)branching bisimulation reduction whenever possible. However, some properties satisfied by an LTS may no longer hold true on the LTS obtained after label hiding and/or (div)branching bisimulation reduction. It is therefore essential to characterize which sets of properties are preserved by which reductions. This is a major subject of this paper.

Strong, branching, and divbranching bisimilarities are congruences for parallel composition and admissible action mapping. This allows reductions to be applied at any intermediate step during the state space construction, thus potentially reducing the overall cost of reduction. However, since processes may constrain each other by synchronization, composing LTS two by two following the algebraic structure of the composition expression and applying reduction after each composition can be orders of magnitude less efficient than other strategies in terms of the largest intermediate LTS. Finding an optimal strategy is difficult. One generally relies on heuristics to select a subset of LTS to compose at each step of the compositional reduction. In this paper, we will use the smart reduction heuristic [START_REF] Crouzen | Smart Reduction[END_REF][START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF], which is implemented within the SVL [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF] tool of CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. This heuristic tries to find an efficient composition order by analysing the synchronization and hiding structure of the composition expression.

Example 1 Consider the system defined as hide a in (P

|[a]| Q) |[b, c]| R
, where P , Q, and R are defined below (throughout this paper, in every graphical representation of an LTS, we use index 0 to denote its initial state):

P = p 0 a � � p 1 d � � p 2 b � � p 3 Q = q 0 a � � q 1 c � � q 2 e � � q 3 R = r 0 b � � r 1 c � �
The order consisting in first computing the minimal LTS corresponding to hide a in (P |[a]| Q), then composing the result with R produces a largest intermediate LTS with 10 states and 13 transitions. On the other hand, computing the minimal LTS corresponding to hide a in (P

|[a]| Q) |[b, c]| R
at once (which is the order chosen by smart reduction in this case) produces a (largest) LTS with 6 states and 5 transitions. Another order consisting in first composing Q and R, then reducing the result and composing it with P produces a largest intermediate LTS with 6 states and 6 transitions.

Note that composing Q and R is possible using, e.g., the composition expres-

sion ρ 1 (Q) |[b � , c � ]| ρ 0 (R), considering that hide a in (P |[a]| Q) |[b, c]| R is equal to hide a in ρ 2 (P |[a, b, c]| (ρ 1 (Q) |[b � , c � ]| ρ 0 (R)))
, where ρ 0 maps b onto {b, b � }, c onto {c, c � }, and a onto {a � } (leaving all other actions unchanged), ρ 1 renames b into b � and c into c � (leaving all other actions unchanged), ρ 2 renames a � into a, b � into b, and c � into c (leaving all other actions unchanged), and a � , b � , c � are fresh actions that do not occur in P , Q, and R. In practice, we do not rewrite composition expressions in this way, but instead translate composition expressions into networks of LTS [START_REF] Frédéric | OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF] and use an operator of aggregation defined in [START_REF] Crouzen | Smart Reduction[END_REF][START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF].

Temporal logics

Definition 9 (Modal µ-calculus [START_REF] Kozen | Results on the propositional µ-calculus[END_REF]) The modal µ-calculus (L µ ) is built from action formulas α and state formulas ϕ, whose syntax and semantics w.r.t. an LTS P = (Σ, A, -→, p init ) are defined as follows:

α ::= a [[a]] A = {a} | false [[false]] A = ∅ | α 1 ∨ α 2 [[α 1 ∨ α 2 ]] A = [[α 1 ]] A ∪ [[α 2 ]] A | ¬α 0 [[¬α 0 ]] A = A \ [[α 0 ]] A ϕ ::= false [[false]] P δ = ∅ | ϕ 1 ∨ ϕ 2 [[ϕ 1 ∨ ϕ 2 ]] P δ = [[ϕ 1 ]] P δ ∪ [[ϕ 2 ]] P δ | ¬ϕ 0 [[¬ϕ 0 ]] P δ = Σ \ [[ϕ 0 ]] P δ | �α� ϕ 0 [[�α� ϕ 0 ]] P δ = {p ∈ Σ | ∃p a -→ p � .a ∈ [[α]] A ∧ p � ∈ [[ϕ 0 ]] P δ } | X [[X]] P δ = δ(X) | µX.ϕ 0 [[µX.ϕ 0 ]] P δ = � {U ⊆ Σ | Φ 0P,δ (U ) ⊆ U }
where:

-X ∈ X are propositional variables, which denote sets of states; -δ : X � → 2 Σ is a context mapping propositional variables to sets of states; [ ] denotes the empty context and δ[U/X] the context identical to δ except for variable X, which is mapped to state set U ; -and Φ 0P,δ : 2 Σ → 2 Σ is the functional associated to the formula µX.ϕ 0 , defined as

Φ 0P,δ (U ) = [[ϕ 0 ]] P δ[U/X].
A closed formula is a formula in which every occurrence of X occurs in the context ϕ 0 of a fixed point operator µX.ϕ 0 or νX.ϕ 0 . For a closed formula ϕ, we write

P |= ϕ (read P satisfies ϕ) for p init ∈ [[ϕ]] P [ ].
Action formulas α are built from actions and Boolean operators. State formulas ϕ are built from Boolean operators, the possibility modality �α� ϕ 0 denoting the states with an outgoing transition labelled by an action satisfying α and leading to a state satisfying ϕ 0 , and the minimal fixed point operator µX.ϕ 0 denoting the least solution of the equation X = ϕ 0 interpreted over 2 Σ . The usual derived operators are defined as follows: Boolean connectors true = ¬false and ϕ 1 ∧ ϕ 2 = ¬(¬ϕ 1 ∨ ¬ϕ 2 ); necessity modality [α] ϕ 0 = ¬�α� ¬ϕ 0 ; and maximal fixed point operator νX.ϕ 0 = ¬µX.¬ϕ 0 [¬X/X], where ϕ 0 [¬X/X] is the syntactic substitution of X by ¬X in ϕ 0 . Syntactically, �� and [] have the highest precedence, followed by ∧, then ∨, and finally µ and ν, so that e.g., the formula µX.�a� true ∧ [b] X ∨ νY.�c� Y is parsed as µX.(((�a� true) ∧ [b] X) ∨ νY.�c� Y ). To have a well-defined semantics, state formulas are syntactically monotonic [START_REF] Kozen | Results on the propositional µ-calculus[END_REF], i.e., in every subformula µX.ϕ 0 , all occurrences of X in ϕ 0 fall in the scope of an even number of negations. Thus, negations can be eliminated by downward propagation.

Although L µ subsumes most action-based logics, its operators are rather lowlevel and lead to complex formulas. In practice, temporal logics or extensions of L µ with higher-level operators are used, avoiding (or at least reducing) the use of fixed point operators and modalities. We review informally some of these logics (whose operators can be translated to L µ ), which will be useful in the sequel.

Propositional Dynamic Logic with Looping The logic PDL-Δ [START_REF] Streett | Propositional dynamic logic of looping and converse is elementarily decidable[END_REF] introduces the modalities �β� ϕ 0 and �β� @, where β is a regular formula defined as follows:

β ::= ϕ? | α | β 1 .β 2 | β 1 |β 2 | β * 0
Regular formulas β denote sets of transition sequences in an LTS: the testing operator ϕ? denotes all zero-step sequences consisting of states satisfying ϕ; α denotes all one-step sequences consisting of a transition labelled by an action satisfying α; the concatenation β 1 .β 2 , choice β 1 |β 2 , and transitive-reflexive closure β * 0 operators have their usual semantics transposed to transition sequences.

The regular diamond modality �β� ϕ 0 denotes the states with an outgoing transition sequence satisfying β and leading to a state satisfying ϕ 0 . The infinite looping operator �β� @ denotes the states having an outgoing transition sequence consisting of an infinite concatenation of subsequences satisfying β. An encoding of PDL-Δ in L µ is formally defined in [START_REF] Emerson | Efficient model checking in fragments of the propositional mu-calculus[END_REF].

Action Computation Tree Logic The logic ACTL\X (ACTL without next operator) [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF] introduces four temporal operators, whose semantics can be found in terms of L µ formulas in [START_REF] Fantechi | From actl to µ-calculus (extended abstract)[END_REF][START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF], where α 1 , α 2 are action formulas interpreted over visible actions:

E(ϕ 1 α 1 U ϕ 2 ), E(ϕ 1 α 1 U α 2 ϕ 2 ), A(ϕ 1 α 1 U ϕ 2 ), A(ϕ 1 α 1 U α 2 ϕ 2 )
A transition sequence satisfies the path formula ϕ 1 α 1 U α 2 ϕ 2 if it contains a visible transition whose action satisfies α 2 and whose target state satisfies ϕ 2 , whereas at any moment before this transition, ϕ 1 holds and all visible actions satisfy α 1 . A sequence satisfies ϕ 1 α 1 U ϕ 2 if it contains a state satisfying ϕ 2 and at any moment before, ϕ 1 holds and all visible actions satisfy α 1 . A state satisfies E(ϕ

1 α 1 U α 2 ϕ 2 ) (resp. E(ϕ 1 α 1 U ϕ 2 )) if it has an outgoing sequence satisfying ϕ 1 α 1 U α 2 ϕ 2 (resp. ϕ 1 α 1 U ϕ 2 ). It satisfies A(ϕ 1 α 1 U α 2 ϕ 2 ) (resp. A(ϕ 1 α 1 U ϕ 2 )
) if all its outgoing sequences satisfy the corresponding path formula. An encoding of ACTL\X in L µ is formally defined in [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF].

The following abbreviations are often used:

EF α (ϕ 0 ) = E(true true U α ϕ 0 ) AG α (ϕ 0 ) = ¬EF ¬α (true) ∧ ¬E(true true U ¬ϕ 0 )
A state satisfies EF α (ϕ 0 ) if it has an outgoing sequence leading to a transition whose action satisfies α and target state satisfies ϕ 0 . A state satisfies AG α (ϕ 0 ) if none of its outgoing sequences leads to a transition labelled by an action not satisfying α or to a state not satisfying ϕ 0 .

Computation Tree Logic The logic CTL [START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF] contains the following operators:

E(ϕ 1 U ϕ 2 ), A(ϕ 1 U ϕ 2 ), E(ϕ 1 W ϕ 2 ), A(ϕ 1 W ϕ 2 ), EF(ϕ 0 ), AG(ϕ 0 ), AF(ϕ 0 ), EG(ϕ 0 ) A state satisfies E(ϕ 1 U ϕ 2 ) (resp. A(ϕ 1 U ϕ 2 )
) if some of (resp. all) its outgoing sequences lead to states satisfying ϕ 2 after passing only through states satisfying

ϕ 1 . It satisfies E(ϕ 1 W ϕ 2 ) (resp. A(ϕ 1 W ϕ 2 )
) if some of (resp. all) its outgoing sequences either contain only states satisfying ϕ 1 , or lead to states satisfying ϕ 2 after passing only through states satisfying ϕ 1 . A state satisfies EF(ϕ 0 ) (resp. AF(ϕ 0 )) if some of (resp. all) its outgoing sequences lead to states satisfying ϕ 0 . A state satisfies EG(ϕ 0 ) (resp. AG(ϕ 0 )) if some of (resp. all) its outgoing sequences contain only states satisfying ϕ 0 . The above CTL operators can be encoded in ACTL\X (hence in L µ ) using the following equations: of L µ is defined as the set of formulas that are semantically equivalent to some formula of the following language (whose modalities are a subset of PDL-Δ regular modalities):

E(ϕ 1 U ϕ 2 ) = E(ϕ 1 true U ϕ 2 ) (Ctl1) A(ϕ 1 U ϕ 2 ) = A(ϕ 1 true U ϕ 2 ) (Ctl2) EF(ϕ 0 ) = E(true true U ϕ 0 ) (Ctl3) AG(ϕ 0 ) = ¬E(true true U ¬ϕ 0 ) (Ctl4) AF(ϕ 0 ) = A(true true U ϕ 0 ) (Ctl5) EG(ϕ 0 ) = ¬A(true true U ¬ϕ 0 ) (Ctl6) E(ϕ 1 W ϕ 2 ) = E(ϕ 1 U ϕ 2 ) ∨ EG(ϕ 1 ) (Ctl7) A(ϕ 1 W ϕ 2 ) = ¬E(¬ϕ 2 U ¬ϕ 1 ∧ ¬ϕ 2 ) (Ctl8)
ϕ ::= false | ϕ 1 ∨ ϕ 2 | ¬ϕ 0 | X | µX.ϕ 0 | �(ϕ 1 ?.α τ ) * � ϕ 2 | �(ϕ 1 ?.α τ ) * .ϕ 1 ?.α a � ϕ 2 | �ϕ 1 ?.α τ � @
The ultra-weak modality �(ϕ 1 ?.α τ ) * � ϕ 2 , weak modality �(ϕ 1 ?.α τ ) * .ϕ 1 ?.α a � ϕ 2 , and weak infinite looping modality �ϕ 1 ?.α τ � @ are shorthand notations defined upon L µ as follows:

�(ϕ 1 ?.α τ ) * � ϕ 2 = µX.ϕ 2 ∨ (ϕ 1 ∧ �α τ � X) �(ϕ 1 ?.α τ ) * .ϕ 1 ?.α a � ϕ 2 = µX.ϕ 1 ∧ (�α a � ϕ 2 ∨ �α τ � X) �ϕ 1 ?.α τ � @ = νX.ϕ 1 ∧ �α τ � X
Derived operators are also defined in terms of L dbr µ as follows:

[(ϕ 1 ?.α τ ) * ] ϕ 2 = ¬�(ϕ 1 ?.α τ ) * � ¬ϕ 2 [ϕ 1 ?.α τ ] � = ¬�ϕ 1 ?.α τ � @ [(ϕ 1 ?.α τ ) * .ϕ 1 ?.α a ] ϕ 2 = ¬�(ϕ 1 ?.α τ ) * .ϕ 1 ?.α a � ¬ϕ 2
Depending on the L µ fragment ϕ belongs to, it is thus possible to determine whether the system can or cannot be reduced for divbranching bisimulation 4 . We refine this result in the next section, where we show that even if ϕ does not belong to L dbr µ , some part of the system might still be minimized for divbranching bisimulation.

Combining Bisimulations Compositionally

The above approach is a mono-bisimulation approach: either the formula is in L dbr µ and then the system is entirely reduced for divbranching bisimulation, or it is not and then the system is entirely reduced for strong bisimulation: the presence in the formula of a single operator that is not encodable in L dbr µ wipes the possibility to use divbranching bisimulation reduction out. In this section, we refine this approach by showing that, even if the formula is not in L dbr µ , it may still be possible to reduce some processes among the parallel processes P 1 , . . . , P n for divbranching instead of strong bisimulation. This approach relies on the fact that, in general, an arbitrary temporal logic formula ϕ may be rewritten in a form that contains both weak modalities, as those present in L dbr µ , and non-weak modalities of L µ (called strong modalities in this context).

To do so, we characterize a family of fragments of L µ , each of which is written L strong Example 2 The PDL formula ϕ = [true * .a 1 .a 2 ] false expresses that the system does not contain two successive transitions labelled by a 1 and a 2 respectively. It is in the fragment L strong µ ({a 2 }) as it is equivalent to [(true?.true) * .true?.a 1 ] [a 2 ] false, but it does not belong to L dbr µ . Indeed, consider the LTS P , P � , Q, and Q � depicted in Figure 1, where P � (resp. Q � ) denotes the minimal LTS equivalent to P (resp. Q) for divbranching bisimulation. The LTS

P |[a 1 ]| Q satisfies ϕ because a 1 is necessarily followed by a τ transition, but P � |[a 1 ]| Q � (which is isomorphic to Q � ) does not.
However, although the system cannot be fully reduced for divbranching, we will see in the sequel that it can be partly reduced, i.e., that P � |[a 1 ]| Q preserves ϕ as well as any other property belonging to some fragment L strong µ (A s ), provided A s does not contain any of the actions occurring in P , namely a 1 and τ . Actions that are not strong are called weak. Intuitively, weak actions are those actions that can always be delayed, i.e., the mere absence or presence of a weak action in a given state cannot validate (resp. invalidate) the property immediately, because there is still a chance that this action occurs (or stops to occur) in a subsequent state, such that it invalidates (resp. validates) the property. A strong action is thus an action that may potentially not be delayed, i.e., may have to occur immediately.

P = p 0 a 1 � � p 1 τ � � Q = q 0 a 1 � � q 1 τ � � q 2 a 2 � � P � = p � 0 a 1 � � Q � = q � 0 a 1 � � q � 1 a 2 � � P |[a 1 ]| Q = (p 0 , q 0 ) a 1 � � (p 1 , q 1 ) τ � � τ � � (p 1 , q 2 ) a 2 � � τ � � (p 1 , q 0 ) τ � � (p 0 , q 1 ) τ � � (p 0 , q 2 ) a 2 � �
Theorem 1 indicates that it is always possible to consider as strong (i.e., immediate) some actions that could be considered as weak (i.e., delayable), whereas the converse is obviously wrong. We will see in the next section that having the most accurate knowledge as possible of which actions are strong and which are weak (i.e., not considering as strong an action that can actually be considered as weak) may help fighting against state explosion more effectively.

Applying divbranching bisimulation to selected components

Theorem 2 below states the main result of this paper, namely that every component process containing only weak actions can be replaced by any divbranching equivalent process, without affecting the truth value of the formula. 5 To show Theorem 2, we first need Lemma 1, which simply lifts a standard property of branching and divbranching bisimulations up to the level of product states.

Lemma 1 Let p 0 , p 1 be states of an LTS P , and q 0 , q � 0 , q 1 be states of an LTS Q, and

consider the composition expression P |[A sync ]| Q. If (p 0 , q 0 ) a -→ (p 1 , q 1
) and q � 0 ∼ dbr q 0 , then there exists a state q � 1 in Q such that q � 1 ∼ dbr q 1 and either:

5 Theorem 2 generalizes easily to more general compositions P || Q (with admissible action mappings) if Q does not contain any action that maps onto a strong action.

-a = τ , p 0 = p 1 , q 0 ∼ dbr q 1 , and

q � 1 = q � 0 , or -there exist q �� 0 , ..., q �� n (n ≥ 0) such that q �� 0 = q � 0 , for all i ∈ 0..n -1, q �� i+1 ∼ dbr q � 0 , (p 0 , q �� i ) τ -→ (p 0 , q �� i+1 ), and (p 0 , q �� n ) a -→ (p 1 , q � 1 )
.

Graphically, this means that one of the diagrams below holds, where solid lines denote universal quantification whereas dotted lines denote existential quantification:

(p 0 , q 0 ) a=τ � � ∼ dbr (p 1 , q 1 ) = ∼ dbr (p 0 , q 1 ) (p 0 , q � 0 ) = (p 1 , q � 1 )
-or -

(p 0 , q 0 ) a � � ∼ dbr (p 1 , q 1 ) ∼ dbr (p 0 , q � 0 ) = (p 0 , q �� 0 ) τ � � ∼ dbr (p 0 , q �� 1 ) τ � � ...∼ dbr ... . . . τ � � (p 0 , q �� n ) a � � (p 1 , q � 1 )
Proof From the definition of P |[A sync ]| Q and the fact that (p 0 , q 0 ) a -→ (p 1 , q 1 ), there are three possible cases:

1. a ∈ A sync , p 0 a -→ P p 1 , and q 0 a -→ Q q 1 , or 2. a / ∈ A sync , p 0 a -→ P p 1 , and q 1 = q 0 , or 3. a / ∈ A sync , p 1 = p 0 , and

q 0 a -→ Q q 1
Instead of considering those three cases, we merge cases 1 and 3 (where q 0 a -→ Q q 1 , whatever p 0 does), which have a similar proof, into a single case. Thus we consider the following two cases, the first one corresponding to case 2 of the above enumeration, and the second one corresponding to cases 1 and 3:

-q 1 = q 0 , a / ∈ A sync , and p 0 a -→ P p 1 . Take q � 1 = q � 0 . We have q � 1 ∼ dbr q 1 because q � 1 = q � 0 , q � 0 ∼ dbr q 0 , and

q 0 = q 1 . The second item of the lemma (bottom diagram) is verified with n = 0, q �� 0 = q �� n = q � 0 , and (p 0 , q �� 0 ) = (p 0 , q �� n ) = (p 0 , q � 0 ) a -→ (p 1 , q � 0 ) = (p 1 , q � 1 )
.

-q 0 a -→ Q q 1 (and either a / ∈ A sync and p 1 = p 0 , or a ∈ A sync and p 0 a -→ P p 1 ). Then since q � 0 ∼ dbr q 0 , we have by definition of ∼ dbr : -Either a = τ and q 0 ∼ dbr q 1 . Since τ / ∈ A sync , we have p 0 = p 1 . Then, we can take q � 1 = q � 0 . Indeed, q � 1 ∼ dbr q 1 because q � 1 = q � 0 , q � 0 ∼ dbr q 0 , and q 0 ∼ dbr q 1 . The first item of the lemma (top diagram) is verified.

-Or there exist q �� 0 , ..., q �� n (n ≥ 0) such that q �� 0 = q � 0 , for all i ∈ 0..n -1, q �� i+1 ∼ dbr q � 0 (by the well-known stuttering lemma of divbranching bisimilarity, see [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF]),

q �� i τ -→ Q q �� i+1 , and q �� n a -→ Q q � 1 .
In this case, we also have

(p 0 , q �� i ) τ -→ (p 0 , q �� i+1 ) and (p 0 , q �� n ) a -→ (p 1 , q � 1 ), i.e., the second item of the lemma (bottom diagram) is verified. � �
We draw the reader's attention to the fact that the top diagram of Lemma 1 concerns only the case (p 0 , q 0 ) τ -→ (p 0 , q 1 ) deriving from a transition q 0 τ -→ Q q 1 where q 0 ∼ dbr q 1 . The bottom diagram concerns all other cases, including (p 0 , q 0 ) τ -→ (p 1 , q 0 ) deriving from p 0 τ -→ p 1 where p 0 ∼ dbr p 1 .

Theorem 2 Consider the finite LTS P = (Σ P , A P ,

-→ P , p init ), Q = (Σ Q , A Q , -→ Q , q init ), and Q � = (Σ Q � , A Q , -→ Q � , q � init ). Let A sync ⊆ A and ϕ ∈ L strong µ (A s ). If A Q ∩ A s = ∅ and Q ∼ dbr Q � , then P |[A sync ]| Q |= ϕ if and only if P |[A sync ]| Q � |= ϕ.
Proof We prove that, given p ∈ Σ P , q ∈ Σ Q , and q � ∈ Σ Q � such that q ∼ dbr q � , (p, q) satisfies ϕ if and only if (p, q � ) satisfies ϕ. We show this claim by structural induction on the formula ϕ. Since we work on finite LTS, every formula containing a fixed point operator µ can be expanded into an equivalent formula by unfolding the fixed point a bounded number of times 6 . This way, we do not have to consider fixed points and propositional variables in this proof, and contexts δ mapping propositional variables to sets of states are always empty in the semantics of formulas. For conciseness, we write

[[ϕ]] instead of [[ϕ]] P |[A sync ]| Q [ ] and [[ϕ]] P |[A sync ]| Q � [ ], respectively, as the LTS "P |[A sync ]| Q" or "P |[A sync ]| Q � "
to which the semantics apply is clear from the context. Note that since the claim is symmetric, it is sufficient to prove one implication only. We thus assume that (p, q) ∈ [[ϕ]] and prove that (p,

q � ) ∈ [[ϕ]]. -Case ϕ = false. It is obvious that both (p, q) / ∈ [[ϕ]] and (p, q � ) / ∈ [[ϕ]]. -Case ϕ = ϕ 1 ∨ ϕ 2 . By definition, either (p, q) ∈ [[ϕ 1 ]] or (p, q) ∈ [[ϕ 2 ]]. If (p, q) ∈ [[ϕ 1 ]] (resp. [[ϕ 2 ]]) then (p, q � ) ∈ [[ϕ 1 ]] (resp. [[ϕ 2 ]]) by the induction hypothesis. Therefore, (p, q � ) ∈ [[ϕ 1 ∨ ϕ 2 ]]. -Case ϕ = ¬ϕ 0 . By definition, (p, q) / ∈ [[ϕ 0 ]]. By the induction hypothesis, (p, q � ) / ∈ [[ϕ 0 ]] and thus (p, q � ) ∈ [[¬ϕ 0 ]]. -Case ϕ = �α s � ϕ 0 . By definition, there exists a ∈ [[α s ]] A such that (p, q) a -→ (p 1 , q 1 ) and (p 1 , q 1 ) ∈ [[ϕ 0 ]]. Let action a be such. Since [[α s ]] A ⊆ A s , A Q ∩ A s = ∅, and a ∈ [[α s ]] A , we have a / ∈ A Q (hence, a /
∈ A sync ). Therefore, q = q 1 , p a -→ P p 1 , and (p, q � ) a -→ (p 1 , q � ). Since q � ∼ dbr q and (p 1 , q) ∈ [[ϕ 0 ]], we have by the induction hypothesis (p

1 , q � ) ∈ [[ϕ 0 ]]. As a consequence, (p, q � ) ∈ [[�α s � ϕ 0 ]]. -Case ϕ = �(ϕ 1 ?.α τ ) * � ϕ 2 . By definition, there exist m ≥ 0, p i ∈ Σ P , q i ∈ Σ Q ,
and

a i ∈ [[α τ ]] A (i ∈ 0..m), such that (p, q) = (p 0 , q 0 ), (p m , q m ) ∈ [[ϕ 2 ]]
, and for all 0

≤ i < m, (p i , q i ) a i -→ (p i+1 , q i+1 ) and (p i , q i ) ∈ [[ϕ 1 ]].
We show that the same holds from state (p, q � ), i.e., there exists a sequence of transitions matching α τ and passing through states satisfying ϕ 1 , until reaching a state satisfying ϕ 2 . By the induction hypothesis, (p,

q � ) = (p 0 , q � 0 ) ∈ [[ϕ 1 ]]. Consider one transition (p i , q i ) a i -→ (p i+1 , q i+1 ). We know that (p i , q i ) ∈ [[ϕ 1 ]].
Assume that there exists q � i ∼ dbr q i . Substituting a i for a, (p i , q i ) for (p 0 , q 0 ), and (p i+1 , q i+1 ) for (p 1 , q 1 ) in the two diagrams of Lemma 1, it appears clearly that there exists a state q � i+1 such that q � i+1 ∼ dbr q i+1 . Moreover, by the induction hypothesis, every state divbranching equivalent to (p i , q i ) in the bottom sequence of the diagrams is in

[[ϕ 1 ]]. Finally, note that τ ∈ [[α τ ]
] by definition, so that each of the τ -transitions in the bottom sequence of the second diagram thus matches α τ . Moreover, (p m , q m ) ∈ [[ϕ 2 ]] and q � m ∼ dbr q m , so by the induction hypothesis, we have also

(p m , q � m ) ∈ [[ϕ 2 ]].
-Case ϕ = �(ϕ 1 ?.α τ ) * .ϕ 1 ?.α a � ϕ 2 . Since �(ϕ 1 ?.α τ ) * .ϕ 1 ?.α a � ϕ 2 is equivalent to �(ϕ 1 ?.α τ ) * � �(ϕ 1 ?.τ ) * .ϕ 1 ?.α a � ϕ 2 and since we have already considered the case ϕ = �(ϕ 1 ?.α τ ) * � ϕ 2 above, we only have to consider ϕ = �(ϕ 1 ?.τ ) * .ϕ 1 ?.α a � ϕ 2 , i.e., α τ = τ . By definition, there exist m ≥ 0,

p i ∈ Σ P , q i ∈ Σ Q (i ∈ 0..m + 1) and a ∈ [[α a ]] A , such that (p, q) = (p 0 , q 0 ), (p m , q m ) a -→ (p m+1 , q m+1 ), (p m+1 , q m+1 ) ∈ [[ϕ 2 ]]
, and for all 0 ≤ i < m, (p i , q i ) τ -→ (p i+1 , q i+1 ) and

(p i , q i ) ∈ [[ϕ 1 ]].
The reasoning is similar to the previous case. It is important to note that the transition (p m , q m ) a -→ (p m+1 , q m+1 ) necessarily has a counterpart in the built sequence, since

a ∈ [[α a ]] A and τ / ∈ [[α a ]]
. Therefore this transition cannot be an inert transition and the first case of Lemma 1 does not apply here.

-Case ϕ = �ϕ 1 ?.α τ � @. By definition, there exists an infinite sequence of states (p 0 , q 0 )

a 0 -→ (p 1 , q 1 ) a 1 -→ . . . (p i , q i ) a i -→ .
. ., such that p 0 = p, q 0 = q, and for all i > 0, (

p i , q i ) ∈ [[ϕ 1 ]] and a i ∈ [[α τ ]].
The reasoning is similar to the previous case. It is important to note that an infinite sequence of τ -transitions (when a i = τ for all i > 0) cannot collapse into an empty sequence, as guaranteed by divbranching bisimulation. � � Note that τ may belong to A s . For instance, the formula [true * .a] �τ � true (which expresses that the target state of every transition labelled by a is also the source state of a transition labelled by τ ) belongs to L strong µ ({τ }). If τ ∈ A s , following Theorem 2, every P i not containing τ can be reduced for divbranching bisimulation, but in the case of a process not containing τ , divbranching bisimulation coincides with strong bisimulation. On the other hand, processes containing the strong action τ cannot be reduced for divbranching bisimulation. In the end, all τ -transitions of the system are preserved, as expected for the truth value of formulas containing strong modalities matching τ to be preserved. Example 3 In Example 2, P does not contain a 2 , the only strong action of the system. Thus, ϕ can be checked on

P � |[a 1 ]| Q (which is isomorphic to Q and has only 3 states) instead of P |[a 1 ]| Q (6
states), while preserving its truth value. In the general case, identifying a minimal set of strong actions is not easy, if at all feasible. One cannot reasonably assume that formulas are written in the obscure

L strong µ (A s ) syntax (see Ex.
2) and that the strong modalities cannot be turned to weak ones. Instead, users shall continue to use "syntactic sugar" extensions of L µ , with operators of e.g., CTL, ACTL, PDL, or PDL-Δ. In Lemmas 2 to 4 below we provide patterns that can be used to prove that a formula written using one of those operators belongs to a particular instance of

L strong µ (A s ). Lemma 2 (Modal µ-calculus) Assume ϕ i ∈ L strong µ (A s ) (i = 0, 1, 2) and [[α s ]] A ⊆ A s .
Then the following hold:

1. �α s � ϕ 0 ∈ L strong µ (A s ) 2. [α s ] ϕ 0 ∈ L strong µ (A s ) since τ / ∈ [[α 2 ]] A , we have [[α 2 ]] A = [[α 2 ]] A \ {τ } = [[α 2 ∧ ¬τ ]]
A and thus �α 2 � ϕ = �α 2 ∧ ¬τ � ϕ for any formula ϕ. We then have the following:

E(ϕ 1 α 1 U ϕ 1 ∧ �α 2 � ϕ 2 ) = µX.(ϕ 1 ∧ �α 2 � ϕ 2 ) ∨ (ϕ 1 ∧ �α 1 ∨ τ � X) by definition of E( U ) = µX.ϕ 1 ∧ (�α 2 � ϕ 2 ∨ �α 1 ∨ τ � X) by factorization of ϕ 1 = µX.ϕ 1 ∧ (�α 2 ∧ ¬τ � ϕ 2 ∨ �α 1 ∨ τ � X) from �α 2 � ϕ 2 = �α 2 ∧ ¬τ � ϕ 2 = E(ϕ 1 α 1 U α 2 ϕ 2 )
by definition of E( U )

In addition to the equations (Ctl1) to (Ctl8) defined in Section 2.2, we will use the following identity, which is easily proven by showing that the modal µ-calculus definitions of the left-hand-side and right-hand-side formulas are equivalent:

A(ϕ 1 U ϕ 2 ) = ¬E(¬ϕ 2 W ¬ϕ 1 ∧ ¬ϕ 2 ) (Ctl9)
We also use the following standard identity of the modal µ-calculus:

¬[α] ϕ 0 = �α� ¬ϕ 0 (Mcl1)

Identifying strong actions in PDL modalities

PDL modalities are a useful means to describe transition sequences in an LTS. We consider here a fragment of PDL named test-free PDL [26, Chap. 10], consisting of modalities on regular action sequences (without the testing operator ϕ?) and standard Boolean connectors ∧, ∨, ¬, etc., which can be encoded in the full syntax of PDL defined in [START_REF] Michael | Propositional dynamic logic of regular programs[END_REF]. Using this fragment of PDL, one can describe sequences of transitions only in terms of their actions, and not of their intermediate states; however, this is often sufficient in the action-based setting for the usual classes of properties: safety (e.g., absence of undesirable sequences), liveness (e.g., presence of desirable sequences), and fairness (e.g., absence of unfair infinite sequences). We propose in this section a method for identifying a reduced set of strong actions present in test-free PDL modalities. In Section 4.3.1, we show how to translate these modalities into an equivalent equational representation, which is more convenient for reasoning about strong actions. Then, in Section 4.3.2, we provide the lemmas for identifying the strong actions in a test-free PDL modality via its corresponding equational representation. Finally, in Section 4.3.3, we give a procedure to obtain a reduced (although not necessarily minimal) set of strong actions for a test-free PDL modality.

Translating PDL modalities to HMLR

In general, every test-free PDL modality �β� ϕ 0 can be rewritten in several ways (by replacing the regular formula β with another, equivalent one). Each of these variants may have a different set of strong actions, which can be identified by translating the modality into an L µ formula using the encoding given in [START_REF] Emerson | Efficient model checking in fragments of the propositional mu-calculus[END_REF]. For example, the modality �b| (¬a.(¬a) * .b)� ϕ 0 is translated into �b� ϕ 0 ∨�¬a� µX.(�b� ϕ 0 ∨�¬a� X), which belongs to

L strong µ ([[¬a]] ∪ {b}) = L strong µ (A \ {a})
according to Definition 11. However, if the modality was written in the equivalent form �(¬a) * .b� ϕ 0 , it would belong to L strong µ (∅), since it is a weak modality of L dbr µ . Searching for an equivalent regular formula with a minimal set of strong actions is more convenient by representing regular formulas as finite automata, which have a canonical form (minimal deterministic automata). In the sequel, we use a modal logic counterpart of finite automata, namely HMLR (Hennessy-Milner Logic with Recursion) [START_REF] Larsen | Proof systems for hennessy-milner logic with recursion[END_REF] specifications, which are equational variants of fixed point L µ formulas. For our purpose, we need only a simple kind of HMLR specifications.

Definition 12 (HMLR specification) A HMLR specification D is a set of minimal fixed point equations of the following form:

D = � X i = � n i j=1 �α ij � X ij ∨ ϕ i � 1≤i≤n
where X 1 , ..., X n are propositional variables, α ij are action formulas, and ϕ i is an arbitrary state formula with free variables among X 1 , . . . , X n . The semantics of D w.r.t. an LTS P = (Σ, A, -→, p init ) is defined as the solution of variable X 1 in the minimal fixed point equation system, i.e., [[D]] P = (µΦ P ) 1 , where (.) 1 denotes the projection of an n-ary tuple on its first component, and the functional

Φ P : (2 Σ ) n → (2 Σ
) n is defined as follows:

Φ P (U 1 , ..., U n ) = ([[ � n i j=1 �α ij � X ij ∨ ϕ i ]] P [U 1 /X 1 , ..., U n /X n ]) 1≤i≤n
where (W i ) 1≤i≤n denotes the tuple (W 1 , ..., W n ). D is called guarded if all the state formulas ϕ i (for

1 ≤ i ≤ n) are closed.
Intuitively, a PDL modality �β� ϕ 0 expresses the existence of a transition sequence matching a regular formula β, and its corresponding HMLR specification provides an equivalent equational counterpart similar to Brzozowski's derivatives for regular expressions [START_REF] Janusz | Derivatives of regular expressions[END_REF]. The translation from PDL to guarded HMLR [START_REF] Mateescu | On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators[END_REF] uses an intermediate form called PDLR (similar to HMLR, but having regular formulas instead of action formulas in modalities), and works by eliminating the regular operators contained in β using classical PDL identities [START_REF] Michael | Propositional dynamic logic of regular programs[END_REF].

The HMLR specifications of Definition 12 (and also the formalization in the remainder of this subsection) are suited for possibility modalities �β� ϕ 0 . Necessity modalities [β] ϕ 0 can be handled either by a dual formalization (replacing disjunctions by conjunctions and minimal fixed points by maximal ones), or simply by observing that negations on state formulas do not change the nature of strong actions in formulas, and therefore [β] ϕ 0 = ¬�β� ¬ϕ 0 has the same set of strong actions as �β� ϕ 0 . To translate ψ to HMLR, we convert it into an equivalent PDLR specification (left), that we refine by eliminating the . and the | operators (right):

   X 1 = �true * .snd.(rec|¬rec.rec| ¬rec.(¬rec) * .¬rec.rec).ack� X 2 X 2 = ϕ 0                                     X 1 = �true * � X 3 X 2 = ϕ 0 X 3 = �snd� X 4 X 4 = �rec� X 5 ∨ �¬rec� X 6 ∨ �¬rec� X 7 X 5 = �ack� X 2 X 6 = �rec� X 5 X 7 = �(¬rec) * � X 8 X 8 = �¬rec� X 9 X 9 = �rec� X 5                                 
Then, we eliminate the * operators (left) and the unguarded occurrences of variables X 3 and X 8 in the equations defining X 1 and X 7 (right):

                                 X 1 = X 3 ∨ �true� X 1 X 2 = ϕ 0 X 3 = �snd� X 4 X 4 = �rec� X 5 ∨ �¬rec� X 6 ∨ �¬rec� X 7 X 5 = �ack� X 2 X 6 = �rec� X 5 X 7 = X 8 ∨ �¬rec� X 7 X 8 = �¬rec� X 9 X 9 = �rec� X 5                                                                   X 1 = �snd� X 4 ∨ �true� X 1 X 2 = ϕ 0 X 3 = �snd� X 4 X 4 = �rec� X 5 ∨ �¬rec� X 6 ∨ �¬rec� X 7 X 5 = �ack� X 2 X 6 = �rec� X 5 X 7 = �¬rec� X 9 ∨ �¬rec� X 7 X 8 = �¬rec� X 9 X 9 = �rec� X 5                                 
Finally, we eliminate the unreachable equations defining X 3 , X 8 and rename the variables, yielding the guarded HMLR specification below:

D =                    X 1 = �snd� X 2 ∨ �true� X 1 X 2 = �rec� X 3 ∨ �¬rec� X 4 ∨ �¬rec� X 5 X 3 = �ack� X 7 X 4 = �rec� X 3 X 5 = �¬rec� X 6 ∨ �¬rec� X 5 X 6 = �rec� X 3 X 7 = ϕ 0                   
Note that equation defining X 7 is the only one containing a state formula (ϕ 0 ), which specifies the ending states of the regular sequence denoted by ψ.

Any HMLR specification D can be converted into an equivalent L µ formula ϕ(D) using the classical translation [START_REF] Cleaveland | Faster model checking for the modal mu-calculus[END_REF], recalled below.

Definition 13 (L µ formula ϕ(D) [START_REF] Cleaveland | Faster model checking for the modal mu-calculus[END_REF]) Let D = {X i = rhs(X i )} 1≤i≤n be a HMLR specification, where we note rhs(X i ) =

� n i j=1 �α ij � X ij ∨ϕ i the formulas in the righthand sides of equations. We also note D 1,i the fragment of D consisting of its first i equations. The L µ formula ϕ(D) = ϕ(D 1,n ) associated to D is defined as follows:

ϕ(D 1,n ) = ϕ(D 1,n-1 [µX n .rhs(X n )/X n ]) ϕ(D 1,1 ) = µX 1 .rhs(X 1 )
where D 1,n-1 [µX n .rhs(X n )/X n ] denotes the syntactic substitution of X n by the formula µX n .rhs(X n ) in all equations of D 1,n-1 .

It was shown in [START_REF] Cleaveland | Faster model checking for the modal mu-calculus[END_REF] that [[ϕ(D)]] P = [[D]] P for any LTS P . Note that the translation in Definition 13 can be also applied to PDLR specifications.

Example 6 Consider the following HMLR specification D 1,3 obtained by translating the PDL modality �true * .snd.(¬rec) * .rec� ϕ 0 :

D 1,3 =    X 1 = �snd� X 2 ∨ �true� X 1 X 2 = �rec� X 3 ∨ �¬rec� X 2 X 3 = ϕ 0   
We can retrieve its equivalent L µ formula ϕ(D 1,3 ) by applying Definition 13 (we simplify µX 3 .ϕ 0 into ϕ 0 because X 3 does not occur free in ϕ 0 ):

ϕ(D 1,3 ) = ϕ(D 1,2 [µX 3 .ϕ 0 /X 3 ]) = ϕ(D 1,1 [ϕ 0 /X 3 ][µX 2 .(�rec� ϕ 0 ∨ �¬rec� X 2 )/X 2 ]) = ϕ({X 1 = �snd� µX 2 .(�rec� ϕ 0 ∨ �¬rec� X 2 ) ∨ �true� X 1 }) = µX 1 .(�snd� µX 2 .(�rec� ϕ 0 ∨ �¬rec� X 2 ) ∨ �true� X 1 )
The formula ϕ(D 1,3 ) contains two minimal fixed points X 1 and X 2 , corresponding to the two * -operators in the initial PDL modality.

Identifying strong actions in HMLR

Given a guarded HMLR specification, we can identify its set of strong actions by inspecting its equations as follows.

Definition 14 (Strong actions for HMLR) Let P = (Σ, A, -→, p init ) be an LTS and D = �

X i = � n i j=1 �α ij � X ij ∨ ϕ i � 1≤i≤n
be a guarded HMLR specification. The set of strong actions associated to D is defined as follows:

A str (D) = n � i=1 n i � j=1    [[α ij ]] A (τ ∈ [[α ij ]] A ∧ X ij � = X i ) ∨ (τ � ∈ [[α ij ]] A ∧ ∀1 ≤ k ≤ n i .(τ � ∈ [[α ik ]] A ∨ X ik � = X i ))    .
Intuitively, the strong actions A str (D) are obtained by collecting, for each equation X i of D, the actions matched by the strong modalities �α ij � X ij present in the equation. Two cases are possible: (i) either α ij captures τ without being a self-loop on variable X i , or (ii) α ij captures only visible actions, and there is no other action formula α ik in the equation capturing τ and being a self-loop on variable X i .

Note that Definition 14 identifies strong actions by inspecting individual equations only, and does not consider the cycles of τ -transitions induced by �τ � X ij modalities occurring in mutual recursive equations. Therefore, several semantically equivalent, but syntactically different HMLR specifications may have different sets of strong actions according to Definition 14. To overcome this issue, one can reason in terms of the canonical representation of a HMLR specification (determinized and minimized), as it is discussed in Section 4.3.3.

Lemma 6 (Test-free PDL modalities) Let �β� ϕ 0 be a test-free PDL modality, D its corresponding guarded HMLR specification, and assume that ϕ 0 ∈ L strong µ (A s ). The following holds:

�β� ϕ 0 ∈ L strong µ (A s ∪ A str (D)). Proof Let D = � X i = � n i j=1 �α ij � X ij ∨ ϕ i � 1≤i≤n
be the guarded HMLR specification obtained by translating �β� ϕ 0 . We prove the statement by constructing a formula of L strong µ (A s ∪A str (D)) equivalent to D. To do so, we first transform D into D � containing only strong modalities on action formulas α such that [[α]] A ⊆ A str (D), and then we show that ϕ

(D � ) ∈ L strong µ (A s ∪ A str (D)). Consider an equation X i = � n i j=1 �α ij � X ij ∨ ϕ i for some 1 ≤ i ≤ n.
We can rewrite its right-hand side as follows:

X i = � j∈J �α ij � X i ∨ � k∈K �α τ ik � X ik ∨ � l∈L �α ail � X il ∨ ϕ i
where the index sets J, K, L form a partition of {1, ...,

n i }, τ ∈ [[α τ ik ]] A and X ik � = X i for all k ∈ K, τ � ∈ [[α ail ]]
A and X il � = X i for all l ∈ L. The three disjuncts indexed by j, k, l represent the "self-loops" leading to X i , the "potentially invisible successors" of X i , and the "visible successors" of X i , respectively. Two cases are possible. (i) There exists a potentially invisible self-loop, i.e., τ ∈ [[α ij ]] A for some j ∈ J.

Using the HML identity �α 1 � ϕ ∨ �α 2 � ϕ = �α 1 ∨ α 2 � ϕ, the equation becomes:

X i = � � j∈J α ij � X i ∨ � k∈K �α τ ik � X ik ∨ � l∈L �α ail � X il ∨ ϕ i
Finally, using the PDL identities �α * � ϕ = ϕ ∨ �α� �α * � ϕ, �α 1 � �α 2 � ϕ = �α 1 .α 2 � ϕ and the distributivity of ∨ over � � , the equation reaches the form:

X i = � k∈K ultra weak � �� � � � � j∈J α ij � * � strong � �� � � α τ ik � X ik ∨ � l∈L weak � �� � � � � j∈J α ij � * .α ail � X il ∨ ultra weak � �� � � � � j∈J α ij � * � ϕ i
This last PDLR specification has the strong actions {ack} (induced by the strong modality in the equation defining X 3 ), and this is the set of strong actions in the initial PDL modality ψ of Example 5.

Determinization can simplify the HMLR specifications considerably and uncover that some action formulas initially appearing as strong (like the actions rec and ¬rec in the HMLR specification of Example 7) are in fact weak. Reasoning on the determinized version det(D) instead of D allows to spot all the potentially invisible self-loops: if such a loop exists somewhere in D, then it must also exist in det(D), since both specifications denote the same regular language.

However, syntactic determinization alone followed by the application of Lemma 6 may artificially increase the set of strong actions, as shown by the example below.

Example 9 Consider the PDL modality �nil|¬a.(¬a) * |a� ϕ 0 , where nil = false * denotes the empty sequence. Its deterministic HMLR specification is:

D =    X 1 = �¬a� X 2 ∨ �a� X 3 ∨ ϕ 0 X 2 = �¬a� X 2 ∨ ϕ 0 X 3 = ϕ 0   
Lemma 6 identifies ¬a as weak (because of the self-loop in the equation defining X 2 ), but also as strong (because of the equation defining X 1 ). Since a is also strong (because of the �a� X 3 modality), this yields

A str (D) = [[¬a]] A ∪ [[a]] A = A.
But D can be simplified by observing that rhs(X 2 ) is included in rhs(X 1 ), and therefore rhs(X 2 ) can be replaced by X 2 in rhs(X 1 ). This produces an unguarded HMLR specification (left), subsequently transformed in PDLR (right):

   X 1 = X 2 ∨ �a� X 3 X 2 = �¬a� X 2 ∨ ϕ 0 X 3 = ϕ 0       X 1 = X 2 ∨ �a� X 3 X 2 = �(¬a) * � ϕ 0 X 3 = ϕ 0   
Using Definition 13, we translate this last PDLR specification into the L µ formula �(¬a) * � ϕ 0 ∨ �a� ϕ 0 , in which the only strong action is a.

To preserve as much as possible the weak modalities identified in an equation X i = rhs(X i ), one must replace all occurrences of rhs(X i ) by X i in all the other rhs(X j ); otherwise, as shown in Example 9, the modalities contained in rhs(X i ) may be considered as strong in another equation X j = rhs(X j ) which includes rhs(X i ). For a minimal deterministic HMLR specification D, the inclusion relation between right-hand sides of equations is acyclic (two equations X i = rhs(X i ) and X j = rhs(X j ) with mutual inclusion between rhs(X i ) and rhs(X j ) would imply X i = X j , and therefore D would not be minimal). Thus, one can carry out the substitutions following an inverse topological order of the inclusion relation, leading to a (unique) unguarded PDLR specification in which all weak modalities identified were kept as much as possible.

This syntactic procedure considers action formulas as literals, and is therefore less precise than a semantic one, in which action formulas denote subsets of actions in A. We leave the investigation of a semantic procedure for future work.

Minimal sets of strong actions

In this section, we present two results about minimal sets of strong actions. First, we show that in general, there may be several minimal sets of strong actions associated to an L µ formula. Second, we show that computing a minimal set of strong actions, if feasible, is at least as hard as checking the satisfiability of an L µ formula.

Theorem 3 There is not a unique minimal set A s such that ϕ ∈ L strong µ (A s ).

Proof Following Lemma 4 (item 14), EF(�a 1 � true ∧ �a 2 � true) belongs to both fragments L strong µ ({a 1 }) and L strong µ ({a 2 }) as it is equivalent both to the formula �(true?.true) * � (�(�a 1 � true?.true) * .�a 1 � true?.a 2 � true) and to the symmetric formula �(true?.true) * � (�(�a 2 � true?.true) * .�a 2 � true?.a 1 � true) where a 1 and a 2 are swapped. Yet, from Lemma 5 (page 18), we know that it is not in L strong µ (∅). Thus, {a 1 } and {a 2 } are both minimal sets of strong actions for the formula EF(�a 1 � true∧�a 2 � true).

� �

Theorem 3 illustrates that when the formula checks for the presence or absence of multiple actions in the same state (such as a 1 and a 2 in the formula EF(�a 1 � true∧ �a 2 � true) used to prove Theorem 3), then not all such actions can be considered as weak. This seems to break the intuition that weak actions are those actions that can always be delayed, because one might argue that both a 1 and a 2 can always be delayed in this example. In fact, this is not true, as a 1 cannot be delayed whenever a 2 occurs (and conversely) without having an effect on the truth value of the formula: at least once, a 1 and a 2 have to occur simultaneously. In this case, one can choose whether the delayable action is a 1 or a 2 , the occurrence of the other action then being subject to the occurrence of the first. For instance, if a 1 is chosen as always delayable (i.e., if a 1 is weak), then at least once in a state where a 1 occurs, a 2 has to occur immediately (i.e., a 2 is strong).

Besides the fact that minimal sets of strong actions are generally not unique, computing such sets also requires to address the potential presence of so-called vacuous modalities, where vacuity is defined as follows.

Definition 15 (Vacuous subformula) Let ϕ be an L µ formula and ϕ � be a subformula of ϕ. The subformula ϕ � is vacuous in ϕ if it occurs in a sub-formula of ϕ whose truth value is constant (either false or true on all models).

Example 10 The subformulas �α� X and X are vacuous in µX.�α� X (which is equivalent to false). The subformula ϕ 0 is vacuous in µX.X ∧ ϕ 0 (which is equivalent to false). The subformula �false� ϕ 0 (which is equivalent to false) is vacuous in any formula containing it, and ϕ 0 is vacuous in �false� ϕ 0 . The subformulas false and false ∧ ϕ 1 are vacuous in any formula containing them, and ϕ 1 is vacuous in �α 0 � ϕ 0 ∨ (false ∧ ϕ 1 ).

Detecting vacuity is an interesting issue on its own, as users generally do not intend to write formulas containing vacuous subformulas, except in the form of the constants true and false. We consider here vacuity as a tool to give a lower-bound on the complexity of the quest for minimality. Obviously, the actions matched by a vacuous strong modality do not have to be considered as strong (unless they are matched by another, non-vacuous strong modality), because there exists an equivalent formula (the one with the constant subformula replaced by its truth value), which does not contain this modality. Theorem 4 below shows that computing a minimal set of strong actions is at least as hard as checking L µ -(un)satisfiability, by reasoning on vacuous modalities.

Theorem 4 If there exists a procedure for extracting a minimal set of strong actions from an arbitrary L µ formula, then this algorithm can also be used to determine the (un)satisfiability of any L µ formula ϕ.

Proof Let ϕ be an L µ formula and let a be an action that is not occurring in the action formulas of ϕ. Without loss of generality, we assume that no action formula α occurring in ϕ matches a. Otherwise, we can consider a new formula ϕ � obtained from ϕ by replacing every action formula α by α ∧ ¬a (e.g., replacing true by ¬a), such that ϕ � has the same satisfiability as ϕ. Indeed, α ∧ ¬a and α either match the same finite sets of actions (which do not contain a), or match infinite sets (which differ only by the presence of a). Therefore, there exists a model satisfying ϕ if and only if there exists a model (obtained by renaming the a-transitions), which satisfies ϕ � .

We show that checking the unsatisfiability of ϕ (meaning that ϕ is equivalent to false) can be reduced to computing a minimal set of strong actions for the formula ϕ ∧ �a� true. The formula ϕ is unsatisfiable if and only if this minimal set of strong actions does not contain a. Indeed, since in general the modality �a� true cannot be weak in ϕ ∧ �a� true (clearly, if a does not occur immediately then ϕ ∧ �a� true does not hold), the procedure should return a set containing a unless �a� true is vacuous in ϕ ∧ �a� true. Since the truth value of �a� true itself is not constant, its vacuity can only be due to the fact that ϕ ∧ �a� true is either constantly true or constantly false. It obviously cannot be constantly true, as its value depends on the presence or not of a transition labelled by a. It is constantly false if and only if ϕ and �a� true are contradictory, i.e., ϕ ⇒ ¬�a� true (or, equivalently, �a� true ⇒ ¬ϕ). However, this is possible if and only if ϕ is false (since no action formula of ϕ matches a, it is not possible that ϕ explicitly forbids the existence of a transition labelled by a), i.e., if and only if ϕ is unsatisfiable. � � Corollary 1 Computing a minimal set of strong actions from an arbitrary L µ formula is EXPTIME-hard.

Proof This is a direct consequence of Theorem 4 and the proof in [START_REF] Streett | An automata theoretic decision procedure for the propositional mu-calculus[END_REF] that the theoretical worst-case complexity of L µ -satisfiability is EXPTIME. � � Even though formulas are usually small, the complexity of computing minimal sets of strong actions is rather high. We believe that it is better to invest in algorithms that do not try to compute a minimal set of strong actions, but one that is close enough to minimality and still allows significant state space reductions. For instance, we would be happy with an algorithm whose resulting set of strong actions is minimal under the condition that the formula does not contain any vacuous modality, while not guaranteeing minimality in the presence of vacuity (although this does not hold on the algorithm for PDL presented in Section 4.3). This is an ambitious enough quest, as eliminating (or at least reducing the number of) vacuous modalities can be handled as an orthogonal problem. Building such an algorithm is still far from trivial and left for future work.

Trivial File Transfer Protocol

The TFTP (Trivial File Transfer Protocol ) case-study10 addresses the verification of an avionic communication protocol between a plane and the ground [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF]. It comprises two instances (A and B) of a process named TFTP, connected through a FIFO buffer. Since the state space is very large in the general case, the authors defined five scenarios named A, B, C, D, and E, depending on whether each instance may write and/or read a file. The system corresponding to each scenario is a parallel composition of eight processes. The requirements consist of 29 properties parameterized by the identity of a TFTP instance, defined in MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF] (an implementation of the alternation-free modal µ-calculus including PDL-Δ modalities and macro definitions enabling the construction of libraries of operators), 24 of which belong to L dbr µ . The remaining five, namely properties 08, 09, 14, 16, and 17, contain both weak and strong modalities. The shape of these properties is described in Table 1, where we do not provide the details of the action formulas, but instead denote them by letters a 1 , a 2 , . . ., where τ / ∈ [[a i ]] A for all i. Strong action formulas are highlighted and one shows easily that the other are weak using the patterns of Lemma 7. This identification of strong action formulas was done by hand.

We consider 31 among a potential of 50 verification tasks (five properties, five scenarios, and two instances) as some properties are not relevant to every TFTP instance and scenario (e.g., in a scenario where one TFTP instance only receives messages, checking a property concerning a message emission is irrelevant). All 31 verification tasks return true and the strong actions occur in only three (although not the same three) out of the eight parallel processes.

Figure 2 shows that the refined approach always reduces LTS size (for both intermediate and final LTS), memory and time following similar curves, up to a factor 7 (the vertical axis is on a logarithmic scale). Detailed data is found in Table 2, where parameters P , S, and I correspond respectively to the property number, the scenario, and the TFTP instance. LTS sizes are given in kilostates, memory in megabytes, and time in seconds. Time does not include LTS generation of the component processes from their LNT specification, which takes only a few seconds and is common to both approaches. The column "Ratio Strong/Combined" shows the gain obtained by applying the combined bisimulations approach rather than the mono-bisimulation approach with respect to largest LTS size, memory peak, and time. In these experiments, time is dominated by the last step of generation and minimization, whereas memory usage is dominated by minimization.

Parallel benchmark of the RERS 2018 challenge

The RERS (Rigorous Examination of Reactive Systems) 11 challenge is an international competition on a benchmark of verification tasks. Since 2018 (8th edition), the challenge features a set of parallel problems where systems are synchronizing LTS and properties are expressed using CTL and modalities. This section illustrates the benefits of our approach on these problems.

The benchmark comprises three specifications of concurrent systems, numbered 101, 102, and 103, each accompanied by three properties to be checked, numbered Table 2 Detailed results of the TFTP case-study p#21, p#22, and p#23, where p is the system number. Thus, nine verification tasks have to be solved. The properties are presented in Table 3, where the strong action formulas are highlighted. One easily shows that all other action formulas are weak using Lemma 4. However, for 103#22 and 103#23, the identity (�α� true ⇒

[α] ϕ) = ([α] false ∨ [α] ϕ) = [α] ϕ (because [α] false ⇒ [α] ϕ
for all ϕ) was applied to obtain the simplified formulas occurring after the = sign in the table. For 102#23, this simplification allowed us to prove that A34 is not a strong action, unlike what appears at first sight. This identification of strong actions was done initially by hand. We later implemented a script dedicated to CTL formulas of similar forms, which automatically returns a set of strong actions by identifying the patterns of Lemma 4. This script does not apply simplifications of the formula as the one described above for 103#22 and 103#23. 4 gives, for each of the nine verification tasks, the number #act of actions in the system, the number #hide of actions in the maximal hiding set, the number #sact of strong actions, the number #proc of parallel processes, the number #sproc of processes in the strong group, the number #sync of inter-group actions, and the best reduction relation among strong bisimulation, divbranching bisimulation, or a combination of both. We observe that:

[A11] A([A2] false W �A6� true) ⇒ [A11] A([A5] false W �A6� true)) true 103#22 EG([A14] false ∧ (�A18� true ⇒ [A18] EG([A21] false ∧ EF(�A19� true)))) true = EG([A14] false ∧ [A18] EG([A21] false ∧ EF(�A19� true))) 103#23 AG(�A34� true ⇒ [A34] A([A68] false W �A59� true)) false = AG([A34] A([A68] false W �A59� true))

Task

-The set of weak actions of 101#21 is empty due to the presence of the "true" strong action formula, whereas the set of strong actions of 102#21 is empty, i.e., the property belongs to L dbr µ . In both cases, our approach coincides with the mono-bisimulation approach. The verification of 101#21 (reduced for strong bisimulation) takes 75 seconds, with a memory peak of [START_REF] Emerson | Efficient model checking in fragments of the propositional mu-calculus[END_REF] Table 5 compares the performance of verifying the latter seven verification tasks using the approaches described above. LTS sizes are given in kilostates, memory in megabytes, and time in seconds. Tasks using more than 3 GB of memory were aborted. We see that our approach reduces both time and memory usage and allows all problems of the challenge to be solved, whereas using strong bisimulation alone fails in five out of those seven tasks. The negligible reductions in time and memory usage observed for tasks 101#22 and 101#23 are due to the fact that time and memory usage are dominated by the algorithm in charge of selecting a subset of processes to be composed and reduced (implemented in smart reduction). The complexity of this algorithm does not depend on the state space size, but on the number of actions and parallel processes, which is almost the same using both approaches. When considering larger examples, memory usage gets dominated by minimisation. In particular, for tasks 102#22, 102#23, 103#21, and 103#23 (and likely also 103#22), memory usage is reduced by several orders of magnitude.

Parallel benchmark of the RERS 2019 challenge

We tried the approach on the benchmark of parallel CTL problems given in the RERS 2019 challenge 13 . The principle of the challenge was the same as in 2018, 12 For problem 103#23, we tried smart strong reduction using the Grid'5000 [START_REF] Bolze | Grid'5000: A large scale and highly reconfigurable experimental grid testbed[END_REF] highperformance computing platform and the distributed LTS generation tool DISTRIBUTOR [START_REF] Garavel | Distributor and bcg merge: Tools for distributed explicit state space generation[END_REF] available in CADP. We could not get the final LTS (it would have required us to ask for a larger disk quota than the current 100 GB, which is already huge), but we obtained an intermediate LTS containing about 4.5 billion states and 36 billion transitions, whose generation took about 50 minutes using 84 distributed processes running on 7 multi-core computers. The largest intermediate LTS obtained using combined bisimulations is thus at least 36,800 times smaller than using strong bisimulation in this example. Experiments on Grid'5000 are courtesy of Wendelin Serwe. 13 http://rers-challenge.org/2019 but the number of CTL formulas was raised from 9 in 2018 to 180 in 2019, the number of systems was raised from 3 in 2018 to 9 in 2019, and the size of systems was increased from up to 34 parallel process and 70 actions in 2018 to 70 parallel processes and 234 actions in 2019. Table 6 gives details on the system sizes. For each system (numbered from 101 to 109), column #proc indicates the number of parallel processes, column #avg-size indicates the average process size in number of states, column #act indicates the number of actions (including the invisible action τ ), column #states gives the (unreduced) state space size of the system in number of states, and column #strong gives the size of the state space once reduced for strong bisimilarity. Unsurprisingly, the state space size grows exponentially with the number of processes and indeed, while we can rather easily generate the state space for the first (smallest) problems, it becomes quickly infeasible for the largest problems. Each system is accompanied by [START_REF] Godefroid | Using partial orders to improve automatic verification methods[END_REF] As in 2018, we analysed the 180 formulas to extract a set of strong actions, then partitioned the processes and refactored their composition into a weak and a strong group, and finally used the smart reduction heuristic to reduce both groups, using strong and divbranching bisimulation where appropriate. Figure 3 shows how such a strategy can be scripted using the SVL [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF] language of CADP for problem 101#01, whose property is A([A20] false W �A25� true ∨ �A21� true). When verifying this property, all actions but A20, A21, and A25 can be hidden, whereas A21 and A25 are the only strong actions.

Using the combined bisimulations approach, we were able to verify all problems concerning systems 101 to 107, except problem 107#08, whose state space remained too large. Tables 7 to 13 indicate for each problem, the truth value, the maximal intermediate LTS size (in number of states), and the final LTS size, using both the mono-bisimulation approach (strong) and the combined bisimulations approach. They show that the combined bisimulations approach really increases our capabilities to verify large concurrent systems, even though the complete exploration of the state space of systems 108 and 109 remains problematic.

It is interesting to see that in some cases (e.g., problems 107#01 and 107#07), the final problem has just one state. In problem 107#01, the formula has the form AG([A108] false), which belongs to L strong µ (∅) (i.e., the strong group is empty), and all the paths are loops that contain the A108 action (which is weak). The final LTS, obtained by divbranching minimization, encodes the process P = A108.P , --not hideable actions: A20, A21, and A25 --strong actions: A21 and A25 --inter-group actions: A4, A9, A10, A11, A14, A23, and A24 --weak group: processes not containing A21 nor A25 "problem101_01_weak.bcg" = smart divbranching reduction of --hiding all but inter-group actions and actions visible in the formula hide all but A4, A9, A10, A11, A14, A20, A21, A23, A24, A25 in par A9, A14 -> "P1.bcg" || A4, A7, A12, A13, A15, A23, A24 -> "P2.bcg" || A7, A12, A13 -> "P3.bcg" || A8, A27 -> "P4.bcg" || A26, A29, A30, A31, A32 -> "P5.bcg" || A8, A10, A11, A26, A27, A28, A29 -> "P8.bcg" end par end hide; --strong group: processes containing A21 and/or A25 "problem101_01_strong.bcg" = smart strong reduction of --hiding all but inter-group actions and actions visible in the formula hide all but A4, A9, A10, A11, A14, A20, A21, A23, A24, A25 in par A1, A2, A3, A4, A5, A6, A16, A17, A18, A19, A20, A21, A22, A23, A24, A25 -> "P6.bcg" || A2, A9, A10, A11, A14, A20, A21 -> "P7.bcg" end par end hide; --group composition "problem101_01_combined.bcg" = strong reduction of --hiding all but actions visible in the formula hide all but A20, A21, A25 in par A4, A9, A10, A11, A14, A23, A24 -> "problem101_01_weak.bcg" || A4, A9, A10, A11, A14, A23, A24 -> "problem101_01_strong.bcg" end par end hide Fig. 3 which is indeed a valid property preserving minimization of the system. Problem 107#07 is similar. Note that some of the RERS 2019 tasks can be evaluated more efficiently using non-compositional approaches, such as on-the-fly model checking (also available in CADP), in cases where proofs or counterexamples can be detected much before having explored the full state space. However, on-the-fly verification fails in many cases, in particular when the verification requires traversing the whole state space, such as the following problems, which all evaluate to true:

-103#06: AG(�A5� true ⇒ A([A45] false W �A46� true) -104#01: AG(�A17� true ⇒ AF(�A16� true)) -105#06: AG(�A1� true ⇒ A([A61] false U �A22� true)) -107#20: AG(�A175� true ⇒ A([A76] false W �A59� true))
This suggests a reasonable approach to tackle model checking problems, consisting in first applying on-the-fly model checking, setting a timeout and a memory quota to stop the verification when it becomes too eager, and then applying compositional reduction for the problems whose on-the-fly verification has been stopped.

The main drawback of our compositional approach with respect to on-the-fly verification is that, due to maximal hiding, the generated counterexamples are given only in terms of the actions visible in the formula, which abstracts out a lot of intermediate transitions. However, this is the price to pay for being able to verify most of the tasks.

Related Work

We make more precise in this section the links between our approach and two other approaches described in the literature, namely partial model checking and partial order reductions.

Given a temporal logic formula ϕ and a system described by a composition of processes P 1 || . . . ||P n , partial model checking [START_REF] Reif | Partial model checking[END_REF] is based on the computation of a quotient ϕ//P i of the formula ϕ with respect to some process P i (i ∈ 1..n). This quotient is a new temporal logic formula, which holds true on the system from which P i has been removed if and only if ϕ holds true on the whole system. This so-called quotienting approach can be applied repeatedly, until the formula evaluates (using partial evaluation rules) to either constant true or false, which happens at the latest when the formula has been quotiented with respect to all processes. At each step, simplifications are applied to the quotient, with the aim to keep it small enough. Successive quotienting of ϕ with respect to processes P 1 , . . . , P i "consumes" the modalities on actions which do not have to be synchronized with the remaining process P i+1 , . . . , P n . As shown in [START_REF] Lang | Partial model checking using networks of labelled transition systems and boolean equation systems[END_REF], quotienting can be assimilated to (and implemented as) a parallel composition between a graph representing the formula and the process P i , partial evaluation of the formula can be implemented as the resolution of a Boolean Equation System, and simplifications can be obtained by a combination of strong bisimulation minimisation and compression of those sequences of transitions representing consumed modalities.

Both compositional minimization and partial model checking are iterative approaches, each step of which starts with a formula ϕ and a composition P 1 || . . . ||P n . Thus virtually, steps of partial model checking and compositional minimization could be intertwined, one potentially having a choice between either generating the state space of (all or some part of) P 1 || . . . ||P n or computing the quotient of ϕ with respect to some P i and then simplifying this quotient. Choosing state space generation enables hiding and bisimulation reduction, possibly taking into account the results presented in the current paper, which is a neat advantage when divbranching bisimulation can be applied. On the other hand, partial model checking, in addition to an overhead due to the representation of the formula, suffers from the fact that once the formula has been quotiented with respect to some process, the potential benefits of minimizing the composition of this process with other processes with respect to divbranching bisimulation is lost. Yet, quotienting may have different benefits in some cases, such as the ability to yield a definitive verdict of the verification before the formula has been quotiented with respect to all processes (when some processes have no influence on the verdict), or the ability to trim processes to only those parts that are actually needed to verify the formula (when the formula requires only a partial traversal of the state space). From our own experience, compositional minimization of the system often shows better performance than partial model checking in practice. Yet, there remain corner cases where partial model checking is the winning strategy.

Our approach (in particular Theorem 2, page 13) is consistent with partial model checking and the mono-bisimulation approach [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] in the following sense: If the system has the form P ||Q where process P contains strong actions and process Q does not, all the modalities on actions present only in P (thus strong modalities) are consumed in ϕ//P , which thus belongs to L dbr µ . Following [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF], since ϕ//P has to be checked on Q, this confirms the main result presented in this paper, namely that Q can be reduced with respect to divbranching bisimulation. Another interesting class of approaches when model checking compositions of processes P 1 || . . . ||P n is partial order reductions [START_REF] Godefroid | Using partial orders to improve automatic verification methods[END_REF], which consist in identifying in P 1 || . . . ||P n sets of transitions that "commute" and whose interleaving can sometimes be avoided. Side criteria guarantee the preservation of some equivalence relation and/or temporal logic. These sets of transitions are computed in each state, either by using a structural analysis of the system [START_REF] Godefroid | Using partial orders to improve automatic verification methods[END_REF][START_REF] Ramakrishna | Partial-order reduction in the weak modal mucalculus[END_REF][START_REF] Peled | Partial order reduction: Linear and branching temporal logics and process algebras[END_REF][START_REF] Valmari | Stubborn set methods for process algebras[END_REF][START_REF] Gerth | A partial order approach to branching time logic model checking[END_REF], or from a local, on-the-fly exploration of the state space, such as in τ -confluence reduction [START_REF] Friso | Confluence for process verification[END_REF][START_REF] Groote | State space reduction using partial τ -confluence[END_REF][START_REF] Mateescu | Sequential and Distributed On-the-Fly Computation of Weak Tau-Confluence[END_REF]. To our knowledge, works on partial order reduction in the action-based setting preserve either logics containing only some forms of weak modalities, but no strong modalities as in L strong µ (A s ). Yet, partial order reductions preserving divbranching bisimulation can be used complementary to the approach presented in this paper, when generating compositions of processes that do not contain strong actions (thus providing an efficient pre-reduction of the resulting state space).

In a recent paper [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF], we refined the approach presented in the current paper by devising a family of bisimilarity relations called sharp bisimilarities, which are weaker than strong bisimilarity and stronger than divbranching bisimilarity. Each of these relations is parameterized by a set A s of strong actions. We showed that a formula is preserved (on all models) by sharp bisimilarity with respect to the set A s of strong actions if and only if the formula belongs to the fragment L strong µ (A s ). Moreover, sharp bisimilarities are congruences for parallel composition and action mapping, and can thus be applied compositionally. The sharp bisimilarity approach is consistent with the combination of strong and divbranching bisimilarities presented in the current paper, in the sense that (1) sharp bisimilarity with respect to any set of actions that do not occur in a process is preserved by divbranching bisimilarity for this process and (2) sharp bisimilarity is also preserved by strong bisimilarity, which is a stronger relation. Although the sharp bisimilarity approach is generally more effective to reduce the state space (in particular it allowed us to verify successfully all problems of the RERS 2019 parallel CTL challenge, including those concerning the largest systems 108 and 109), the current approach has the advantage that it can be applied using standard bisimilarity relations (implemented in various toolsets), namely strong and divbranching, and does not require a specific implementation of sharp bisimilarity reduction.

Conclusion and Future Work

In this paper, we proposed a compositional verification approach that refines a previous approach [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] and consists of three steps: First, so-called strong actions are identified, corresponding to those actions of the system that the formula cannot match using weak modalities in the sense of the L µ fragment L dbr µ adequate with divbranching bisimulation. These actions are used to partition the parallel processes into those containing strong actions and the others. Second, maximal hiding and compositional reduction are used to minimize the composition of processes not containing strong actions for divbranching bisimulation, and the other processes for strong bisimulation. Finally, the property is verified on the reduced system.

  P |[a, b]| Q and P |[]| Q instead of P |[{a, b}]| Q and P |[{}]| Q.

Fig. 1

 1 Fig. 1 LTS used in Examples 2 and 3

4

  Identifying Strong Actions in Formulas 4.1 Identifying strong actions in L µ , ACTL, and CTL operators

Example 5

 5 Consider the following (overly complicated) PDL modality: ψ = �true * .snd.(rec|¬rec.rec|¬rec.(¬rec) * .¬rec.rec).ack� ϕ 0

  * .a 1 .a 2 ] false 09 [true * .a 1 .a 2 .((a 3 .(¬a 4 ) * .a 5 )|(a 6 .(¬a 7 ) * .a 8 ))] false 14 [true * .a 1 .a 2 .(¬a 3 ) * .a 4 .a 5 ] false 16 [(¬a 1 ) * .a 2 .(¬a 3 ) * .a 4 ] �((¬a 5 ) * .a 6 .a 7 ).((¬a 5 ) * .a 6 .a 7 )� true 17 Same shape as property Nr. 16

Fig. 2

 2 Fig. 2 Results of the TFTP case-study (vertical axis is on a logarithmic scale)

  AG([A21] [A23] [A4] [true] false) false 101#22 AG([A3] AF(�A2� true)) false 101#23 AG(�A20� true ⇒ �A20� A([A23] false W �A8� true)) true 102#21 EF(AG([A5] false)) true 102#22 EG([A35] E([A23] false U �A35� true)) false 102#23 AG([A22] A([A8] false U �A22� true)) false 103#21 AG(

  2.3 Compositional property-dependent LTS reductionsGiven a formula ϕ ∈ L µ and a composition of processes P 1 || . . . || P n ,[START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] shows two results that allow P 1 || . . . || P n to be reduced compositionally, while preserving the truth value of ϕ. The first result is a procedure, called maximal hiding, which extracts systematically from ϕ a set of actions H(ϕ) that are not discriminated by any action formula occurring in ϕ. It is shown that P 1 || . . . || P n |= ϕ if and only if hide H(ϕ) in (P 1 || . . . || P n ) |= ϕ. The second result is the identification of a fragment of L µ , called L dbr µ , which is strictly more expressive than µACTL\X 3 and adequate with divbranching bisimulation. This fragment is defined as follows. By convention, we use the symbols α τ and α a to denote action formulas such that τ ∈ [[α τ ]] A and

	Definition 10 (Modal µ-calculus fragment L dbr µ [40]) τ / ∈ [[α a ]] A . The fragment L dbr µ

Table 1

 1 TFTP properties (strong action formulas are highlighted)

Table 3

 3 RERS 2018 properties (strong action formulas are highlighted)

Table 4

 4 Some numbers about the RERS 2018 parallel benchmark

		#act	#hide	#sact	#proc #sproc	#sync	relation
	101#21	24	21	24	9	9	-	strong
	101#22	24	22	1	9	4	11	combination
	101#23	24	21	2	9	3	9	combination
	102#21	28	27	0	20	0	-	divbranching
	102#22	28	26	2	20	10	14	combination
	102#23	28	26	1	20	4	12	combination
	103#21	70	66	2	34	8	12	combination
	103#22	70	66	3	34	6	18	combination
	103#23	70	67	1	34	7	10	combination
	Table

  MB and a largest LTS of 83, 964 states and 374, 809 transitions. The verification of 102#21 (reduced for divbranching bisimulation) takes 261 seconds, with a memory peak of 22 MB and a largest LTS of 243 states and 975 transitions. -101#22, 101#23, 102#22, 102#23, 103#21, 103#22, and 103#23 contain both weak and strong actions. They are used to evaluate our approach.

Table 5

 5 Experimental results of the RERS 2018 parallel benchmark

				12
		Strong bisimulation		Combined bisimulations
		Kstates	verif.	Kstates	verif.
	Task	largest	final	MB	sec.	largest	final	MB	sec.
	101#22	84	77	10	77	1.4	1.4	10	72
	101#23	84	77	11	80	0.5	0.5	8	73
	102#22	-	-	-	-	611	585	57	295
	102#23	-	-	-	-	17	9.8	22	260
	103#21	-	-	-	-	734	313	101	604
	103#22	-	-	-	-	14,143	14,141	1575	2533
	103#23	-	-	-	-	122	122	35	566

Table 6

 6 CTL formulas numbered from 01 to 20. Some numbers about systems of the RERS 2019 parallel challenge

	System	#proc #avg-size	#act	#states	#strong
	101	8	12	30	26, 996	6, 600
	102	10	19	59	290, 149	149, 040
	103	12	12	66	791, 862	300, 000
	104	15	19	54	1, 667, 045	589, 680
	105	20	19	78	52, 946, 151	6, 036, 800
	106	25	22	106	> 300, 000, 000
	107	50	19	180
	108	60	19	218
	109	70	16	234

  SVL encoding of combined bisimulations approach for problem 101#01

	���	������	��������	������	��������	������		�����	������	��������	������	��������
	�������� ����� ������������ ��������������	���� ����	� ����	��� ��	���� ����	� �����	�� ��	���� ����	� ����	��� ��	���� ����	� �����	�� ��	���� ����	� �����	� ��
	�������� ����� ������������ ��������������	���� ����	� ����	��� ��	���� ����	� ����	��� ���	���� ����	� ����	��� ��	���� ����	� �����	��� ��	���� ����	�� ����	�� ���
	�������� ����� ������������ ��������������	���� ����	�� �����	�� ��	���� ����	�� ����	��� ���	���� ����	�� ����	��� ��	���� ����	�� ����	�� ��	���� ����	�� ����	� ��
	�������� ����� ������������ ��������������	���� ����	�� ����	��� ��	���� ����	�� ����	��� ��	���� ����	�� ����	��� ��	���� ����	�� �����	��� ��	���� ����	�� ����	�� ���

Table 7

 7 Results for problem 101 of the RERS 2019 parallel CTL challenge

	���	������	��������	������	��������	������	��������	������	��������	������	��������
	�������� ����� ������������ ��������������	����� �����	� ����	��� ��	����� �����	� �����	��� ���	����� �����	� ����	��� ��	����� �����	� ����	��� ���	����� �����	� �����	��� ���
	�������� ����� ������������ ��������������	����� �����	� �����	��� ���	����� �����	� �����	��� ��	����� �����	� �����	��� ��	����� �����	� �����	��� ���	����� �����	�� ����	��� ���
	�������� ����� ������������ ��������������	����� �����	�� �����	��� ���	����� �����	�� �����	��� ��	����� �����	�� �����	��� ��	����� �����	�� ����	��� ���	����� �����	�� ����	��� ���
	����������� ����� ������������ ��������������	����� �����	�� �����	��� ���	����� �����	�� ����	��� ���	����� �����	�� ����	��� ��	����� �����	�� ����	��� ��	����� �����	�� �����	� ���

Table 8

 8 Results for problem 102 of the RERS 2019 parallel CTL challenge

	���	������		��������	������	��������	������		��������	������	��������	������	��������
	�������� ����� ������������ ��������������	������ ������	� ����	��� ���	������ �����	� �����	��� ���	������ �����		� ����	�� ��	������ ������	� ����	�� ��	������ ����� ����� �	��� ���
	�������� ����� ������������ ��������������	������ �����		� ����	��� ���	������ �����	� �����	�� ��	������ �����	� ����	�� ��	������ ������	� ����	��� ���	������ ������	�� ����	�� ��
	�������� ����� ������������ ��������������	������ �����		�� ����	���� ���	������ �����	�� �����	��� ���	������ �����	�� �����	��� ���	������ �����	�� ����	�� ��	������ ������	�� ����	��� ���
	�������� ����� ������������ ��������������	������ ������	�� �����	�� ��	������ ������	�� ����	�� ��	������ ������	�� ����	�� ��	������ ������ ����� ��	�� ��	������ �����	�� �����	�� ��

Table 9

 9 Results for problem 103 of the RERS 2019 parallel CTL challenge

	���	������	��������	������		��������	������	��������	������		��������	������	��������
	�������� ����� ������������ ��������������	������ ������	� ����	��� ��	������ ������	� ����	��� ��	������ ������ ����� �	���� ���	������ ������ ����� �	��� ��	������ ������ ����� �	�� ����
	�������� ����� ������������ ��������������	������ ������	� ����	��� ��	������ ������	� �����	��� ��	������ ������	� ����	��� ��	������ ������	� ����	��� ��	������ ������	�� ����	�� ���
	�������� ����� ������������ ��������������	������ ������	�� ����	����� ���	������ ������	�� �����	���� ��	������ ������ ����� ��	����� ���	������ ������		�� ����	��� ��	������ ������ ����� ��	�� ���
	�������� ����� ������������ ��������������	������ ������	�� ����	���� ��	������ ������	�� �����	��� ��	������ ������	�� ����	����� ���	������ ������	�� �����	����� ���	������ ������	�� ����	�� ���

Table 10

 10 Results for problem 104 of the RERS 2019 parallel CTL challenge

	���	������	��������	������	��������	������	��������	������	��������	������	��������
	�������� ����� ������������ ��������������	������� ������� ���� �	���� ���	������� ������� ���� �	���� ���	������� ������� ����� �	���� ���	������� ������� ���� �	��� ���	������� ������� ���� �	��� ����
	�������� ����� ������������ ��������������	������� ������� ���� �	��� ��	������� ������� ����� �	��� ��	������� ������� ���� �	���� ���	������� ������� ����� �	��� ��	������� ������� ���� ����	�� ���
	�������� ����� ������������ ��������������	������� ������� ���� ��	�� ���	������� ������� ����� ��	��� ��	������� ������� ����� ��	��� ��	������� ������� ���� ��	���� ���	������� ������� ���� ��	��� ���
	�������� ����� ������������ ��������������	������� ������� ���� ��	���� ����	������� ������� ����� ��	��� ��	������� ������� ����� ��	��� ���	������� ������� ���� ��	��� ��	������� ������� ���� ��	��� ���

Table 11

 11 Results for problem 105 of the RERS 2019 parallel CTL challenge

	���	������	��������	������	��������	������	��������	������	��������	������	��������
	�������� ����� ������������ ��������������	� �	� �����	��� ��	� �	� �����	��� ���	� �	� ����	��� ��	� �	� ����	��� ��	� �	� �����	�� ���
	�������� ����� ������������ ��������������	� �	� ����	��� ��	� �	� �����	��� ��	� �	� ����	��� ��	� �	� ����	��� ���	� �	�� �����	�� ���
	�������� ����� ������������ ��������������	� �	�� �����	��� ��	� �	�� �����	��� ��	� �	�� �����	��� ��	� �	�� ����	��� ���	� �	�� ����	��� ���
	�������� ����� ������������ ��������������	� �	�� �����	��� ��	� �	�� �����	��� ��	� �	�� ����	��� ��	� �	�� ����	��� ��	� �	�� �����	�� ���

Table 12

 12 Results for problem 106 of the RERS 2019 parallel CTL challenge

	���	������	��������	������	��������	������	��������	������	��������	������	��������
	�������� ����� ������������ ��������������	� �	� �����	��� �	� �	������� ��� ���� �	� �	�������� ��� ���� �	� �	��������� ���� ���� �	� �	��� �������� ���� �
	�������� ����� ������������ ��������������	� �	������ �� ����� �	� �	� �����	��� �	� �	� �����	���� ���	� �	� ����	������ ��	� �	�� �����	��� �����
	�������� ����� ������������ ��������������	� �	�� ����		����� ��	� �	�������� ��� ����� ��	� �	�������� ��� ����� ��	� �	�� ����	���� ���	� �	��� ������� ����� ��
	�������� ����� ������������ ��������������	� �	�� ����	������ ��	� �	�� ����	���� ���	� �	������ �� ����� ��	� �	������� ���� ����� ��	� �	�� ����	�� �����

Table 13

 13 Results for problem 107 of the RERS 2019 parallel CTL challenge

µACTL\X denotes ACTL\X plus fixed points. The authors of[START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] claim that L dbr µ is as expressive as µACTL\X, but they omit that the �ϕ 1 ?.α τ � @ weak infinite looping modality cannot be expressed in µACTL\X.

Note however that there is no proof that the test ϕ ∈ L dbr µ is decidable. So far, we can only conjecture it, based on the fact that testing equivalence between L µ formulas is decidable[START_REF] Streett | An automata theoretic decision procedure for the propositional mu-calculus[END_REF].

Note that this number may be different for P |[A sync ]| Q and for P |[A sync ]| Q � . We have to take the maximum.

Any action formula can be reduced to one of two forms: either a disjunction a 1 ∨ ... ∨ a n , or a conjunction of negations ¬b 1 ∧ ... ∧ ¬b m . Two action formulas are syntactically equal if they are of the same form and contain the same set of actions.

Otherwise, our approach coincides with the mono-bisimulation approach of[START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF]. In all the examples addressed in this section, there is always a unique minimal set A s , whose identification is made easy using Lemmas 2 to 4.

Specification available at ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_05

Acknowledgements

This work has been partially funded by the 4SECURail project. The 4SECURail project received funding from the Shift2Rail Joint Undertaking under the European Union's Horizon 2020 research and innovation programme under grant agreement No 881775 in the context of the open call S2R-OC-IP2-01-2019, part of the "Annual Work Plan and Budget 2019", of the programme H2020-S2RJU-2019. The content of this paper reflects only the authors' view and the Shift2Rail Joint Undertaking is not responsible for any use that may be made of the included information.

The authors warmly thank Wendelin Serwe for his comments on earlier versions of this paper and his help to carry on experiments on Grid'5000. They also are extremely grateful to Hubert Garavel, who triggered the author's collaboration between Grenoble and Pisa and who provided the TFTP case-study (together with Damien Thivolle). They thank the organizers of the RERS challenge, who produced the numerous examples from which we could develop these ideas. Finally, they thank the anonymous referees of FM'2019 for their useful comments on the short version of this paper and of FMSD for the current version.

¬ϕ

Proof Immediate from the definition of L strong µ (A s ) (see Def. 11) and the wellknown identities ϕ 1 ∧ ϕ 2 = ¬(¬ϕ 1 ∨ ¬ϕ 2 ) and ϕ 1 ⇒ ϕ 2 = ¬ϕ 1 ∨ ϕ 2 . � � Lemma 3 (Action Computation Tree Logic) Assume that ϕ i ∈ L strong µ (A s ) (i = 1, 2). Then the following hold:

Proof It was shown in [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] that the operators of ACTL\X can be encoded using the weak modalities of L dbr µ . Therefore, the only strong modalities that remain in these formulas are those occurring in ϕ 1 and ϕ 2 , which by definition match only labels in A s . Therefore, these formulas belong to L strong µ (A s ). � � Lemma 4 (Computation Tree Logic) Assume that ϕ i ∈ L strong µ (A s ) (i = 0, 1, 2) and τ / ∈ [[α a ]] A . Then the following hold:

Proof We first prove the following identity, which will be used in the sequel:

This identity is easily proven by showing that the modal µ-calculus definitions of the left-hand-side and right-hand-side formulas are equivalent. First note that Items 1 to 8 are a direct consequence of Lemma 3 and the fact that these operators can be translated to ACTL\X, as shown by equations (Ctl1) to (Ctl8). The proof of Items 9 to 14 follows:

By (Actl1) and τ / ∈ [[α a ]] A which is in L strong µ (A s ) following Item 6 and Lemmas 2 and 3. ) is true, then there is a reachable state satisfying ϕ 1 ∧ �α a � ϕ 2 , by definition of EF. This state also satisfies �(ϕ 1 ?.true) * .ϕ 1 ?.α a � ϕ 2 , after an empty sequence of steps matching (ϕ 1 ?.true) * . On the other hand, if a reachable state satisfies �(ϕ 1 ?.true) * .ϕ 1 ?.α a � ϕ 2 , then a reachable state satisfies both ϕ 1 and �α a � ϕ 2 , by definition of the weak modality, i.e, the LTS satisfies EF(ϕ 1 ∧ �α a � ϕ 2 ). � � More complex formula patterns can be easily shown to be in L strong µ (A s ) by extension of Lemma 4. For instance, if ϕ 1 , . . . , ϕ n ∈ L strong µ (A s ), since we have

Example 4 Let a 1 , a 2 , and a 3 be visible actions and recall that A denotes the set of all actions of the system. Lemmas 2 to 4 allow the following to be shown (this is left as an exercise):

4.2 Combinations of CTL operators and modalities that are not in

We have given in Section 4.1 a set of formula patterns obtained by combination of CTL operators and L µ modalities, which belong to L strong µ (A s ). In this section, we review other combinations, which do not belong to L strong µ (A s ). For each combination, we explain why. Below, we assume ϕ 0 , ϕ 1 , ϕ 2 ∈ L strong µ (A s ) and a, a 1 , a 2 / ∈ A s .

-AG(�a� ϕ 0 ) and EG(�a� ϕ 0 ) generally 7 do not belong to L strong µ (A s ), because these formulas require that a occurs immediately. They become false if a is delayed by a τ -transition. For instance below, AG(�a� true) and EG(�a� true) do not belong to L strong µ (∅) because these formulas are satisfied by LTS P 1 but not by the divbranching bisimilar LTS Q 1 (where a is delayed by a τtransition from q 0 to q 1 ). As a consequence, EF([a] ϕ 0 ) = ¬AG(�a� ¬ϕ 0 ) and AF([a] ϕ 0 ) = ¬EG(�a� ¬ϕ 0 ) generally do not belong to L strong µ (A s ) either.

, and E(�a� ϕ 1 W ϕ 2 ) generally do not belong to L strong µ (A s ), for similar reasons. In particular, A(�a� ϕ 0 W false) = AG(�a� ϕ 0 ) and E(�a� ϕ 0 W false) = EG(�a� ϕ 0 ), which have been shown to be outside L strong µ (A s ) in the previous item. 7 Obviously, there are particular instances of such formulas that belong to L strong µ (A s ), e.g., AG(�a� false) and EG(�a� false), which are equivalent to false.

-AF(�a� ϕ 0 ) generally does not belong to L strong µ (A s ) because even though �a� ϕ 0 is satisfied in a state, AF(�a� ϕ 0 ) is not necessarily satisfied in divbranching bisimilar states where a is delayed. For instance below, AF(�a� true) does not belong to L strong µ (∅) because this formula is satisfied by LTS P 2 but not by the divbranching bisimilar LTS Q 2 (where a is delayed by a τ -transition from q 0 to q 1 ). As a consequence, EG([a] ϕ 0 ) = ¬AF(�a� ¬ϕ 0 ) generally does not belong to L strong µ (A s ) either.

as formalized by Lemma 5 below.

Lemma 5 There are action formulas α a1 , α a2 and state formulas

Proof Let A s = ∅ and consider the formula EF(�a 1 � true ∧ �a 2 � true), i.e., α a1 = a 1 , α a2 = a 2 , and ϕ 1 = ϕ 2 = true. We have ϕ 1 ∈ L strong µ (∅) and ϕ 2 ∈ L strong µ (∅). We know that if EF(�a 1 � true ∧ �a 2 � true) ∈ L strong µ (∅), then it has the same truth value when evaluated on divbranching equivalent LTS. This is not the case as shown by the divbranching equivalent LTS P and Q depicted below. Indeed, EF(�a 1 � true ∧ �a 2 � true) evaluates to true on P , whereas it evaluates to false on Q. Therefore,

So far, we did not mention explicitly the next operators of ACTL. We do it here for completeness: -EX α a ϕ is equivalent to �α a � ϕ and thus makes all actions satisfying α a strong, unless it occurs in the immediate context of an EF operator. -Finally, EX τ ϕ is equivalent to �τ � ϕ and thus makes τ strong. (ii) There is no potentially invisible self-loop, i.e., τ � ∈ [[α ij ]] A for any j ∈ J. In this case, all the modalities present in the equation are considered as strong, according to Definition 14, and the equation is left unchanged.

After modifying all equations of D that match case (i), we obtain a HMLR specification D � whose strong modalities contain the action formulas satisfied by the actions in A str (D). It remains to show that ϕ(D � ) ∈ L strong µ (A s ∪ A str (D)). By hypothesis, we know that ϕ 0 ∈ L strong µ (A s ). The translation from PDL to guarded HMLR [START_REF] Mateescu | On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators[END_REF] propagates ϕ 0 in all equations, i.e., ϕ i = ϕ 0 for all 1 ≤ i ≤ n. Thus, the right-hand side formulas of all equations in D � belong to L strong µ (A s ∪ A str (D)). By applying the translation in Definition 13, which does not change the structure of the formulas in the right-hand sides but only introduces fixed point operators, we obtain a formula ϕ(D � ) ∈ L strong µ (A s ∪ A str (D)). � � Example 7 Consider the guarded HMLR specification D in Example 5. We update the equations of D according to Lemma 6 and obtain the specification D � below:

We see that the strong actions of D � are [[rec]] A (imposed by the equations defining X 2 , X 4 , and X 6 ), [[¬rec]] A (imposed by the equations defining X 2 and X 5 ), and [[ack]] A (imposed by the equation defining X 3 ), and thus

which is equal to A str (D) according to Definition 14.

Test-free PDL modalities without nesting of * -operators can be handled by applying a simpler criterion, stated below.

Lemma 7 (Simple PDL modalities) Let A s be a set of strong actions and assume that ϕ

Then the following hold:

Proof It was shown in [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] that these weak PDL-Δ modalities can be encoded in

The proposed encoding also works when ϕ 0 ∈ L strong µ (A s ). As this encoding does not add more strong modalities than already present in ϕ 0 , these properties belong to L strong µ (A s ). � �

Reducing the number of strong actions

Lemma 6 identifies the strong actions in a guarded HMLR specification D corresponding to a PDL modality �β� ϕ 0 . However, in general there are several such HMLR specifications D (and even an infinite number of them if D contains cyclic dependencies between variables), each one with its own set A str (D). Identifying, among all these HMLR specifications, the one having the minimal set of strong actions is a non-trivial problem. We sketch below a procedure to obtain a D with a reduced (not necessarily minimal) number of strong actions.

All guarded HMLR specifications D corresponding to a PDL modality �β� ϕ 0 represent the regular language denoted by β. Every such specification D can be brought to a canonical form by determinizing and minimizing it similarly to a finite automaton. For the sake of simplicity, we use a syntactic notion of determinization, by considering each action formula in a modality of D as a literal. Thus, a guarded HMLR specification is deterministic if, for each of its equations

all action formulas α ij are syntactically different 8 . The determinization of a guarded HMLR specification D can be done using the classical subset construction, as shown in [START_REF] Mateescu | On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators[END_REF].

Example 8 Consider the guarded HMLR specification D of Example 5, whose equations defining X 2 and X 5 are nondeterministic because each one contains two modalities on ¬rec. By applying the subset construction, we obtain (sets of propositional variables are represented by sets of indexes):

After eliminating the equations defining X {4,5} and X {5,6} (both equal to X {2} ) and renaming the variables, we obtain a deterministic HMLR specification (left), which can be further refined by identifying the weak modalities in the equations defining X 1 and X 2 (right):

Regarding ACTL\X and CTL\X, we showed in Section 4.1 that all operators of those two logics (thus not considering fixed points and L µ modalities) are part of L strong µ (A s ) for any A s , in particular L strong µ (∅). Therefore, for a formula ϕ expressed using a combination of those operators and L µ modalities, the set of strong actions is included in the actions matched by the L µ modalities of ϕ. It is therefore safe to take as set A s exactly the set of actions matched by the L µ modalities occurring in ϕ. If at least one process does not contain one of such actions, this safe approach enables the state space to be reduced more than with the mono-bisimulation approach. One can do better by excluding the actions matched only by modalities occurring in specific contexts, as expressed by Lemmas 3 and 4.

Applications

We consider two examples to illustrate our new verification approach combining strong and divbranching bisimulation and show how it can reduce both time and memory usage when associated to the smart reduction heuristic. In both examples, the aim is to perform a set of verification tasks, each consisting in checking a formula ϕ on a system of parallel processes P 1 || . . . || P n . Since our approach can only improve the verification of formulas containing both strong and weak modalities, we consider only the pairs of formulas and systems such that the formula is part of L strong µ (A s ) for some minimal A s that is not empty and that is strictly included in the set of visible actions of the system. 9 For each verification task, we compare the largest intermediate LTS size, the verification time, and the memory peak obtained using the following two approaches: Mono-bisimulation approach: ϕ is verified on hide H(ϕ) in (P All experiments were done on a 3GHz/12GB RAM/8-core Intel Xeon computer running Linux, using the specification languages and 32-bit versions of tools provided in the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] version 2019-a "Pisa".

The originality of this approach is to combine strong and divbranching bisimulation, as opposed to the mono-bisimulation approach of [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF]. We proved it correct by characterizing a family of fragments of the logic L µ , called L strong µ (A s ), parameterized by the set A s of strong actions. We also showed under which conditions action-based branching-time temporal logic formulas containing well-known operators from the logics CTL, ACTL, PDL, and PDL-Δ are part of L strong µ (A s ) when A s is fixed. In the future, it might be worth investigating whether more operators can be considered, e.g., from the linear-time logic LTL.

This approach may significantly improve the verification performance for systems containing both processes with and without strong actions, as illustrated by two case-studies. In particular, it allowed the whole parallel CTL benchmark of the RERS 2018 challenge to be solved on a standard computer.

Identifying minimal sets of strong actions for arbitrary formulas manually is a cumbersome task, prone to errors. We shall investigate ways to compute such sets automatically. As illustrated by verification task 103#23 of RERS 2018, the problem is not purely syntactic: considering non-trivial semantic equivalences may prove useful to eliminate actions that appear strong at first sight. Yet, we trust that the presented approach has potential to be implemented in automated software tools, such as those available in the CADP toolbox.