Gabriel Kalyon

Tristan Le Gall

Hervé Marchand

Thierry Massart

Global State Estimates for Distributed Systems

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

During the execution of a computer system, the knowledge of its global state may be crucial information, for instance to control which action can or must be done, to monitor its behavior or perform some diagnostic. Distributed systems, are generally divided into two classes, depending on whether the communication between subsystems is synchronous or not. When the synchrony hypothesis [START_REF] Berry | The esterel synchronous programming language: Design, semantics, implementation[END_REF] can be made, each local subsystem can easily know, at each step of the execution, the global state of the system (assuming that there is no internal action). When considering asynchronous distributed systems, this knowledge is in general impossible, since the communication delays between the components of the system must be taken into account. Therefore, each local subsystem can a priori not immediately know either the local state of the other subsystems or the messages that are currently in transfer.

In this paper, we are interested in the asynchronous framework where we consider that the system is composed of n subsystems that asynchronously communicate through reliable unbounded FIFO channels. These subsystems are modeled by communicating finite state machines (CFSM) [START_REF] Brand | On communicating finite-state machines[END_REF] that explicitly express the work and communications of a distributed system. This model appears to be essential for concurrent systems in which components cooperate via asynchronous message passing through unbounded buffers (they are e.g. widely used to model communication protocols). We thus assume that the distributed system is already built and the architecture of communication between the different subsystems is fixed. Our aim is to provide an algorithm that allows us to compute, in each subsystem of a distributed system T , an estimate of the current state of T . More precisely, each subsystem or a local associated estimator computes a set of possible global states, including the contents of the channels, in which the system T can be; it can be seen as a particular case of monitoring with partial observation. In our framework, we assume that the subsystems (or associated estimators) can record their own state estimate and that some extra information can be piggybacked to the messages normally exchanged by the subsystems. Indeed, without this additional information, since a local subsystem cannot observe the other subsystems nor the FIFO channel contents, the computed state estimates might be too rough. Our computation is based on the use of the reachability operator, which cannot always be done in the CFSM model for undecidability reasons. To overcome this obstacle, we rely on the abstract interpretation techniques we presented previously in [START_REF] Gall | Verification of communication protocols using abstract interpretation of fifo queues[END_REF]. They ensure the termination of the computations of our algorithm by overapproximating in a symbolic way the possible FIFO channel contents (and hence the state estimates) by regular languages. Computing state estimates is useful in many applications. For example, this information can be used to locally control the system in order to prevent it from reaching some given forbidden global states [START_REF] Cassandras | Introduction to Discrete Event Systems[END_REF], or to perform some diagnosis to detect some faults in the system [START_REF] Debouk | Coordinated decentralized protocols for failure diagnosis of discrete event systems[END_REF][START_REF] Sampath | Failure diagnosis using discrete event models[END_REF]. For these two potential applications, a more precise state estimate allows the controller or the diagnoser to take better decisions. This problem differs from the synthesis problem (see e.g. [START_REF] Massart | A calculus to define correct tranformations of lotos specifications[END_REF][START_REF] Genest | On implementation of global concurrent systems with local asynchronous controllers[END_REF][START_REF] Chatain | Natural specifications yield decidability for distributed synthesis of asynchronous systems[END_REF]) which consists in synthesizing a distributed system (together with its architecture of communication) equivalent to a given specification. It also differs from the methodology described in [START_REF] Hélouet | Diagnosis from scenarios[END_REF] in the sense that in their framework, the authors try to infer from a distributed observation of a distributed system (modeled by a High Level Message Sequence Chart) the set of sequences that explains this observation. It is also different from model checking techniques [START_REF] Boigelot | The power of QDDs[END_REF][START_REF] Bouajjani | Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations[END_REF][START_REF] Finkel | Well-abstracted transition systems: application to fifo automata[END_REF][START_REF] Heußner | Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems[END_REF] that proceed to a symbolic exploration of all the possible states of the system, without running it. We however use the same symbolic representation of queue contents as in [START_REF] Boigelot | The power of QDDs[END_REF][START_REF] Heußner | Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems[END_REF]. In [START_REF] Xu | Distributed state estimation in discrete event systems[END_REF], Kumar and Xu propose a distributed algorithm which computes an estimate of the current state of a system. More precisely, local estimators maintain and update local state estimates from their own observation of the system and information received from the other estimators. In their framework, the local estimators communicate between them through reliable FIFO channels with delays, whereas the system is monolithic and therefore in their case, a global state is simpler than for our distributed systems composed of several subsystems together with communicating FIFO channels. In [START_REF] Tripakis | Decentralized control of discrete event systems with bounded or unbounded delay communication[END_REF], Tripakis studies the decidability of the existence of controllers such that a set of responsiveness properties is satisfied in a decentralized framework with communication delays between the controllers. He shows that the problem is undecidable when there is no communication or when the communication delays are unbounded. He conjectures that the problem is decidable when the communication delays are bounded. Other works dealing with communication (with or without delay) between agents can be found in [START_REF] Ricker | Mind the gap: Expanding communication options in decentralized discrete-event control[END_REF][START_REF] Lin | Minimal communication for essential transitions in a distributed discrete-event system[END_REF]. Below, in section 2, we define the formalism of communicating finite state machines, that we use. We formally define, in section 3, the state estimate mechanisms and the notion of state estimators. In section 4, we provide an algorithm to compute an estimate of the current state of a distributed system and prove its correctness. We explain, in section 5, how we can ensure the termination of this algorithm by using abstract interpretation techniques. Finally, section 6 gives some experimental results. Technical proofs are given in Appendix A.

We model a distributed system by the standard formalism of communicating finite state machines [START_REF] Brand | On communicating finite-state machines[END_REF] which use reliable unbounded FIFO channels (also called queues) to communicate. A global state in this model is given by the local state of each subsystem together with the content of each FIFO queue. Therefore, since no bound is given either in the transmission delay, or on the length of the FIFO queues, the global state space of the distributed system is a priori infinite.

Definition 1 (Communicating Finite State Machines).

A communicating finite state machine (CFSM) T is defined as a 6-tuple L, 0 , Q, M, Σ, ∆ , where (i) L is a finite set of locations, (ii) 0 ∈ L is the initial location, (iii) Q is a set of queues that T can use, (iv) M is a finite set of messages, (v) Σ ⊆ Q × {!, ?} × M is a finite set of actions, that are either an output a!m to specify that the message m ∈ M is written on the queue a ∈ Q or an input a?m to specify that the message m ∈ M is read on the queue a ∈ Q, (vi) ∆ ⊆ L × Σ × L is a finite set of transitions.

An output transition , i!m,

indicates that when the system moves from the location to , a message m is added at the end of the queue i. An input transition , i?m, indicates that, when the system moves from to , a message m must be present at the beginning of the queue i and is removed from this queue. Moreover, throughout this paper, we assume that T is deterministic, meaning that for all ∈ L and σ ∈ Σ, there exists at most one location ∈ L such that , σ, ∈ ∆. For σ ∈ Σ, Trans(σ) denotes the set of transitions of T labeled by σ. The occurrence of a transition will be called an event and given an event e, δ e denotes the corresponding transition. Note that the model could also have included internal events; but, since it does not bring any particular difficulty, to simplify the presentation, we have not integrated them here. The semantics of a CFSM is defined as follows:

Definition 2 (Semantics). The semantics of a CFSM T = L, 0 , Q, M, Σ, ∆ is given by an infinite Labeled Transition System (LTS) [[T ]] = X, x 0 , Σ, → , where (i) X def = L × (M * ) |Q| is the set of states, (ii) x 0 def = 0 , , . . . , is the initial state, (iii) Σ is the set of actions, and (iv)

→ def = δ∈∆ δ -→ ⊆ X × Σ × X is the transition relation where δ -→ is defined by: δ = , i!m, ∈ ∆ w i = w i • m , w 1 , . . . , w i , . . . , w |Q| δ → , w 1 , . . . , w i , . . . , w |Q| δ = , i?m, ∈ ∆ w i = m • w i , w 1 , . . . , w i , . . . , w |Q| δ → , w 1 , . . . , w i , . . . , w |Q| A global state of a CFSM T is thus a tuple , w 1 , ..., w |Q| ∈ X = L × (M * ) |Q|
where is the current location of T and w 1 , ..., w |Q| are finite words on M * which give the content of the queues in Q. At the beginning, all queues are empty, so the initial state is x 0 = 0 , ε, • • • , ε . Given a CFSM T , two states x, x ∈ X and an event e, to simplify the notations we sometimes denote

x δe → x by x e → x . An execution of T is a sequence x 0 e1 -→ x 1 e2 -→ . . . em --→ x m where x i ei+1 ---→ x i+1 ∈-→ ∀i ∈ [0, m-1]. Given a set of states Y ⊆ X, Reach T ∆ (Y ) corresponds to the set of states that are reachable in [[T ]] from Y only firing transitions of ∆ ⊆ ∆ in T . It is defined by Reach T ∆ (Y ) def = n≥0 (Post T ∆ (Y )) n where (Post T ∆ (Y )) n is the n th functional power of Post T ∆ (Y ), defined by: Post T ∆ (Y ) def = {x ∈ X|∃x ∈ Y, ∃δ ∈ ∆ : x δ → x }.
Although there is no general algorithm that can exactly compute the reachability set in our setting [START_REF] Brand | On communicating finite-state machines[END_REF], there exist some techniques that allow us to compute an overapproximation of this set (see section 5). Given a sequence of actions σ = σ 1 • • • σ m ∈ Σ * and two states x, x ∈ X, x σ → x denotes that the state x is reachable from x by executing σ.

Asynchronous Product. A distributed system T is generally composed of several subsystems T i (∀i ∈ [1, n]) acting in parallel. In fact, T is defined by a CFSM resulting from the asynchronous (interleaved) product of the n subsystems T i , also modeled by CFSMs. This can be defined through the asynchronous product of two subsystems.

Definition 3. Given 2 CFSMs T i = L i , 0,i , Q i , M i , Σ i , ∆ i (i = 1, 2), their asyn- chronous product, denoted by T 1 ||T 2 , is defined by a CFSM T = L, 0 , Q, M, Σ, ∆ , where L def = L 1 × L 2 , 0 def = 0,1 × 0,2 , Q def = Q 1 ∪ Q 2 , M def = M 1 ∪ M 2 , Σ def = Σ 1 ∪ Σ 2 , and ∆ def = { 1 , 2 , σ 1 , 1 , 2 |( 1 , σ 1 , 1 ∈ ∆ 1 ) ∧ ( 2 ∈ L 2 )} ∪ { 1 , 2 , σ 2 , 1 , 2 |( 2 , σ 2 , 2 ∈ ∆ 2 ) ∧ ( 1 ∈ L 1 )}.
Note that in the previous definition, Q 1 and Q 2 are not necessarily disjoint; this allows the subsystems to communicate between them via common queues. Composing the various subsystems T i (∀i ∈ [1, n]) two-by-two in any order and again for their results gives the global distributed system T whose semantics (up to state isomorphism) does not depend on the order of grouping.

Definition 4 (Distributed system). A distributed system T = L, 0 , Q, M, Σ, ∆ is defined by the asynchronous product of n CFSMs

T i = L i , 0,i , Q i , M, Σ i , ∆ i (∀i ∈ [1, n])
acting in parallel and exchanging information through FIFO channels.

Note that a distributed system is also modeled by a CFSM, since the asynchronous product of several CFSMs is a CFSM. To avoid the confusion between the model of one process and the model of the whole system, in the sequel, a CFSM T i always denotes the model of a single process, and a distributed system T = L, 0 , Q, M, Σ, ∆ always denotes the model of the global system, as in Definition 4. Below, unless stated explicitly, T = T 1 || . . . ||T n is the considered distributed system.

Communication Architecture of the System. We consider an architecture for the system T = T 1 || . . . ||T n defined in Definition 4 with point-to-point communication i.e., any subsystem T i can send messages to any other subsystem T j through a queue 4 Q i,j . Thus, only T i can write a message m on Q i,j (this is denoted by Q i,j !m) and only T j can read a message m on this queue (this is denoted by Q i,j ?m). Moreover, we suppose that the queues are unbounded, that the message transfers between the subsystems are reliable and may suffer from arbitrary non-zero delays, and that no global clock or perfectly synchronized local clocks are available. With this architecture, the set

Q i of T i (∀i ∈ [1, n]) can be rewritten as Q i = {Q i,j , Q j,i | (1 ≤ j ≤ n) ∧ (j = i)} and ∀j = i ∈ [1, n], Σ i ∩ Σ j = ∅. Let δ i = i , σ i , i ∈ ∆ i be a transition of T i , global(δ i ) def = { 1 , . . . , i-1 , i , i+1 , . . . , n , σ i , 1 , . . . , i-1 , i , i+1 , . . . , n ∈ ∆ |∀j = i ∈ [1, n] : j ∈ L j }
is the set of transitions of ∆ that can be built from δ i in T . We extend this definition to sets of transitions D ⊆ ∆ i of the subsystem T i : global(D) def = δi∈D global(δ i ). We abuse notation and write ∆ \ ∆ i instead of ∆ \ global(∆ i ) to denote the set of transitions of ∆ that are not built from ∆ i . Given the set Σ i of T i (∀i ∈ [1, n]) and the set Σ of T , the projection P i of Σ onto Σ i is standard: P i (ε) = ε and ∀w ∈ Σ * , ∀a ∈ Σ, P i (wa) = P i (w)a if a ∈ Σ i , and P i (w) otherwise. The inverse projection

P -1 i is defined, for each L ⊆ Σ * i , by P -1 i (L) = {w ∈ Σ * | P i (w) ∈ L}. B 0 B 1 B 2 B 3 C 0 C 1 A 1 A 2 A 0 A er Q 2,1 ?b Q 2,1 ?b Q 2,1 ?b Q 2,1 !b T 1 T 2 T 3 Q 1,2 !c Q 2,1 ?a Q 3,1 ?d Q 2,1 ?a Q 1,2 !d Q 2,1 ?a Q 1,2 ?c Q 2,1 !a Q 2,3 !d Q 2,3 !d Q 1,2 ?d Q 2,3 ?d Q 3,1 !d Example 1.
Let us illustrate the concepts of distributed system and CFSM with our running example depicted on the right hand side. It models a factory composed of three components T 1 , T 2 and T 3 . The subsystem T 2 produces two kinds of items, a and b, and sends these items to T 1 to finish the job. At reception, T 1 must immediately terminate the process of each received item. T 1 can receive and process b items at any time, but must be in a turbo mode to receive and process a items. The subsystem T 1 can therefore be in normal mode modeled by the location A 0 or in turbo mode (locations A 1 and A 2 ). In normal mode, if T 1 receives an item a, an error occurs (transition in location A er ). Since T 1 cannot always be in turbo mode, a protocol between T 1 and T 2 is imagined. At the beginning, T 1 informs (connect action, modeled by Q1,2!c → ) T 2 that it goes in a turbo mode, then T 2 sends a and b items. At the end of a working session, T 2 informs T 1 (disconnect action, modeled by Q2,3!d → ) that it has completed its session, so that T 1 can go back in normal mode. However, this information has to transit through T 3 via queues Q 2,3 and Q 3,1 , as T 3 must also record this end of session. Since the message d can be transmitted faster than some items a and b, one can easily find a scenario where T 1 decides to go back to A 0 and ends up in the A er location by reading the message a. It is due to the fact that the subsystems cannot observe the content of the queues and thus T 1 does not know whether there is a message a in queue Q 2,1 when it arrives in A 0 . This motivates the interest of computing good state estimates of the current state of the system. Indeed, if each subsystem maintains good estimates of the current state of the system, then T 1 can know whether there is a message a in Q 2,1 , and reach the location A 0 only if it is not the case.

State Estimates of Distributed Systems

We introduce here the framework and the problem we are interested in.

Local View of the Global System. A global state of T = T 1 || . . . ||T n is given by a tuple of locations (one for each subsystem) and the content of all the FIFO queues. Informally our problem consists in defining one local estimator per subsystem, knowing that each of them can only observe the occurrences of actions of its own local subsystem, such that these estimators compute online (i.e., during the execution of the system) estimates of the global state of T . We assume that each local estimator E i has a precise observation of subsystem T i , and that the model of the global system is known by all the estimators (i.e., the structure of each subsystem and the architecture of the queues between them). Each estimator E i must determine online the smallest possible set of global states E i that contains the actual current global state. Note that if E i observes that the location of T i is i , a very rough state estimate is

L 1 × . . . × { i } × • • • × L n × (M * ) |Q| .
In other words all the global states of the system such that location of T i is i ; however, this rough estimate does not provide a very useful information.

Online State Estimates. The estimators must compute the state estimates online. Since each estimator E i is local to its subsystem, we suppose that E i synchronously observes the actions fired by its subsystem; hence since each subsystem is deterministic, each time an event occurs in the local subsystem, it can immediately infer the new location of T i and use this information to define its new state estimate. In order to have better state estimates, we also assume that the estimators can communicate with each other by adding some information (some timestamps and their state estimates) to the messages exchanged by the subsystems. Notice that, due to the communication delay, the estimators cannot communicate synchronously, and therefore the state estimate attached to a message might be out-of-date. A classical way to reduce this uncertainty is to timestamp the messages, e.g., by means of vector clocks (see section 4.1).

Estimates Based on Reachability Sets. Each local estimator maintains a symbolic representation of all global states of the distributed system that are compatible with its observation and with the information it received previously from the other estimators. In section 4.2, we detail the algorithms which update these symbolic representations whenever an event occurs. But first, let us explain the intuition behind the computation of an estimate. We consider the simplest case: the initial state estimate before the system begins its execution. Each FIFO channel is empty, and each subsystem T i is in its initial location i,0 . So the initial global state is known by every estimator E i . A subsystem T j may however start its execution, while T i is still in its initial location, and therefore E i must thus take into account all the global states that are reachable by taking the transitions of the other subsystems T j . The initial estimate E i is this set of reachable global states. This computation of reachable global states also occurs in the update algorithms which take into account any new local event occurred or message received (see section 4.2). The reachability problem is however undecidable for distributed FIFO systems. In section 5, we explain how we overcome this obstacle by using abstract interpretation techniques. Properties of the Estimators. Estimators may have two important properties: soundness and completeness. Completeness refers to the fact that the current state of the global system is always included in the state estimates computed by each state estimator. Soundness refers to the fact that all states included in the state estimate of E i (∀i ∈ [1, n]) can be reached by one of the sequences of actions that are compatible with the observation of T i performed by E i .

Definition 5 (Completeness and Soundness). The estimators

(E i ) i≤n are (i) complete if and only if, for any execution x 0 e1 -→ x 1 e2 -→ . . . em --→ x m of T , x m ∈ n i=1 E i , and (ii) sound if and only if, for any execution x 0 e1 -→ x 1 e2 -→ . . . em --→ x m of T , E i ⊆ {x ∈ X|∃σ ∈ P -1 i (P i (σ e1 .σ e2 . . . σ em )) : x 0 σ → x } (∀i ≤ n) where σ e k (∀k ∈ [1, m]
) is the action that labels the transition corresponding to e k .

Algorithm to Compute the State Estimates

We now present our algorithm that computes estimates of the current state of a distributed system. But first, we recall the notion of vector clocks [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], a standard concept that we shall use to compute a more precise state estimates.

Vector Clocks

To allow the estimators to have a better understanding of the concurrent execution of the distributed system, it is important to determine the causal and temporal relationship between the events that occur in its execution. In a distributed system, events emitted by the same process are ordered, while events emitted by different processes are generally not. When the concurrent processes communicate, additional ordering information can however be obtained. In this case, the communication scheme can be used to obtain a partial order on the events of the system. In practice, vectors of logical clocks, called vector clocks [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], can be used to time-stamp the events of the distributed system. The order of two events can then be determined by comparing the value of their respective vector clocks. When these vector clocks are incomparable, the exact order in which the events occur cannot be determined. Vector clocks are formally defined as follows:

Definition 6 (Vector Clocks). Let D, be a partially ordered set, a vector clock mapping of width n is a function

V : D → N n such that ∀d 1 , d 2 ∈ D : (d 1 d 2 ) ⇔ (V (d 1 ) ≤ V (d 2 )).
In general, for a distributed system composed of n subsystems, the partial order on events is represented by a vector clock mapping of width n. The method for computing this vector clock mapping depends on the communication scheme of the distributed system. For CF-SMs, this vector clock mapping can be computed by the Mattern's algorithm [START_REF] Mattern | Virtual time and global states of distributed systems[END_REF], which is based on the causal and thus temporal relationship between the sending and reception of any message transferred through any FIFO channel. This information is then used to determine a partial order, called causality (or happened-before) relation ≺ c , on the events of the distributed system. This relation is actually the smallest transitive relation satisfying the following conditions: (i) if the events e i = e j occur in the same subsystem T i and if e i comes before e j in the execution, then e i ≺ c e j , and (ii) if e i is an output event occurring in T i and if e j is the corresponding input event occurring in T j , then e i ≺ c e j . In Mattern's algorithm [START_REF] Mattern | Virtual time and global states of distributed systems[END_REF], each process

T i (∀i ∈ [1, n]) has a vector clock V i ∈ N n of width n and each element V i [j] (∀j ∈ [1, n]
) is a counter which represents the knowledge of T i regarding T j and which means that T i knows that T j has executed at least V i [j] events. Each time an event occurs in a subsystem T i , the vector clock V i is updated to take into account the occurrence of this event (see [START_REF] Mattern | Virtual time and global states of distributed systems[END_REF] for details). When T i sends a message to some subsystem T j , this vector clock is piggybacked and allows T j , after reception, to update its own vector clock. Our state estimate algorithm uses vector clocks and follows Mattern's algorithm, which ensures the correctness of the vector clocks that we use (see section 4.2).

Computation of State Estimates

Our state estimate algorithm computes, for each estimator E i and for each event occurring in the subsystem T i , a vector clock V i and a state estimate E i that contains the current state of T and any future state that can be reached from this current state by firing actions that do not belong to T i . This computation obviously depends on the information that E i receives. As a reminder, E i observes the last action fired by T i and can infer the fired transition. T i also receives from the other estimators E j their state estimate E j and their vector clock V j . Our state estimate algorithm proceeds as follows :

-When the subsystem T i sends a message m to T j , T i attaches the vector clock V i and the state estimate E i of E i to this message. Next, E i receives the action fired by T i , and infers the fired transition. It then uses this information to update its state estimate E i . -When the subsystem T i receives a message m from T j , E i receives the action fired by T i and the information sent by T j i.e., the state estimate E j and the vector clock V j of E j . It computes its new state estimate from these elements. In both cases, the computation of the new state estimate E i depends on the computation of reachable states. In this section, we assume that we have an operator that can compute an approximation of the reachable states (which is undecidable is the CFSM model). We will explain in section 5 how such an operator can be computed effectively. State Estimate Algorithm. Our algorithm, called SE-algorithm, computes estimates of the current state of a distributed system. It is composed of three sub-algorithms: (i) the initialization algorithm, which is only used when the system starts its execution, computes, for each estimator, its initial state estimate (ii) the outputTransition algorithm computes online the new state estimate of E i after an output of T i , and (iii) the inputTransition algorithm computes online the new state estimate of E i after an input of T i .

INITIALIZATION Algorithm: According to the Mattern's algorithm [START_REF] Mattern | Virtual time and global states of distributed systems[END_REF], each component of the vector V i is set to 0. To take into account that, before the execution of the first action of T i , the other subsystems T j (∀j = i ∈ [1, n]) could perform inputs and outputs, the initial state estimate of E i is given by E i = Reach T ∆\∆i ( 0,1 , . . . , 0,n , , . . . , ).

Algorithm 1: initialization(T )

input : T = T1|| . . . ||Tn . output: The initial state estimate Ei of the estimator Ei (∀i ∈ [1, n]). begin

1 for i ← 1 to n do for j ← 1 to n do Vi[j] ← 0 2 for i ← 1 to n do Ei ← Reach T ∆\∆ i ( 0,1, . . . , 0,n, , . . . , ) 3 return (E1, . . . , En) 4 end 5
OUTPUT Algorithm: Let E i be the current state estimate of E i . When T i wants to execute a transition δ = 1 , Q i,j !m, 2 ∈ ∆ i corresponding to an output on the queue Q i,j , the following instructions are computed to update the state estimate E i :

• according to the Mattern's algorithm [START_REF] Mattern | Virtual time and global states of distributed systems[END_REF],

V i [i] is incremented (i.e., V i [i] ← V i [i] + 1)
to indicate that a new event has occurred in T i . • T i tags message m with E i , V i , δ and writes this information on the queue Q i,j . The state estimate E i tagging m contains the set of states in which T can be before the Algorithm 2: outputTransition(T , V i , E i , δ)

input : T = T1|| . . . ||Tn, the vector clock Vi of Ei, the current state estimate Ei of Ei, and a transition δ = 1, Qi,j!m, 2 ∈ ∆i. output: The state estimate Ei after the output transition δ. begin

1 Vi[i] ← Vi[i] + 1 2
Ti tags message m with Ei, Vi, δ and it writes this tagged message on Qi,j

3 Ei ← Reach T ∆\∆ i (Post T δ (Ei)) 4 return (Ei) 5 end 6
execution of δ. The additional information E i , V i , δ will be used by T j to refine its state estimate. • the state estimate E i is updated as follows, to contain the current state of T and any future state that can be reached from this current state by firing actions that do not belong to T i :

E i ← Reach T ∆\∆i (Post T δ (E i )). More precisely, Post T δ (E i )
gives the set of states in which T can be after the execution of δ. After the execution of this transition, T j (∀j = i ∈ [1, n]) could however read and write on their queues. Therefore, we define the state estimate

E i by Reach T ∆\∆i (Post T δ (E i )).
if Vj[i] = Vi[i] then T emp1 ← Post T δ (Reach T ∆\∆ i (Post T δ (Ej))) else T emp1 ← Post T δ (Reach T ∆ (Post T δ (Ej))) 5 Ei ← Post T δ (Ei) \\ We update Ei 6 Ei ← Ei ∩ T emp1 \\ Ei = updates of Ei ∩ update of Ej (i.e., T emp1) 7 Vi[i] ← Vi[i] + 1 8 for k ← 1 to n do Vi[k] ← max(Vi[k], Vj[k]) 9 return (Ei) 10 end 11
INPUT Algorithm: Let E i be the current state estimate of E i . When T i executes a transition δ = 1 , Q j,i ?m, 2 ∈ ∆ i , corresponding to an input on the queue Q j,i , it also reads the information E j , V j , δ (where E j is the state estimate of E j before the execution of δ by T j , V j is the vector clock of E j after the execution of δ by T j , and δ = 1 , Q j,i !m, 2 ∈ ∆ j is the output corresponding to δ) tagging m, and the following operations are performed to update E i :

• we update the state estimate E j of E j (this update is denoted by T emp 1 ) by using the vector clocks to guess the possible behaviors of T between the execution of the transition δ and the execution of δ. We consider three cases :

-if V j [i] = V i [i] : T emp 1 ← Post T δ (Reach T ∆\∆i (Post T δ (E j ))).
In this case, thanks to the vector clocks, we know that T i has executed no transition between the execution of δ by T j and the execution of δ by T i . Thus, only transitions in ∆ \ ∆ i could have occurred during this period. We then update E j as follows. We compute (i) Post T δ (E j ) to take into account the execution of δ by T j , (ii)

Reach T ∆\∆i (Post T δ (E j ))
to take into account the transitions that could occur between the execution of δ and the execution of δ, and (iii)

Post T δ (Reach T ∆\∆i (Post T δ (E j ))) to take into account the execution of δ. -else if Vj[j] > Vi[j] : T emp1 ← Post T δ (Reach T ∆\∆ i (Reach T ∆\∆ j (Post T δ (Ej)))).
Indeed, in this case, we can prove (see the proof of Theorem 1) that if we reorder the transitions executed between the occurrence of δ and the occurrence of δ in order to execute the transitions of ∆ i before the ones of ∆ j , we obtain a correct update of E i . Intuitively, this reordering is possible, because there is no causal relation between the events of T i and the events of T j , that have occurred between δ and δ. So, in this reordered sequence, we know that, after the execution of δ, only transitions in ∆\∆ j could occur followed by transitions in ∆ \ ∆ i .

-

else 5 T emp 1 ← Post T δ (Reach T ∆ (Post T δ (E j )))
. Indeed, in this case, the vector clocks do not allow us to deduce information regarding the behavior of T between the execution of δ and the execution of δ. Therefore, to have a correct state estimate, we update E j by taking into account all the possible behaviors of T between the execution of δ and the execution of δ.

• we update the state estimate E i to take into account the execution of the input transition δ: E i ← Post T δ (E i ).

• we have two different state estimates: T emp 1 and E i . Thus, we intersect them to obtain a better state estimate:

E i ← E i ∩ T emp 1 .
• according to the Mattern's algorithm [START_REF] Mattern | Virtual time and global states of distributed systems[END_REF], the vector clock V i is incremented to take into account the execution of δ and subsequently is set to the component-wise maximum of V i and V j . This last operation allows us to take into account the fact that any event that precedes the sending of m should also precede the occurrence of δ. Example 2. We illustrate SE-algorithm with a sequence of actions of our running example depicted in Figure 1 (the vector clocks are given in the figure). A state of the global system is denoted by 1 , 2 , 3 , w 1,2 , w 2,1 , w 2,3 , w 3,1 where i is the location of T i (for i = 1, 2, 3) and w 1,2 , w 2,1 , w 2,3 and w 3,1 denote the content of the queues Q 1,2 , Q 2,1 , Q 2,3 and Q 3,1 .At the beginning of the execution, the state estimates of the three subsystems are (i)

Q 1,2 !c T 1 T 2 T 3 [1, 0, 0] [1, 1, 0] [1, 2, 0] [1, 3, 0] [1, 3, 1] [1, 3, 2] [2, 3, 2] [4, 3, 2] [3, 3, 2] Q 1,2 ?c Q 2,1 !a Q 2,3 !d Q 2,3 ?d Q 3,1 !d Q 3,1 ?d Q 1,2 !d Q 2,1 ?a
E 1 = { A 0 , B 0 , C 0 , , , , }, (ii) E 2 = { A 0 , B 0 , C 0 , , , , , A 1 , B 0 , C 0 , c, , , }, and (iii) E 3 = { A 0 , B 0 , C 0 , , , , , A 1 , B 0 , C 0 , c, , , , A 1 , B 1 , C 0 , , b * , , , A 1 , B 2 , C 0 , , b * (a+ ), , , A 1 , B 3 , C 0 , , b * (a+ ), d, }. Af- ter the first transition A 0 , Q 1,2 !c, A 1 ,
the state estimate of the estimator E 1 is not really precise, because a lot of events may have happened without the estimator E 1 being informed:

E 1 = { A 1 , B 0 , C 0 , c, , , , A 1 , B 1 , C 0 , , b * , , , A 1 , B 2 , C 0 , , b * a, , , A 1 , B 3 , C 0 , , b * (a + ), d, , A 1 , B 3 , C 1 , , b * (a + ), , , A 1 , B 3 , C 0 , , b * (a +
), , d }. However, after the second transition B 0 , Q 1,2 ?c, B 1 , the estimator E 2 has an accurate state estimate: ,,,}. We skip a few steps and consider the state estimates before the sixth transition C 1 , Q 3,1 !d, C 0 : E 1 is still the same, because the subsystem T 1 did not perform any action,

E 2 = { A 1 , B 1 , C 0 ,
E 3 = { A 1 , B 3 , C 1 , , b * (a + ), , }, and we do not indicate E 2 , because T 2 is no longer involved. When T 3 sends the message d to T 1 (the transition C 1 , Q 3,1 !d, C 0 ), it attaches E 3 to this message. When T 1 reads this message, it computes E 1 = { A 2 , B 3 , C 0 , , b * (a + ),
, } and when it reads the message a, it updates

E 1 : E 1 = { A 2 , B 3 , C 0 , , b * , , }.
Thus, E 1 knows, after this action, that there is no message a in Q 2,1 , and that after writing d on Q 1,2 , it cannot reach A er from A 0 . This example shows the importance of knowing the content of the queues as without this knowledge, E 1 may think that there is an a in the queue, so an error might occur if the transition

A 2 , Q 1,2 !d, A 0 is enabled.
Properties. As explained above, we assume that we can compute an approximation of the reachable states. In this part, we present the properties of our state estimate algorithm w.r.t. the kind of approximations that we use. Theorem 1. SE-algorithm is complete, if the Reach operator computes an overapproximation of the reachable states.

The proof is given in Appendix A. If we compute an underapproximation of the reachable states, our state estimate algorithm is not complete.

Theorem 2. SE-algorithm is sound, if the Reach operator computes an underapproximation of the reachable states.

The proof is given in Appendix A. If we compute an overapproximation of the reachable states, our state estimate algorithm is not sound.

Depending on the used approximations, our algorithm is either complete or sound. Completeness is a more important property, because it ensures that the computed state estimates always contains the current global state. Therefore, in section 5, we define an effective algorithm for the state estimate problem by computing overapproximations of the reachable states. Finally, note that our method proposes that we only add information to existing transmitted messages. We can show that increasing the information exchanged between the estimators (for example, each time an estimator computes a new state estimate, this estimate is sent to all the other estimators) improves their state estimate. This can be done only if the channels and the subsystems can handle this extra load. Interpretation

The algorithm described in the previous section requires the computation of reachability operators. But they cannot always be computed for undecidability (or complexity) reasons. In this section, we explain how to overcome this obstacle by using abstract interpretation techniques (see e.g. [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Gall | Verification of communication protocols using abstract interpretation of fifo queues[END_REF]). In our case, abstract interpretation allows us to compute, in a finite number of steps, an overapproximation of the reachability operators and thus of the state estimates E i .

Computation of Reachability Sets by the Means of Abstract Interpretation. For a given set of global states X ⊆ X and a given set of transitions ∆ ⊆ ∆, the reachability set from X can be characterized by the least fixpoint:

Reach T ∆ (X ) = µY.X ∪ Post T ∆ (Y ).
Abstract interpretation provides a theoretical framework to compute efficient overapproximation of such fixpoints. The concrete domain (i.e., the sets of states 2 X ), is substituted by a simpler abstract domain Λ, linked by a Galois Connection 2 X --→ ←--

α γ Λ [7],
where α (resp. γ) is the abstraction (resp. concretization) function. The fixpoint equation is transposed into the abstract domain. So, the equation to solve has the form:

λ = F ∆ (λ), with λ ∈ Λ and F ∆ α • F ∆ • γ.
In this setting, a standard way to ensures that the fixpoint computation converges after a finite number of steps to some overapproximation λ ∞ , is to use a widening operator ∇. The concretization c ∞ = γ(λ ∞ ) is an overapproximation of the least fixpoint of the function F ∆ .

Choice of the Abstract Domain. In abstract interpretation based techniques, the quality of the approximation we obtain depends on the choice of the abstract domain Λ. In our case, the main issue is to abstract the content of the FIFO channels. Since the CFSM model is Turing-powerful, the language that represents all the possible contents of the FIFO channels may be recursively enumerable. As discussed in [START_REF] Gall | Verification of communication protocols using abstract interpretation of fifo queues[END_REF], a good candidate, that abstracts the contents of the queues, to use is the class of regular languages, which can be represented by finite automata. Let us recall the main ideas of this abstraction.

Finite Automata as an Abstract Domain. We first assume that there is only one queue in the distributed system T ; we explain later how to handle a distributed system with several queues.

With one queue, the concrete domain of the system T is defined by X = 2 L×M * . A set of states Y ∈ 2 L×M * can be viewed as a map Y : L → 2 M * that associates a language Y ( ) with each location ∈ L; Y ( ) therefore represents the possible contents of the queue in the location . To simplify the computation, we substitute the concrete domain L → 2 M * , ⊆, ∪, ∩, L × M * , ∅ by the abstract domain L → Reg(M ), ⊆, ∪, ∩, L × M * , ∅ , where Reg(M ) is the set of regular languages over the alphabet M . This substitution consists in abstracting, for each location, the possible contents of the queue by a regular language. Since regular languages have a canonical representation given by finite automata, each operation (union, intersection, left concatenation,...) in the abstract domain can be performed on finite automata.

Widening Operator. With our abstraction, the widening operator we use to ensure the convergence of the computation, is also performed on a finite automaton, and consists in quotienting the nodes 6 of the automaton by the k-bounded bisimulation relation ≡ k ; k ∈ N is a parameter which allows us to tune the precision, since increasing k improves the quality of the abstractions in general. Two nodes are equivalent w.r.t. ≡ k if they have the same outgoing path (sequence of labeled transitions) up to length k. While we merge the equivalent nodes, we keep all transitions and we obtain an automaton recognizing a larger language. Note that for a fixed k, the class of automata which results from such a quotient operation from any original automaton, is finite and its cardinality is bounded by a number which is only function of k. This is the reason why when we apply this widening operator regularly, the fixpoint computation terminates (see [START_REF] Gall | Verification of communication protocols using abstract interpretation of fifo queues[END_REF] for more details). Example 3. We consider the automaton A depicted in Figure 2, whose recognized language is a + ba + bba + bbba. We consider the 1-bounded bisimulation relation i.e., two nodes of the automaton are equivalent if they have the same outgoing transitions. So, nodes 0, 1, 2 are equivalent, since they all have two transitions labeled by a and b. Nodes 3 and 4 are equivalent to no other node since 4 has no outgoing transition whereas only a is enabled in node 3. When we quotient A by this equivalent relation, we obtain the automaton on the right side of Figure 2, whose recognized language is b * a.

When the system contains several queues Q = {Q 1 , . . . , Q r }, their content can be represented by a concatenated word w 1 . . . w r with one w i for each queue Q i and , a delimiter. With this encoding, we represent a set of queue contents by a finite automaton of a special kind, namely a QDD [START_REF] Boigelot | The power of QDDs[END_REF]. Since QDDs are finite automata, classical operations (union, intersection, left concatenation,...) in the abstract domain are performed as was done previously. We must only use a slightly different widening operator not to merge the different queue contents [START_REF] Gall | Verification of communication protocols using abstract interpretation of fifo queues[END_REF].

Effective SE-algorithm. The Reach operator is computed using those abstract interpretation techniques: we proceed to an iterative computation in the abstract domain of regular languages and the widening operator ensures that this computation terminates after a finite number of steps [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. So the Reach operator always gives an overapproximation of the reachable states regardless the distributed system. The efficiency of these approximations is measured in the experiments of section 6. Because of Theorem 1, our SE-algorithm is complete.

Experiments

We have implemented the SE-algorithm as a new feature of the McScM tool [18], a model checker for distributed systems modeled by CFSM. Since it represents queue contents by QDDs, this software provides most of the functionalities needed by our algorithm, like effective computation of reachable states. We have also added a mechanism to manage vector clocks, and an interactive simulator. This simulator first computes and displays the initial state estimates. At each step, it asks the user to choose a possible transition.

If the chosen transition is an output, it attaches the current state estimate of the active subsystem and its vector clock to the message sent, and updates the local state estimate. If the transition is an input, the local estimator reads the information attached to the received message and updates its state estimate. We proceeded to an evaluation of our algorithm measuring the size of the state estimates. Note that this size is not the number of global states of the state estimate (which may be infinite) but the number of nodes of its QDD representation. We generated random sequences of transitions for our running example and some other examples of [START_REF] Heußner | Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems[END_REF]. Table 1 shows the average execution time for a random sequence of 100 transitions, the memory required (heap size), the average and maximal size of the state estimates. Default value of the widening parameter is k = 1. Experiments were done on a standard MacBook Pro with a 2. [START_REF] Brand | On communicating finite-state machines[END_REF] These results show that the computation of state estimates takes about 50ms per transition and that the symbolic representation of state estimates we add to messages are automata with a few dozen nodes. A sensitive element in the method is the size of the computed and transmitted information. It can be improved by the use of compression techniques to reduce the size of this information. A more evolved technique would consist in the offline computation of the set of possible estimates. Estimates are indexed in a table, available at execution time to each local estimator. If we want to keep an online algorithm, we can use the memoization technique. When a state estimate is computed for the first time, it is associated with an index that is transmitted to the subsystem which records both values. If the same estimate must be transmitted, only its index can be transmitted and the receiver can find from its table the corresponding estimate. Those techniques are not yet implemented.

We also highlight that our method works better on the real-life communication protocols we have tested (alternating bit protocol, sliding window, POP3) than on the examples we introduced to test our tool. More details about the tool and experiments are given in Appendix B.

Conclusion and Future Work

We have proposed an effective algorithm to compute online, locally to each subsystem, an estimate of the global state of a running distributed system, modeled as communicating finite state machines with reliable unbounded FIFO queues. With such a system, a global state is composed of the current location of each subsystem together with the channel contents. The principle is to add a local estimator to each subsystem such that most of the system is preserved; each local estimator is only able to compute information and in particular symbolic representations of state estimates and to piggyback some of this computed information to the transmitted messages. Since these estimates may be infinite, a crucial point of our work has been to propose and evaluate the use of regular languages to abstract sets of FIFO queues. In practice, we have used k-bisimilarity relations, which allows us to represent each (possibly infinite) set of queue contents by the minimal and canonical k-bisimilar finite automaton which gives an overapproximation of this set. Our algorithm transmits state estimates and vector clocks between subsystems to allow them to refine and preserve consistent state estimates. More elaborate examples must be taken to analyze the precision of our algorithm and see, in practice, if the estimates are sufficient to solve diagnosis or control problems. Anyway, it appears important to study the possibility of reducing the size of the added communication while preserving or even increasing the precision in the transmitted state estimates. Lemma 3. Given a distributed system T = T 1 || . . . ||T n , and a sequence se

1 = x 0 e1 -→ x 1 e2 -→ . . . ei-1 ---→ x i-1 ei -→ x i ei+1 ---→ x i+1 ei+2 ---→ . . . em --→ x m executed by T , if e i ≺ c e i+1 , then the sequence se 2 = x 0 e1 -→ x 1 e2 -→ . . . ei-1 ---→ x i-1 ei+1 ---→ x i ei -→ x i+1 ei+2 ---→ . . . em --→
x m can also occur in the system T .

Proof. We suppose that δ ei = ei , σ ei , ei ∈ ∆ i and δ ei+1 = ej , σ ej , ej ∈ ∆ j . Note that i = j; otherwise, we would have e i ≺ c e i+1 (by definition of ≺ c ). We can prove this property by showing that Post T δe i+1

(Post T δe i (x i-1 )) = Post T δe i (Post T δe i+1 (x i-1 )).
For that, we consider two cases: 1) δ ei and δ ei+1 act on different queues: we suppose that δ ei and δ ei+1 respectively act on the queues Q ki and Q kj . We also suppose that

x i-1 = 1 , . . . ,
(Post T δe i (x i-1 )) = Post T δe i (Post T δe i+1 (x i-1 )).
2) δ ei and δ ei+1 act on the same queue Q k : we consider two cases: a)

σ i = Q k !m i is an output and σ i+1 = Q k ?m j is
(Post T δe i (x i-1 )) = Post T δe i (Post T δe i+1 (x i-1 )). b) σ i = Q k ?m i is an input and σ i+1 = Q k !m j is an output: the state Post T δe i+1 (Post T δe i (x i-1
)) = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , w.m j , . . . , w |Q| where w.m j is the content of the queue Q k . Next, similarly to the previous case, we can prove that Post T δe i+1

(Post T δe i (x i-1 )) = Post T δe i (Post T δe i+1 (x i-1 )).
The cases, where δ ei and δ ei+1 are both an input or an output, are not possible, because these transitions would then be executed by the same process and hence we would have e i ≺ c e i+1 . This property means that if two consecutive events e i and e i+1 are such that e i ≺ c e i+1 , then these events can be swapped without modifying the reachability of x m . We finally prove the following lemma.

Lemma 4. Given a distributed system T = T 1 || . . . ||T n , a transition δ i = i , Q t,i ?m i , i ∈ ∆ i (with t = i), and a set of states B ⊆ X, then Reach T ∆\∆i (Post T δe i (Reach T ∆\∆i (B))) = Post T δe i (Reach T ∆\∆i (B)). Proof. First, the inequality Post T δe i (Reach T ∆\∆i (B)) ⊆ Reach T ∆\∆i (Post T δe i (Reach T ∆\∆i (B)
)) holds trivially. To prove the other inclusion, we have to show that if a state

x m ∈ Reach T ∆\∆i (Post T δe i (Reach T ∆\∆i (B))), then x m ∈ Post T δe i (Reach T ∆\∆i (B)).
We actually prove a more general result. We show that each sequence

x 1 e2 -→ x 2 e3 -→ . . . e k-1 ---→ x k-1 e k -→ x k e k+1 ---→ x k+1 e k+2 ---→ . . . em --→ x m (where (i) x 1 ∈ B, (ii)
the event e k corresponds to the transition δ e k = δ i ∈ ∆ i , and (iii) the event e b , for each b = k ∈ [2, m], corresponds to a transition δ e b ∈ ∆ \ ∆ i ) can be reordered to execute e k at the end of the sequence without modifying the reachability of x m i.e., the following sequence can occur:

x 1 e2 -→ x 2 e3 -→ . . . e k-1 ---→ x k-1 e k+1 ---→ x k+1 e k+2 ---→ . . . em --→ x m e k
-→ x m . This reordered sequence can be obtained thanks to Lemma 3, but to use this lemma, we must prove that

e k ≺ c e b (∀b ∈ [k + 1, m]).
The proof is by induction on the length of the sequence of events that begins from x k :

• Base case: we must prove that e k ≺ c e k+1 . By definition of ≺ c , since e k and e k+1 occur in different subsystems and are consecutive events, there is one possibility to have e k ≺ c e k+1 : it is when e k is an output and e k+1 is the corresponding input. But e k is an input and hence e k ≺ c e k+1 .

• Induction step: we suppose that e k ≺ c e k+r (∀r ∈ [1, j]) and we prove that e k ≺ c e k+j+1 . By definition of ≺ c , since e k and e k+1 occur in different subsystems, there are two possibilities to have e k ≺ c e k+j+1 :

1) e k is an output and e k+j+1 is the corresponding input. However, e k is an input and thus this case is impossible.

2) e k ≺ c e k+r (with r ∈ [1, j]) and e k+r ≺ c e k+j+1 . But by induction hypothesis, e k ≺ c e k+r (∀r ∈ [1, j]) and thus this case is impossible. Therefore, e k ≺ c e k+j+1 .

A.2 Proof of Theorem 1

To show that this theorem holds, we prove by induction on the length m of an execution

x 0 e1 -→ x 1 e2 -→ . . . em --→ x m of the system T that ∀i ∈ [1, n] : Reach T ∆\∆i (x m ) ⊆ E m i . Since x m ∈ Reach T ∆\∆i (x m ), we have then that x m ∈ E m i .
In this proof, when e i ≺ c e j , we say that e j causally depends on e i (or e i happened-before e j ).

• Base case (m = 0):

For each i ∈ [1, n], the set E 0 i = Reach T
∆\∆i ( 0,1 , . . . , 0,n , , . . . , ) (see Algorithm 1). Therefore, we have that

Reach T ∆\∆i (x 0 ) = E 0 i (∀i ∈ [1, n]
), because x 0 = 0,1 , . . . , 0,n , , . . . , . • Induction step: We suppose that the property holds for the executions of length k ≤ m

(i.e., ∀ 0 ≤ k ≤ m, ∀i ∈ [1, n] : Reach T ∆\∆i (x k ) ⊆ E k i )
and we prove that the property also holds for the executions of length m + 1. For that, we suppose that the event e m+1 has been executed by T i . We must consider two cases:

1) δ em+1 is an output on the queue Q i,k (with k = i ∈ [1, n]): We must prove that ∀j ∈ [1, n] : Reach T ∆\∆j (x m+1 ) ⊆ E m+1 j
and we consider again two cases to prove this property: a) j = i: By induction hypothesis, we know that Reach T ∆\∆j (x m ) ⊆ E m j . Moreover, we have that:

x m ⊆ Reach T ∆\∆j (x m ), by definition of Reach ⇒ Post T δe m+1 (x m ) ⊆ Post T δe m+1 (Reach T ∆\∆j (x m )), as Post is monotonic ⇒ x m+1 ⊆ Reach T ∆\∆j (x m ), because δ em+1 ∈ ∆ \ ∆ j (as δ em+1 ∈ ∆ i ) and Post T δe m+1 (x m ) = x m+1 ⇒ Reach T ∆\∆j (x m+1 ) ⊆ Reach T ∆\∆j (Reach T ∆\∆j (x m )), as Reach is monotonic ⇒ Reach T ∆\∆j (x m+1 ) ⊆ Reach T ∆\∆j (x m ) ⇒ Reach T ∆\∆j (x m+1 ) ⊆ E m j ⇒ Reach T ∆\∆j (x m+1 ) ⊆ E m+1 j
, because E m j = E m+1 j (due to the fact that e m+1 has not been executed by T j ) b) j = i: By induction hypothesis, we know that

Reach T ∆\∆i (x m ) ⊆ E m i . The set E m+1 i = Reach T ∆\∆i (Post T δe m+1 (E m i )) (see Algorithm 2)
. Moreover, we have that:

x m ⊆ Reach T ∆\∆i (x m ) ⇒ Post T δe m+1 (x m ) ⊆ Post T δe m+1 (Reach T ∆\∆i (x m )) ⇒ x m+1 ⊆ Post T δe m+1 (Reach T ∆\∆i (x m )), as Post T δe m+1 (x m ) = x m+1 ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Reach T ∆\∆i (Post T δe m+1 (Reach T ∆\∆i (x m ))) ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Reach T ∆\∆i (Post T δe m+1 (E m i )), by induction hypothesis ⇒ Reach T ∆\∆i (x m+1 ) ⊆ E m+1 i , by definition of E m+1 i Thus, for each j ∈ [1, n], we have that Reach T ∆\∆j (x m+1 ) ⊆ E m+1 j
. Moreover, since we compute an overapproximation of E m+1 j (∀j ∈ [1, n]), this inclusion remains true 8 .

2) δ em+1 is an input on the queue Q k,i (with

k = i ∈ [1, n]): We must prove that ∀j ∈ [1, n] : Reach T ∆\∆j (x m+1 ) ⊆ E m+1 j
and we consider again two cases: a) j = i: The proof is similar to the one given in the case where δ em+1 in an output. b) j = i: By induction hypothesis, we know that (E m i ) and next we show that Reach T ∆\∆i (x m+1 ) ⊆ T emp 1 . The first inclusion is proved as follows:

Reach T ∆\∆i (x m ) ⊆ E m i . By Al- gorithm 3, the set E m+1 i = T emp 1 ∩ Post T δe m+1 (E m i ) (in
x m ⊆ Reach T ∆\∆i (x m ) ⇒ Post T δe m+1 (x m ) ⊆ Post T δe m+1 (Reach T ∆\∆i (x m )) ⇒ x m+1 ⊆ Post T δe m+1 (Reach T ∆\∆i (x m )), because Post T δe m+1 (x m ) = x m+1 ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Reach T ∆\∆i (Post T δe m+1 (Reach T ∆\∆i (x m ))) ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Post T δe m+1 (Reach T ∆\∆i (x m )), by Lemma 4 ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Post T δe m+1 (E m i )

, by induction hypothesis

To prove the second inclusion, we must consider three cases which depend on the definition of T emp 1 . Let e t (with t ≤ m) be the output (executed by

T k with k = i ∈ [1, n]) corresponding to the input e m+1 : A) T emp 1 = Post T δe m+1 (Reach T ∆\∆i (Post T δe t (E t-1 k ))) and V k [i] = V i [i]
(as a reminder, V k represents the vector clock of T k after the occurrence of the event e t and V i represents the vector clock of T i before the occurrence of the event e m+1 ): By induction hypothesis, we know that Reach T ∆\∆ k (x t-1 ) ⊆ E t-1 k . Moreover, we have that:

x t-1 ⊆ Reach T ∆\∆ k (x t-1 ) ⇒ x t-1 ⊆ E t-1 k , by induction hypothesis ⇒ Post T δe t (x t-1 ) ⊆ Post T δe t (E t-1 k ) ⇒ x t ⊆ Post T δe t (E t-1 k ), as Post T δe t (x t-1 ) = x t ⇒ Reach T ∆\∆i (x t ) ⊆ Reach T ∆\∆i (Post T δe t (E t-1 k )) (β) However, since V k [i] = V i [i],
we know that, between the moment where e t has been executed and the moment where e m has been executed, the vector clock V i [i] has not been modified. Thus, during this period no transition of T i has been executed. In consequence, we have that x m ⊆ Reach T ∆\∆i (x t ) and hence x m ⊆ Reach T ∆\∆i (Post T δe t (E t-1 k )) by (β). From this inclusion, we deduce that:

Post T δe m+1 (x m ) ⊆ Post T δe m+1 (Reach T ∆\∆i (Post T δe t (E t-1 k ))) ⇒ x m+1 ⊆ Post T δe m+1 (Reach T ∆\∆i (Post T δe t (E t-1 k ))), because x m+1 = Post T δe m+1 (x m ) ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Reach T ∆\∆i (Post T δe m+1 (Reach T ∆\∆i (Post T δe t (E t-1 k )))) ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Post T δe m+1 (Reach T ∆\∆i (Post T δe t (E t-1 k ))), by Lemma 4 ⇒ Reach T ∆\∆i (x m+1 ) ⊆ T emp 1 , by definition of T emp 1 B) T emp 1 = Post T δe m+1 (Reach T ∆\∆i (Reach T ∆\∆ k (Post T δe t (E t-1 k )))) and V k [k] > V i [k]
(as a reminder, V k represents the vector clock of T k after the occurrence of the event e t and V i represents the vector clock of T i before the occurrence of the event e m+1 ): By induction hypothesis, we know that Reach T ∆\∆ k (x t-1 ) ⊆ E t-1 k . Moreover, we have that:

x t-1 ⊆ Reach T ∆\∆ k (x t-1 ) ⇒ x t-1 ⊆ E t-1 k , by induction hypothesis ⇒ Post T δe t (x t-1 ) ⊆ Post T δe t (E t-1 k ) ⇒ x t ⊆ Post T δe t (E t-1 k ), because Post T δe t (x t-1 ) = x t (γ)
This inclusion is used further in the proof. Now, we prove that x m ⊆ Reach T ∆\∆i (Reach T ∆\∆ k (x t )). For that, let us consider the subsequence se =

x t et+1 ---→ x t+1 et+2 ---→ . . . em --→ x m of the execution x 0 e1 -→ x 1 e2 -→ . . . em --→ x m .
Let e K1 be the first event of the sequence se executed9 by T k and s I = e I1 , . . . , e I (with I 1 < . . . < I ) be the events of the sequence se executed10 by T i . If I < K 1 (i.e., e I has been executed before e K1 ), then

x m ⊆ Reach T ∆\∆i (Reach T ∆\∆ k (x t ))
, because all the events of the sequence se executed by T i have been executed before the first event e K1 of T k . Otherwise, let s I = e I d , . . . , e I be the events of s I executed after e K1 . We must reorder the sequence se to obtain a new sequence where all the actions of T i are executed before the ones of T k and x m remains reachable. Lemma 3 allows us to swap two consecutive events without modifying the reachability when these events are not causally dependent. To use this lemma, we must prove that the events e I d , . . . , e I do not causally depend on e K1 . For that, we first prove that e K1 ≺ c e I . By assumption, we know that ≺ c e Ic . Now, in the sequence se, we will move the events e I d , . . . , e I to execute them before e K1 without modifying the reachability of x m . We start by moving the element e I d . To obtain a sequence where e I d precedes e K1 , we swap e I d with the events which precede it and we repeat this operation until the event e K1 . Lemma 3 ensures that x m remains reachable if e I d is swapped with an element e such that e ≺ c e I d . However, between e K1 and e I d there can be some events, that happened-before e I d . We must thus move these events before moving e I d . More precisely, let s b = e b1 , . . . , e bp (with b 1 < . . . < b p ) be the greatest sequence of events such that (i) these events are executed between the occurrence of e K1 and the occurrence of e I d and (ii) ∀e bc ∈ s b : e bc ≺ c e I d (note that the events of the sequence s b are not executed by T k ; otherwise, we would have e K1 ≺ c e I d ). The sequence of events s = e K1 , e K1+1 , e K1+2 , . . . , e b1-1 executed between e K1 and e b1 is such that ∀e t ∈ s : e t ≺ c e b1 . Indeed, if e t ≺ c e b1 , then by transitivity we would have e t ≺ c e I d , but this is not possible, because e t ∈ s. Thus, by Lemma 3, in the sequence x t et+1 ---→ . . .

V k [k] > V i [k]. V k
e K 1 --→ x K1 e K 1 +1 ----→ x K1+1 e K 1 +2 ----→ . . . e b 1 -1 ---→ x b1-1 e b 1 --→ x b1 e b 1 +1
---→ . . . em --→ x m , we can safely swap the events e b1-1 and e b1 . We then obtain a reordered sequence where x m remains reachable i.e., we

obtain x t et+1 ---→ . . . e K 1 --→ x K1 e K 1 +1 ----→ x K1+1 e K 1 +2 ----→ . . . e b 1 -2 ---→ x b1-2 e b 1 --→ x b1 e b 1 -1 ---→ x b1 e b 1 +1
---→ . . . em --→ x m . By repeating this swap with the events e b1-2 , e b1-3 , . . . , e K1+1 , e K1 , we obtain a reordered sequence where (i) e b1 is executed before e K1 and (ii) x m remains reachable (by Lemma 3). We repeat the operations performed for e b1 with the events e b2 , . . . , e bp and e I d to obtain a reordered sequence where (i) e I d is executed before e K1 and (ii) x m is reachable. Finally, we repeat the operations performed for e I d with the other elements of the sequence s I to obtain a reordered sequence where (i) x m is reachable from x t and (ii) the events of T i are executed before the ones of T k , which implies that x m ⊆ Reach T ∆\∆i (Reach T ∆\∆ k (x t )). Next, from this inclusion, we deduce that:

Post T δe m+1 (x m ) ⊆ Post T δe m+1 (Reach T ∆\∆i (Reach T ∆\∆ k (x t ))) ⇒ x m+1 ⊆ Post T δe m+1 (Reach T ∆\∆i (Reach T ∆\∆ k (x t ))), because x m+1 = Post T δe m+1 (x m ) ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Reach T ∆\∆i (Post T δe m+1 (Reach T ∆\∆i (Reach T ∆\∆ k (x t )))) ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Post T δe m+1 (Reach T ∆\∆i (Reach T ∆\∆ k (x t ))), by Lemma 4 ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Post T δe m+1 (Reach T ∆\∆i (Reach T ∆\∆ k (Post T δe t (E t-1 k )))), by (γ) ⇒ Reach T ∆\∆i (x m+1 ) ⊆ T emp 1 , by definition of T emp 1 C) T emp 1 = Post T δe m+1 (Reach T ∆ (Post T δe t (E t-1 k ))): By induction hypothesis, we know that Reach T ∆\∆ k (x t-1 ) ⊆ E t-1 k
. Moreover, we have that:

x t-1 ⊆ Reach T ∆\∆ k (x t-1 ) ⇒ x t-1 ⊆ E t-1 k , by induction hypothesis ⇒ Post T δe t (x t-1 ) ⊆ Post T δe t (E t-1 k ) ⇒ x t ⊆ Post T δe t (E t-1 k ), as Post T δe t (x t-1 ) = x t ⇒ Reach T ∆ (x t ) ⊆ Reach T ∆ (Post T δe t (E t-1 k )) (α)
However, the events e t+1 , . . . , e m leading to x m from the state x t correspond to transitions which belong to ∆. Thus, x m ⊆ Reach T ∆ (x t ) and hence x m ⊆ Reach T ∆ (Post T δe t (E t-1 k )) by (α). From this inclusion, we deduce that:

Post T δe m+1 (x m ) ⊆ Post T δe m+1 (Reach T ∆ (Post T δe t (E t-1 k ))) ⇒ x m+1 ⊆ Post T δe m+1 (Reach T ∆ (Post T δe t (E t-1 k ))), as x m+1 =Post T δe m+1 (x m ) ⇒ x m+1 ⊆ Reach T ∆ (Post T δe t (E t-1 k )), because δ em+1 ∈ ∆ ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Reach T ∆\∆i (Reach T ∆ (Post T δe t (E t-1 k ))) ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Reach T ∆ (Post T δe t (E t-1 k )), because ∆ \ ∆ i ⊆ ∆ ⇒ Reach T ∆\∆i (x m+1 ) ⊆ Post T δe m+1 (Reach T ∆ (Post T δe t (E t-1 k ))), because δ em+1 ∈ ∆ ⇒ Reach T ∆\∆i (x m+1 ) ⊆ T emp 1 , by definition of T emp 1
In conclusion, we have proven, for each definition of T emp 1 , that

Reach T ∆\∆i (x m+1 ) ⊆ T emp 1 and hence Reach T ∆\∆i (x m+1 ) ⊆ E m+1 i . Thus, for each j ∈ [1, n], we have that Reach T ∆\∆j (x m+1 ) ⊆ E m+1 j
. Moreover, since we compute an overapproximation of E m+1 j (∀j ∈ [1, n]), this inclusion remains true.

A.3 Proof of Theorem 2

To show that this theorem holds, we prove by induction on the length m of the sequences of events e 1 , . . . , e m (let δ e k = e k , σ e k , e k be the transition corresponding to e k , for each k ∈ [1, m]) executed by the system that ∀i ∈

[1, n] : E m i ⊆ {x r ∈ X|∃σ ∈ P -1 i (P i (σ e1 .σ e2 . . . σ em )) : x 0 σ → x r }:
• Base case (m = 0): The initial state x 0 = 0,1 , . . . , 0,n , , . . . , and we must prove that ∀i ∈ [1, n] :

E 0 i ⊆ {x r ∈ X|∃σ ∈ P -1 i (P i ( )) : x 0 σ → x r }. The set E 0 i = Reach T ∆\∆i (x 0 ) (see Algorithm 1) and Reach T ∆\∆i (x 0 ) = {x r ∈ X|∃σ ∈ P -1 i (P i ( )) : x 0 σ → x r }, which implies that E 0 i = {x r ∈ X|∃σ ∈ P -1 i (P i ( )) : x 0 σ → x r }. Moreover, since we compute an underapproximation of E 0 i (∀j ∈ [1, n]
), this inclusion remains true 12 .

• Induction step: We suppose that the property holds for the sequences of events of length k ≤ m and we prove that the property remains true for the sequences of length m + 1.

We suppose that e m+1 has been executed by T i . We consider two cases: 1) δ em+1 is an output: We must prove that ∀j ∈ [1, n] : E m+1 j ⊆ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r } and we consider again two cases: a) i = j: By induction hypothesis, we know that E m j ⊆ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em )) :

x 0 σ → x r }. Since E m+1 j = E m j (by definition), we have that E m+1 j ⊆ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em )) : x 0 σ → x r }.
Moreover, {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em )) :

x 0 σ → x r } = {x r ∈
X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r }, as P j (σ e1 .σ e2 . . . σ em ) = P j (σ e1 .σ e2 . . . σ em+1 ) (because σ em+1 ∈ Σ j ). Therefore, we have that E m+1 (E m j )) and P j (σ e1 .σ e2 . . . σ em+1 ) = P j (σ e1 .σ e2 . . . σ em ).σ em+1 , because σ em+1 ∈ Σ j . We prove that if x ∈ E m+1 j , then x ∈ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) :

x 0 σ → x r }. If x ∈ E m+1 j , then there exists a state x ∈ E m j such that x ∈ Reach T ∆\∆j (Post T δe m+1 (x ))
. Let em+1 , σ em+1 , em+1 , t1 , σ t1 , t1 , . . . , t k , σ t k , t k be the sequence of transitions which leads to x from x i.e., x

σe m+1 .σt 1 ...σt k ----------→ x. The transition t b , σ t b , t b ∈ ∆ \ ∆ j (for each b ∈ [1, k]
), which implies that σ em+1 .σ t1 . . . σ t k ∈ P -1 j (σ em+1 ). Moreover, by induction hypothesis, the state x ∈ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em )) : x 0 σ → x r }, which implies that ∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em )) : x 0 σ → x .

Since P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) = [P -1 j (P j (σ e1 .σ e2 . . . σ em )).P -1 j (σ em+1 )], the sequence σ = σ .σ em+1 .σ t1 . . . σ t k belongs to P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )). For that, we show that if x ∈ Post T δe m+1

(E m j ), then x ∈ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) :

x 0 σ → x r }. If x ∈ Post T δe m+1
(E m j ), then there exists a state x ∈ E m j such that x = Post T δe m+1 (x ). By induction hypothesis, the state x ∈ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em )) : x 0 σ → x r }, which implies that ∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em )) : x 0 σ → x . Since P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) = [P -1 j (P j (σ e1 .σ e2 . . . σ em )).P -1 j (σ em+1 )], the sequence σ = σ .σ em+1 belongs to P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )). Moreover, x 0

B Experiments

This appendix presents some additional details about the current implementation of our algorithm. The source code is available: [18] version "0.02 Control". Note that this tool is still under development.

B. The input is the model of the distributed system. The engine is called "control" because we aim at the control of distributed systems. By default, it starts with an interactive simulation of the model. At each step, the current state and the possible transitions are displayed. The user chooses one of these transitions and the tool updates the state of the system and the state estimates according to our algorithm. By default, the state estimates are not displayed, but their size is displayed.

B.2 Experiment on the running example

Here are some of the state estimates computed while the system executes the sequence of actions of Example 2. The widening parameter is k = 1. Each estimate is a map from a global location to a queue content. We first give the initial estimate of each process.

With the option -display-estimate, the tool displays, for each estimate and each location, the internal representation of the queue content -a QDD. We give here a more readable representation as regular expression. We also give here the queue names as they appear in the paper -the implementation uses numbers instead of names.

E 1 Location Q 1,2 Q 2,1 Q 2,3 Q 3,1 A 0 × B 0 × C 0 ε ε ε ε E 2 Location Q 1,2 Q 2,1 Q 2,3 Q 3,1 A 0 × B 0 × C 0 ε ε ε ε A 1 × B 0 × C 0 c ε ε ε E 3 Location Q 1,2 Q 2,1 Q 2,3 Q 3,1 A 0 × B 0 × C 0 ε ε ε ε A 1 × B 0 × C 0 c ε ε ε A 1 × B 1 × C 0 ε b * ε ε A 1 × B 2 × C 0 ε b * a + ε ε ε A 1 × B 3 × C 0 ε b * a + ε d ε Location Q 1,2 Q 2,1 Q 2,3 Q 3,1 A 1 × B 0 × C 0 c ε ε ε A 1 × B 1 × C 0 ε b * ε ε A 1 × B 2 × C 0 ε b * a ε ε A 1 × B 3 × C 0 ε b * a d ε A 1 × B 3 × C 0 ε b * a ε d A 1 × B 3 × C 1 ε b * a ε ε
At the beginning, E 1 knows exactly the current state, because nothing can happen if T 1 does not send message c to T 2 . E 2 is almost as precise. However E 3 is less precise, because many events could occur before T 3 receives its first message. After the first transition A 0 , Q 1,2 !c, A 1 , the state estimate of the estimator E 1 is similar to E 3 , but:

1

T 1 Q 1,2 !c 42 -- T 2 Q 1,2 ?c -4 - T 2 Q 2,1 !a -9 - T 2 Q 2,3 !d -46 - T 3 Q 2,3 ?d --7 T 3 Q 3,1 !d --132 T 1
Q 2,1 ?a 14 --T 1 Q 3,1 ?d 4 --

Algorithm 3 : 1 \\

 31 inputTransition(T , V i , E i , δ) input : T = T1|| . . . ||Tn , the vector clock Vi of Ei, the current state estimate Ei of Ei and a transition δ = 1, Qj,i?m, 2 ∈ ∆i. Message m is tagged with the triple Ej, Vj, δ where (i) Ej is the state estimate of Ej before the execution of δ by Tj, (ii) Vj is the vector clock of Ej after the execution of δ by Tj, and (iii) δ = We consider three cases to update Ej

2

 2

Fig. 1 .

 1 Fig. 1. An execution of the running example.

Fig. 2 .

 2 Fig. 2. Illustration of the 1-bounded bisimulation relation ≡1 for A.

  represents the vector clock of T k after the execution of e t and V i represents the vector clock of T i before the execution of e m+1 , which givesV k (e t )[k] > V i (e m )[k]. Moreover, V i (e m )[k] ≥ V i (e I )[k] (because e I has been executed before 11 e m ) and V k (e K1 )[k] ≥ V k (e t )[k] + 1 (because e K1 is the event which follows e t in the execution of the subsystem T k ). Thus, V k (e K1 )[k] > V i (e I )[k], and hence e K1 ≺ c e I . Next, since e Ic ≺ c e I (∀e Ic = e I ∈ s I ) and since e K1 ≺ c e I , we have by Lemma 2 that e K1

  j ⊆ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r }. Moreover, since we compute an underapproximation of E m+1 j , this inclusion remains true.

Moreover, x 0 σ

 0 → x (because x 0 σ → x and x σe m+1 .σt 1 ...σt k ----------→ x) which implies that x ∈ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r }. Hence, E m+1 j ⊆ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r }. Again, since we compute an underapproximation of E m+1 j , this inclusion remains true. 2) δ em+1 is an input: We must prove that ∀i ∈ [1, n] : E m+1 j ⊆ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r } and we consider again two cases: a) i = j: the proof is similar the one given in the case where δ em+1 is an output. b) i = j: The set E m+1 j = Post T δe m+1 (E m j ) ∩ T emp 1 (see Algorithm 3). Thus, we have that E m+1 j ⊆ Post T δe m+1 (E m j ) and it then suffices to prove that Post T δe m+1 (E m j ) ⊆ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r }.

→

  x and x = Post T δe m+1 (x )) which implies that x ∈ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r }. Therefore, we have thatE m+1 j ⊆ {x r ∈ X|∃σ ∈ P -1 j (P j (σ e1 .σ e2 . . . σ em+1 )) : x 0 σ → x r }. Again, sincewe compute an underapproximation of E m+1 j , this inclusion remains true.

Table 1 .

 1 GHz Intel 2 duo CPU. Experiments

	example	# subsystems # channels time [s] memory [MB] maximal size average size
	running example	3	4	7.13	5.09	143	73.0
	c/d protocol	2	2	5.32	8.00	183	83.2
	non-regular protocol	2	1	0.99	2.19	172	47.4
	ABP	2	3	1.19	2.19	49	24.8
	sliding window	2	2	3.26	4.12	21	10.1
	POP3	2	2	3.08	4.12	22	8.5

  ei ,. . . , ej , . . . , n , w 1 , . . . , w ki , . . . , w kj , . . . , w |Q| (where w ki and w kj respectively denote the content of the queues Q ki and Q kj ), and that the action σ ei (resp. σ ej ), which acts on the content w ki (resp. w kj ), modifies it to give w ki (resp. w kj ). In consequence, Post T δe i (x i-1 ) = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , w ki , . . . , w kj , . . . , w |Q|

	and Post T δe i+1	(Post T δe

i (x i-1 )) = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , w ki , . . . , w kj , . . . , w |Q| . Since e i ≺ c e i+1 , we have that Post T δe i+1 (x i-1 ) = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , w ki , . . . , w kj , . . . , w |Q| and Post T δe i (Post T δe i+1 (x i-1 )) = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , w ki , . . . , w kj , . . . , w |Q| , which implies that Post T δe i+1

  an input: the message written by δ ei cannot be read by the transition δ ei+1 , because, in this case, we would have e i ≺ c e i+1 . Thus, Post T , w 1 , . . . , w.m i , . . . , w |Q| where w.m i is the content of the queue Q k . Therefore, the state Post T δe i (x i-1 ) = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , m j .w.m i , . . . , w |Q| and the state x i-1 = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , m j .w, . . . , w |Q| . Next, we compute the state Post T δe i+1 (x i-1 ) = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , w, . . . , w |Q| and the state Post T )) = 1 , . . . , ei ,. . . , ej , . . . , n , w 1 , . . . , w.m i , . . . , w |Q| . In consequence, Post T

	δe i+1	(Post T δe δe i	(Post T δe i+1	(x i-1 δe i+1

i (x i-1 )) = 1 , . . . , ei ,. . . , ej , . . . , n

  our algorithm, the set T emp 1 can have three possible values). To prove that Reach T

	E m+1 i	, we first prove that Reach T ∆\∆i (x m+1 ) ⊆ Post T δe m+1	∆\∆i (x m+1 ) ⊆

  1 McScM tool -control version McScM [18] is a model checker for distributed systems modeled by CFSMs. It has been developed by Alexander Heussner, Gregoire Sutre and Tristan Le Gall, and is distributed under the LGPL license. We added, to this tool, an implementation of the state estimate algorithm presented in this paper. McScM offers several model checking engines. The module we implemented is considered as a "new" engine. We call it by the command line:

mcscm.native -mc-engine control -simulation-only [other options] <input>

  . E 1 does not know if T 3 received d and sent another message d in channel Q 3,1 . 2. the content of channel Q 2,1 is a bit more precise, b * a instead of b * a + ε, because E 1 knows that T 1 did not receive any message. Note that location A 1 × B 3 × C 0 appears two times. The actual regular expression associated to this location is ε#b * a#(d#ε + ε#d) where # is a special symbol to separate the different queues. So we write it as ε#b * a#d#ε + ε#b * a#ε#d in this state estimate. If we continue, the tool calculates and displays the estimate as in Example 2. We only give, in the table below, the size of the estimates.

	Subsystem Event E 1 E 2 E 3 -start 4 9 35

To simplify the presentation of our method, we suppose there is one queue from Ti to Tj. But, our implementation is more permissive: there can be zero, one or more queues from Ti to Tj.

, Qj,i!m,

∈ ∆j is the output corresponding to δ. output: The state estimate Ei after the input transition δ. begin

else if Vj[j] > Vi[j] then T emp1 ← Post T δ (Reach T ∆\∆ i (Reach T ∆\∆ j (Post T δ (Ej))))

It can be shown that the set T emp1 computed in the second case is better that the one computed in the third case.

The states of an automaton representing the queue contents are called nodes to avoid the confusion with the states of a CFSM.

In this way, we do not need to introduce, for each subsystem, a parameter giving the number of events that has been executed so far by each subsystem

Note that if we compute an underapproximation of E m+1 j , the inclusion does not always hold.

If this element does not exist, then the transitions executed in this sequence do not belong to ∆ k ; thus, xm ⊆ Reach T ∆\∆ k (xt) and hence xm ⊆ Reach T ∆\∆ i (Reach T ∆\∆ k (xt))

If the sequence sI is empty, then the transitions executed in the sequence se do not belong to ∆i; thus, xm ⊆ Reach T ∆\∆ i (xt) and hence xm ⊆ Reach T ∆\∆ i (Reach T ∆\∆ k (xt)), because xt ⊆ Reach T ∆\∆ k (xt)

Note that if we compute an overapproximation of the reachable states, the inclusion does not always hold.

This work has been done in the MoVES project (P6/39), part of the IAP-Phase VI Interuniversity Attraction Poles Programme funded by the Belgian State, Belgian Science Policy.

A Proofs of Theorems 1 and 2

In this section, we prove Theorems 1 and 2. These proofs use the lemmas given in section A.1 and the following notations.

Let

x m be an execution of the global system T . When the subsystem T i executes an event e k (with k ∈ [1, m]) of this sequence, the state estimate, computed by E i at this step, is denoted by E t i , where t is the number of events executed by T i in the subsequence x 0

-→ x k . However, to be more concise in our presentation, we use an abuse of notation: when an event e k is executed in the sequence s, the state estimate of each state estimator E i is denoted by 7 E k i . This state estimate is defined in the following way: if e k has not been executed by T i , then

Otherwise, the value of E k i is computed by the state estimator from E k-1 i , the observed event, and the information that possibly tags this event.

The vector clock V i , computed after the occurrence of an event e in the subsystem T i , is denoted by V i (e).

A.1 Lemmas

The following lemma proves the correctness of the vector clock mapping computed by the Mattern's algorithm for the relation ≺ c : Lemma 1 ( [START_REF] Mattern | Virtual time and global states of distributed systems[END_REF]). Given n subsystems T i (∀i ∈ [1, n]) and two events e 1 = e 2 occurring respectively in T i and T j (i can be equal to j), we have the following equivalence: e 1 ≺ c e 2 if and only if V i (e 1 ) ≤ V j (e 2 ). Lemma 2. Given n subsystems T i (∀i ∈ [1, n]) and three events e i = e j = e k occurring respectively in T i , T j and T k , if e k ≺ c e j and e i ≺ c e j , then e k ≺ c e i .

Proof. Let us assume that e k ≺ c e i . Since e k ≺ c e j , there exists ∈