Luca Di

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

Compositional verification of priority systems using sharp bisimulation

Keywords: Concurrency, Congruence, Enumerative verification, Finite state processes, State space reduction

Introduction

We consider the verification of systems consisting of parallel processes that execute asynchronously and that may synchronize by rendezvous. The toolbox CADP1 [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] provides languages for the description of such systems (in particular the language LNT2 [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 7.0)[END_REF], which inherits many features from process algebra), languages for the description of properties (in particular the temporal logic MCL3 [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF], which is an extension of the modal µ-calculus with regularexpressions on actions and data handling constructs), and various tools for generating and minimizing state spaces, composing state spaces, evaluating temporal logic properties on state spaces, generating tests, etc. CADP provides various verification methods, some of the most successful of which are based on a compositional minimization of the system using appropriate equivalence relations [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF][START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF][START_REF] Lang | Compositional verification of concurrent systems by combining bisimulations[END_REF][START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF].

As such, sharp bisimulation [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF] was proposed recently as a relation parameterized by a subset of the system's actions, called strong actions. These actions are generally obtained by analysis of the property under verification, ensuring that this property is preserved by equivalence. Strong bisimulation [START_REF] Park | Concurrency and Automata on Infinite Sequences[END_REF] and branching bisimulation [START_REF] Van Glabbeek | Branching-Time and Abstraction in Bisimulation Semantics[END_REF][START_REF] Van Glabbeek | Branching Time and Abstraction in REFERENCES Bisimulation Semantics[END_REF] are instances of sharp bisimulation, all actions being strong in the former, and all actions being weak (i.e., not strong) in the latter. Keeping the set of strong actions as small as possible allows smaller quotients to be obtained. Sharp bisimulation is a congruence for many process algebraic operators, such as parallel composition, hide, cut, and rename, and can therefore be used compositionally. A divergence-preserving variant of sharp bisimulation (named divsharp bisimulation in the current paper) was applied successfully to the CTL verification problems of the RERS verification challenges 4 in 2019 5 and 2020, 6 where it allowed properties not preserved by divergence-preserving branching (a.k.a. divbranching) bisimulation to be verified on systems whose state space could not be generated using compositional strong bisimulation reduction.

In this paper, we present contributions that are complementary to the already published results on sharp bisimulation [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF]:

• We consider systems, some actions of which may be preempted by others using an action priority operator, similar in spirit to the one of ACP [START_REF] Baeten | Syntax and defining equations for an interrupt mechanism in process algebra[END_REF]. It is well-known that strong bisimulation equivalence is a congruence for such an operator, but also that branching is not. We give sufficient conditions relating the set of strong actions and the priority rules, so that sharp bisimulation equivalence is a congruence for priority. We provide a proof of congruence. • We establish a precise relationship between sharp bisimulation and orthogonal bisimulation [START_REF] Bergstra | Branching time and orthogonal bisimulation equivalence[END_REF], the latter being also a congruence for priority. We prove that if the internal action τ does neither give priority to nor take priority over any other action, then sharp minimization can be applied compositionally and cannot reduce less than orthogonal minimization. We exhibit an example where sharp minimization produces an LTS that is several orders of magnitude smaller than the one obtained using orthogonal minimization. • While previous work only described a partial reduction algorithm preserving sharp bisimulation, we provide an algorithm based on signatures, which computes the quotient of a system with respect to sharp bisimulation equivalence. We compare the performance of its implementation in the BCG_MIN tool with strong and divbranching minimizations. • Finally, we describe an application of compositional sharp minimization to the verification of a collective adaptive system, which uses action priority.

This paper is not only a theoretical paper. It combines theory with implementation in software tools distributed in CADP, a widely used toolbox, which has been continuously maintained, improved, and extended over the past three decades.

Overview.

Processes and their compositions, sharp bisimulation, and the priority operator are presented in Section 2. Congruence of sharp bisimulation equivalence for the priority operator, which depends on strong actions, is proven in Section 3. A comparison between sharp bisimulation and orthogonal bisimulation is made in Section 4. The signature-based sharp minimization algorithm is presented in Section 5, where we also describe how it can be adapted to implement orthogonal minimization. A toy example illustrating the potential benefit of using sharp bisimulation rather than orthogonal bisimulation is presented in Section 6. The case study is presented in Section 7. We discuss related work in Section 8. Finally, we conclude in Section 9.

Data availability statement.

The datasets generated and analysed during the current study, as well as the scripts used to define the experiments, are available as a replication package at https://doi.org/10.5281/zenodo.7602897.

Background

Processes

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

Definition 1 (LTS). Let A be an infinite set of actions including the invisible action τ and visible actions A \ {τ }. An LTS P 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.

We may write Σ P , A P , -→ P for the sets of states, actions, and transitions of an LTS P , and init(P ) for its initial state. We write p a -→ p ′ for (p, a, p ′ ) ∈ -→ and p A -→ for (∃p ′ ∈ Σ P , a ∈ A) p a -→ p ′ .

To build complex behaviours, LTSs can be composed and abstracted using standard process algebraic operators, such as parallel composition, hide, cut, and rename (see e.g., [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF]). In this paper, we will use the following parallel composition operator.

Definition 2 (Parallel composition of LTSs). Let P and Q be LTSs and let A ⊆ A \ {τ } be a set of visible actions. The parallel composition of P and Q with synchronization on A, written "P |[A]| Q", is defined as the LTS (Σ P × Σ Q , A P ∪ A Q , -→, (init(P ), init(Q))), where (p, q) a -→ (p ′ , q ′ ) iff:

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

Sharp Bisimulation

LTSs can be compared and reduced modulo bisimulation relations between states. We consider the family of sharp bisimulations as well as their divergence-preserving variants [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF] defined hereafter in a general form subsuming strong [START_REF] Park | Concurrency and Automata on Infinite Sequences[END_REF], branching, and divbranching [START_REF] Van Glabbeek | Branching-Time and Abstraction in Bisimulation Semantics[END_REF][START_REF] Van Glabbeek | Branching Time and Abstraction in REFERENCES Bisimulation Semantics[END_REF] bisimulations.

Definition 3 (Sharp bisimulation [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF]). A sharp bisimulation 7 w.r.t. a set of strong actions A s is a symmetric relation R ⊆ Σ × Σ such that if (p, q) ∈ R then for all p a -→ p ′ , there exists q ′ such that (p ′ , q ′ ) ∈ R and either of the following holds:

1. q a -→ q ′ , or 2. a = τ , τ / ∈ A s , and q ′ = q, or 3. a / ∈ A s , and there exist q 0 τ -→ . . . τ -→ q n a -→ q ′ (n ≥ 0) such that q 0 = q, and for all i ∈ 1..n, (p, q i ) ∈ R.

A divergence-preserving sharp bisimulation (called divsharp bisimulation in the sequel) R additionally satisfies the following divergence-preservation condition: for all (p 0 , q 0 ) ∈ R such that p 0 τ -→ p 1 τ -→ p 2 τ -→ . . . with (p i , q 0 ) ∈ R for all i ≥ 0, there is also an infinite sequence q 0

τ -→ q 1 τ -→ q 2 τ -→ . . . such that (p i , q j ) ∈ R for all i, j ≥ 0.
States p, q are sharp (resp. divsharp) bisimilar w.r.t. A s , written p ∼ ♯As q (resp. p ∼ @ ♯As q), iff there exists a sharp (resp. divsharp) bisimulation R w.r.t. A s such that (p, q) ∈ R.

A sharp bisimulation is a hybrid between a strong and a branching bisimulation, characterized by the set of strong actions. If a state has a transition labelled by a strong action, every sharp bisimilar state must also have a similar transition labelled by the same strong action. This transition cannot be delayed by a transition labelled by τ (or τ -transition). By contrast, a transition labelled by a weak action can be delayed under the same condition as branching bisimulation.

Sharp bisimulation generalizes results that are well-known in the framework of strong and (div)branching bisimulations [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF]. For all sets of strong actions A s and A ′ s : • ∼ ♯As (resp. ∼ @ ♯As ) is an equivalence relation. The quotient of an LTS P w.r.t. this equivalence relation (written P/ ∼ ♯As ) is unique and minimal both in number of states and number of transitions. Computing this quotient is called minimization. • If A s = A (i.e., all actions are strong, including τ ), then sharp bisimulation and divsharp bisimulation coincide with strong bisimulation, whose equivalence is written ∼. • If A s = ∅ (i.e., all actions are weak), then sharp (resp. divsharp) bisimulation coincides with branching (resp. divbranching) bisimulation, whose equivalence is written ∼ br (resp. ∼ dbr ). • The set of sharp (resp. divsharp) bisimulation equivalences equipped with set inclusion actually forms a complete lattice whose supremum is branching (resp. divbranching) bisimulation equivalence and whose infimum is strong bisimulation equivalence.

• If A ′ s ⊂ A s then ∼ ♯As (resp. ∼ @ ♯As ) is strictly stronger than ∼ ♯A ′ s (resp. ∼ @ ♯A ′
s ), hence generalizing that strong bisimulation equivalence is strictly stronger than (div)branching. As a consequence, an LTS minimized for ∼ ♯A ′ s (resp. ∼ @ ♯A ′ s ) cannot be larger than the same LTS minimized for ∼ ♯As (resp. ∼ @ ♯As ), i.e., the fewer strong actions, the greater the reduction.

• ∼ ♯As (resp. ∼ @ ♯As ) is a congruence for all abstraction and composition operators encodable as admissible networks of LTSs [START_REF] De Putter | Compositional model checking with divergence preserving branching bisimilarity is lively[END_REF][START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF][START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF], such as synchronization vectors and the parallel composition, hide, cut, and rename operators of CCS [START_REF] Milner | Communication and Concurrency[END_REF], CSP [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF], mCRL [START_REF] Groote | The Syntax and Semantics of µCRL[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]ISO/IEC: Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001[END_REF], and LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 7.0)[END_REF], including the operator of Definition 2. Minimization can thus be applied compositionally through these operators. Note that, just like (div)branching, ∼ ♯As and ∼ @ ♯As are not congruences for the nondeterministic choice operator (written "+" in CCS and mCRL, "[]" in CSP and LOTOS, and select in LNT), unless all initial actions of the nondeterministic choice are strong actions. In particular, strong bisimulation equivalence is a congruence for the nondeterministic choice operator, because all actions are strong.

• Finally, ∼ @ ♯As is adequate with a well-characterized fragment L strong µ (A s ) of the modal µ-calculus, 8 also parameterized by A s . The union indexed by A s of all such fragments is the modal µ-calculus itself, so that every formula belongs to some of these fragments. Thus, identifying a small enough A s to which a temporal logic formula belongs 9 provides more chances for the system to be reduced efficiently. See [START_REF] Lang | Compositional verification of concurrent systems by combining bisimulations[END_REF][START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF] for details.

Action Priority

A classification of priority operators in process algebra is given in [START_REF] Cleaveland | Priority in process algebras[END_REF]. With respect to this classification, the operator presented in this section is static prioritized choice with global preemption. This priority operator is implemented in the tool EXP.OPEN [START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF] distributed in the CADP toolbox. Strong and orthogonal bisimulation equivalences [START_REF] Bergstra | Branching time and orthogonal bisimulation equivalence[END_REF] are congruences for this operator, which has lots of similarities with the priority operator of ACP [START_REF] Baeten | Syntax and defining equations for an interrupt mechanism in process algebra[END_REF]. Definition 4. We consider action formulas α, whose syntax and semantics w.r.t. a set of actions A 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
Operators true and ∧ are derived from the above using equations true = ¬false and

α 1 ∧ α 2 = ¬(¬α 1 ∨ ¬α 2 ).
Definition 5. An action priority rule π is an ordered pair of the form α ≻ α ′ , where α and α ′ are action formulas such that

[[α]] A ̸ = ∅, [[α ′ ]] A ̸ = ∅, and [[α]] A ∩ [[α ′ ]] A = ∅.
To an action priority rule π = α ≻ α ′ , we associate the 8 Adequacy of an equivalence and a logic means that two LTSs are equivalent iff they verify exactly the same formulas of the logic. 9 It was shown that such a smallest fragment is not unique [START_REF] Lang | Compositional verification of concurrent systems by combining bisimulations[END_REF]. Also, given As, deciding whether a formula belongs to L strong µ (As) is still an open problem.

following antisymmetric relation ≻ π,A :

≻ π,A = {(a, a ′ ) | a ∈ [[α]] A ∧ a ′ ∈ [[α ′ ]] A } Given π = α ≻ α ′ ,
we write greater A (π) for the set [[α]] A of labels of A that take priority over some other labels, and lesser A (π) for the set [[α ′ ]] A of labels of A that give priority to some other label, following rule π.

A priority set Ω is a set {π 1 , . . . , π n } of priority rules. To a priority set Ω, we associate the following relation ≻ Ω,A :

≻ Ω,A = ≻ π1,A ∪ . . . ∪ ≻ πn,A
We write > Ω,A for the transitive closure of ≻ Ω,A . A priority set Ω is valid if > Ω,A is a strict (partial) order relation, i.e., antireflexive and antisymmetric (and of course transitive, which is granted by definition).

If Ω is a valid priority set and P is the LTS (Σ, A, -→, p init ), then the expression "prio Ω in P " is defined as the LTS (Σ, A, -→ ′ , p init ) such that -→ ′ is the following set of transitions:

-→ ′ = {(p, a, p ′ ) | p a -→ p ′ ∧ (∀p ′′ ∈ Σ, a ′ ∈ A) p a ′ -→ p ′′ ⇒ ¬(a ′ > Ω,A a)}
Finally, we extend the operations greater A and lesser A to priority sets as follows:

greater This example illustrates that greater A (Ω) and lesser A (Ω) are not necessarily disjoint.

A (Ω) = πi∈Ω greater A (π i ) lesser A (Ω) = πi∈Ω lesser A (π i ) Example
Lemma 1. The following propositions hold:

• a ∈ greater A (Ω) iff a ∈ A and there exists a ′ ∈ A such that a > Ω,A a ′ . • a ∈ lesser A (Ω) iff a ∈ A and there exists a ′ ∈ A such that a ′ > Ω,A a.
Proof Immediate from the definitions of greater A (Ω) and lesser A (Ω). □

Sharp Congruences for Action Priority

It is well-known that, although strong bisimulation equivalence is a congruence for priority, (div)branching bisimulation equivalence is not. This latter fact can be illustrated by the following example. -→ q 1 . The LTS corresponding to this network is depicted in Figure 1. Note that there is no transition labelled by b from (p 1 , q 0 ) to (p 1 , q 1 ) because the outgoing transition labelled by a from (p 1 , q 0 ) has priority. P is branching equivalent to P ′ , which consists of the single transition

(p 0 , q 0 ) τ G G b (p 1 , q 0 ) a G G (p 2 , q 0 ) b (p 0 , q 1 ) τ G G (p 1 , q 1 ) a G G (p 2 , q 1 )
p ′ 0 a -→ p ′ 1 . The LTS corresponding to "prio a ≻ b in P ′ |[∅]| Q" is the sequence of transitions (p ′ 0 , q 0 ) a -→ (p ′ 1 , q 0 ) b -→ (p ′ 1 , q 1 )
. It is clear that (p 0 , q 0 ), from which actions a and b can be fired in any order, is not branching equivalent to (p ′ 0 , q 0 ), from which a can only be fired before b.

Theorem 1 below expresses however that (div)sharp bisimulation equivalence is a congruence for priority, provided (1) all actions that may take priority over some other action are strong and (2) τ does not give priority to any other action.

Theorem 1. If greater A (Ω) ⊆ A s , τ / ∈ lesser A (Ω), and P ∼ ♯As P ′ , then prio Ω in P ∼ ♯As prio Ω in P ′ . This also holds when replacing ∼ ♯As by ∼ @ ♯As .

Proof The key of the proof is that a state has a prioritized transition iff every ∼ ♯As bisimilar state also has a similar transition with same label, as this label belongs to As, and that τ -transitions cannot be cut by transitions with a higher priority. Formally, let R be a (div)sharp bisimulation w.r.t. As between P and P ′ . We show that R is also a (div)sharp bisimulation w.r.t. As between "prio Ω in P " and "prio Ω in P ′ ". Let (p 0 , p ′ 0 ) ∈ R and assume that there exists p 1 such that "prio Ω in P " has a transition p 0 a -→ p 1 . By definition of prio, P also has this transition.

For all labels a ′ such that a ′ > Ω,A a, we have a ′ ∈ greater A (Ω), which implies a ′ ∈ As since greater A (Ω) ⊆ As. By definition of prio, since "prio Ω in P " has a transition p 0 a -→ p 1 , then P has no transition of the form p 0 a ′ -→ p 2 (otherwise this transition would take priority over p 0 a -→ p 1 , which would then not occur in "prio Ω in P "). By definition of R, since (p 0 , p ′ 0 ) ∈ R and a ′ ∈ As, P ′ thus has no transition of the form p ′ 0 a ′ -→ p ′ 2 either. By definition of (div)sharp bisimulation, since P has a transition p 0 a -→ p 1 , and (p 0 , p ′ 0 ) ∈ R, then P ′ has a state p ′ 1 such that one of the following three conditions is satisfied in P ′ ; in each case, we show that the same condition is satisfied in "prio Ω in P ′ ":

1. P ′ has a transition p ′ 0 a -→ p ′ 1 . Since P ′ has no transition of the form p ′ 0 a ′ -→ p ′
2 with a ′ > Ω,A a, then "prio Ω in P ′ " does also have the same transition

p ′ 0 a -→ p ′ 1 . 2. a = τ , τ /
∈ A s , and p ′ 1 = p ′ 0 . This condition obviously keeps holding true in "prio Ω in P ′ ".

a /

∈ A s and P ′ has a sequence q 0 τ -→ . . .

τ -→ q n a -→ p ′ 1 (n ≥ 0) such that q 0 = p ′
0 and for all i ∈ 1..n, (p 0 , q i ) ∈ R. Since τ / ∈ lesser A (Ω), no label can take priority over τ -transitions, hence "prio Ω in P ′ " has the same sequence of τ -transitions q 0 τ -→ . . . τ -→ q n with q 0 = p ′ 0 and for all i ∈ 1..n, (p 0 , q i ) ∈ R. In particular, (p 0 , q n ) ∈ R, which implies that, since P has no transition of the form p 0 a ′ -→ p 2 with a ′ > Ω,A a, then P ′ has no transition of the form q n a ′ -→ p ′ 2 with a ′ > Ω,A a either. "prio Ω in P ′ " thus has the transition q n a -→ p ′ 1 .

Finally, if R is a divsharp bisimulation and if p 0 has a divergence in P , then this divergence is also present in "prio Ω in P ", because τ / ∈ lesser A (Ω). Therefore, p ′ 0 also has a divergence in P ′ because (p 0 , p ′ 0 ) ∈ R, and also in "prio Ω in P ′ ", again because τ / ∈ lesser A (Ω). □ Example 3. Back to Example 2, we know from Theorem 1 that if we replace respectively P and Q by any sharp equivalent LTSs, then we will get as the result an LTS that is sharp equivalent -hence branching equivalent-to the network "prio a ≻ b in P |[∅]| Q", provided a is a strong action. Note however that both P and Q are minimal for ∼ ♯{a} . They are therefore also minimal for any sharp bisimulation equivalence where a is a strong action.

Note that the proof of congruence of strong bisimulation for priority can be derived from the above proof by replacing the condition greater A (Ω) ⊆ A s by A s = A (the condition under which (div)sharp bisimulation coincides with strong bisimulation), which makes items 2 and 3 inapplicable and relaxes the (now useless) assumption τ / ∈ lesser A (Ω).

Sharp vs. Orthogonal Bisimulation

Sharp bisimulation has resemblances with orthogonal bisimulation [START_REF] Bergstra | Branching time and orthogonal bisimulation equivalence[END_REF], whose equivalence is also a congruence for many operators including choice and action priority, even if τ is subject to priority. We show the precise relationship between orthogonal and sharp bisimulations.

Definition 6 (Orthogonal bisimulation [START_REF] Bergstra | Branching time and orthogonal bisimulation equivalence[END_REF]). An orthogonal bisimulation is a symmetric relation R ⊆ Σ × Σ such that if (p, q) ∈ R then for all p a -→ p ′ , there exists q ′ such that (p ′ , q ′ ) ∈ R and either of the following holds:

1. a ̸ = τ and q a -→ q ′ , or 2. a = τ and q τ -→ and there exists a sequence of transitions q 0 τ -→ . . . τ -→ q n (n ≥ 0) such that q 0 = q, q n = q ′ , and for all i ∈ 1..n -1, (p, q i ) ∈ R.

• τ G G a • τ G G a • a • τ G G • τ G G • • τ G G a • a • τ G G • • a • (a) (b) (c)
Two states p and q are orthogonally bisimilar, written p ∼ ⊥ q, iff there exists an orthogonal bisimulation R such that (p, q) ∈ R.

Divergence-preserving orthogonal bisimulation, written ∼ @ ⊥ , is also defined in [START_REF] Bergstra | Branching time and orthogonal bisimulation equivalence[END_REF], by adding the same divergence-preserving condition as divbranching and divsharp bisimulations (see Definition 3).

The above definition shows that orthogonal bisimulation is stronger than branching bisimulation and weaker than strong bisimulation, with which it coincides if all actions are visible. As regards τ -transitions, orthogonal bisimulation may compress their sequences, but always preserves at least one. It is not a sharp bisimulation, as shown in the following example. ∈ A s , and in LTS (a) itself when τ ∈ A s . Interestingly, in our framework, LTS (a) can be reduced to LTS (c) if τ does neither give nor take priority to any other label. By contrast, orthogonal bisimulation enables only reduction to LTS (b) in all cases, which has twice as many states and four times more transitions than LTS (c).

Theorem 2 gives the precise relationship between orthogonal and sharp bisimulations.

Theorem 2. A relation R ⊆ Σ × Σ is an orthogonal bisimulation (resp. divergence-preserving orthogonal bisimulation) iff (1) R ∈ ∼ ♯A\{τ } (resp. ∼ @ ♯A\{τ } ) and (2) for all (p, q) ∈ R, p τ -→ implies q τ -→.
Proof This is quite intuitive by looking closely at the definitions of sharp bisimulation and orthogonal bisimulation. A formal equivalence proof in eight steps follows (we skip divergence-preservation, which is obvious). To help reading, we decorate each step of the proof by putting in shaded background the parts that will change (i.e., that will be either modified, moved, or removed) in the next step, and by putting in boxes the parts that changed in the current step.

R ∈ ∼ ♯A\{τ } ∧ (∀(p, q) ∈ R) (p τ -→ ⇒ q τ -→) ⇔ (∀(p, q) ∈ R, a ∈ A, p ′ ∈ Σ) (p a -→ p ′ ⇒ (∃q ′ ∈ Σ) (p ′ , q ′ ) ∈ R ∧ (q a -→ q ′ ∨ (a = τ ∧ τ / ∈ A \ {τ } ∧ q ′ = q) ∨ ( a / ∈ A \ {τ } ∧ (∃n ≥ 0, q 0 , . . . , qn ∈ Σ) q 0 τ -→ . . . τ -→ qn a -→ q ′ ∧ q 0 = q ∧ (∀i ∈ 1..n) (p, q i ) ∈ R))) ∧ (q, p) ∈ R ∧ (p τ -→ ⇒ q τ -→) by definition of ∼ ♯A\{τ } ⇔ (∀(p, q) ∈ R, a ∈ A, p ′ ∈ Σ) (p a -→ p ′ ⇒ (∃q ′ ∈ Σ) (p ′ , q ′ ) ∈ R ∧ (q a -→ q ′ ∨ ( a = τ ∧ q ′ = q) ∨ ( a = τ ∧ (∃n ≥ 0, q 0 , . . . , qn ∈ Σ) q 0 τ -→ . . . τ -→ qn τ -→ q ′ ∧ q 0 = q ∧ (∀i ∈ 1..n) (p, q i ) ∈ R))) ∧ (q, p) ∈ R ∧ (p τ -→ ⇒ q τ -→) because τ / ∈ A \ {τ } is trivial and a / ∈ A \ {τ } iff a = τ ⇔ (∀(p, q) ∈ R, a ∈ A, p ′ ∈ Σ) (p a -→ p ′ ⇒ (∃q ′ ∈ Σ) (p ′ , q ′ ) ∈ R ∧ (q a -→ q ′ ∨ ( a = τ ∧ (q ′ = q ∨ ((∃ n ≥ 0 , q 0 , . . . , qn ∈ Σ) q 0 τ -→ . . . τ -→ qn τ -→ q ′ ∧ q 0 = q ∧ (∀ i ∈ 1..n ) (p, q i ) ∈ R))) ∧ (q, p) ∈ R ∧ (p τ -→ ⇒ q τ -→) by factoring a = τ ⇔ (∀(p, q) ∈ R, a ∈ A, p ′ ∈ Σ) (p a -→ p ′ ⇒ (∃q ′ ∈ Σ) (p ′ , q ′ ) ∈ R ∧ (q a -→ q ′ ∨ (a = τ ∧ ( q ′ = q ∨ ((∃ n > 0 , q 0 , . . . , qn ∈ Σ) q 0 τ -→ . . . τ -→ qn ∧ q 0 = q ∧ qn = q ′ ∧ (∀ i ∈ 1..n -1 ) (p, q i ) ∈ R))) ∧ (q, p) ∈ R ∧ (p τ -→ ⇒ q τ -→) by reworking indices (qn becomes q n-1 , q ′ becomes qn) ⇔ (∀(p, q) ∈ R, a ∈ A, p ′ ∈ Σ) (p a -→ p ′ ⇒ (∃q ′ ∈ Σ) (p ′ , q ′ ) ∈ R ∧ ( q a -→ q ′ ∨ (a = τ ∧ ((∃ n ≥ 0 , q 0 , . . . , qn ∈ Σ) q 0 τ -→ . . . τ -→ qn ∧ q 0 = q ∧ qn = q ′ ∧ (∀i ∈ 1..n -1) (p, q i ) ∈ R))) ∧ (q, p) ∈ R ∧ (p τ -→ ⇒ q τ -→) because q ′ = q is subsumed by case n = 0 ⇔ (∀(p, q) ∈ R, a ∈ A, p ′ ∈ Σ) (p a -→ p ′ ⇒ (∃q ′ ∈ Σ) (p ′ , q ′ ) ∈ R ∧ (( a ̸ = τ ∧ q a -→ q ′ ) ∨ (a = τ ∧ ((∃n ≥ 0, q 0 , . . . , qn ∈ Σ) q 0 τ -→ . . . τ -→ qn ∧ q 0 = q ∧ qn = q ′ ∧ (∀i ∈ 1..n -1) (p, q i ) ∈ R))) ∧ (q, p) ∈ R ∧ (p τ -→ ⇒ q τ -→) because q τ -→ q ′ is subsumed by case n = 1 ⇔ (∀(p, q) ∈ R, a ∈ A, p ′ ∈ Σ) (p a -→ p ′ ⇒ (∃q ′ ∈ Σ) (p ′ , q ′ ) ∈ R ∧ ((a ̸ = τ ∧ q a -→ q ′ ) ∨ (a = τ ∧ q τ -→ ∧ ((∃n ≥ 0, q 0 , . . . , qn ∈ Σ) q 0 τ -→ . . . τ -→ qn ∧ q 0 = q ∧ qn = q ′ ∧ (∀i ∈ 1..n -1) (p, q i ) ∈ R))) ∧ (q, p) ∈ R by moving q τ -→ under the assumption a = τ ⇔ R ∈ ∼ ⊥ by definition of ∼ ⊥ □
As orthogonal bisimulation equivalence requires every visible action to be strong (only τ being weak), a consequence is that it is strictly stronger than any sharp bisimulation equivalence where τ is weak. In this case, the quotient of the system for sharp bisimulation equivalence cannot be larger than the one for orthogonal bisimulation equivalence. The fewer actions are declared as strong (i.e., the fewer actions being prioritized), the more sharp bisimulation can improve the reduction as compared to orthogonal bisimulation.

Equiv. R for system τ ∈ A<? τ ∈ A>? τ ∈ As? Equiv. R ′ for P i (i ∈ 0..n) yes - yes ∼ yes - no ∼ ⊥ no yes yes ∼ ♯As∪A> no yes no ∼ ♯As∪A> , ∼ ⊥ no no - ∼ ♯As∪A> ∼ ⊥ - - - ∼ ⊥ ∼ ♯As
Table 1 Weakest equivalence relations R ′ (among the relations addressed in this paper), which can be used on the subsystems P 0 , . . . , Pn for "prio

Ω in P 0 |[A 1 ]| . . . |[An]| Pn" to preserve the equivalence relation R (A< = lesser A (Ω) and A> = greater A (Ω)).
A practical consequence of Theorems 1 and 2 is that if one needs to generate the LTS of a network of the form "prio Ω in

(P 0 |[A 1 ]| . . . |[A n ]| P n )"
in a way that preserves ∼ ♯As (e.g., because the property to be verified on the network is in the modal µ-calculus fragment L strong µ (A s )), then P 0 , . . . , P n can be reduced with respect to ∼ ♯As∪A> beforehand, where A > = greater A (Ω) and A = A P1 ∪ . . . ∪ A Pn . Here, the set A s ∪ A > is optimal, in the sense that if we take any set A ⊂ strictly included in A s ∪ A > instead, we can always find instances of φ ∈ L strong µ (A s ), Ω, P 0 , . . . , P n , and A 1 , . . . , A n such that "prio

Ω in P 0 |[A 1 ]| . . . |[A n ]| P n " satisfies φ but "prio Ω in P 0 / ∼ ♯A⊂ |[A 1 ]| . . . |[A n ]| P n / ∼ ♯A⊂
" does not. However, for specific instances, it may happen that minimizing P 0 , . . . , P n with respect to ∼ ♯A⊂ will preserve φ; in particular, this is the case if

A > ⊆ A ⊂ and φ ∈ L strong µ (A ⊂ ∩ A s ) (which is a subset of L strong µ (A s ))
, or if minimizations with respectively ∼ ♯As∪A> and ∼ ♯A⊂ give the same result when applied to the LTS "P

0 |[A 1 ]| . . . |[A n ]| P n ".
Note however that the principle exposed in the previous paragraph requires τ / ∈ lesser A (Ω). Otherwise, one has to use either strong bisimulation ∼ or orthogonal bisimulation ∼ ⊥ , for which the congruence property holds. Note however that ∼ ⊥ can only be used in the case where τ / ∈ A s , because it cannot preserve ∼ ♯{τ } . Finally, if τ / ∈ lesser A (Ω) and τ / ∈ A s , then each P i can be reduced with respect to both ∼ ⊥ and ∼ ♯As∪A> . If in addition τ / ∈ A > , then the former is subsumed by the latter (because it is stronger), but this is not the case if τ ∈ A > . In the latter case, it may be worth combining both equivalences.

These principles, which are summarized in Table 1, also hold when replacing ∼ ♯As , ∼ ♯As∪A> , and ∼ ⊥ by their divergence-preserving variants ∼ @ ♯As , ∼ @ ♯As∪A> , and ∼ @ ⊥ , respectively. They could be implemented in a procedure that decides automatically which equivalence is to be used on the subsystems, e.g., in the SVL scripting language [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF] of CADP.

Finally, as the congruence property for orthogonal bisimulation does not require the condition τ / ∈ lesser A (Ω) (unlike sharp bisimulation), one might wonder whether an equivalence relation ∼ ♯As⊥ (and its divergence-preserving variant), which combines sharp bisimulation and orthogonal bisimulation as given by the following definition:

R ∈ ∼ ♯As⊥ ⇔ R ∈ ∼ ♯As ∧ (∀(p, q) ∈ R) p τ -→ ⇒ q τ -→
would have the congruence property without requiring τ / ∈ lesser A (Ω). (Note that ∼ ⊥ = ∼ ♯A\{τ }⊥ .) In other words, can we relax the definition of orthogonal bisimulation so as to consider a reduced set of strong actions instead of all visible actions, while preserving the congruence when τ may give priority to other actions? The answer is no, as shows the counter-example of Figure 3.

P = p 0 b τ G G p 1 b ~τ Ô Ô a p 2 p 3 ∼ ♯{b}⊥ q 0 τ Ô Ô b a G G q 1 q 2 = Q prio b ≻ τ in P = p 0 b p 2 ̸ ∼ ♯{b}⊥ q 0 b a G G q 1 q 2 = prio b ≻ τ in Q Fig. 3
Counter-example showing that combining sharp and orthogonal bisimulations does not allow the condition τ / ∈ lesser A (Ω) to be removed from Theorem 1.

5 Signature-Based Sharp Minimization

Partition-Refinement using Signatures

Efficient LTS minimization algorithms are generally based on partition refinement: starting from an initial partition10 {Σ} of the set of states Σ, refinement (i.e., block splitting) is applied until each block represents an equivalence class. Signature-based partition refinement was first proposed by Blom & Orzan [START_REF] Blom | Distributed Branching Bisimulation Reduction of State Spaces[END_REF][START_REF] Blom | A Distributed Algorithm for Strong Bisimulation Reduction of State Spaces[END_REF][START_REF] Blom | Distributed State Space Minimization[END_REF] as a conceptually simple way to implement partition refinement for strong and (div)branching bisimulations, among others. Although signature-based partition refinement algorithms are not optimal, with a worstcase time complexity of O(mn 2 ) where m is the number of transitions and n is the number of states (to be compared with the best-known worst-case time complexity of O(m log n) for both strong [START_REF] Valmari | Bisimilarity minimization in O(m log n) time[END_REF] and (div)branching [START_REF] Jansen | An O(m log n) algorithm for branching bisimilarity on labelled transition systems[END_REF] bisimulations), they are quite efficient in practice and suitable for distributed implementations 11 . In the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], the BCG_MIN tool implements sequential signature-based partition refinement for strong bisimulation, branching bisimulation, divbranching bisimulation, as well as stochastic and probabilistic extensions. Its companion tool BCG_CMP checks bisimulation equivalence between LTSs, by testing whether the initial states of both LTSs are in the same equivalence class. In this section, we present a signature-based partition refinement algorithm that implements sharp minimization and that is implemented in BCG_MIN and BCG_CMP.

We start from a generic signature-based partition refinement algorithm. For a bisimulation equivalence R, this algorithm uses a function sig R (s, P ), which returns the signature of a state s with respect to the current partition P . The signature σ of a state s in the partition P is a set of ordered pairs σ ∈ 2 A×P , each pair consisting of a label a ∈ A and a block B ∈ P . Its precise definition for strong, (div)branching, and (div)sharp bisimulations will be detailed later. Function sig R naturally extends to blocks B as follows:

sig R (B, P ) = {sig R (s, P ) | s ∈ B}
In a given partition P , a block B may be split into several blocks using the function split R (B, P ) defined as follows:

split R (B, P ) = {{s | s ∈ B ∧ sig R (s, P ) = σ} | σ ∈ sig R (B, P )}
When a block B cannot be split anymore, i.e., the signature is the same for all states of B, then split R (B, P ) returns the singleton set {B}. The generic signature-based partition refinement algorithm can be defined as follows: P := {Σ}; loop P ′ , P := P, B∈P split R (B, P ) until P = P ′ end loop; return P This algorithm can be refined to avoid unnecessary work. For instance, during an iteration, blocks can be partitioned into splitter and non-splitter blocks, so that signatures of blocks which are not predecessors of splitter blocks do not need to be split, as their signatures would remain unchanged. However, we do not detail such improvements further as they are not specific to sharp bisimulation.

Computing Signatures

We first recall the signature definitions for strong and (div)branching bisimulations. We will then define signatures for (div)sharp bisimulation and explain how they can be computed in practice. To this aim, we introduce a few notations.

Definition 7. We use the following notations, where a is a label, B a block, P a partition, s, s ′ are states, and n is a natural number:

τ B,P (s, s ′ ) = B ∈ P ∧ s, s ′ ∈ B ∧ s τ -→ s ′ τ n B,P (s, s ′ ) = (∃s 0 , . . . , s n ) s = s 0 ∧ (∀i ∈ 0..n -1) τ B,P (s i , s i+1 ) ∧ s n = s ′ τ * B,P (s, s ′ ) = (∃n ≥ 0) τ n B,P (s, s ′ ) τ ω B,P (s) = (∀n ≥ 0) (∃s ′ ∈ B) τ n B,P (s, s ′ ) τ P (s, s ′ ) = (∃B ∈ P ) τ B,P (s, s ′ ) τ n P (s, s ′ ) = (∃B ∈ P ) τ n B,P (s, s ′ ) τ * P (s, s ′ ) = (∃B ∈ P ) τ * B,P (s, s ′ ) τ ω P (s) = (∃B ∈ P ) τ ω B,P (s) s a -→ P B = B ∈ P ∧ (∃s ′ ∈ B) s a -→ s ′ s a =⇒ P B = B ∈ P ∧ (∃s ′ ∈ Σ, s ′′ ∈ B) τ * P (s, s ′ ) ∧ s ′ a -→ s ′′ ∧ (a ̸ = τ ∨ s / ∈ B)
The meaning of these notations can be phrased as follows. A τ -transition is called inert w.r.t. a state partition P (or simply inert if P is clear from the context) if its source and target states belong to the same block. States s and s ′ belonging to the same block B of partition P , the notation τ B,P (s, s ′ ) indicates that there is an inert transition from s to s ′ , τ n B,P (s, s ′ ) that there is a sequence of n inert transitions from s to s ′ , τ * B,P (s, s ′ ) that there is a sequence of (zero or more) inert transitions from s to s ′ , and τ ω B,P (s) that s is the source of an infinite sequence of inert transitions. The variants of these notations where B does not appear in the subscript have a similar meaning, except that the block to which s and s ′ belong is unspecified. The notation s a -→ P B indicates that s has a transition labelled by a to some state that belongs to block B of partition P and s a =⇒ P B that there is an arbitrary long sequence of inert transitions starting in s, which leads to a state that has a non-inert transition labelled by a to some state that belongs to block B of partition P .

The signatures of a state for respectively strong, branching, and divbranching bisimulations are defined as follows:

sig ∼ (s, P ) = {(a, B) | s a -→ P B} sig ∼ br (s, P ) = {(a, B) | s a =⇒ P B} sig ∼ dbr (s, P ) = sig ∼ br (s, P ) ∪ {(τ, B) | τ ω
B,P (s)} In the case of (div)branching bisimulation, computing signatures efficiently requires care, due to the necessity to compute the relation a =⇒ P , built upon the transitive closure of the relation τ P . In particular, one has to take care of cycles of τ -transitions. However, one can exploit the fact that all states in the same cycle of τ -transitions are (div)branching bisimilar. To this aim, we use a procedure SCC τ , which takes as input a block B and returns an ordered list (C 1 , . . . , C n ) such that:

i ∈ C i , s j ∈ C j , if s i τ -→ s j then j ≤ i.
Such a procedure can be implemented in linear-time using, e.g., a famous algorithm due to Tarjan [START_REF] Tarjan | Depth First Search and Linear Graph Algorithms[END_REF]. It is applied to the initial partition {Σ}, with a role that is twofold:

• All states in the same C i are (div)branching bisimilar and can therefore be compressed into a single representative state. In the divergence-preserving case, a self τ -loop is added on the representative state if there is a τtransition whose source and target are in C i . This allows the condition τ ω B,P (s) to be replaced by (∃s ′ ∈ Σ) τ * B,P (s, s ′ ) ∧ τ B,P (s ′ , s ′ ), which can be checked more efficiently. In the non divergence-preserving case, all such τ -transitions are eliminated.

• The ordering of SCCs C 1 , . . . , C n (or more precisely, of their representative states) is preserved when splitting blocks: representatives occur in the same relative order as long as they remain in the same block. The signatures of states in a block are computed following this order, so that if there is an inert transition s τ -→ P s ′ with s ′ ̸ = s, then the signature of s ′ is fully computed before starting to compute that of s. The signature of s can therefore be computed just by inspecting its immediate transitions and the signatures of the target states for those transitions which are inert.

For (div)sharp bisimulation, the signature of a state is a combination of the signatures for strong and (div)branching bisimulation, defined as follows:

sig ∼ ♯As (s, P ) = {(a, B) | (a ∈ A s ∧ s a -→ P B) ∨ (a / ∈ A s ∧ s a =⇒ P B)} sig ∼ @ ♯As (s, P ) = sig ∼ ♯As (s, P ) ∪ {(τ, B) | τ ω B,P (s)}
As for branching and divbranching bisimulations, we must be careful when computing the transitive closure of the relation τ P . However, it is not possible to compress cycles of τ -transitions beforehand, because states on such cycles are not necessarily bisimilar, as illustrated by the following example.

Example 5. The LTSs depicted in Figure 4 are ∼ ♯{a} bisimilar, while the rightmost one is minimal with respect to ∼ ♯{a} . Observe that states p ′ 0 and p ′ 2 belong to the same cycle of τ -transitions but are not ∼ ♯{a} bisimilar because p ′ 0 is source of a transition labelled by the strong action a, whereas p ′ 2 is not.

p 0 a G G τ p 1 p 2 τ G G p 3 τ a y y p ′ 0 a G G τ p ′ 1 p ′ 2 τ
Fig. 4 LTSs of Example 5

Instead, the procedure SCC τ is used each time the signatures of a block need to be updated, i.e., just before splitting the block. Details are presented in Algorithm 1, where we use the following notations:

• for all signatures σ, we write

σ \\ A s for {(a, B ′ ) | (a, B ′ ) ∈ σ ∧ a / ∈ A s }, i.e.
, the elements of σ whose label is not in A s • for all states s, we write succ B,P (s) for {(a,

B ′ ) | s a -→ P B ′ ∧ (τ ∈ A s ∨ a ̸ = τ ∨ B ′ ̸ = B)}, i.e.
, the signature corresponding to the non-inert immediate successors of s

The function call signatures_sharp(B, P ) returns a function sig that implements sig ∼ @ ♯As (s, P ) for each state s of block B. The algorithm performs the following steps:

1. The signatures corresponding to the non-inert successors of all states s of block B (line 2) and the (ordered) SCCs of the τ -transition graph internal to block B are computed (line 3). 2. Within each SCC, the signature elements that are common to all states of the SCC are accumulated in variable σ. For each state s of the SCC, σ is extended with all ordered pairs (a, B ′ ) such that a / ∈ A s and s a -→ B ′ (line 8), all ordered pairs (a, B ′ ) part of the signature of some state s ′ such that a / ∈ A s , τ P (s, s ′ ), and s ′ is in a distinct SCC from s (lines 9 to 11), and a divergence (τ, B) if s has an inert transition internal to the SCC (lines 12 and 13). To implement ∼ ♯As minimization (i.e., without preservation of divergences), lines 12 and 13 just have to be removed. 3. Finally, once σ contains the signature elements accumulated in all states of the SCC, the signatures of all states of the SCC are extended with σ (line 17).

Termination and Correctness

Termination and correctness of our algorithm rely on the termination and correctness of signatures_sharp(B, P ). For the whole algorithm, the argument is the same as for Blom & Orzan's algorithm.

Termination is immediate, because all five foreach loops enumerate values belonging to finite sets.

A correctness proof consists in showing that the equivalent assertions at lines 20 and 21, which are direct consequences of the invariant at line 5, hold. This invariant is obviously valid initially. We thus have to show that, under the assumption that the invariant holds in the current iteration and the fact It is easy to check that all pairs (a, B) added to sig (s) at line 2 actually belong to sig ∼ @ ♯As (s, P ) and that all pairs added to σ at lines 8, 11, 13, and finally to sig (s) at line 17 belong to sig ∼ @ ♯As (t, P ) for all states t in the same SCC as s. From the definition of sig ∼ @ ♯As (s, P ), it remains to show that, for all state s ∈ C i :

• if (∃a, B ′ ) a ∈ A s ∧ s a -→ P B ′ then (a, B ′ ) ∈ sig (s)
. This is ensured by the initialization of sig at line 2, because then (a, B ′ ) ∈ succ B,P (s).

• if (∃a, B ′ ) a / ∈ A s ∧ s a =⇒ P B ′ then (a, B ′ ) ∈ sig (s). If s a -→ P B ′ ,
then this is ensured by the initialization of sig at line 2 again. Otherwise, there exists n > 0 and s ′ such that τ n P (s, s ′ ) and s ′ a -→ P B ′ . Without loss of generality, the n inert transitions from s to s ′ can be decomposed into k transitions internal to the SCC C i followed by l transitions outside C i . Formally, we consider the largest natural number k such that there exist a state t ∈ C i and a natural number l satisfying n = k + l, τ k P (s, t), and τ l P (t, s ′ ). If l = 0, this means that t = s ′ , i.e., s ′ ∈ C i ; then (a, B ′ ) is added to σ in some iteration of line 8, since a / ∈ A s . Otherwise, l > 0. There is a first inert transition outside the SCC C i , i.e., there exists a state u / ∈ C i such that τ P (t, u) and τ * P (u, s ′ ). Due to the ordering of SCCs, we know that u ∈ C j for some j < i. Therefore, due to the invariant, (a, B ′ ) ∈ sig (u). Since s and t are both in C i , (a, B ′ ) is added to σ at line 11. Thereafter, σ is added to sig (s) at line 17.

• if τ ω B,P (s), then the condition at line 10 is necessarily falsified at least once for all states belonging to the SCC of s, and (τ, B) is added to σ at line 13. Thereafter, σ is added to sig (s) at line 17.

Time and Space Complexity

Computing the signatures of the states of a given block in Blom & Orzan's branching bisimulation reduction algorithm [START_REF] Blom | Distributed Branching Bisimulation Reduction of State Spaces[END_REF] requires to enumerate both the states of each block, as well as their outgoing transitions, similarly to our Algorithm 1. The most notable difference is the call to SCC τ at line 3, which is known to be feasible using Tarjan's algorithm in time linear in both the number of states in B and the number of transitions going out from states belonging to B and thus does not change the complexity of signature computation. Thus, the complexity of our algorithm is unchanged with respect to Blom & Orzan's, namely O(mn 2 ). The argument is similar for space complexity, which is O(mn).

Performance

Our minimization algorithm was implemented in the tools BCG_MIN and BCG_CMP and released since CADP version 2021-f "Saarbruecken" (May 2021). To assess the performance of this implementation, we made several measurements on a computer with Intel Core i5 quad-core processor at 2.5 GHz using 16 GB of RAM, running GNU/Linux.

First, we applied divsharp minimization to the 180 CTL problems 12 of the RERS 2019 challenge 13 . We compared the obtained LTS sizes to those obtained initially using the partial reduction algorithm presented in [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF], which was applied compositionally. The detailed results can be found in Appendix A. On average, the final LTS obtained using divsharp minimization has 7.69 times fewer states and 11.99 times fewer transitions than using partial divsharp reduction. The maximum is for problem 106#16, where the final LTS obtained using divsharp minimization has 3 states and 4 transitions instead of 527 states and 1314 transitions, that is 175 times fewer states and 328 times fewer transitions (i.e., a reduction rate of more than 99 %). In this experiment, the size of the largest LTS drops from 3363 states and 12427 transitions using partial sharp reduction down to 813 states and 2256 transitions using minimization. We also checked (without surprise) that the CTL properties were preserved by minimization, as theoretically expected.

Second, we compared the memory and time consumed by divsharp minimization in the two particular cases where the set of strong actions is either empty (∅) or maximal (A) with the (equivalent in terms of resulting LTS) respective minimization algorithms specialized for strong and divbranching already implemented in BCG_MIN since 2010. This comparison allows us both to validate our implementation in those two extreme cases, and to assess the overhead induced by checking action strongness/weakness, as well as the use of the Tarjan SCC algorithm implementing SCC τ , which is called to update the state signatures each time a block has been split.

We applied this comparison to four different packages of LTSs accumulated over time, represented in the BCG format of CADP: (1) a package BCG1 comprising 8995 "small" LTSs having less than 500, 000 transitions; (2) a package BCG2 comprising 542 "medium-size" LTSs having between 500, 000 and 5, 000, 000 transitions; (3) a package BCG3 comprising 265 "large" LTSs having between 5, 000, 000 and 50, 000, 000 transitions; and (4) the public benchmark VLTS14 comprising 40 LTSs ranging from 289 states and 1224 transitions up to 33, 949, 609 states and 165, 318, 222 transitions. The results are given in Tables 2 and3, where for each package, we give the average memory, time consumption, and number of LTSs whose minimization requires more than the 16 GB of RAM available on the computer to complete (column fails). Each overhead represents the value (memory or time) obtained on a package using the general divsharp minimization algorithm (using either A or ∅ as set of strong actions) divided by the value obtained on the same package using the corresponding specialized minimization algorithm (i.e., strong or divbranching minimization), once the entries concerning LTSs on which at least one minimization failed have been removed. Time is expressed in seconds and memory is expressed in megabytes. This comparison shows that the overhead is not negligible, but acceptable.

Our implementation of (div)sharp minimization is most useful in cases where the set of strong actions is somewhere between the two extremes A and ∅, where it cannot be replaced by the implementation of strong or (div)branching minimization. From these experiments, we extrapolate that in such cases, the overhead of (div)sharp minimization should be compensated enough by the gain on LTS sizes, compared to strong minimization. This is at least what happened in our experiments concerning the RERS 2019 challenge.

Theorem 2 implies that orthogonal minimization can be implemented as a minor variation of ∼ ♯A\{τ } minimization, by starting from an initial partition having at most two blocks, one block containing those states which are the source of a τ -transition (if any), and the other containing those which are not (if any). Finally, states of the quotient which were originally in the block containing states which are source of a τ -transition but are not anymore must

∼ dbr minimization ∼ @ ♯∅ minimization overhead ∼ @
♯∅ / ∼ dbr Table 3 Performance of ∼ @ ♯∅ minimization vs. dedicated ∼ dbr minimization be decorated with a self τ -loop. We implemented this algorithm in BCG_MIN, based on the implementation of sharp minimization.

Compositional Verification: A Toy example

In Section 4, we showed that sharp minimization cannot reduce less than orthogonal minimization, as long as τ is a weak action. In this section, we provide a toy example to illustrate how much compositional verification can be improved, using sharp minimization rather than orthogonal minimization. This example is crafted on-purpose to be favorable to sharp bisimulation. Our example is defined using two series of LTSs, namely P m (m ≥ 1) and Q n,m (n ≥ 0, m ≥ 1) defined as follows:

(∀m ≥ 1) P m = p 0 τ -→ p 1 b -→ p 2 . . . p 2m-2 τ -→ p 2m-1 b -→ p 2m (∀m ≥ 1) Q 0,m = q 0 a G G q 1 (∀m, n ≥ 1) Q n,m = prio a ≻ b in (Q n-1,m |[∅]| P m )
Informally, P m is a sequence of 2m transitions in which the labels τ and b alternate, whereas Q n,m is the interleaving of n instances of P m with an LTS consisting of a single transition labelled by a, to which the priority rule a ≻ b is applied.

We propose to generate the quotient of Q n,m for branching bisimulation equivalence, which is a sequence consisting of one transition labelled by a followed by nm transitions labelled by b. To this aim, we consider the compositional minimization strategy that consists in minimizing P m and the LTS corresponding to Q i,m (i ∈ 0..n) in sequence. In principle, branching minimization cannot be used for that purpose, as branching bisimulation equivalence is not a congruence for "prio a ≻ b". Instead, either minimization with respect to orthogonal bisimulation equivalence ∼ ⊥ or sharp bisimulation equivalence ∼ ♯{a} can be used, because they both preserve branching bisimulation equivalence and are congruences for parallel composition and "prio a ≻ b". A key difference is that P m is minimal for ∼ ⊥ , whereas all its τ -transitions are inert with respect to ∼ ♯{a} and can thus be eliminated. Since none of the LTSs has divergences, the choice among sharp and divsharp bisimulation does not matter.

We compare the effectiveness of this compositional verification strategy using both equivalence relations, for m and n ranging in the interval 1..9. The results are given in Tables 4 and5, in terms of the largest intermediate LTS size, i.e., number of states of the LTS corresponding to Q n,m before the final minimization. The tables show that while the largest intermediate LTS explodes using orthogonal minimization, it grows almost linearly in function of both n and m using sharp bisimulation. Note that the final LTS generated using sharp minimization is minimal for branching bisimulation equivalence in this example.

To understand the difference of effectiveness, consider the case Q 2,1 , whose unreduced LTS is depicted in Figure 5 (top). Using compositional sharp minimization, we obtain the LTS depicted in Figure 5 (bottom). Using compositional orthogonal bisimulation, we obtain the LTS depicted in Figure 5 (middle), which is branching equivalent but has a stairs shape. Similar stairs shapes can be observed in all LTSs obtained using orthogonal bisimulation, for larger values of m and n.

This illustrates that orthogonal bisimulation actually keeps most often more than one τ in every sequence of branching inert τ -transitions. Indeed, this can be seen in the above LTS, which is minimal for orthogonal bisimulation equivalence as none of its τ -transitions is inert with respect to orthogonal bisimulation:

• States t 2 , t 3 , and t 4 are not orthogonally equivalent to respectively t 5 , t 6 , and t 7 , as each of the former is the source of a τ -transition, whereas each of the latter is not. • State t 1 is not orthogonally equivalent to t 3 , as t 3 is the source of a transition labelled by b, whereas t 1 is not. • Finally, state t 0 is not orthogonally equivalent to t 2 as the transition labelled by a going out of t 0 goes to state t 1 , which we have just shown to be not orthogonally equivalent to t 3 , the target of the transition labelled by a going out of t 2 .

In terms of verification time and memory usage, the compositional verification scenario to generate Q 9,9 takes:

• 18 minutes and 4.5 GB of memory, yielding an LTS with 4, 686, 835 states and 28, 120, 969 transitions when orthogonal minimization is used • 18 seconds and 4 MB of memory, yielding an LTS with 83 states and 82 transitions when ∼ ♯{a} minimization is used

Q 2,1 = (q 0 , p 1 , p 0 ) a G G τ 8 8 (q 1 , p 1 , p 0 ) b G G τ 8 8 (q 1 , p 2 , p 0 ) τ G G (q 1 , p 2 , p 1 ) b (q 0 , p 0 , p 0 ) τ V V a G G τ 8 8 (q 1 , p 0 , p 0 ) τ V V τ 8 8
(q 0 , p 1 , p 1 ) a G G (q 1 , p 1 , p 1 ) b V V b 8 8 (q 1 , p 2 , p 2 ) (q 0 , p 0 , p 1 ) a G G τ V V (q 1 , p 0 , p 1 ) b G G τ V V (q 1 , p 0 , p 2 ) τ G G (q 1 , p 1 , p 2 ) b y y Q 2,1 / ∼ ⊥ = t 0 τ a G G t 1 τ t 2 τ a G G t 3 τ b G G t 4 τ t 5 a G G t 6 b G G t 7 b G G t 8
state equivalent state(s) in Q 2,1 t 0 (q 0 , p 0 , p 0 ) t 1 (q 1 , p 0 , p 0 ) t 2 (q 0 , p 1 , p 0 ), (q 0 , p 0 , p 1 ) t 3 (q 1 , p 0 , p 1 ), (q 1 , p 1 , p 0 ) t 4 (q 1 , p 2 , p 0 ), (q 1 , p 0 , p 2 ) t 5 (q 0 , p 1 , p 1 ) t 6 (q 1 , p 1 , p 1 ) t 7 (q 1 , p 1 , p 2 ), (q 1 , p 2 , p 1 )

t 8 (q 1 , p 2 , p 2 ) Q 2,1 / ∼ ♯{a} = s 0 a G G s 1 b s 3 s 2 b o o state equivalent state(s) in Q 2,1 s 0 (q 0 ,
p 0 , p 0 ), (q 0 , p 1 , p 0 ), (q 0 , p 0 , p 1 ), (q 0 , p 1 , p 1 ) s 1 (q 1 , p 0 , p 0 ), (q 1 , p 0 , p 1 ), (q 1 , p 1 , p 0 ), (q 1 , p 1 , p 1 ) s 2 (q 1 , p 2 , p 0 ), (q 1 , p 0 , p 2 ), (q 1 , p 2 , p 1 ), (q 1 , p 1 , p 2 ) s 3 (q 1 , p 2 , p 2 )

Fig. 5 LTSs Q 2,1 (top), Q 2,1 / ∼ ⊥ (middle), and Q 2,1 / ∼ ♯{a} (bottom).
As expected, both LTSs are branching equivalent. Using ∼ ♯{a} minimization, we were able to generate Q 40,40 in 189 seconds using 6.4 MB of memory.

Following Theorem 2, we know that the quotient of an LTS w.r.t. orthogonal bisimulation should not have more than twice the number of states as the quotient of the same LTS w.r.t. sharp bisimulation when all visible actions are strong. This shows that the gains observed here are mostly due to the possibility offered by sharp bisimulation to consider some actions as weak, such as b in this example.

Case Study: Bully Leader Election

As an example of a priority system, we consider a slight variation on the classic bully leader election algorithm [START_REF] Garcia-Molina | Elections in a Distributed Computing System[END_REF]. We assume a system of n nodes, or agents, each with a unique numeric identifier, or id. In the typical bully election, each agent continuously broadcasts advertisement messages with the id of their current leader. Initially, every agent regards itself as the leader; however, whenever an agent receives a message with an id i lower than its current leader, it appoints i as its new leader. Therefore, the whole system eventually elects the agent with the lowest identifier.

Our variation is written in LAbS [START_REF] De Nicola | Multi-agent systems with virtual stigmergy[END_REF], a simple language where agents cannot perform explicit message passing, but instead exploit an indirect communication mechanism based on stigmergy variables [START_REF] Pinciroli | Buzz: An extensible programming language for heterogeneous swarm robotics[END_REF]. Just like an ordinary variable, a stigmergy variable may be assigned to (denoted by x <~e, where e is an arithmetic expression) or referenced within an expression. When an agent assigns a value to one such variable, say x, the value is timestamped with the time of assignment. 15 Asynchronously, this will trigger a stigmergic propagation where the agent sends its (timestamped) value of x to all its neighbours. Neighbourhood is defined in the system specifications as a predicate over the state of a message sender and its potential receiver. This is called a link predicate, and LAbS allows different variables to have different predicates. Receivers will replace their own value with the received one if the latter is newer (i.e., it has a higher timestamp). Otherwise, they ignore the message. The semantics of LAbS assume that, whenever a propagation takes place, every receiver gets the message and possibly update their state atomically, similarly to a multi-party rendezvous.

Correspondingly, whenever an agent accesses a stigmergy variable x to evaluate an expression, it will later emit a confirmation message to ask neighbours whether its value for x is sufficiently up-to-date. Neighbours will still receive a timestamped value of x, and update their value if the received one is newer. However, in the case their local value is newer than the received one, they will (asynchronously) respond by propagating it in turn. These mechanisms allow knowledge to spread through the system and for new values to eventually replace old ones, which ensures eventual consistency.

In this example (Listing 1), each agent stores the id of its current leader in a stigmergy variable ℓ, defined (and initialized to n) at line 6. The definition is preceded by a line that defines the link predicate for the variable (line 5). In this case, the predicate is true, meaning that stigmergic messages will be broadcasted to every agent in the system. We assume identifiers of agents to be in the range [0, n -1], and that ℓ is initially set to n for every agent. As the system evolves, each agent repeatedly assigns its own id to ℓ, but only as long as ℓ > id (lines 12-13). The repetitiveness of the agents' behaviour is implemented by the recursive call to Behavior at line 14.

Due to the stigmergic interaction mechanisms, it may happen that agents with lower ids choose one with a higher id as their leader, simply because that value is newer. However, high-id agents will eventually receive a value for ℓ that makes them stop, while the one with the lowest id will be able to perform one last assignment and one last broadcast to win the election.

A system of autonomous agents such as this one may be seen as a network of LTSs, namely one per agent plus an additional one that stores information about the timestamps. For the scope of this work, we developed a workflow [START_REF] Di Stefano | Compositional verification of stigmergic collective systems[END_REF] in the SLiVER tool 16 [14, 12] that turns a LAbS specification into an LNT program with this network structure, shown in Listing 2. Intuitively, agents in this LNT program may perform refresh actions to obtain a fresh timestamp for the stigmergy variable ℓ; stig actions to signal that they have set some stigmergic variable to a new value; 17 and request actions to compare timestamps with the sender of a stigmergy message. These actions are always decorated with the identifier of the agent performing them. For instance, a transition whose label starts with "request !0" denotes that the agent with id 0 is performing a request action. To perform a request or refresh action, an agent must synchronize with the timestamp process, whereas stig actions may be end par end hide end par end process performed freely. The timestamp server performs an action debug(...) before every synchronization, to display its current internal state. This action does not affect the behaviour of the system in any way and is just a convenience feature to show more detailed information to the user. Additionally, agents may synchronize to exchange stigmergy messages (over the put, qry gates), or to decide which agent should act next (over the tick gate). We hide the put, qry gates, and leave tick visible.

A potential drawback of this encoding is that agents may react to a new message in any order: thus, each message-passing operation (which, as stated earlier, is atomic in the LAbS semantics) is split into a diamond with a large number of intermediate states and transitions which all lead to a single final state. What is worse, the size of these diamonds increases exponentially with the number of agents, as well as the number of transitions that each agent must perform to carry out the message reception. Similar diamonds can appear in the initialization phase of the system, where each agent initializes its state (in our example, setting ℓ to n) in any order.

By prioritizing some actions over the others, we can collapse these diamonds into much smaller ones. In the best case, i.e., when every intermediate state has a single outgoing transition that takes priority over all the others, the diamond effectively collapses into a single, representative path. Consider, for instance, the diamond in Figure 6: this is what we would obtain when three agents with ids 0, 1, 2 independently react to the same message (sent by a fourth agent, not shown). For the sake of simplicity, we assume that each agent of id n only has to perform one transition, which is labelled by a n . If we assume the priority relation a 0 ≻ a 1 ≻ a 2 during LTS generation, all the dashed transitions in the diamond will be cut on the fly, leaving only the sequence

• a0 -→ • a1 -→ • a2 -→ •.
To demonstrate the effect of priorities on these systems more concretely, we consider two leader election systems leader3 and leader4, containing

• a0 G G a2 0 0 • a2 0 0 • a1 d d a2 0 0 a0 G G • a1 d d a2 0 0 • a0 G G • • a1 d d a0 G G • a1 d d
Fig. 6 Example of a diamond when 3 agents perform independent actions a 0 , a 1 , and a 2 . Dotted transitions are cut by applying the priority relation 6. An arrow x → y denotes that x ≻ y.

a 0 ≻ a 1 ≻ a 2 . refresh !0 ... G G refresh !1 ... G G v v refresh !2 ... G G r r refresh !3 ... q q stig !0 ... G G stig !1 ... G G v v stig !2 ... G G r r stig !3 ... q q request !0 ... G G request !1 ... G G request !2 ... G G request !3 ...
respectively 3 and 4 agents, plus the aforementioned timestamp server. After translating each system to an LNT program, we use CADP to generate the LTS S of its Main process, describing the whole system (as shown in Listing 2).

We then reduce S modulo strong, orthogonal and divbranching bisimulation, obtaining three additional LTSs S ∼ , S ⊥ , and S dbr . We also generate an LTS S Ω = prio Ω in S, and minimize it modulo the aforementioned bisimulations to obtain S Ω ∼ , S Ω ⊥ , and S Ω dbr . The priority relation Ω used in this phase is visualized in Figure 7, namely, refresh !. * ≻ stig !. * ≻ request !. * , regardless of which agent is performing it; furthermore, whenever two or more agents may perform the same action, the agent with the lowest identifier has the highest priority. Having set these priorities, we can now find a corresponding set of strong actions A s that satisfies the requirements of Theorem 1, namely the set comprising all actions of the form "refresh !. * ", "stig !. * ", and "request !. * ". Thus, we also reduce both S and S Ω modulo divsharp bisimulation w.r.t A s , and denote by S ♯ and S Ω ♯ the resulting LTSs. Notice that we merely use divbranching reduction as a theoretical optimum that divsharp minimization may achieve, since in general ∼ dbr is not a congruence for priorities.

Table 6 shows the number of states and transitions for each LTS, and the overall resources (time and memory) needed to generate the LTS with priorities. Reported times only refer to the actual LTS generation process, i.e., excluding the time required to compile the LNT sources. On the one hand, we can observe that orthogonal bisimulation is slightly more effective than strong bisimulation. On the other hand, divsharp minimization proves even more effective, producing LTSs as small as the ones obtained by divbranching minimization (i.e., the optimum). Notice that, since A s satisfies the premises of Theorem 1 with respect to the priority rules Ω, we could have obtained the same LTS as S Ω ♯ by minimising S modulo ∼ @ ♯As before applying the priority rules to the resulting LTS. https://www.overleaf.com/project/621e0ce6c0f594d6d5119a21 Another insight from Table 6 is that adding one agent induces a 10-fold increase in the size of the LTS. This state space explosion makes "naive" state space generation impractical for larger systems: in fact, we tried generating the LTS for a leader5 system but hit a 1-hour timeout limit. Therefore, we performed additional experiments using a compositional strategy, namely root leaf reduction [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF], to see whether it would bring significant improvements to state space generation over the sequential approach used so far. This strategy consists in generating and minimizing the individual LTSs in the network (the leaves), then composing them to generate the LTS of the network, and finally performing one last minimization of the composite LTS (the root). If any priority rules are given, they are applied on the fly during composition. In our experiments, we carry out minimizations using either orthogonal or divsharp bisimulation. Results are shown in Table 7. In each sub-table, we first report the size of the Timestamp and Agent processes, before and after minimization. Once the individual LTSs are ready, we compose them to obtain the LTS for both the unprioritized and prioritized systems.

These two composite LTS are denoted Main and prio Ω in Main in our table, respectively. Notice that in both cases we report the size of the composite LTS both before and after performing the "root" minimization. We also report the time and memory needed to generate each LTS with divsharp reduction. We omit measurements related to orthogonal reduction, as they do not significantly differ from the reported ones. Again, all reported times ignore the overhead introduced by LNT compilation.

Notice that, in a system of n agents, the procedure will generate n Agent LTSs. These have the same size, but different ids and therefore a potentially different behaviour. For these LTSs, we report the average time and memory consumption. To allow easier comparisons with the data in Table 6, the Main and prio Ω in Main lines, before and after reduction, report aggregate measures. Namely, the "time" column shows the time needed to generate each individual LTS, plus the time required to compose them (and optionally to reduce the composite LTS); the "memory" column reports the maximum amount of memory consumed at any moment during the whole process.

From the table, one can still appreciate some form of explosive state space growth as the number of agents in the system increases. This is most noticeable in the Timestamps process, which displays the same 10-fold size increase seen in the LTSs of Table 6. In any case, the compositional procedure appears to handle larger systems more gracefully than the sequential one, at the cost of being slightly less effective on smaller instances. In fact, when the system contains only 3 agents, the sequential approach is faster, requiring 2 seconds to generate the LTS of the priority system compared to the 5.80 s of the compositional procedure. The most likely explanation for this is that the intermediate steps needed by the compositional approach introduce some amount of overhead, which at this small scale is significant. Still, we observe that the procedure is slightly more memory-efficient, consuming around 300 kB less than the sequential approach. However, with 4 agents we can already see that the sequential approach takes 110.14 s, while the compositional procedure finishes in 7.05 s. Memory savings are also significant, as the compositional approach uses 6.3 MB less than the sequential one to complete its task. These observations suggest that the latter may scale better with bigger systems. These gains become even more evident on leader5, where the sequential procedure times out after 1 hour, but the compositional one is able to complete the task in 9.79 s. Even when considering the LNT compilation overhead, the whole procedure finishes in less than a minute (namely, 55.43 s).

Related Work

The current work takes its place in the history of bisimulation tools, an extended survey of which can be found in [START_REF] Garavel | Equivalence Checking 40 Years After: A Review of Bisimulation Tools[END_REF].

Several approaches for priority in process languages have been proposed since the early 1980s. The interested reader may have a look at the introduction of [START_REF] Cleaveland | Priority in process algebras[END_REF] for a classification. Our aim in this paper is not to promote one approach over the other, but more pragmatically to provide a theoretical framework that suits well with the priority operator that was implemented in the EXP.OPEN tool of CADP more than 15 years ago.

Another congruence for parallel composition and priority in a setting close to ours is prioritized weak bisimulation equivalence [START_REF] Cleaveland | Priority in process algebras[END_REF], which is based on weak (a.k.a. observational) bisimulation [START_REF] Milner | Communication and Concurrency[END_REF] rather than (div)branching. Weak bisimulation equivalence is known to have less efficient algorithms than Verification of Priority Systems Using Sharp Bisimulation (div)branching. As sharp bisimulation, prioritized weak bisimulation takes into account the set of prioritized actions in its definition, which is however much more involved than sharp bisimulation. We are not aware of any available implementation of prioritized weak bisimulation. Also, there are differences in the definition of the priority operator (based on CCS), which makes it difficult to precisely compare both approaches in practice.

Orthogonal minimization has to face a similar problem as sharp minimization, namely states in the same cycle of τ transitions are not necessarily orthogonally bisimilar. This issue was addressed by Vu [START_REF] Vu | Deciding orthogonal bisimulation[END_REF], whose algorithm, similarly to ours, also relies on a linear-time procedure for computing the SCCs of a directed graph applied inside blocks, initially and after each block splitting. This preserves the time complexity of the algorithm it was based on, namely Groote & Vaandrager's algorithm for branching minimization [START_REF] Groote | An efficient algorithm for branching bisimulation and stuttering equivalence[END_REF]. The worst-case time complexity O(mn) of this algorithm (where n and m are respectively the numbers of states and transitions of the LTS) is lower than that of signature-based minimization O(mn 2 ) on which our algorithm is based. However, an experimental evaluation would be interesting to gain more insight, as our experience indicates that signature-based minimization may be more efficient than Groote & Vaandrager's algorithm in many practical cases,18 see e.g., [START_REF] Groote | An O(m log n) algorithm for computing stuttering equivalence and branching bisimulation[END_REF] (Fig. 9, right). Unfortunately, we could not find any implementation of Vu's algorithm. Orthogonal bisimulation is also implemented in the tool Sigref [START_REF] Wimmer | Sigref -A symbolic bisimulation tool box[END_REF], which uses a symbolic representation of state spaces (in the form of Binary Decision Diagrams) and implements the transitive closure of τ -inert transitions using the iterative squaring method of symbolic model checking [START_REF] Burch | Sequential circuit verification using symbolic model checking[END_REF].

Going further on complexity, there exists a recent algorithm for (div)branching minimization, with worst-case time complexity O(m log n) [START_REF] Jansen | An O(m log n) algorithm for branching bisimilarity on labelled transition systems[END_REF]. The question whether this algorithm could be adapted to implement (div)sharp minimization while keeping its complexity is open.

Inductive sequentialization [START_REF] Kragl | Inductive sequentialization of asynchronous programs[END_REF] is a technique where an asynchronous program is analysed by constructing a sequential reduction, i.e., a sequential program that captures every behaviour of the original up to reordering of commutative actions. This is similar to our use of priorities to remove diamonds from LTSs that encode a concurrent system (e.g., the leader election of Section 7). Both approaches still require a certain amount of creative work. Inductive sequentialization requires one to come up with an idealized sequential execution, while our approach requires finding an adequate priority set. Applying priorities to a system does not generally preserve its behaviour. In other words, typically P and prio Ω in P are not bisimilar. However, if the altered behaviour does not affect the satisfaction of a given formula φ, then verifying φ against the prioritized system can be seen as a form of partial order reduction [START_REF] Alur | Partial-order reduction in symbolic state space exploration[END_REF]. This is what happens in our case study: since we know that the prioritized system conforms to the semantics of LAbS, we are not interested in the portion of state space that gets cut thanks to the priority operator. These reductions are known to be effective in countering state-space explosion [START_REF] Alur | Partial-order reduction in symbolic state space exploration[END_REF][START_REF] Flanagan | Dynamic partial-order reduction for model checking software[END_REF]. In order to be generally applicable they usually require the system of interest to be equipped with a partial order semantics, whereas LAbS and LNT currently rely on interleaving semantics.

Conclusion

Sharp bisimulation was already known as an efficient way to tackle verification problems by taking a fine account of the temporal logic formula to be verified and by being suitable for compositional verification. In this paper, we extended the set of fundamental results on sharp bisimulation equivalence, by showing that it may be a for action priority operators. Therefore, it is also appropriate to verify systems with priority compositionally. The relationship between sharp bisimulation and orthogonal bisimulation, another congruence for priority, was clarified.

We also solved the problem of minimizing a process with respect to sharp bisimulation equivalence in an efficient way, providing an extension of Blom & Orzan's signature-based partition-refinement algorithm for (div)branching minimization. The extension is not trivial, as sharp bisimulation equivalence does not allow cycles of τ -transitions to be eliminated beforehand, unlike branching bisimulation. Instead, blocks must be traversed using a linear-time algorithm for detecting strongly-connected components at each partitionrefinement step. Our results are implemented in tools in CADP, namely BCG_MIN and BCG_CMP for (div)sharp minimization and comparison, and EXP.OPEN for action priority and other LTS composition operators.

We applied those tools successfully to a crafted toy example, showing that using sharp bisimulation may produce LTSs that are several orders of magnitude smaller than those obtained using orthogonal bisimulation, and to a case study in the domain of collective adaptive systems, where action priority is used to restrict the state space. Remarkably, minimization of the composed processes with respect to divsharp bisimulation equivalence offers more reduction than strong and orthogonal bisimulations, and even as much reduction as divbranching bisimulation. Yet, contrary to (div)branching bisimulation, (div)sharp bisimulation offers all theoretical guarantees for the resulting state space to preserve the semantics of the non-reduced system. The effect of (div)sharp minimization on state space size could be greatly amplified in systems whose network definition is hierarchical, the composed processes being themselves the result of compositions and minimizations. The initialization creates two empty sets Zput, Zqry that will track pending stigmergy messages, and sets the agent's state to its (potentielly nondeterministic) initial as described in the input specifications, implemented by the helper process InitAgent. The agent's state includes its local stigmergy variables L and a set of local variables I that are not subject to stigmergic interaction, but may influence the agents' link predicates.

The event loop allows the agent to perform an individual action, wait for another agent to make its move, and to send or react to a stigmergy message. Notice that this scheme also features an additional gate dead, which we omitted from the main text for sake of brevity. It will be used by the agent to signal whether it is in a deadlocked state. Individual actions. Listing 5 shows the behaviours related to individual actions in more detail. These behaviours are guarded by a multi-party rendezvous on the tick gate. Every agent can always do nothing and allow a different one to act (line 2), or try and perform an action (lines 5-17). When multiple agents are all willing to make a move, the rendezvous will force the system to choose one.

Furthermore, an agent may only try to make a move if it has no pending messages (this is specified in the semantics of LAbS): the only if block at line 5 implements this rule by making this branch of the select deadlocked until the condition is met. Every individual action in the original behaviour is encoded into its own process action _ <x> (lines 8-14). These processes are always guarded by a condition on the pc variable: this variable is the program counter of the agent and tracks its execution point. Since LAbS also has guarded processes (like the ℓ > id -> . . . one in Listing 1, lines [START_REF] Di Stefano | Verifying temporal properties of stigmergic collective systems using CADP[END_REF][START_REF] Di Stefano | Compositional verification of stigmergic collective systems[END_REF][START_REF] Di Stefano | Combining SLiVER with CADP to analyze multi-agent systems[END_REF], some of these actions may be further guarded by additional conditions. Thus, before getting to choose the next action to perform, we evaluate a function canProceed that tells us whether at least one of these guards can be satisfied (line 7). If this is not the case, we send the agent to a sink state where it endlessly performs a dead action to signal it is deadlocked (line 15).

Exchange of stigmergy messages. An exchange of a message is triggered by a rendezvous on either the put or qry gate. This, combined with the fact that actions over tick also require a multi-party rendezvous, guarantees that message exchange never overlap with each other or with individual actions. We only report the details about put behaviour, as the one for qry is quite similar. To propagate a variable, an agent must have at least one variable in its set of pending messages Zput: if this is the case, the agent may nondeterministically select one of these variables, offer it over put along with additional information, and remove the variable from Zput (lines 2-2). Each receiver, on the other hand, waits until a rendezvous on put becomes available (that is, until another agent s is willing to propagate: line 13). Then, it gets the appropriate timestamp comparison from the timestamp server, by means of a request transition (line 14). Finally, if the link predicate holds and the comparison value is GREATER, it overwrites its value for variable x with the one coming from the sender (lines [START_REF] Flanagan | Dynamic partial-order reduction for model checking software[END_REF][START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF][START_REF] Garavel | Equivalence Checking 40 Years After: A Review of Bisimulation Tools[END_REF][START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF][START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. It also adds x to the pending propagation messages and removes it from that of pending confirmation messages, since receiving a new value is enough to conclude that the previous one was not up-to-date (lines 20-21).

1 .

 1 Let A be the set of actions {a, b, c, d, e, f } and Ω be the priority set {a ≻ b, b ≻ c∨d, d ≻ ¬(a∨b∨c∨d∨e)}, denoting that (using transitivity): a takes priority over b, c, d, and f ; b takes priority over c, d, and f ; and d takes priority over f . We have greater A (Ω) = {a, b, d}, and lesser A (Ω) = {b, c, d, f }.

Fig. 1 LTS of Example 2 Example 2 .τ-→ p 1 a-→ p 2

 12212 Fig. 1 LTS of Example 2

Fig. 2

 2 Fig. 2 Three LTSs of Example 4

Example 4 .

 4 Consider the three LTSs displayed in Figure 2. Orthogonal minimization of LTS (a) results in LTS (b). However, sharp minimization of LTS (a) results in LTS (c) when τ /

Fig. 7 A

 7 Fig.7A representation of the priority relation Ω used for the experiments in Table6. An arrow x → y denotes that x ≻ y.

•

  C 1 , . . . , C n are the SCCs (Strongly Connected Components) of the τtransition graph of B, i.e., a partition of B such that any two states s and s ′ are in the same SCC C i iff s States that are not part of any cycle of τ -transitions are therefore singletons in {C 1 , . . . , C n }. • For all s

	τ

* -→ s ′ τ * -→ s.

  Algorithm 1 Divsharp signature computation 1 function signatures_sharp(B, P ) is 2 foreach s ∈ B loop sig(s) := succ B,P (s) end loop; 3 (C 1 , . . . , C n ) := SCC τ (B);

	4	foreach i ∈ 1..n loop
	5	-invariant: (∀j ∈ 1..i -1) (∀s ∈ C j ) sig(s) = sig ∼ @ ♯As (s, P )
	6	σ := ∅;
	7	foreach s ∈ C i loop
	8	σ := σ ∪ (sig(s) \\ A s );
	9	foreach s ′ such that τ P (s, s ′ ) loop
	10	if s ′ / ∈ C i then
	11	σ := σ ∪ (sig(s ′ ) \\ A s )
	12	else
	13	σ := σ ∪ {(τ, B)}
	14	end if
	15	end loop
	16	end loop;
	17	foreach s ∈ C

i loop sig(s) := sig(s) ∪ σ end loop 18 -assert:

(∀s ∈ C i ) sig(s) = sig ∼ @ ♯As (s, P ) 19 end loop; 20 -assert: (∀j ∈ 1..n) (∀s ∈ C j ) sig(s) = sig ∼ @ ♯As (s, P ) 21 -assert: (∀s ∈ B) sig(s) = sig ∼ @ ♯As (s, P ) 22

return sig 23 end function that the SCCs C i are ordered, the initialization of sig at line 2 combined with the code from line 6 to 17 ensure the assertion expressed at line 18, which ensures that the invariant still holds in the next iteration.

Table 4

 4 Largest intermediate LTS size (in number of states) during compositional ∼ @

									n
			1	2	3	4		5	6		7	8	9
		1	5	13	24	38		55	75		98	124	153
		2	7	29	81	183		360	642		1064	1666	2493
		3	9	53	202	596		1480	3246		6482	12,028	21,039
		4	11	85	411	1493	4465	11,595		27,041	57,931	115,848
	m	5	13	125	732	3154	11,021	33,045		88,102	213,944	481,356
		6	15	173	1189	5923	23,670	80,456	241,346	655,060	1,637,628
		7	17	229	1806	10,208	45,910	174,432	581,414	1,744,216	4,796,568
		8	19	293	2607	16,481	82,375	345,945	1,268,435	4,167,685	12,503,025
		9	21	365	3616	25,278	138,995	639,343	2,557,338	9,133,316	29,683,243
	minimization of Qn,m								⊥
									n
					1	2	3	4	5	6	7	8	9
				1	3	5	7	9	11	13	15	17	19
				2	4	10	16	22	28	34	40	46	52
				3	5	17	29	41	53	65	77	89	101
				4	6	26	46	66	86	106	126	146	166
			m	5	7	37	67	97	127	157	187	217	247
				6	8	50	92	134	176	218	260	302	344
				7	9	65	121	177	233	289	345	401	457
				8	10	82	154	226	298	370	442	514	586
				9	11	101	191	281	371	461	551	641	731

Table 5

 5

Largest intermediate LTS size (in number of states) during compositional ∼ ♯{a} minimization of Qn,m Listing 1 Bully leader election in LAbS.

  Listing 2 Structure of an LNT program encoding a LAbS system.

	process Main[refresh, request, debug, tick, ... : any] is
	par refresh, request in
	Timestamps [refresh, request, debug]
	||
	hide put, qry: any in
	par tick, put, qry in
	Agent [tick, put, qry, refresh, request, stig] (ID(0))
	||
	Agent [tick, put, qry, refresh, request, stig] (ID(1))
	|| • • • ||
	Agent [tick, put, qry, refresh, request, stig] (ID(n -1))

Table 6

 6 State space generation of leader election systems (with and without priorities) using different bisimulations.

			Main			prio Ω in Main
			states transitions states	tr.	time (s) memory (kB)
	leader3	LTS ∼ ∼ ⊥ ∼ dbr ♯A ∼ @	1372 633 621 582 582	2375 1115 1097 1037 1037	884 427 415 379 379	1453 733 715 661 661	1.93 2.17 2.19 2.01 2.00	12940
	leader4	LTS ∼ ∼ ⊥ ∼ dbr ♯A ∼ @	16912 5450 5402 5138 5138	33368 9895 9823 9427 9427	6334 2572 2524 2324 2324	10427 4458 4386 4086 4086	110.02 110.35 110.25 110.17 110.14	14628

Table 7

 7 Compositional state space generation of distributed leader election systems.

  Listing 6 Agent process: exchange of propagation messages.

	1	--send put
	2	only if length (Zput) > 0 then
	3	var key: Nat in
	4	key := any Nat where (key < NVARS) and member(key, Zput);
	5	put(id, key, L, I);
	6	Zput := remove (key, Zput)
	7	end var
	8	end if
	9 []
	10	--receive put
	11	var s:ID, k:Nat, Ls:Lstig, Is:Iface, cmp:Comparison, lnk:Bool
	12	in
	13	put(?s, k, ?Ls, ?Is) where (s != id) and (k < NVARS);
	14	request(id, k, s, ?cmp);
	15	lnk := link(Is, I, Ls, L, s, id, k) and (cmp == GREATER)
	16
	17	if lnk then
	18	L[key] := Ls[key];
	19	stig (id, key, L[k]);
	20	Zput := insert(key, Zput);
	21	Zqry := remove(key, Zqry)
	22	end if
	23	end var

http://cadp.inria.fr

LNT stands for LOTOS New Technology.

MCL stands for Model Checking Language.

Note that sharp bisimulation as defined in[START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF] corresponds to divsharp bisimulation in the current paper. We prefer this naming, which is more in line with the distinction between branching and divbranching bisimulations.

A partition of a set S is a set of non-empty disjoint subsets of S (called blocks), whose union is S itself.

The difference between O(m log n) and O(mn 2 ) may seem big, and it is, indeed. However, O(mn 2 ) is the complexity upper bound, reached only in few corner cases (e.g., long sequences or large trees of transitions all labelled by the same action). Moreover, the bottleneck for state space reduction is usually memory rather than time. Even though they may be sensibly slower, signature-based partition refinement algorithms behave well in terms of memory consumption.

We only considered the "parallel CTL" category, because it turned out that the LTL formulas proposed in the "parallel LTL" category in 2019 were all preserved by divbranching bisimulation, for which we already had a minimization algorithm.

http://www.rers-challenge.org/2019

http://cadp.inria.fr/resources/vlts

For the sake of simplicity, we assume that timestamps are provided by a global clock, so that there cannot be two different values with the same timestamp.

Available at https://github.com/labs-lang/sliver

Our case study features only one such variable, namely ℓ. However, we always rely on a single gate stig to signal all updates, and put the name of the variable as data sent over the gate. This way, our encoding procedure is highly decoupled from the specific system being encoded.

For the anecdote, branching minimization was based on Groote & Vaandrager's algorithm in version 1 of BCG_MIN. In 2010, we released version 2, whose implementation based on signatures was found 20 times faster on a benchmark of 3700 realistic examples systematically collected over time.

See https://www.grid5000.fr

Acknowledgments

A part of this work has been performed in the A-IQ Ready project, which receives funding within the Key Digital Technologies Joint Undertaking (KDT JU) -the Public-Private Partnership for research, development and innovation under Horizon Europe -and National Authorities under grant agreement

.inria.fr/news13.html#section-3

no. 101096658. It was also partly upported by ERC consolidator grant no. 772459 D-SynMA (Distributed Synthesis: from Single to Multiple Agents).

Some experiments presented in this paper were carried out using the Grid'5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several Universities as well as other organizations. 19 The authors would like to warmly thank the anonymous referees, as well as David Jansen who inspired this work by pointing to the second author a possible relation between orthogonal and sharp bisimulations during a presentation of [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF] at TACAS'2021.

Appendix A Detailed Results on RERS 2019

The following tables give, for each problem of the "parallel CTL" category of the RERS 2019 challenge, the size of the LTS obtained using the partial sharp reduction described in [START_REF] Lang | Sharp congruences adequate with temporal logics combining weak and strong modalities[END_REF] and the size of the LTS obtained using sharp minimization. The last column indicates the reduction rate (in number of states) obtained using minimization with respect to partial reduction. Each problem consists of the number of a model (from 101 to 109) and the number of a property that depends on the model (from 01 to 20). In each case, the set of strong actions is determined by the property, so that its preservation by sharp bisimulation can be ensured.

problem

Appendix B LNT encoding of timestamp server

In this section we give some details about the LNT process that stores information about the timestamps of stigmergy variables. Specifically, for every pair of agents i, j and every stigmergy variable x, the process records whether the timestamp that agent i binds to x is greater, equal, or smaller than the one bound by j to the same variable. Since the LAbS semantics only cares about these comparisons, there is no need to store actual timestamps. We encode these comparisons as an LNT enumeration Comparison with three values GREATER, SAME, and LESS. So, the process essentially has to maintain an n × n matrix of comparisons M x for each stigmergy variable x, and provide responses when queried about its contents.

Listing 3 shows a sketch of our implementation of the timestamps server. Notice that MatrixVar is the type of a 2-dimensional matrix associated to a single variable, whereas Matrix is the type of a 3-dimensional matrix composed of one MatrixVar for each variable. We use NVARS to denote the number of variables.

At first, the server initializes every element of M to SAME (line 3). Then, it enters a loop where it repeatedly sends M over the debug gate and handles a message from the environment. The send action does not affect the server in any way, and is only there to provide a richer counterexample to the user when it tries to model-check a property that does not hold. As outlined in Section 7, the server accepts messages over two gates refresh and request. Gate refresh allows an agent i to ask for one of its own timestamps to be updated (lines [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF][START_REF] Burch | Sequential circuit verification using symbolic model checking[END_REF]. The server handles this request by calling a helper function refreshVar(M, x, i): this, in turn, updates M so that M x i,j = GREATER for every j ̸ = i. Gate request, instead, allows an agent to retrieve the value of M x i,j (lines [START_REF] Cleaveland | Priority in process algebras[END_REF][START_REF] De Nicola | Multi-agent systems with virtual stigmergy[END_REF][START_REF] Di Stefano | Verifying temporal properties of stigmergic collective systems using CADP[END_REF][START_REF] Di Stefano | Compositional verification of stigmergic collective systems[END_REF][START_REF] Di Stefano | Combining SLiVER with CADP to analyze multi-agent systems[END_REF][START_REF] Flanagan | Dynamic partial-order reduction for model checking software[END_REF][START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF][START_REF] Garavel | Equivalence Checking 40 Years After: A Review of Bisimulation Tools[END_REF]. What actually happens, here, is that the server simultaneously offers all the contents of M over this gate. Since we force synchronization over request, the server will just wait for an agent to synchronize on one of these offers. After this happens, if the element M x i,j that was offered was GREATER, we need to perform some bookkeeping on M . Namely, this means that the receiver j has gotten a stigmergy message from i with a newer value of x than its own local one. According to the semantics of LAbS, then, j will update its value and timestamp to the ones in the message.

While the value update is handled within the Agent process, the timestamp update must be implemented in the server. This essentially amounts to setting M x i,j to SAME and then copying the column M x i onto M x j . These operations are implemented by a helper function sync, not shown here.

Appendix C LNT encoding of agents

The behaviour of LAbS agents is encoded into a parameterized LNT process Agent(id), where the parameter id is a unique numeric identifier. The structure of this process is shown in Listing 4. Similarly to the timestamp server (Appendix B), Agent is composed of an initialization step (lines 5-6) followed by an event loop (lines 8-15).