Radu Mateescu
email: radu.mateescu@inria.fr

Anton Wijs
email: anton.wijs@inria.fr

Keywords: boolean equation system, branching bisimulation, labeled transition system, partial order reduction, on-the-fly verification système d'équations booléennes, bisimulation de branchement, système de transitions étiquetées, réduction par ordre partiel, vérification à la volée

The notion of τ -confluence provides a form of partial order reduction of Labelled Transition Systems (Ltss), by allowing to identify the τ -transitions whose execution does not alter the observable behaviour of the system. Several forms of τ -confluence adequate with branching bisimulation were studied in the literature, ranging from strong to weak ones according to the length of τ -transition sequences considered. Weak τ -confluence is more complex to compute than strong τ -confluence, but provides better Lts reductions. In this report, we aim at devising an efficient detection of weak τ -confluent transitions during an on-the-fly exploration of Ltss. To this purpose, we define and prove new encodings of several weak τ -confluence variants using alternation-free boolean equation systems (Bess), and we apply efficient local Bes resolution algorithms to perform the detection. The resulting reduction module, developed within the Cadp toolbox using the generic Open/Caesar environment for Lts exploration, was experimented on numerous examples of large Ltss underlying communication protocols and distributed systems. These experiments assessed the efficiency of the reduction and allowed us to identify the best variants of weak τ -confluence that are useful in practice.

Introduction

Explicit-state verification consists in exploring the state space of a concurrent program by enumerating its states and transitions in order to determine whether it satisfies a temporal logic formula (model checking) or it is equivalent to an automaton (equivalence checking). Although this method allows a fast and economic detection of errors in real-life systems, in practice it is confronted with the well-known problem of state explosion, i.e., an exponential growth of the state space w.r.t. the size of the program under verification when it contains many concurrent processes and complex data structures. Several techniques were proposed to combat state explosion in explicit-state verification, among which on-the-fly verification (incremental construction of the state space during verification) [START_REF] Holzmann | The SPIN Model Checker -Primer and Reference Manual[END_REF][START_REF] Du | Local Model Checking and Protocol Analysis[END_REF], partial order reduction (elimination of redundant sequences caused by the interleaving of independent transitions) [START_REF] Peled | Ten Years of Partial Order Reduction[END_REF][START_REF] Godefroid | Using Partial Orders to Improve Automatic Verification Methods[END_REF], and massively parallel verification (usage of the computing resources of several machines connected by a network) [START_REF] Ciardo | Distributed and Structured Analysis Approaches to Study Large and Complex Systems[END_REF][START_REF] Stern | Parallelizing the Murϕ Verifier[END_REF].

Here we focus on combining on-the-fly verification and partial order reduction for the analysis of concurrent systems described using process algebraic languages, whose natural models are Labeled Transition Systems (Ltss). In this context, specific variants of partial order reduction, such as τ -confluence [START_REF] Groote | State Space Reduction using Partial τ -Confluence[END_REF], were proposed for reducing Ltss whilst preserving branching bisimulation. Basically, confluent τ -transitions do not alter the observable behaviour of the system, and therefore they can be prioritized by ignoring their neighbour transitions, which reduces the amount of redundant interleavings. The on-the-fly detection of confluent τ -transitions in Ltss can be done by encoding the problem as the local resolution of an alternation-free Boolean Equation System (Bes) [START_REF] Andersen | Model Checking and Boolean Graphs[END_REF][START_REF] Mader | Verification of Modal Properties Using Boolean Equation Systems[END_REF], which was successfully applied for strong τ -confluence [START_REF] Pace | Calculating τ -Confluence Compositionally[END_REF]. The reductions can be further improved, at a higher computation cost, using weaker forms of τ -confluence, as those studied in [START_REF] Groote | Confluence for process verification[END_REF][START_REF] Ying | Weak confluence and τ -inertness[END_REF][START_REF] Blom | Partial τ -confluence for Efficient State Space Generation[END_REF], but no attempt of fully implementing them on-the-fly in the explicit-state setting has been done so far.

In this report, we propose a new encoding of weak τ -confluence by using alternation-free Bess. The idea is to consider τ -convergent Ltss (without cycles of τ -transitions), for which the computation of τ -closures can be done using maximal (instead of minimal) fixed point equations. These equations can be merged with those of the maximal fixed point Bes encoding the confluence detection, yielding an alternation-free Bes containing a single equation block. The on-the-fly detection of weakly confluent τ -transitions is carried out by combining the local Bes resolution with a τ -compression [START_REF] Mateescu | On-the-fly State Space Reductions for Weak Equivalences[END_REF] of the Lts, which collapses the strongly connected components (Sccs) of τ -transitions in order to obtain a τ -convergent Lts on which the Bes encoding operates correctly. A similar scheme was succesfully applied to obtain alternation-free Bes encodings of weak and branching bisimulation [START_REF] Mateescu | Improved On-the-Fly Equivalence Checking using Boolean Equation Systems[END_REF]. We study a hierarchy containing seven variants of weak τ -confluence, some of them not considered before in the literature, with the goal of achieving better reductions than strong τ -confluence (which is on top of the hierarchy) without penalizing the performance. For each variant R, we propose two Bes encodings, an individual one that implements the mathematical definition of R, and a hierarchical one meant to speed up the convergence of Bes resolution by trying to detect first the τ -transitions confluent modulo variants R ′ that are stronger (and therefore easier to compute) than R.

This resulted in sixteen different Bes encodings of weak τ -confluence variants, all of which were implemented within the Cadp toolbox [START_REF] Garavel | CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] using the Open/Caesar [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF] generic environment for on-the-fly Lts manipulation. We carried out an extensive set of experiments by trying each Bes encoding of weak τ -confluence on Ltss corresponding to communication protocols and other real-life distributed systems. The measures included the memory and execution time for reducing each Lts, and also the amount of reduction achieved w.r.t. the Lts minimized modulo branching bisimulation. This enabled us to identify the Bes encodings that offer the best compromise between the computation cost and the amount of reduction achieved.

Related work. In [START_REF] Groote | Confluence for process verification[END_REF], the relation between several notions of confluence and τ -inertness is explained. Besides strong and weak confluence, several other versions are discussed, which relax the confluence condition by allowing the branches to end up in two different states (instead of a single one), which are related modulo some equivalence relation (strong, weak, branching, or finite trace). In [START_REF] Groote | State Space Reduction using Partial τ -Confluence[END_REF], an algorithm is presented to determine a set of strongly confluent τ -transitions for a given Lts, in order to reduce it; repeated application leads to increasingly smaller Ltss.

Another hierarchy of variants of τ -confluence is presented in [START_REF] Blom | Partial τ -confluence for Efficient State Space Generation[END_REF]. Also here, strong and weak τ -confluence, the latter being called ultra weak, form the two extremes. The two variants in between, confluence and weak confluence, however, are not represented in our hierarchy, since these ones are not suitable for Bes encodings. As in our report, a method is described to detect confluent τ -transitions on-the-fly, here using a depth-first search through the confluent transition graph to determine representatives of states and detect terminal Sccs. An implementation of weak τ -confluence using this method is reported in [START_REF] Blom | Partial τ -confluence for Efficient State Space Generation[END_REF][START_REF] Blom | State Space Reduction by Proving Confluence[END_REF]; it is able to handle infinite-state spaces by means of symbolic reasoning, but considers sequences of at most two τ -transitions.

Report outline. Section 2 recalls the basic definitions of τ -confluence and introduces the hierarchy of weak τ -confluence variants that we consider. Section 3 defines the individual and hierarchical Bes encodings of the variants, and states their correctness. Section 4 briefly describes the implementation of the reductor module based on Bes resolution. Section 5 shows experimental figures and compares the performance of the encodings on various Ltss. Section 6 summarizes the results and gives directions of future work. Annex A contains the definitions of all Bes encodings and Annex B gives the proofs of their correctness.

Hierarchy of Weak Tau-Confluence Variants

The reduction by τ -confluence operates on Ltss, which are the natural models for actionbased description languages, such as process algebras. An Lts is a tuple M = S, A, T , s 0 , where S is the set of states, A is the set of actions (including the internal action τ ), T ⊆ S ×A×S is the transition relation, and s 0 ∈ S is the initial state. A transition (s 1 , a, s 2 ) ∈ T INRIA (also noted s 1 a → s 2 ) indicates that the system can move from state s 1 to state s 2 by executing action a. The notation

s 1 a → s 2 is equivalent to s 1 a → s 2 if a = τ and to s 1 τ → s 2 ∨ s 1 = s 2 otherwise.
The definition of weak τ -confluence below is based on the notion introduced in [START_REF] Groote | Confluence for process verification[END_REF] and revisited in [START_REF] Blom | Partial τ -confluence for Efficient State Space Generation[END_REF] under the name ultra weak τ -confluence.

Definition 1 (Weak τ -confluence) Given an Lts M = S, A, T , s 0 , and S ⊆ S 2 , we say that S is weak τ -confluent in M if for every s 1 , s 2 ∈ S and s 1 a → s 3 , we have s 1 τ → s 2 , and for some n, m, p > 0 there exist s 2,0 , . . . , s 2,n , s ′ 2,0 , . . . , s ′ 2,m , s 4 ∈ S with s 2,0 = s 2 , and s 3,0 , . . . , s 3,p ∈ S with Weak τ -confluence is illustrated graphically by the R 8 diagram at the bottom of the hierarchy shown in Figure 1. The transitions drawn with solid lines are given, whereas the existence of the dashed ones must be proven in order to make the diagram confluent. Transitions that are τ -confluent (i.e., belong to S) are labeled by τ c . The diagram R 1 at the top of the hierarchy corresponds to strong τ -confluence [START_REF] Groote | State Space Reduction using Partial τ -Confluence[END_REF] and the other diagrams denote particular cases of weak τ -confluence obtained either by dropping sequences s i τ * c → s j or by replacing them with single-step sequences s i τc → s j . Arrows between diagrams indicate that the source diagram is a particular case of the target diagram. In [START_REF] Groote | Confluence for process verification[END_REF][START_REF] Groote | State Space Reduction using Partial τ -Confluence[END_REF][START_REF] Blom | Partial τ -confluence for Efficient State Space Generation[END_REF] it was shown that both strong and weak τ -confluence are adequate w.r.t. branching bisimulation, i.e., if a transition s 1 τ → s 2 is τ -confluent, then s 1 and s 2 are branching bisimilar [START_REF] Groote | Confluence for process verification[END_REF][START_REF] Blom | Partial τ -confluence for Efficient State Space Generation[END_REF]. Therefore, all intermediate τ -confluence variants R 2 -R 7 are also adequate w.r.t. branching bisimulation.

s 3,0 = s 3 such that s 2,i τ → s 2,i+1 and s 2,i , s 2,i+1 ∈ S for 0 ≤ i < n, s 2,n a → s ′ 2,0 , s ′ 2,j τ → s ′ 2,j+1 and s ′ 2,j , s ′ 2,j+1 ∈ S for 0 ≤ j < m, s ′ 2,m τ → s 4 and s ′ 2,m , s 4 ∈ S, s 3,k τ → s 3,
The τ -confluence reduction proposed in [START_REF] Groote | State Space Reduction using Partial τ -Confluence[END_REF] consists of detecting confluent τ -transitions s 1 τc → s 2 and prioritizing them by deleting all their neighbour transitions s 1 a → s 3 , thus obtaining an Lts smaller, but still branching bisimilar to the original one. The detection of confluent τ -transitions during an on-the-fly exploration of the Lts can be performed efficiently using local Bes resolution, as shown in the sequel.

BES Encodings of Weak Tau-Confluence

An alternation-free boolean equation system (Bes) [START_REF] Andersen | Model Checking and Boolean Graphs[END_REF][START_REF] Mader | Verification of Modal Properties Using Boolean Equation Systems[END_REF] is a set of fixed point equations having boolean variables in their left-hand sides and boolean formulas in their right-hand sides. For our purpose, we consider maximal fixed point Bess containing simple equations [START_REF] Arnold | A Linear Algorithm to Solve Fixed-Point Equations on Transition Systems[END_REF], i.e., whose boolean formulas in the right-hand sides are either purely disjunctive, or purely conjunctive. We propose below new encodings of the weak τ -confluence variants R 2 -R 8 using alternation-free Bess. For each weak τ -confluence variant R i , we give an individual encoding derived from its definition, and several hierarchical encodings taking into account the variants stronger than R i present in the hierarchy.

a R 1 R 2 R 3 R 4 R 5 R 6 R 7 R 8
Figure 1: Variants of τ -confluence, ranging from strong (R 1 ) to weak (R 8 )

Individual encodings

An alternation-free Bes encoding for the strong τ -confluence (R 1 ) was proposed in [START_REF] Pace | Calculating τ -Confluence Compositionally[END_REF] and applied for reducing Ltss in networks of automata. To devise a similar encoding for weak τ -confluence (R 8 ), we associate to each transition s 1 τc → s 2 a boolean variable X s 1 ,s 2 indicating whether the transition is weakly τ -confluent or not. A direct encoding of the diagram R 8 yields the Bes (a) below. This Bes is further simplified by introducing additional vari-

INRIA

ables and equations to factor subformulas, such that every right-hand side formula becomes disjunctive or conjunctive, yielding the Bes (b).

   X s1,s2 ν = s1 a →s3 s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true    s 1 , s 2 ∈ S a ∈ A                    X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 τ * c →s ′ 2 Z s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = s ′ 2 a →s ′′ 2 U s ′′ 2 ,s3 U s ′′ 2 ,s3 ν = s ′′ 2 τ * c →s4 V s3,s4 V s3,s4 ν = s3 τ * c →s4 true                    s 1 , s 2 , s ′ 2 , s ′′ 2 , s 3 , s 4 ∈ S, a ∈ A (a) (b)
We observe that the evaluation of the formulas in the right-hand sides of the equations defining Y s 2 ,s 3 ,a , U s ′′ 2 ,s 3 , and V s 3 ,s 4 requires to compute transitive reflexive closures over confluent τ -transitions. These τ -closure computations correspond to the evaluation of minimal fixed points and can be encoded using an additional block of minimal fixed point equations. Since these equations refer back to the variables X s 1 ,s 2 of the maximal fixed point equation block encoding the τ -confluence detection, the resulting Bes would be of alternation depth two, a class with quadratic resolution complexity [START_REF] Vergauwen | Efficient Local Correctness Checking for Single and Alternating Boolean Equation Systems[END_REF]. However, when the Lts is τ -convergent (i.e., it does not contain cycles of τ -transitions), τ -closures can be encoded using maximal (instead of minimal) fixed point equations, which can be added to the other equations of the Bes (b). This produces the Bes below:

                           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = Z s2,s3,a ∨ s2 τ →s ′ 2 Y ′ s2,s ′ 2 ,s3,a Y ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ Y s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = (a = τ ∧ U s ′ 2 ,s3 ) ∨ s ′ 2 a →s ′′ 2 U s ′′ 2 ,s3 U s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ s ′′ 2 τ →s4 U ′ s ′′ 2 ,s4,s3 U ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ U s4,s3 V s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 V ′ s3,s ′ 3 ,s4 V ′ s3,s ′ 3 ,s4 ν = X s3,s ′ 3 ∧ V s ′ 3 ,s4                            s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
The detection of confluent τ -transitions is performed by solving the X s 1 ,s 2 variables of this Bes using the local resolution algorithms presented in [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF]. The local Bes resolution triggers a forward exploration of the Lts transitions in order to evaluate the formulas in the righthand sides of equations, and therefore is compatible with an on-the-fly exploration of the Lts. Since this encoding scheme is correct only on τ -convergent Ltss, the cycles of τ -transitions possibly present in the Lts must be eliminated on-the-fly during the Bes resolution, e.g., by using the τ -compression algorithm proposed in [START_REF] Mateescu | On-the-fly State Space Reductions for Weak Equivalences[END_REF].

The Bes encodings of the other weak τ -confluence variants R 2 -R 7 of the hierarchy are obtained as particular cases of the Bes above (see Annex A.1).

Hierarchical encodings

The Bes encoding of weak τ -confluence (diagram R 8 in Figure 1) defined in Section 3.1 yields very good reductions, the resulting Ltss being sometimes very close to their minimized versions modulo branching bisimulation. However, when the Lts contains large τ -diamonds produced by the interleaved internal activity of concurrent processes, the size of the Bes (number of variables and operators) may become quadratic w.r.t. the size of the Lts (number of states and transitions). On the other hand, detecting strong τ -confluence (diagram R 1 ) yields smaller Bess, of size linear in the number of τ -transitions and quadratic in the branching factor of the Lts [START_REF] Pace | Calculating τ -Confluence Compositionally[END_REF], but always provides less reduction than the other τ -confluence variants (diagrams R 2 -R 8 ).

To achieve the best compromise between the amount of reduction and the computational effort, one can proceed as follows: for each τ -transition encountered, first try to detect whether it is strongly confluent (R 1 ), then try a weaker variant of τ -confluence (e.g., R 2 ), then a weaker one (e.g., R 6 ), and finally try the weak τ -confluence itself (R 8 ). This reduces the average complexity of the τ -confluence detection by allowing a local Bes resolution algorithm to stop as soon as it has established that the τ -transition under analysis matches some τ -confluence variant among R 1 -R 8 . In practice, this hierarchical detection of weak τconfluence can be achieved by means of a Bes allowing the resolution algorithms to consider in turn the desired τ -confluence variants, which amounts to follow a particular path in the diagram hierarchy shown in Figure 1.

We construct below the Bes corresponding to the path R 1 -R 2 -R 6 -R 8 . Using the fact that the local Bes resolution algorithms scan the right-hand sides of equations from left to right, it is sufficient to put in the right-hand sides of the equations defining X s 1 ,s 2 the boolean formulas corresponding to the four diagrams R 1 , R 2 , R 6 , R 8 in this order:

                 X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ (R 1 ) s2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ (R 2 ) s2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true ∨ (R 6 ) s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true (R 8 )                  s 1 ,s 2 ∈S
It is worth noticing that this Bes is equivalent to (i.e., yields the same solution for the X s 1 ,s 2 variables) the Bes given in Section 3.1 for the individual encoding of weak τ -confluence, because the first three disjuncts in the right-hand side formula are absorbed by (i.e., are particular cases of) the last disjunct, which corresponds to R 8 . Upon simplification and factorization of common disjunctive subformulas, the Bes above takes the following form (note that s 4 was renamed into s ′′ 2 in the first disjunct):

       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s3 τ * c →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 s ′′ 2 τ * c →s4 s3 τ * c →s4 true        s 1 , s 2 , s 3 ∈ S, a ∈ A

INRIA

The equation defining Y s 2 ,s 3 ,a can be simplified by absorbing the disjunct true. Such simplifications can be applied as long as they do not perturbate the evaluation order of the four cases R 1 , R 2 , R 6 , R 8 , which correspond to the disjuncts present in the right-hand side of the equation defining Y s 2 ,s 3 ,a . Finally, after factoring τ -closures apart and encoding them using additional equations using the same scheme as in Section 3.1, we obtain the Bes corresponding to the hierarchical encoding of weak τ -confluence:

                                   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s2,s3 ) ∨ s2 a →s ′′ U s2,s3,a ν = (a = τ ∧ V s2,s3 ) ∨ s2 a →s ′′ 2 V s ′′ 2 ,s3 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a                                    s 1 , s 2 , s ′ 2 , s ′′ 2 , s 3 , s ′ 3 , s 4 ∈ S, a ∈ A
We also devised the hierarchical encodings for the five other paths from R 1 to R 8 , and similarly for the other variants R 2 -R 7 in the hierarchy (see Annex A.2). Some of these encodings led to identical Bess, ending up with only eight different hierarchical Bes encodings instead of fifteen.

Implementation

The Bes encodings of the weak τ -confluence variants proposed in Section 3 provide the basis for an on-the-fly Lts reduction procedure. We implemented this procedure as a reductor module within the Cadp1 verification toolbox [START_REF] Garavel | CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] using the generic Open/Caesar environment [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF] for Lts exploration. This environment is centered around an implicit representation of Ltss defined by an Api in C allowing to manipulate the transition relation as a "successor function" enumerating the transitions going out of a given state. Open/Caesar provides a rich set of primitives dedicated to graph exploration (stacks, edge lists, hash tables, etc.). It also contains the generic Caesar Solve library [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF] for local Bes resolution, which operates on Bess given as boolean graphs [START_REF] Andersen | Model Checking and Boolean Graphs[END_REF] represented implicitly in a way similar to Ltss. This library currently offers nine resolution algorithms based on various exploration strategies (depth-first, breadth-first, etc.), each of them being able to generate diagnostics (boolean subgraphs) illustrating the truth value of a boolean variable. Caesar Solve serves as verification engine for several on-the-fly Lts analysis tools of Cadp, such as the model checker Evaluator 3.x [START_REF] Mateescu | Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus[END_REF][START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF] and the equivalence checker Bisimulator 2.0 [START_REF] Mateescu | Improved On-the-Fly Equivalence Checking using Boolean Equation Systems[END_REF].

The architecture of the reductor module is shown in Figure 4. It takes as input an implicit Lts (represented by its successor function) and produces as output the implicit Lts reduced modulo weak τ -confluence. The input Lts is first processed on-the-fly by the τ -compression module proposed in [START_REF] Mateescu | On-the-fly State Space Reductions for Weak Equivalences[END_REF], which produces the implicit τ -convergent Lts obtained after collapsing the τ -Sccs and replacing them by their representative states, namely their roots in Tarjan's terminology [START_REF] Tarjan | Depth First Search and Linear Graph Algorithms[END_REF]. This τ -convergent Lts serves as input both for an encoder module (this newly added module is about 13, 300 lines of C), which translates the weak τ -confluence into an implicit Bes as described in Section 3, and for an explorer module, which actually performs the detection of weakly confluent τ -transitions s 1 τ → s 2 by calling the Bes resolution engine Caesar Solve to obtain the value of the boolean variables X s 1 ,s 2 of the Bes. Besides prioritizing confluent τ -transitions as described in [START_REF] Groote | State Space Reduction using Partial τ -Confluence[END_REF], the explorer module also compresses the sequences of confluent τ -transitions using the on-the-fly algorithm given in [START_REF] Mateescu | On-the-fly State Space Reductions for Weak Equivalences[END_REF], which achieves additional reduction by exploiting the fact that the source and target states of each such transition are branching bisimilar. The explorer module provides as output the successor function of the reduced Lts obtained after applying these transformations.

τ -confluence reductor

Experimental Results

We studied the performance of all the individual and hierarchical Bes encodings extensively.

For this, we used around 30 Ltss from the Vlts benchmark suite2 stemming from industrial case studies and 7 communication protocols taken from the Cadp demo examples 3 . All experiments were run on a Linux machine with a 2.2 GHz Cpu and 16 Gb of memory.

Here, we present in several graphs the most interesting results obtained, concerning the individual encodings of R 1 and R 8 , and four hierarchical encodings, namely

R 1-2-4 , R 1-3-7 , R 1-5-7-8 , and R 1-3-4-8 .
In the graph at the top of Figure 5, the different sizes of the output Ltss are compared to the usual sizes without any confluence checking ("full") and the minimal sizes obtainable by reducing the full Ltss modulo branching bisimulation ("min"). We observe that for many of the Vlts cases displayed, there are no big differences between the sizes, while for the case studies there are. Most of the Vlts examples do not stem from communication protocols, and they seem less sensitive to which encoding we use.

The graphs at the middle and the bottom of Figure 5 show the execution times of the different encodings when using two different resolution algorithms available in the Caesar Solve library [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF][START_REF] Mateescu | Improved On-the-Fly Equivalence Checking using Boolean Equation Systems[END_REF] of Cadp, namely A5 and A8, which exhibit the best performance for solving Bess encoding τ -confluence detection. Clearly, besides R 1 , which produces the worst reduction, encodings R 1-2-4 and R 1-3-7 are on average the fastest. The experiments point out that incorporating R 8 into a hierarchical encoding can be particularly costly with respect to time, hence it should only be done if the gain in reduction of the output Lts justifies it. The performance of the other two hierarchical encodings excluding R 8 tends to be in between the performance of these two.

The last two graphs shown in Figure 5 display the number of boolean variables created in memory in order to solve the Bess using algorithms A5 and A8, respectively. Algorithm A8 tends to be more economic in memory, which comes at the price of longer execution times.

Based on these results, we conclude that on average the performance of R i , with i ∈ {4, 7, 8}, is worse than any hierarchical encoding incorporating R i . Concerning R 8 , encoding R 1-3-4-8 is often most efficient, but usually still very costly, and the same or slightly worse results can be obtained more efficiently using an encoding to R 7 , particularly R 1-3-7 . Looking at Figure 1, our experiments point out that if we want to incrementally check for confluences weaker than strong, we should first try to detect strong confluence, then try to detect a sequence of confluent τ -transitions starting at s 2 , i.e., the difference between R 3 and R 1 , then if desired try to detect a sequence of confluent τ -transitions after the following a, as in R 4 , and finally extend the check of s

3 τc → s 4 to s 3 τ * c → s 4 (encoding R 1-3-4 , not shown in

Conclusion and Future Work

The possibility of efficiently reducing an Lts on-the-fly while preserving branching bisimulation is a useful feature for equivalence checkers and model checkers. In this report we studied a hierarchy of weak τ -confluence variants and proposed new (individual and hierarchical) encodings of these variants in terms of alternation-free Bess, which provided the basis of a reduction procedure based on local Bes resolution. The resulting reductor module, built using the Open/Caesar [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF] environment of Cadp [START_REF] Garavel | CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] and the Caesar Solve [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF] boolean resolution library, can be used as accelerator for various on-the-fly verification tools. The experiments we carried out on benchmark Ltss coming from real-life case-studies enabled us to identify the combinations of weak τ -confluence variants and Bes encodings that provide the best compromise between the amount of reduction achieved and the complexity of its computation. This improves over existing results in this setting, which concerned mainly strong τ -confluence and (to a limited extent only) weak τ -confluence.

We plan to continue our work by first experimenting the new reductor module in conjunction with other on-the-fly verification tools of Cadp, such as the (sequential) model checker Evaluator 3.x [START_REF] Mateescu | Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus[END_REF][START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF] and equivalence checker Bisimulator 2.0 [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF][START_REF] Mateescu | Improved On-the-Fly Equivalence Checking using Boolean Equation Systems[END_REF] in order to determine the most appropriate weak τ -confluent variant suitable for these tools. Another line of work concerns the combination of the reductor module with the Distributor tool [START_REF] Garavel | DISTRIBUTOR and BCG MERGE: Tools for Distributed Explicit State Space Generation[END_REF] for distributed state space generation, which currently provides only τ -compression and strong τ -confluence as reduction features. Finally, we will seek to devise Bes encodings for other forms of τ -confluence, such as those defined in [START_REF] Groote | Confluence for process verification[END_REF].

A Encodings of the τ -confluence variants

A.1 Individual encodings

Encoding of R 1 A direct encoding of the diagram R 1 yields the Bes below:      X s 1 ,s 2 ν = s 1 a →s 3 s 2 a →s 4 s 3 τc →s 4 true      s 1 ,s 2 ∈S,a∈A
Simplifying the Bes such that every equation has a single boolean operator in its right-hand side yields the following Bes:

     X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 Z s3,s4 Z s3,s4 ν = s3 τc →s4 true      s 1 ,s 2 ,s 3 ,s 4 ∈S,a∈A
Encoding the τ -closures using maximal fixed point variables produces the following Bes:

   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 Z s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s4 X s3,s4    s 1 ,s 2 ,s 3 ,s 4 ∈S,a∈A
Encoding of R 2 A direct encoding of the diagram R 2 yields the Bes below:

       X s 1 ,s 2 ν = s 1 a →s 3 s 2 a →s ′′ 2 τ * c →s 4 s 3 τc →s 4 true        s 1 ,s 2 ∈S,a∈A
Simplifying the Bes such that every equation has a single boolean operator in its right-hand side yields the following Bes:

           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = s ′′ 2 τ * c →s4 U s3,s4 U s3,s4 ν = s3 τc →s4 true            s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A
Encoding the τ -closures using maximal fixed point variables produces the following Bes:

             X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s2,s3 ) ∨ s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = U s3,s ′′ 2 ∨ s ′′ 2 τ →s4 Z ′ s ′′ 2 ,s3,s4 Z ′ s ′′ 2 ,s3,s4 ν = X s ′′ 2 ,s4 ∧ Z s4,s3 U s3,s ′′ 2 ν = (s 3 = s ′′ 2 ) ∨ s3 τ →s ′′ 2 X s3,s ′′ 2              s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

RR n 7000

Encoding of R 3 A direct encoding of the diagram R 3 yields the Bes below:

       X s 1 ,s 2 ν = s 1 a →s 3 s 2 τ * c →s ′ 2 a →s 4 s 3 τc →s 4 true        s 1 ,s 2 ∈S,a∈A
Simplifying the Bes such that every equation has a single boolean operator in its right-hand side yields the following Bes:

           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 τ * c →s ′ 2 Z s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = s ′ 2 a →s4 U s3,s4 U s3,s4 ν = s3 τc →s4 true            s 1 ,s 2 ,s ′ 2 ,s 3 ,s 4 ∈S,a∈A
Encoding the τ -closures using maximal fixed point variables produces the following Bes:

             X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = Z s2,s3,a ∨ s2 τ →s ′ 2 Y ′ s2,s ′ 2 ,s3,a Y ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ Y s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = (a = τ ∧ U s3,s ′ 2 ) ∨ s ′ 2 a →s4 U s3,s4 U s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s4 X s3,s4              s 1 ,s 2 ,s ′ 2 ,s 3 ,s 4 ∈S,a∈A
Encoding of R 4 A direct encoding of the diagram R 4 yields the Bes below:

       X s 1 ,s 2 ν = s 1 a →s 3 s 2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s 4 s 3 τc →s 4 true        s 1 ,s 2 ∈S,a∈A
Simplifying the Bes such that every equation has a single boolean operator in its right-hand side yields the following Bes:

                 X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 τ * c →s ′ 2 Z s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = s ′ 2 a →s ′′ 2 U s ′′ 2 ,s3 U s ′′ 2 ,s3 ν = s ′′ 2 τ * c →s4 V s3,s4 V s3,s4 ν = s3 τc →s4 true                  s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

INRIA

Encoding the τ -closures using maximal fixed point variables produces the following Bes:

                       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = Z s2,s3,a ∨ s2 τ →s ′ 2 Y ′ s2,s ′ 2 ,s3,a Y ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ Y s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = (a = τ ∧ U s ′ 2 ,s3 ) ∨ s ′ 2 a →s ′′ 2 U s ′′ 2 ,s3 U s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ s ′′ 2 τ →s4 U ′ s ′′ 2 ,s3,s4 U ′ s ′′ 2 ,s3,s4 ν = X s ′′ 2 ,s4 ∧ U s4,s3 V s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s4 X s3,s4                        s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A
Encoding of R 5 A direct encoding of the diagram R 5 yields the Bes below:

     X s 1 ,s 2 ν = s 1 a →s 3 s 2 a →s 4 s 3 τ * c →s 4 true      s 1 ,s 2 ∈S,a∈A
Simplifying the Bes such that every equation has a single boolean operator in its right-hand side yields the following Bes:

     X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 Z s3,s4 Z s3,s4 ν = s3 τ * c →s4 true      s 1 ,s 2 ,s 3 ,s 4 ∈S,a∈A
Encoding the τ -closures using maximal fixed point variables produces the following Bes:

         X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 Z s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 Z ′ s3,s ′ 3 ,s4 Z ′ s3,s ′ 3 ,s4 ν = X s3,s ′ 3 ∧ Z s ′ 3 ,s4          s 1 ,s 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of R 6 A direct encoding of the diagram R 6 yields the Bes below:

       X s 1 ,s 2 ν = s 1 a →s 3 s 2 a →s ′′ 2 τ * c →s 4 s 3 τ * c →s 4 true        s 1 ,s 2 ∈S,a∈A

RR n 7000

Simplifying the Bes such that every equation has a single boolean operator in its right-hand side yields the following Bes:

           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = s ′′ 2 τ * c →s4 U s3,s4 U s3,s4 ν = s3 τ * c →s4 true            s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A
Encoding the τ -closures using maximal fixed point variables produces the following Bes:

                   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s2,s3 ) ∨ s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = U s3,s ′′ 2 ∨ s ′′ 2 τ →s4 Z ′ s ′′ 2 ,s3,s4 Z ′ s ′′ 2 ,s3,s4 ν = X s ′′ 2 ,s4 ∧ Z s4,s3 U s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 U ′ s3,s ′ 3 ,s4 U ′ s3,s ′ 3 ,s4 ν = X s3,s ′ 3 ∧ U s ′ 3 ,s4                    s 1 ,s 2 ,s ′′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of R 7 A direct encoding of the diagram R 7 yields the Bes below:

       X s 1 ,s 2 ν = s 1 a →s 3 s 2 τ * c →s ′ 2 a →s 4 s 3 τ * c →s 4 true        s 1 ,s 2 ∈S,a∈A
Simplifying the Bes such that every equation has a single boolean operator in its right-hand side yields the following Bes:

           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 τ * c →s ′ 2 Z s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = s ′ 2 a →s4 U s3,s4 U s3,s4 ν = s3 τ * c →s4 true            s 1 ,s 2 ,s ′ 2 ,s 3 ,s 4 ∈S,a∈A
Encoding the τ -closures using maximal fixed point variables produces the following Bes:

                   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = Z s2,s3,a ∨ s2 τ →s ′ 2 Y ′ s2,s ′ 2 ,s3,a Y ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ Y s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = (a = τ ∧ U s3,s ′ 2 ) ∨ s ′ 2 a →s4 U s3,s4 U s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 U ′ s3,s ′ 3 ,s4 U ′ s3,s ′ 3 ,s4 ν = X s3,s ′ 3 ∧ U s ′ 3 ,s4                    s 1 ,s 2 ,s ′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A INRIA A.

Hierarchical encodings

Encoding of the path R 1 -R 2 -R 4 -R 8 Combining the boolean formulas corresponding to the four diagrams R 1 , R 2 , R 4 , R 8 yields the following:

                 X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true                  s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the first disjunct):

         X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s3 τ * c →s4 true          s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (absorption of the disjunct

                           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 Z s ′′ 2 ,s3 ∨ U s2,s3,a Z s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 V s3,s4 V s3,s4 ν = s3 τc →s4 true U s2,s3,a ν = s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 W s ′′ 2 ,s3 W s ′′ 2 ,s3 ν = s ′′ 2 τ * c →s4 S s3,s4 S s3,s4 ν = s3 τ * c →s4 true                            s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

RR n 7000

Finally, after encoding τ -closures using boolean equations, we obtain the Bes below:

                                           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s2,s3 ) ∨ s2 a →s ′′ 2 Z s ′′ 2 ,s3 ∨ U s2,s3,a Z s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ s ′′ 2 τ →s4 Z ′ s ′′ 2 ,s4,s3 Z ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ Z s4,s3 V s3,s ′′ 2 ν = (s 3 = s ′′ 2 ) ∨ s3 τ →s ′′ 2 X s3,s ′′ 2 U s2,s3,a ν = (a = τ ∧ W s2,s3 ) ∨ s2 a →s ′′ 2 W s ′′ 2 ,s3 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a W s ′′ 2 ,s3 ν = S s3,s ′′ 2 ∨ s ′′ 2 τ →s4 W ′ s ′′ 2 ,s4,s3 W ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ W s4,s3 S s3,s ′′ 2 ν = (s 3 = s ′′ 2 ) ∨ s3 τ →s ′ 3 S ′ s3,s ′ 3 ,s ′′ 2 S ′ s3,s ′ 3 ,s ′′ 2 ν = X s3,s ′ 3 ∧ S s ′ 3 ,s ′′ 2                                            s 1 , s 2 , s ′ 2 , s ′′ 2 , s 3 , s ′ 3 , s 4 ∈ S, a ∈ A Encoding of the path R 1 -R 5 -R 6 -R 8
Combining the boolean formulas corresponding to the four diagrams R 1 , R 5 , R 6 , R 8 yields the following:

                 X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s4 s3 τ * c →s4 true ∨ s2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true                  s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the first and second disjunct):

       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s3 τ * c →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τ * c →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 s ′′ 2 τ * c →s4 s3 τ * c →s4 true        s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (absorption of the disjunct

                 X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = Z s2,s3,a ∨ s2 τ * c →s ′ 2 Z s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = s ′ 2 a →s ′′ 2 U s ′′ 2 ,s3 U s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 V s3,s4 V s3,s4 ν = s3 τ * c →s4 true                  s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

INRIA

Finally, after encoding τ -closures using boolean equations, we obtain a Bes identical to the encoding of R 8 :

                           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = Z s2,s3,a ∨ s2 τ →s ′ 2 Y ′ s2,s ′ 2 ,s3,a Y ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ Y s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = (a = τ ∧ U s ′ 2 ,s3 ) ∨ s ′ 2 a →s ′′ 2 U s ′′ 2 ,s3 U s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ s ′′ 2 τ →s4 U ′ s ′′ 2 ,s4,s3 U ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ U s4,s3 V s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 V ′ s3,s ′ 3 ,s4 V ′ s3,s ′ 3 ,s4 ν = X s3,s ′ 3 ∧ V s ′ 3 ,s4                            s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 5 -R 7 -R 8 Combining the boolean formulas corresponding to the four diagrams R 1 , R 5 , R 7 , R 8 yields the following:

                 X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s4 s3 τ * c →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τ * c →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true                  s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the first and second disjunct):

         X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s3 τ * c →s ′′ 2 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 s3 τ * c →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τ * c →s4 true ∨          s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (absorption of the disjunct

                 X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 Z s3,s ′′ 2 ∨ U s2,s3,a Z s3,s ′′ 2 ν = s3 τ * c →s ′′ 2 true U s2,s3,a ν = s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 V s ′′ 2 ,s3 V s ′′ 2 ,s3 ν = Z s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 Z s3,s4                  s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

RR n 7000

Finally, after encoding τ -closures using boolean equations, we obtain the Bes below:

                             X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s ′′ 2 Z s3,s ′′ 2 ∨ U s2,s3,a Z s3,s ′′ 2 ν = (s 3 = s ′′ 2 ) ∨ s3 τ →s ′ 3 Z ′ s3,s ′ 3 ,s ′′ 2 Z ′ s3,s ′ 3 ,s ′′ 2 ν = X s3,s ′ 3 ∧ Z s ′ 3 ,s ′′ 2 U s2,s3,a ν = (a = τ ∧ V s2,s3 ) ∨ s2 a →s ′′ 2 V s ′′ 2 ,s3 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a V s ′′ 2 ,s3 ν = Z s3,s ′′ 2 ∨ s ′′ 2 τ →s4 V ′ s ′′ 2 ,s4,s3 V ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ V s4,s3                              s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 3 -R 4 -R 8 Combining the boolean formulas corresponding to the four diagrams R 1 , R 3 , R 4 , R 8 yields the following:

                 X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true                  s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the second disjunct):

       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s3 τ * c →s4 true        s 1 , s 2 , s 3 ∈ S, a ∈ A
Further simplifications (absorption of the disjunct

                     X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = s3 τc →s4 true U s2,s3,a ν = s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 V s ′′ 2 ,s3 V s ′′ 2 ,s3 ν = Z s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 W s3,s4 W s3,s4 ν = s3 τ * c →s4 true                      s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

INRIA

Finally, after encoding τ -closures using boolean equations, we obtain the Bes below (note that on the right hand side of V s ′′ 2 ,s 3 , the disjunct Z s 3 ,s ′′ 2 is absorbed by W s 3 ,s ′′ 2 ):

                                 X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s4 X s3,s4 U s2,s3,a ν = (a = τ ∧ V s2,s3 ) ∨ s2 a →s ′′ 2 V s ′′ 2 ,s3 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a V s ′′ 2 ,s3 ν = W s3,s ′′ 2 ∨ s ′′ 2 τ →s4 V ′ s ′′ 2 ,s4,s3 V ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ V s4,s3 W s3,s ′′ 2 ν = (s 3 = s ′′ 2 ) ∨ s3 τ →s ′ 3 W ′ s3,s ′ 3 ,s ′′ 2 W ′ s3,s ′ 3 ,s ′′ 2 ν = X s3,s ′ 3 ∧ W s ′ 3 ,s ′′ 2                                  s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 3 -R 7 -R 8 Combining the boolean formulas corresponding to the four diagrams R 1 , R 3 , R 7 , R 8 yields the following:

                 X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τ * c →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true                  s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the second and third disjunct):

       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s3 τ * c →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τ * c →s4 true        s 1 , s 2 , s 3 ∈ S, a ∈ A
Further simplifications (absorption of the disjunct

                     X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = s3 τc →s4 true U s2,s3,a ν = s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 V s ′′ 2 ,s3 V s ′′ 2 ,s3 ν = W s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 W s3,s4 W s3,s4 ν = s3 τ * c →s4 true                      s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

RR n 7000

Finally, after encoding τ -closures using boolean equations, we obtain a Bes identical to the one for

R 1 -R 3 -R 4 -R 8 :                                  X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s4 X s3,s4 U s2,s3,a ν = (a = τ ∧ V s2,s3 ) ∨ s2 a →s ′′ 2 V s ′′ 2 ,s3 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2.s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a V s ′′ 2 ,s3 ν = W s3,s ′′ 2 ∨ s ′′ 2 τ →s4 V ′ s ′′ 2 ,s4,s3 V ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ V s4,s3 W s3,s ′′ 2 ν = (s 3 = s ′′ 2 ) ∨ s3 τ →s ′ 3 W ′ s3,s ′ 3 ,s ′′ 2 W ′ s3,s ′ 3 ,s ′′ 2 ν = X s3,s ′ 3 ∧ W s ′ 3 ,s ′′ 2                                  s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 2 Combining the boolean formulas corresponding to the two diagrams R 1 , R 2 yields the following:

   X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true    s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the first disjunct):

   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τc →s4 true    s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (factoring τ -closures apart into equations) yield the following Bes:

           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = U s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 U s3,s4 U s3,s ′′ 2 ν = s3 τc →s ′′ 2 true            s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A
Finally, after encoding τ -closures using boolean equations, we obtain a Bes identical to the one for R 2 :

               X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s2,s3 ) ∨ s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = U s3,s ′′ 2 ∨ s ′′ 2 τ →s4 Z ′ s ′′ 2 ,s4,s3 Z ′ s ′′ 2 .s4,s3 ν = X s ′′ 2 ,s4 ∨ Z s4,s3 U s3,s ′′ 2 ν = (s 3 = s ′′ 2 ) ∨ s3 τ →s ′′ 2 X s3,s ′′ 2                s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

INRIA

Encoding of the path R 1 -R 5 Combining the boolean formulas corresponding to the two diagrams R 1 , R 5 yields the following:

   X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s4 s3 τ * c →s4 true    s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows:

   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 s3 τc →s4 true ∨ s3 τ * c →s4 true    s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (absorption of the disjunct

     X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 Z s3,s4 Z s3,s4 ν = s3 τ * c →s4 true      s 1 ,s 2 ,s 3 ,s 4 ∈S,a∈A
Finally, after encoding τ -closures using boolean equations, we obtain a Bes identical to the one for R 5 :

         X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 Z s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 Z ′ s3,s ′ 3 ,s4 Z ′ s3,s ′ 3 ,s4 ν = X s3,s ′ 3 ∧ Z s ′ 3 ,s4          s 1 ,s 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 3 Combining the boolean formulas corresponding to the two diagrams R 1 , R 3 yields the following:

   X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τc →s4 true    s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows:

     X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s4 s3 τc →s4 true      s 1 ,s 2 ,s 3 ∈S,a∈A

RR n 7000

Further simplifications (factoring τ -closures apart into equations) yield the following Bes:

           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = Z s2,s3,a ∨ s2 τ * c →s ′ 2 Z s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = s ′ 2 a →s4 U s3,s4 U s3,s4 ν = s3 τc →s4 true            s 1 ,s 2 ,s ′ 2 ,s 3 ,s 4 ∈S,a∈A
Finally, after encoding τ -closures using boolean equations, we obtain a Bes identical to the encoding of R 3 :

             X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = Z s2,s3,a ∨ s2 τ →s ′ 2 Y ′ s2,s ′ 2 ,s3,a Y ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ Y s ′ 2 ,s3,a Z s ′ 2 ,s3,a ν = (a = τ ∧ U s3,s ′ 2 ) ∨ s ′ 2 a →s4 U s3,s4 U s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s4 X s3,s4              s 1 ,s 2 ,s ′ 2 ,s 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 2 -R 6 Combining the boolean formulas corresponding to the three diagrams R 1 , R 2 , R 6 yields the following:

           X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true            s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the first disjunct):

   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s3 τ * c →s4 true    s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (absorption of the disjunct

                 X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 U s3,s4 U s3,s4 ν = s3 τ * c →s4 true V s3,s ′′ 2 ν = s3 τc →s ′′ 2 true                  s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

INRIA

Finally, after encoding τ -closures using boolean equations, we obtain a Bes identical to the encoding of R 6 (note that on the right hand side of Z s ′′ 2 ,s 3 , the disjunct V s 3 ,s ′′ 2 is absorbed by

U s 3 ,s ′′ 2 ):                    X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s2,s3 ) ∨ s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = U s3,s ′′ 2 ∨ s ′′ 2 τ →s4 Z ′ s ′′ 2 ,s4,s3 Z ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ Z s4,s3 U s3,s ′′ 2 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 U ′ s3,s ′ 3 ,s ′′ 2 U ′ s3,s ′ 3 ,s ′′ 2 ν = X s3,s ′ 3 ∧ U s ′ 3 ,s ′′ 2                    s 1 ,s 2 ,s ′′ 2 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 5 -R 6 Combining the boolean formulas corresponding to the three diagrams R 1 , R 5 , R 6 yields the following:

           X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s4 s3 τ * c →s4 true ∨ s2 a →s ′′ 2 τ * c →s4 s3 τ * c →s4 true            s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the first and second disjunct):

   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,
           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = U s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 U s3,s4 U s3,s4 ν = s3 τ * c →s4 true            s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A
Finally, after encoding τ -closures using boolean equations, we obtain a Bes identical to the encoding of R 6 :

                   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s2,s3 ) ∨ s2 a →s ′′ 2 Z s ′′ 2 ,s3 Z s ′′ 2 ,s3 ν = U s3,s ′′ 2 ∨ s ′′ 2 τ →s4 Z ′ s ′′ 2 ,s4,s3 Z ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ Z s4,s3 U s3,s ′′ 2 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 U ′ s3,s ′ 3 ,s ′′ 2 U ′ s3,s ′ 3 ,s ′′ 2 ν = X s3,s ′ 3 ∧ U s ′ 3 ,s ′′ 2                    s 1 ,s 2 ,s ′′ 2 ,s ′ 3 ,s 4 ∈S,a∈A

RR n 7000

Encoding of the path R 1 -R 2 -R 4 Combining the boolean formulas corresponding to the three diagrams R 1 , R 2 , R 4 yields the following:

           X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true            s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the first disjunct):

       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 s ′′ 2 τ * c →s4 s3 τc →s4 true        s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (factoring τ -closures apart into equations) yield the following Bes:

                     X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s ′′ 2 Z s ′′ 2 ,s3 ∨ U s2,s3,a Z s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ W s ′′ 2 ,s3 V s3,s ′′ 2 ν = s3 τc →s ′′ 2 true U s2,s3,a ν = s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 W s ′′ 2 ,s3 W s ′′ 2 ,s3 ν = s ′′ 2 τ * c →s4 V s3,s4                      s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A
Finally, after encoding τ -closures using boolean equations, we obtain the Bes below:

                             X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s2,s3 ) ∨ s2 a →s ′′ 2 Z s ′′ 2 ,s3 ∨ U s2,s3,a Z s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ W s ′′ 2 ,s3 V s3,s ′′ 2 ν = (s 3 = s ′′ 2 ) ∨ s3 τ →s ′′ 2 X s3,s ′′ 2 U s2,s3,a ν = (a = τ ∧ W s2,s3 ) ∨ s2 a →s ′′ 2 W s ′′ 2 ,s3 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a W s ′′ 2 ,s3 ν = V s3,s ′′ 2 ∨ s ′′ 2 τ →s4 W ′ s ′′ 2 ,s4,s3 W ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ W s4,s3                              s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A

INRIA

Encoding of the path R 1 -R 3 -R 4 Combining the boolean formulas corresponding to the three diagrams R 1 , R 3 , R 4 yields the following:

           X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s4 s3 τc →s4 true            s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows (note that s 4 was renamed into s ′′ 2 in the second disjunct):

       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 s3 τc →s ′′ 2 true ∨ s ′′ 2 τ * c →s4 s3 τc →s4 true        s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (factoring τ -closures apart into equations) yield the following Bes:

                 X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = s3 τc →s4 true U s2,s3,a ν = s2 τ * c →s ′ 2 s ′ 2 a →s ′′ 2 V s ′′ 2 ,s3 V s ′′ 2 ,s3 ν = Z s3,s ′′ 2 ∨ s ′′ 2 τ * c →s4 Z s3,s4                  s 1 ,s 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A
Finally, after encoding τ -closures using boolean equations, we obtain the Bes below:

                         X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s4 X s3,s4 U s2,s3,a ν = (a = τ ∧ V s2,s3 ) ∨ s2 a →s ′′ 2 V s ′′ 2 ,s3 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2.s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a V s ′′ 2 ,s3 ν = Z s3,s ′′ 2 ∨ s ′′ 2 τ →s4 V ′ s ′′ 2 ,s4,s3 V ′ s ′′ 2 ,s4,s3 ν = X s ′′ 2 ,s4 ∧ V s4,s3                          s 1 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 3 -R 7 Combining the boolean formulas corresponding to the three diagrams R 1 , R 3 , R 7 yields the following:

           X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τ * c →s4 true            s 1 ,s 2 ∈S

RR n 7000

Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows:

       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 s3 τc →s4 true ∨ s2 τ * c →s ′ 2 s ′ 2 a →s4 s3 τc →s4 true ∨ s3 τ * c →s4 true        s 1 ,s 2 ,s 3 ∈S,a∈A
Further simplifications (absorption of the disjunct

                 X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = s3 τc →s4 true U s2,s3,a ν = s2 τ * c →s ′ 2 s ′ 2 a →s4 V s3,s4 V s3,s4 ν = s3 τ * c →s4 true                  s 1 ,s 2 ,s 3 ,s 4 ∈S,a∈A
Finally, after encoding τ -closures using boolean equations, we obtain the Bes below:

                         X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s4 X s3,s4 U s2,s3,a ν = (a = τ ∧ V s3,s2 ) ∨ s2 a →s4 V s3,s4 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a V s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 V ′ s3,s ′ 3 ,s4 V ′ s3,s ′ 3 ,s4 ν = X s3,s ′ 3 ∧ V s ′ 3 ,s4                          s 1 ,s 2 ,s ′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
Encoding of the path R 1 -R 5 -R 7 Combining the boolean formulas corresponding to the three diagrams R 1 , R 5 , R 7 yields the following:

           X s1,s2 ν = s1 a →s3 s2 a →s4 s3 τc →s4 true ∨ s2 a →s4 s3 τ * c →s4 true ∨ s2 τ * c →s ′ 2 a →s4 s3 τ * c →s4 true            s 1 ,s 2 ∈S
Upon simplification and factorization of common disjunctive subformulas, the Bes above becomes as follows:

       X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,
           X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = s3 τ * c →s4 true U s2,s3,a ν = s2 τ * c →s ′ 2 s ′ 2 a →s4 Z s3,s4            s 1 ,s 2 ,s 3 ,s 4 ∈S,a∈A
Finally, after encoding τ -closures using boolean equations, we obtain the Bes below:

                   X s1,s2 ν = s1 a →s3 Y s2,s3,a Y s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 ∨ U s2,s3,a Z s3,s4 ν = (s 3 = s 4 ) ∨ s3 τ →s ′ 3 Z ′ s3,s ′ 3 ,s4 Z ′ s3,s ′ 3 ,s4 ν = X s3,s ′ 3 ∧ Z s ′ 3 ,s4 U s2,s3,a ν = (a = τ ∧ Z s3,s2 ) ∨ s2 a →s4 Z s3,s4 ∨ s2 τ →s ′ 2 U ′ s2,s ′ 2 ,s3,a U ′ s2,s ′ 2 ,s3,a ν = X s2,s ′ 2 ∧ U s ′ 2 ,s3,a                    s 1 ,s 2 ,s ′ 2 ,s 3 ,s ′ 3 ,s 4 ∈S,a∈A
RR n 7000

B Proofs of the BES Encodings

We prove in the sequel the correctness of our Bes encoding for weak τ -confluence (R 8 in Figure 1). The correctness proofs for encodings of τ -confluences R 1 , . . . , R 7 and the hierarchical encodings are very similar to the one for R 8 and are therefore left as exercise for the interested reader.

A few additional notions are needed in order to proceed. Let M = S, A, T , s 0 be an Lts.

Γ( b s 1 ,s 2 s 1 ,s 2 ∈S ) = { s 1 , s 2 | b s 1 ,s 2 = true}.
It is straightforward to show that Γ is an isomorphism, i.e., it is a bijection preserving the compatibility of operations (b

⊑ b ′ ⇔ Γ(b) ⊆ Γ(b ′ ), Γ(false |S| 2 ) = ∅, Γ(true |S| 2 ) = S 2 , Γ(b ⊔ b ′ ) = Γ(b) ∪ Γ(b ′ ), and Γ(b ⊓ b ′ ) = Γ(b) ∩ Γ(b ′ )).
Furthermore, we define that b s 1 ,s 2 = true iff s 1 τc → s 2 , i.e. b s 1 ,s 2 expresses whether there exists a confluent τ -transition between states s 1 and s 2 .

We provide below a definition of weak τ -confluence, based on the definitions of τ -confluence by [START_REF] Pace | Calculating τ -Confluence Compositionally[END_REF] and ultra weak confluence by [START_REF] Blom | Partial τ -confluence for Efficient State Space Generation[END_REF], and recall two corresponding Bes encodings given in Section 3.1, namely the direct encoding of diagram R 8 , and the encoding such that each equation contains a single boolean operator, and τ -closures are encoded using maximal fixed point variables.

Definition 2 (Weak τ -confluence) Given an Lts M = S, A, T , s 0 , and S ⊆ S 2 , we say that S is weak τ -confluent in M if for every s 1 , s 2 ∈ S and s 1 a → s 3 , we have s 1 τ → s 2 , and for some n, m, p > 0 there exist s 2,0 , . . . , s 2,n , s ′ 2,0 , . . . , s ′ 2,m , s 4 ∈ S with s 2,0 = s 2 , and s 3,0 , . . . , s 3,p ∈ S with s 3,0 = s 3 such that s 2,i τ → s 2,i+1 and s 2,i , s 2,i+1 ∈ S for 0

≤ i < n, s 2,n a → s ′ 2,0 , s ′ 2,j τ → s ′ 2,j+1 and s ′ 2,j , s ′ 2,j+1 ∈ S for 0 ≤ j < m, s ′ 2
B wtc1 =        X s 1 ,s 2 ν = s 1 a →s 3 s 2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s 4 s 3 τ * c →s 4 true        s 1 ,s 2 ∈S,a∈A

INRIA

The interpretation [[B wtc1 ]] is defined as the maximal fixed point νΦ wtc1 , where Φ wtc1 : Bool |S| 2 → Bool |S| 2 is the (monotonic) functional associated to B wtc1 :

Φ wtc1 ( b s 1 ,s 2 s 1 ,s 2 ∈S ) = [[ s 1 a →s 3 s 2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s 4 s 3 τ * c →s 4 true]][b s 1 ,s 2 /X s 1 ,s 2 ] s 1 ,s 2 ∈S .
Definition 4 (Weak τ -confluence BES) Let M = S, A, T , s 0 be a τ -convergent Lts.

The weak τ -confluent set T(S) ⊆ S 2 is encoded by the maximal fixed point Bes below:

B wtc =                                  X s 1 ,s 2 ν = s 1 a →s 3 Y s 2 ,s 3 ,a Y s 2 ,s 3 ,a ν = Z s 2 ,s 3 ,a ∨ s 2 τ →s ′ 2
From Tarski's theorem [START_REF] Tarski | A Lattice-Theoretical Fixpoint Theorem and its Applications[END_REF], the maximal fixed point νΦ wtc1 can be computed as follows:

νΦ wtc1 = {b ∈ Bool |S| 2 | b ⊑ Φ wtc1 (b)}.
The following lemma provides a link between sets of confluent transitions and the functional associated to the Bes B wtc1 .

Lemma 1 Let (S, A, T , s 0 ) be an Lts, and let b ∈ Bool |S| 2 . Then:

b ⊑ Φ wtc1 (b) iff Γ(b) is weak τ -confluent. Proof If. Let b = b s 1 ,s 2 s 1 ,s 2 ∈S such that Γ(b) is weak τ -confluent. We must show that b ⊑ Φ wtc1 (b).
Let A useful property of weak τ -confluent sets is that they are closed under union, i.e., the union of two weak τ -confluent sets is also weak τ -confluent. This property can be easily shown for our notion of weak τ -confluence in the same way it was shown for τ -confluence in [START_REF] Groote | State Space Reduction using Partial τ -Confluence[END_REF]. The proposition below states the correctness of the direct Bes encoding of weak τ -confluence. Before proving the correctness of B wtc , we show first a lemma concerning the computation of τ -closures using boolean equations, and then we show the main proposition.

= s 3 such that s 2,i τ → s 2,i+1 and s 2,i , s 2,i+1 ∈ S for 0 ≤ i < n, s 2,n a → s ′ 2,0 , s ′ 2,j τ → s ′ 2,j+1 and s ′ 2,j , s ′ 2,j+1 ∈ S for 0 ≤ j < m, s ′ 2
Lemma 2 Let M = S, A, T , s 0 be a τ -convergent Lts, and consider the Bess: From Tarski's theorem [START_REF] Tarski | A Lattice-Theoretical Fixpoint Theorem and its Applications[END_REF], this implies νΦ δ ⊑ νΦ ′ δ . It remains to show that the strict inclusion νΦ δ < νΦ ′ δ does not hold. Suppose that νΦ δ < νΦ ′ δ , meaning that:

B =          Y s 2 ,
(νΦ δ ) s 2 ,s 3 ,a , (νΦ δ ) s ′′ 2 ,s 3 , (νΦ δ ) s 3 ,s 4 < (νΦ ′ δ ) s 2 ,s 3 ,a , (νΦ ′ δ ) s ′′ 2 ,s 3 , (νΦ ′ δ ) s 3 ,s 4

Three cases are possible, depending on whether the first, the second, or the third component of νΦ δ is smaller than the corresponding component of νΦ ′ δ . We begin by considering the first case. Let s 2 , s 3 ∈ S and a ∈ A such that (νΦ δ ) s 2 ,s 3 ,a = false and (νΦ ′ δ ) s 2 ,s 3 ,a = true. From the definition of Φ δ , we infer that contradicts the hypothesis of M being τ -convergent, and therefore concludes the proof for the first case.

Next, we look at the third case. Let s 3 , s 4 ∈ S and a ∈ A such that (νΦ δ ) s 3 ,s 4 = false and (νΦ ′ δ ) s 3 ,s 4 = true. From the definition of Φ δ , we infer that From the definition of Φ ′ δ and the fact that νΦ ′ δ is a fixed point, we infer that (s 3 = s 4 ) ∨ true. By assumption, we know that δ(X s ′′ 2 ,s 4 ) = true, hence it remains to be shown that (νΦ ′ δ ) s 4 ,s 3 = true. By repeating the above reasoning, each time, we can distinguish two possibilities; since the first possibility always infers an infinite τ -sequence from s 3 , contradicting the hypothesis of M being τ -convergent, we have to consider the second possibility every time. By this, we can construct an infinite sequence (s =)s 2,0 Proof By Proposition 1, we have [[B wtc1 ]] = T(S). Note that this proof is valid for arbitrary Ltss, and therefore also for τ -convergent Ltss. From this, we progressively refine B wtc1 until obtaining the full Bes encoding given by Definition 4.

We now refine the Bes B wtc1 into a Bes B wtc2 by replacing certain subformulas with new variables defined by additional equations, such that the right-hand side of each equation of B wtc2 contains a single type of boolean operator:

B wtc2 =                      X s 1 ,

  k+1 and s 3,k , s 3,k+1 ∈ S for 0 ≤ k < p, and s 3,p τ → s 4 and s 3,p , s 4 ∈ S. The maximal τ -confluent set T(S) ⊆ S 2 is the union of all τ -confluent sets of M.

1 τ → s 2 variableFigure 2 :

 122 Figure 2: Architecture of the τ -confluence reductorCurrently the τ -confluence reductor module covers all the weak τ -confluence variants of the hierarchy considered in Section 2 by implementing the sixteen different Bes encodings identified in Section 3 (eight individual encodings and eight hierarchical ones). Since this module acts as a filter on implicit Ltss, it can be easily plugged in the architecture of various on-the-fly verification tools of Cadp in order to improve their performance by reducing the Lts simultaneously with the verification. In the next section, we show the application of this

Figure 3 :→ s 4 or s ′′ 2 τ * c → s 4

 324 Figure 3: Performance of weak τ -confluence reductions (I)

Figure 4 :

 4 Figure 4: Performance of weak τ -confluence reductions (II)

  τ -closures apart into equations) yield the following Bes:

  τ -closures apart into equations) yield the following Bes:

  τ -closures apart into equations) yield the following Bes:

  τ -closures apart into equations) yield the following Bes:

  τ -closures apart into equations) yield the following Bes:

  τ -closures apart into equations) yield the following Bes:

  τ -closures apart into equations) yield the following Bes:

  τ -closures apart into equations) yield the following Bes:

  τ -closures apart into equations) yield the following Bes:

s 1

 1 ,s 2 ,s 3 ∈S,a∈A INRIA Further simplifications (absorption of the disjunct τ -closures apart into equations) yield the following Bes:

,m τ → s 4

 4 and s ′ 2,m , s 4 ∈ S, s 3,k τ → s 3,k+1 and s 3,k , s 3,k+1 ∈ S for 0 ≤ k < p, and s 3,p τ → s 4 and s 3,p , s 4 ∈ S. The maximal τ -confluent set T(S) ⊆ S 2 is the union of all τ -confluent sets of M. Definition 3 (Directly encoded weak τ -confluence BES) Let (S, A, T , s 0 ) be a τ -convergent Lts. The weak τ -confluent set T(S) ⊆ S 2 is directly encoded by the maximal fixed point Bes below:

,m τ → s 4 1 a→ s 3 → s 3 ,→ s 4 . 1 a 4 true[[ s 1 a →s 3 s 2 [[ s 1 a →s 3 s 2 τ * c →s ′ 2 a →s ′′ 2 τ * c →s 4 s 3 τ * c →s 4 INRIA Let s 1 a→ s 3 4 true 2 and s 2 ,n = s ′ 2 , s 2 2 ,

 41334141212223413422222 and s ′ 2,m , s 4 ∈ S, s 3,k τ → s 3,k+1 and s 3,k , s 3,k+1 ∈ S for 0 ≤ k < p, and s 3,p τ → s 4 and s 3,p , s 4 ∈ S.Let s be a transition. From the condition above, for some n, m, p > 0 there exist s 2,0 , . . . , s 2,n , s ′ 2,0 , . . . , s ′ 2,m , s 4 ∈ S with s 2,0 = s 2 , and s 3,0 , . . . , s 3,p ∈ S with s 3,0 = s 3 such that s 2,i τ → s 2,i+1 for 0 ≤ i < n, s 2,n a k+1 for 0 ≤ k < p, and s 3,p τ This means that s 2,i , s 2,i+1 ∈ Γ(b), which from the definition of Γ implies b s 2,i ,s 2,i+1 = true, for 0≤ i < n, s ′ 2,j , s ′ 2,j+1 ∈ Γ(b), which implies b s ′ 2,j ,s ′ 2,j+1 = true, for 0 ≤ j < m, s ′ 2,m , s 4 ∈ Γ(b), which implies b s ′ 2,m ,s 4 = true, s 3,k , s 3,k+1 ∈ Γ(b), which implies b s 3,k ,s 3,k+1 = true, for 0 ≤ k < p,and s 3,p , s 4 ∈ Γ(b), which implies b s 3,p ,s 4 = true. Furthermore, it means that s 3,k , s 3,k+1 ∈ Γ(b), which from the definition of Γ implies b s 3,k ,s 3,k+1 = true, for 0 ≤ k < p, and s 3,p , s 4 ∈ Γ(b), which implies b s 3,p ,s 4 = true. By definition of b s 1 ,s 2 , this means that the boolean formula s is also true. From the interpretation of boolean formulas given in Definition 3, this implies: [b s 1 ,s 2 /X s 1 ,s 2 ] s 1 ,s 2 ∈S = true meaning that (Φ wtc1 (b)) = true. Therefore, b ⊑ Φ wtc1 (b). Only if. Let b = b s 1 ,s 2 s 1 ,s 2 ∈S such that b ⊑ Φ wtc1 (b). We must show that Γ(b) is weak τ -confluent, i.e., it satisfies Definition 2. Let s 1 , s 2 ∈ Γ(b). From the definition of Γ, this implies b s 1 ,s 2 = true. Since b ⊑ Φ wtc1 (b), from Definition 3 and the interpretation of boolean formulas, this implies:true]][b s 1 ,s 2 /X s 1 ,s 2 ] s 1 ,s 2 ∈S = true. be a transition. From the condition above, each conjunct associated to such a transition must be true, i.e., = true. This means that some disjunct corresponding to transitions s 2,i τc → s 2,i+1 for some n > 0 with 0 ≤ i < n, s 2,0 = s j+1 for some m > 0 with 0 ≤ j < m and s ′ 2,0 = s ′′ 2 , s ′ 2,m τc → s 4 , s 3,k τc → s 3,k+1 for some p > 0, with 0 ≤ k < p and s 3,0 = s 3 , and s 3,p τc → s 4 , must be true. From the definition of b s 1 ,s 2 , this implies that for 0 ≤ i < n, 0 ≤ j < m, and 0 ≤ k < p, we have b s 2,i ,s 2,i+1 = true, b s ′ 2,j ,s ′ 2,j+1 = true, and b s 3,k ,s 3,k+1 = true. Besides that, b s ′ 2,m ,s 4 = true and b s 3,p ,s 4 = true. This, by the definition of Γ, implies that s 2,i , s 2,i+1 ∈ Γ(b) for 0 ≤ i < n, s ′ 2,j , s ′ 2,j+1 ∈ Γ(b) for 0 ≤ j < m, s 3,k , s 3,k+1 ∈ Γ(b) for 0 ≤ k < p, s ′ 2,m , s 4 ∈ Γ(b), and s 3,p , s 4 ∈ Γ(b), which means that Γ(b) satisfies Definition 2, and therefore Γ(b) is a weak τ -confluent set. 2

Proposition 1 (

 1 Correctness of directly encoded weak τ -confluence BES) Let M = (S, A, T , s 0 ) be an Lts, and let B wtc1 be the Bes directly encoding a weak τ -confluent set of M. Then:Γ([[B wtc1 ]]) = T(S). Proof Γ([[B wtc1 ]]) = Γ(νΦ wtc1 ) by Definition 3 = Γ( {b | b ∈ Bool |S| 2 ∧ b ⊑ Φ wtc1 (b)}) by Tarski's theorem = {Γ(b) | b ∈ Bool |S| 2 ∧ b ⊑ Φ wtc1 (b)} by Γ isomorphism = {Γ(b) | b ∈ Bool |S| 2 ∧ Γ(b) is confluent} by Lemma 1 = {U ⊆ S 2 | U is confluent} by Γ bijection = T(S)by closure under union. 2

4 V s 3 ,s 4 V s 3 (s 3 = s 4 ) 4 true 2 δ(Z s ′ 2 ,s 3 4 true) s 3 ,s 4 )) s ′′ 2 ,s 3 , ( s 3 τ * c →s 4 true) s 3 ,s 4 by

 43433442234342344 by definition of τ c and the assumption about δ concerning X s 1 ,s 2 = ( ,a )) s 2 ,s 3 ,a , ( definition of τ -closure = νΦ δ by definition of νΦ δ .

4 true

 4 = false, meaning that there is no τsequence going out of s 3 , leading to state s 4 .

τ → s 2 , 1 τ→ s 2 , 2 τ 2 Proposition 2 (

 212222 → • • •with s 2,0 = s ′′ 2 and s 2,1 = s 4 such that (νΦ ′ δ ) s 2,i ,s 3 = true for all i ≥ 0. This contradicts the hypothesis of M being τ -convergent, and therefore concludes the proof for this possibility of the third case. Correctness of weak τ -confluence BES) Let M = S, A, T , s 0 be a τ -convergent Lts, and let B wtc be the Bes encoding the weak τ -confluent set of M. Then:Γ([[B wtc ]]) = T(S).

3 Y s 2 4 V s 3 ,s 4 V s 3 s 1 4 V s 3 ,s 4 V s 3 ,s 4 νs 2

 3243431434342 ,s 3 ,a Y s 2 ,s 3 ,s 2 ,s ′ 2 ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A This transformation into a simple Bes B wtc2 does not change the interpretation of the variables X s 1 ,s 2 of the original Bes, i.e., ([[B wtc1 ]]) Xs 1 ,s 2 = ([[B wtc2 ]]) Xs 1 ,s 2 for all s 1 , s 2 ∈ S. The final step towards the Bes B wtc given in Definition 4 is to get rid of the τ -closures present in the right-hand sides of the equations defining Y s 2 ,s 3 ,a , U s ′ 2 ,s 3 , and V s 3 ,s 4 . To achieve this, we consider the following Bes: ,s ′′ 2 ,s 3 ,s 4 ∈S,a∈A RR n 7000

  Consider the two lattices Bool |S| 2 , ⊑, false |S| 2 , true |S| 2 , ⊔, ⊓ and 2 S 2 , ⊆, ∅, S 2 , ∪, ∩ , where the relation ⊑ and the operations ⊔, ⊓ are defined as the pointwise extensions of the boolean connectors ⇒, ∨, and ∧, respectively. These lattices are isomorphic, being related by the function Γ : Bool |S| 2 → 2 S 2 defined below:

  s 1 , s 2 ∈ S such that b s 1 ,s 2 = true. From the definition of Γ, this implies s 1 , s 2 ∈ Γ(b). Since Γ(b) is weak τ -confluent, from Definition 2 this implies that for all s 1 , and for some n, m, p > 0 there exist s 2,0 , . . . , s 2,n , s ′ 2,0 , . . . , s ′ 2,m , s 4 ∈ S with s 2,0 = s 2 , and s 3,0 , . . . , s 3,p ∈ S with s 3,0

	have s 1	τ → s 2	a → s 3 , we

RR n 7000

See http://www.inrialpes.fr/vasy/cadp RR n 7000

See http://www.inrialpes.fr/vasy/cadp/resources/benchmark bcg.html

See http://www.inrialpes.fr/vasy/cadp/demos/demo XX.html RR n 7000

Mateescu & Wijs

Acknowledgements

This research was partially funded by the Ec-Moan project no. 043235 of the Fp6-Nest-Path-Com European program.

We first define some notations, and then we prove the correctness of the Bes encodings for weak τ -confluence.

Definition 5 Let X be a set of boolean variables including X 1 , ..., X n , X n+1 . Let B = {X i ν = ϕ i } 1≤i≤n and B ′ = {X i ν = ϕ i } 1≤i≤n+1 be two Bess having their first n equations identical (ϕ i are boolean formulas built from disjunctions and conjunctions) and δ : X → Bool be a context. Let Φ δ : Bool n → Bool n and Φ ′ δ : Bool n+1 → Bool n+1 be the two functionals associated to B and B ′ in the context δ:

where δ ⊘ [b j /X j ] 1≤j≤n denotes a context identical to δ except for variables X 1 , ..., X n , which are assigned values b 1 , ..., b n . According to Kleene's theorem [START_REF] Kleene | Introduction to Metamathematics[END_REF], the maximal fixed points of the functionals Φ δ and Φ ′ δ can be computed as follows:

The notation e i , e 1≤i≤n , where e i and e are boolean expressions, is a shorthand for e 1 , ..., e n , e . We define the series U k ∈ Bool n+1 associated to B, B ′ , and δ as follows:

We are now ready to show the correctness of the Bes encodings for weak τ -confluence. We start by proving the correctness of B wtc1 .

, where B ′ is defined as follows:

By virtue of Lemma 4 of the full version of [START_REF] Mateescu | Improved On-the-Fly Equivalence Checking using Boolean Equation Systems[END_REF], these Bess have the same interpretation (the context δ becomes useless since both Bess are closed), meaning that B wtc has in turn the same interpretation as B wtc1 , and thus it reflects the weak τ -confluent set of the τ -convergent Lts M correctly.