CONCUR 2000, 11th International Conference on Concurrency Theory Proceedings: Catuscia Palamidessi (ed.) Springer Lecture Notes in Computer Science 1877 (2000), 521–535.

Synthesizing distributed finite-state systems from MSCs^{⋆}

Madhavan Mukund^{1}, K. Narayan Kumar^{1}, and Milind Sohoni^{2}

1 Chennai Mathematical Institute, Chennai, India.

             E-mail: {madhavan,kumar}@smi.ernet.in

2 Indian Institute of Technology Bombay, Mumbai, India

               E-mail: sohoni@cse.iitb.ernet.in

Abstract. Message sequence charts (MSCs) are an appealing visual formalism often used to capture system requirements in the early stages of design. An important question concerning MSCs is the following: how does one convert requirements represented by MSCs into state-based specifications? A first step in this direction was the definition in [9] of regular collections of MSCs, together with a characterization of this class in terms of finite-state distributed devices called message-passing automata. These automata are, in general, nondeterministic. In this paper, we strengthen this connection and describe how to directly associate a deterministic message-passing automaton with each regular collection of MSCs. Since real life distributed protocols are deterministic, our result is a more comprehensive solution to the synthesis problem for MSCs. Our result can be viewed as an extension of Zielonka’s theorem for Mazurkiewicz trace languages [6, 19] to the setting of finite-state message-passing systems.

1 Introduction

Message sequence charts (MSCs) are an appealing visual formalism often used to capture system requirements in the early stages of design. They are particularly suited for describing scenarios for distributed telecommunication software [16]. They have also been called timing sequence diagrams, message flow diagrams and object interaction diagrams and are used in a number of software engineering methodologies [4, 7, 16]. In its basic form, an MSC depicts the exchange of messages between the processes of a distributed system along a single partiallyordered execution. A collection of MSCs is used to capture the scenarios that a designer might want the system to exhibit (or avoid).

Given the requirements in the form of a collection of MSCs, one can hope to do formal analysis and discover errors at an early stage. A standard way to

⋆ This work has been supported in part by Project DRD/CSE/98-99/MS-4 between the Indian Institute of Technology Bombay and Ericsson (India), Project 2102-1 of the Indo-French Centre for Promotion of Advanced Research and NSF grant CDA9805735.

generate a collection of MSCs is to use a High Level Message Sequence Chart (HMSC) [12]. An HMSC is a finite directed graph in which each node is labelled, in turn, by an HMSC. The HMSCs labelling the vertices may not refer to each other. The collection of MSCs represented by an HMSC consists of all MSCs obtained by tracing a path in the HMSC from an initial vertex to a terminal vertex and concatenating the MSCs that are encountered along the path.

In order to analyze the collection of MSCs represented by an HMSC, one desirable property is that these MSCs correspond to the behaviour of a finite-state system. This property would be violated if the specification were to permit an unbounded number of messages to accumulate in a channel. A sufficient condition to rule out such divergence in an HMSC is described in [3]. Subsequently, it has been observed that HMSCs can also violate the finite-state property by exhibiting nonregular behaviour over causally independent bounded channels [2]. To remedy this, a stronger criterion is established in [2] which suffices to ensure that the behaviour described by an HMSC can be implemented by a (global) finite-state system. This leads to a more general question of when a collection of MSCs should be called regular. A robust notion of regularity has been proposed in [9]. As shown in [8], this notion strictly subsumes the finite-state collections generated by HMSCs. It turns out that the collections defined by HMSCs correspond to the class of finitely-generated regular collections of MSCs.

One of the main contributions of [9] is a characterization of regular collections of MSCs in terms of (distributed) finite-state devices called message-passing automata. This addresses the important synthesis problem for MSCs, first raised in [5]; namely, how to convert requirements as specified by MSCs into distributed, state-based specifications. The message-passing automata associated with regular collections of MSCs in [9] are, in general, nondeterministic. In this respect the solution to the synthesis problem in [9] is not completely satisfactory, since real life distributed protocols are normally deterministic.

In this paper, we strengthen the result of [9] by providing a technique for decomposing a sequential automaton accepting a regular collection of MSCs into a deterministic message-passing automaton. Our result can be viewed as the message-passing analogue of the celebrated theorem of Zielonka from Mazurkiewicz trace theory establishing that regular trace languages precisely correspond to the trace languages accepted by deterministic asynchronous automata [19].

In related work, a number of studies are available which are concerned with individual MSCs in terms of their semantics and properties [1, 10]. A variety of algorithms have been developed for HMSCs in the literature—for instance, pattern matching [11, 14, 15] and detection of process divergence and non-local choice [3]. A systematic account of the various model-checking problems associated with HMSCs and their complexities is given in [2].

The paper is organized as follows. In the next section we introduce MSCs and regular MSC languages. In Section 3 we define message-passing automata and state the problem. Section 4 describes a time-stamping result for message-passing systems from [13] which is crucial for proving our main result. In Section 5 we then introduce the notion of residues and show how the ability to locally compute residues would solve the decomposition problem. The next section describes a procedure for locally updating residues. This procedure is formalized as a message-passing automaton in Section 7.

2 Regular MSC Languages

Let P = {p, q, r, …} be a finite set of processes which communicate with each other through messages. We assume that messages are never inserted, lost or modified—that is, the communication medium is reliable. However, there may be an arbitrary delay between the sending of a message and its receipt. We assume that messages are delivered in the order in which they are sent—in other words, the buffers between processes behave in a FIFO manner.

For each process p ∈ P, we fix Σ_{p} = {p!q | p ≠ q}∪{p?q | p ≠ q} to be the set of communication actions in which p participates. The action p!q is to be read as p sends to q and the action p?q is to be read as p receives from q. We shall not be concerned with the actual messages that are sent and received—we are primarily interested in the pattern of communication between agents. We will also not deal with the internal actions of the agents. We set Σ = ⋃_{p∈P} Σ_{p} and let a, b range over Σ.

For a ∈ Σ and u ∈ Σ^{∗}, #_{a}(u) denotes the number of occurrences of a in u. A word u ∈ Σ^{∗} is a proper communication sequence of the processes if for each prefix v of u and each pair of processes p, q ∈ P, #_{p!q}(v) ≥ #_{q?p}(v)— that is, at any point in the computation, at most as many messages have been received at q from p as have been sent from p to q. We say that u is a complete communication sequence if u is a proper communication sequence and for each pair of processes p, q ∈ P, #_{p!q}(u) = #_{q?p}(u)—in other words, at the end of u, all messages that have been sent have also been received. We shall often say that u is proper (respectively, complete) to mean that u is a proper (respectively, complete) communication sequence over Σ.

Let u = a_{0}a_{1} … a_{n} ∈ Σ^{∗} be proper. We can associate a natural Σ-labelled partial order M_{u} = (E_{u}, ≤, λ) with u where:

– E = {(i, a_{i}) | i ∈ {1, 2, …, n}.

– λ((i, a_{i})) = a_{i}. (If λ(e) ∈ Σ_{p}, we say that e is a p-event.)

– For p, q ∈ P, we define relations <_{pq} ⊆ E × E as follows:

• For p ∈ P, (i, a_{i}) <_{pp} (j, a_{j}) if a_{i}, a_{j} ∈ Σ_{p}, i < j and there is no i < k < j such that a_{k} ∈ Σ_{p}.

• For p, q ∈ P, p ≠ q, (i, a_{i}) <_{pq} (j, a_{j}) if a_{i} = p!q, a_{j} = q?p and the sets {(k, a_{k}) | k < i, a_{k} = p!q} and {(k, a_{k}) | k < j, a_{k} = q?p} are of the same cardinality. Since messages are assumed to be read in FIFO fashion, (i, a_{i}) <_{pq} (j, a_{j}) implies that the message read at the receive event (j, a_{j}) is the one sent at the send event (i, a_{i}).

– The partial order ≤ is the reflexive, transitive closure of the relations ⋃_{p,q∈P} <_{pq}.

We shall call the structure M_{u} generated from a complete communication sequence u a Message Sequence Chart (MSC).^{1} The partial order between events in M_{u} is a more faithful representation of the causality between events in u than the sequential order induced by writing u as a string.

Henceforth, we shall implicitly associate with each proper word u the corresponding structure M_{u} = (E_{u}, ≤, λ). In particular, E_{u} always refers to the set of events associated with the structure M_{u} generated from a proper word u. Abusing terminology, we refer to M_{u} as an MSC even if u is not complete.

Let M_{u} = (E_{u}, ≤, λ) be an MSC. For e ∈ E_{u}, e↓ denotes, as usual, the set {f ∈ E_{u} | f ≤ e}. For X ⊆ E_{u}, X↓ is defined to be ⋃_{e∈X} e↓.

We define a context-sensitive independence relation I ⊆ Σ^{∗} × (Σ × Σ) as follows: (u, a, b) ∈ I provided that u is proper, a ∈ Σ_{p} and b ∈ Σ_{q} for distinct processes p and q, and, further, if a = p!q and b = q?p then #_{a}(u) > #_{b}(u). Observe that if (u, a, b) ∈ I then (u, b, a) ∈ I.

Let Σ^{∘} = {u ∈ Σ^{∗} | u is complete}. We define ∼ ⊆ Σ^{∘} × Σ^{∘} to be the least equivalence relation such that if u = u_{1}abu_{2} and u′ = u_{1}bau_{2} and (u_{1}, a, b) ∈ I then u ∼ u′. It is important to note that ∼ is defined over Σ^{∘} (and not Σ^{∗}).

The following simple observation shows that each MSC corresponds to a ∼-equivalence classes of complete communication sequences over Σ.

Proposition 2.1. Let u, v ∈ Σ^{∘}. Then, v is a linearization of M_{u} iff u ∼ v.

We define L ⊆ Σ^{∗} to be a MSC language if every member of L is complete and L is ∼-closed (that is, for each u ∈ L, if u ∈ L and u ∼ v then v ∈ L.) We say that an MSC language L is a regular if L is a regular subset of Σ^{∗}.

Given a regular subset L ⊆ Σ^{∗}, we can decide whether L is a regular MSC language. We say that a state s in a finite-state automaton is live if there is a path from s to a final state. We then have the following result from [9].

Lemma 2.2. Let A = (S, Σ, s_{in}, δ, F) be the minimal DFA representing L. Let Chan = {(p, q) | p, q ∈ P, p ≠ q} denote the set of channels. L is a regular MSC language iff we can associate with each live state s ∈ S, a channel-capacity function K_{s} : Chan → ℕ which satisfies the following conditions.

(i) If s ∈ {s_{in}} ∪ F then K_{s}(c) = 0 for every c ∈ Ch. (ii) If s, s′ are live states and δ(s, p!q) = s′ then K_{s′}((p, q)) = K_{s}((p, q))+1 and

K_{s′}(c) = K_{s}(c) for every c ≠ (p, q). (iii) If s, s′ are live states δ(s, q?p) = s′ then K_{s}((p, q)) > 0, K_{s′}((p, q)) =

K_{s}((p, q))−1 and K_{s′}(c) = K_{s}(c) for every c ≠ (p, q). (iv) Suppose δ(s, a) = s_{1} and δ(s_{1}, b) = s_{2} with a ∈ Σ_{p} and b ∈ Σ_{q}, p ≠ q. If it

is not the case that a = p!q and b = q?p, or it is the case that K_{s}((p, q)) > 0, there exists s′_{1} such that δ(s, b) = s′_{1} and δ(s′_{1}, a) = s_{2}.

1 Our definition captures the standard partial-order semantics associated with MSCs [1, 16]. See [9] for an equivalent definition of MSCs in terms of labelled partial orders.

Observe that the conditions described in the lemma can be checked in time linear in the size of δ.

Item (iv) of the lemma has useful consequences. As usual, we extend δ to words and let δ(s_{in}, u) denote the (unique) state reached by A on reading an input u. Let u be a proper word and let a, b be communication actions such that (u, a, b) belongs to the context-sensitive independence relation defined earlier. Item (iv) guarantees that δ(s_{in}, uab) = δ(s_{in}, uba). From this, we can conclude that if v, w are complete words such that v ∼ w, then δ(s_{in}, v) = δ(s_{in}, w).

3 Message-passing automata

We now define distributed automata which accept MSC languages. Message-passing automaton A message-passing automaton over Σ is a structure A = ({A_{p}}_{p∈P}, M, s_{in}, F) where

– M is a finite alphabet of messages.

– Each component A_{p} is of the form (S_{p}, →_{p}) where • S_{p} is a finite set of p-local states.

• →_{p} ⊆ (S_{p} × Σ_{p} × M × S_{p}) is the p-local transition relation.

– s_{in} ∈ ∏_{p∈P} S_{p} is the global initial state.

– F ⊆ ∏_{p∈P} S_{p} is the set of global final states.

The local transition relation →_{p} specifies how the process p sends and receives messages. The transition (s, p!q, m, s′) specifies that when p is in the state s, it can send the message m to q (by executing the communication action p!q) and go to the state s′. The message m is, as a result, appended to the queue of messages in the channel (p, q). Similarly, the transition (s, p?q, m, s′) signifies that at the state s, the process p can receive the message m from q by executing the action p?q and go to the state s′. The message m is removed from the head of the queue of messages in the channel (q, p).

We say that A is deterministic if the local transition relation →_{p} for each component A_{p} satisfies the following conditions:

– (s, p!q, m_{1}, s′_{1}) ∈ →_{p} and (s, p!q, m_{2}, s′_{2}) ∈ →_{p} imply m_{1} = m_{2} and s′_{1} = s′_{2}.

– (s, p?q, m, s′_{1}) ∈ →_{p} and (s, p?q, m, s′_{2}) ∈ →_{p} imply s′_{1} = s′_{2}.

In other words, when a component A_{p} of a deterministic automaton A executes a send action, the current state of A_{p} uniquely determines the message sent as well as the new state of A_{p}, and when A_{p} executes a receive action, the current state of A_{p} and the nature of the message at the head of the queue uniquely determine the new state of A_{p}.

The set of global states of A is given by ∏_{p∈P} S_{p}. For a global state s, we let s_{p} denote the pth component of s. A configuration is a pair (s, χ) where s is a global state and χ : Chan → M^{∗} is the channel state which specifies the queue of messages currently residing in each channel c. The initial configuration of A is (s_{in}, χ_{ε}) where χ_{ε}(c) is the empty string ε for every channel c. The set of final configurations of A is F × {χ_{ε}}.

We now define the set of reachable configurations Conf_{A} and the global transition relation ⇒ ⊆ Conf_{A} × Σ × Conf_{A} inductively as follows:

– (s_{in}, χ_{ε}) ∈ Conf_{A}.

– Suppose (s, χ) ∈ Conf_{A}, (s′, χ′) is a configuration and (s_{p}, p!q, m, s′_{p}) ∈ →_{p} such that the following conditions are satisfied:

• r ≠ p implies s_{r} = s′_{r} for each r ∈ P.

• χ′((p, q)) = χ((p, q)) · m and for c ≠ (p, q), χ′(c) = χ(c).

Then (s, χ) ⟹^{p!q} (s′, χ′) and (s′, χ′) ∈ Conf_{A}.

– Suppose (s, χ) ∈ Conf_{A}, (s′, χ′) is a configuration and (s_{p}, p?q, m, s′_{p}) ∈ →_{p} such that the following conditions are satisfied:

• r ≠ p implies s_{r} = s′_{r} for each r ∈ P.

• χ((q, p)) = m · χ′((q, p)) and for every channel c ≠ (q, p), χ′(c) = χ(c).

Then (s, χ) ⟹^{p?q} (s′, χ′) and (s′, χ′) ∈ Conf_{A}.

Let u ∈ Σ^{∗}. A run of A on u is a map ρ : Pre(u) → Conf_{A} (where Pre(u) is the set of prefixes of u) such that ρ(ε) = (s_{in}, χ_{ε}) and for each τa ∈ Pre(u), ρ(τ) ⟹^{a} ρ(τa). The run ρ is accepting if ρ(u) is a final configuration. Let L(A) = {u | A has an accepting run on u}. It is easy to see that every member of L(A) is complete and L(A) is ∼-closed—that is, u ∈ L(A) and u ∼ u′ implies u′ ∈ L(A).

Unfortunately, L(A) need not be regular. Consider, for instance, a messagepassing automaton for the canonical producer-consumer system in which the producer p sends an arbitrary number of messages to the consumer q. Since we can reorder all the p!q actions to be performed before all the q?p actions, the queue in channel (p, q) is unbounded. Hence, the reachable configurations of this system are not bounded and the corresponding language is not regular.

For B ∈ ℕ, we say that a configuration (s, χ) of the message-passing automaton A is B-bounded if for every channel c ∈ Chan, it is the case that |χ(c)| ≤ B. We say that A is a B-bounded automaton if every reachable configuration (s, χ) ∈ Conf_{A} is B-bounded.

Proposition 3.1. Let A be a B-bounded automaton over Σ. Then L(A) is a regular MSC language.

This result follows easily from the definitions. Our goal is to prove the converse, which may be stated as follows.

Theorem 3.2. Let L be a regular MSC language over Σ. Then, there is a deterministic B-bounded message-passing automaton A over Σ such that L(A) = L.

Our strategy to prove this result is as follows. For a regular MSC language L, we consider the minimal DFA A_{L} for L. We construct a message-passing automaton A which simulates the behaviour of A_{L} on each complete word u ∈ Σ^{∗}. The catch is that no single component of A is guaranteed to see all of u.

Thus, from the partial information available in each component about u, we have to reconstruct the behaviour of A_{L} on all of u. To achieve this, we need to time-stamp events so that components can keep track of each others’ information about the computation.

4 Bounded time-stamps

Partial computations Let u ∈ Σ^{∗} be proper. A set of events I ⊆ E_{u} is called an (order) ideal if I is closed with respect to ≤—that is, e ∈ I and f ≤ e implies f ∈ I as well.

Ideals denote consistent partial computations of u—notice that any linearization of an ideal forms a proper communication sequence. p-views For an ideal I, the ≤-maximum p-event in I is denoted max_{p}(I), provided #_{Σ_{p}}(I) > 0. The p-view of I, ∂_{p}(I), is the ideal max_{p}(I)↓. Thus, ∂_{p}(I) consists of all events in I which p can “see”. (By convention, if max_{p}(I) is undefined—that is, if there is no p-event in I—the p-view ∂_{p}(I) is empty.) For P ⊆ P, we use ∂_{P} (I) to denote ⋃_{p∈P} ∂_{p}(I). Latest information Let I ⊆ E_{u} be an ideal and p, q ∈ P. Then latest(I) denotes the set of events {max_{p}(I) | p ∈ P}. For p ∈ P, we let latest_{p}(I) denote the set latest(∂_{p}(I)). A typical event in latest_{p}(I) is of the form max_{q}(∂_{p}(I)) and denotes the ≤-maximum q-event in ∂_{p}(I). This is the latest q-event in I that p knows about. For convenience, we denote this event latest_{p←q}(I). (As usual, if there is no q-event in ∂_{p}(I), the quantity latest_{p←q}(I) is undefined.)

It is clear that for q ≠ p, latest_{p←q}(I) will always correspond to a send action from Σ_{q}. However latest_{p←q}(I) need not be of the form q!p; the latest information that p has about q in I may have been obtained indirectly. Message acknowledgments Let I ⊆ E_{u} be an ideal and e ∈ I an event of the form p!q. Then, e is said to have been acknowledged in I if the corresponding receive event f such that e <_{pq} f exists and, moreover, belongs to ∂_{p}(I). Otherwise, e is said to be unacknowledged in I.

Notice that it is not enough for a message to have been received in I to deem it to be acknowledged. We demand that the event corresponding to the receipt of the message be “visible” to the sending process.

For an ideal I and a pair of processes p, q, let unack_{p→q}(I) be the set of unacknowledged p!q events in I. B-bounded computations Let u ∈ Σ^{∗} be proper and let M_{u} = (E_{u}, ≤, λ). We say that u is B-bounded, for B ∈ ℕ, if for every pair of processes p, q and for every ideal I ⊆ E, unack_{p→q}(I) contains at most B events.

The following result is immediate.

Proposition 4.1. Let u ∈ Σ^{∗} be proper. The word u is B-bounded iff for every linearization v of M_{u}, for every prefix w of v and for every pair of processes p, q, #_{p!q}(w) − #_{q?p}(w) ≤ B.

It is easy to see that during the course of a B-bounded computation, none of the message buffers ever contains more than B undelivered messages, regardless of how the events are sequentialized. Thus, if each component A_{p} of a messagepassing automaton is able to keep track of the sets {unack_{p→q}(E_{u})}_{q∈P} for each word u, this information can be used to inhibit sending messages along channels which are potentially saturated. This would provide a mechanism for constraining an arbitrary message-passing automaton to be B-bounded. Primary information Let I ⊆ E be an ideal. The primary information of I, primary(I), consists of the following events in I:

– The set latest(I) = {max_{p}(I) | p ∈ P}.

– The collection of sets unack(I) = {unack_{p→q}(I) | p, q ∈ P}.

For p ∈ P, we denote primary(∂_{p}(I)) by primary_{p}(I). Thus, primary_{p}(I) reflects the primary information of p in I. Observe that for B-bounded computations, the number of events in primary(I) is bounded.

In [13], a protocol is presented for processes to keep track of their primary information during the course of an arbitrary computation.^{2} This protocol involves appending a bounded amount of information to each message in the underlying computation, provided the computation is B-bounded. To ensure that the message overhead is bounded, the processes use a distributed time-stamping mechanism which consistently assigns “names” to events using a bounded set of labels. Consistent time-stamping Let L be a finite set of labels. For a proper communication sequence u, we say that τ : E_{u} → L is a consistent time-stamping of E_{u} by L if for each pair of (not necessarily distinct) processes p, q and for each ideal I the following holds: if e_{p} ∈ primary_{p}(I), e_{q} ∈ primary_{q}(I) and τ(e_{p}) = τ(e_{q}) then e_{p} = e_{q}.

In the protocol of [13], whenever a process p sends a message to q, it first assigns a time-stamp to the new message from a finite set of labels. Process p then appends its primary information to the message being sent. Notice that the current send event will form part of the primary information since it is the latest p-event in ∂_{p}(E_{u}). When q receives the message, it can consistently update its primary information to reflect the new information received from p.

The two tricky points in the protocol are for p to decide when it is safe to reuse a time-stamp, and for q to decide whether the information received from p is really new. In order to solve these problems, the protocol of [13] requires processes to also maintain additional time-stamps, corresponding to secondary information. Though we do not need the details of how the protocol works, we will need to refer to secondary information in the proof of our main theorem. Secondary information Let I be an ideal. The secondary information of I is the collection of sets primary(e↓) for each event e in primary(I). This collection

2 In [13], the primary information of an ideal I is defined to include more events than just latest(I) ∪ unack(I). However, for our purposes, it suffices to treat events in latest(I) ∪ unack(I) as primary.

of sets is denoted secondary(I). As usual, for p ∈ P, secondary_{p}(I) denotes the set secondary(∂_{p}(I)).

In our framework, the protocol of [13] can now be described as follows.

Theorem 4.2. For any B ∈ ℕ, we can construct a deterministic B-bounded message-passing automaton A^{B} = ({A_{p}^{B}}_{p∈P}, M^{B}, s_{in}^{B}, F^{B}) such that for every B-bounded proper communication sequence u, A^{B} inductively generates a consistent time-stamping τ of E_{u}. Moreover, for each component A_{p}^{B} of A^{B}, the local state of A_{p}^{B} at the end of u records the information primary_{p}(E_{u}) and secondary_{p}(E_{u}) in terms of the time-stamps assigned by τ.

5 Residues and decomposition

As we mentioned earlier, our strategy to prove our main theorem is to construct a message-passing automaton A which simulates the behaviour of the minimal DFA for L, A_{L} = (S, Σ, s_{in}, δ, F), on each complete communication sequence u. In other words, after reading u, the components in A must be able to decide whether δ(s_{in}, u) ∈ F. Unfortunately, after reading u each component in A only has partial information about δ(s_{in}, u)—the component A_{p} only “knows about” those events from E_{u} which lie in the p-view ∂_{p}(E_{u}). We have to devise a scheme to recover the state δ(s_{in}, u) from the partial information available with each process after reading u.

Another complication is that processes can only maintain a finite amount of information. We need a way of representing arbitrary words in a bounded, finite way. This can be done by recording for each word w, its “effect” as dictated by the minimal automaton A_{L}. We associate with each word u a function f_{u} : S → S, where S is the set of states of A_{L}, such that f_{u}(s) = δ(s, u). The following observations follow from the fact that A_{L} is the minimal DFA recognizing L.

Proposition 5.1. Let u, w ∈ Σ^{∗}. Then:

(i) δ(s_{in}, u) = f_{u}(s_{in}). (ii) f_{uw} = f_{w} ∘ f_{u}, where ∘ denotes function composition.

Clearly the function f_{w} : S → S corresponding to a word w has a bounded representation. For an input u, if the components in A could compute the function f_{u} they would be able to determine whether δ(s_{in}, u) ∈ F —by part (i) of the preceding proposition, δ(s_{in}, u) = f_{u}(s_{in}). As the following result demonstrates, for any input u, it suffices to compute f_{v} for some linearization v of the MSC M_{u}.

Proposition 5.2. Let L̂ be a regular MSC language. For complete sequences u, v ∈ Σ^{∗}, if u ∼ v then f_{u} = f_{v}.

Proof: Follows from the structural properties of A_{L} described in Lemma 2.2. □

Before proceeding, we need a convention for representing the subsequence of communication actions generated by a subset of the events in an MSC. Partial words Let u = a_{1}a_{2} … a_{n} be proper and let X ⊆ E_{u} be given by {(i_{1}, a_{i_{1}}), (i_{2}, a_{i_{2}}), …, (i_{k}, a_{i_{k}})}, where i_{1} < i_{2} < ⋯ < i_{k}. Then, u[X] denotes the subsequence a_{i_{1}}a_{i_{2}} … a_{i_{k}} (which need not be proper).

The following fact, analogous to standard results in Mazurkiewicz trace theory, will be used several times in our construction. We omit the proof.

Lemma 5.3. Let u be proper and let I, J ⊆ E_{u} be ideals such that I ⊆ J. Then u[J] ∼ u[I]u[J \ I].

Corollary 5.4. Let u be a word and I_{1} ⊆ I_{2} ⊆ ⋯ ⊆ I_{k} ⊆ E_{u} be a sequence of nested ideals. Then u[I_{k}] ∼ u[I_{1}]u[I_{2} \ I_{1}] ⋯ u[I_{k} \ I_{k−1}].

Returning to our problem, suppose that P consists of m processes {p_{1}, p_{2}, …, p_{m}}. Consider a complete word u. We wish to compute f_{v} for some v ∼ u. Suppose we construct a chain of subsets of processes ∅ = Q_{0} ⊂ Q_{1} ⊂ Q_{2} ⊂ ⋯ ⊂ Q_{m} = P such that for j ∈ {1, 2, …, m}, Q_{j} = Q_{j−1} ∪ {p_{j}}. From Corollary 5.4, we then have

u = u[∂_{Q_{m}}(E_{u})] ∼ u[∂_{Q_{0}}(E_{u})]u[∂_{Q_{1}}(E_{u}) \ ∂_{Q_{0}}(E_{u})] ⋯ u[∂_{Q_{m}}(E_{u}) \ ∂_{Q_{m−1}}(E_{u})]

Observe that ∂_{Q_{j}}(E_{u}) \ ∂_{Q_{j−1}}(E_{u}) is the same as ∂_{p_{j}}(E_{u}) \ ∂_{Q_{j−1}}(E_{u}). Thus, we can rewrite the expression above as

u = u[∂_{Q_{m}}(E_{u})] ∼ u[∅]u[∂_{p_{1}}(E_{u}) \ ∂_{Q_{0}}(E_{u})] ⋯ u[∂_{p_{m}}(E_{u}) \ ∂_{Q_{m−1}}(E_{u})] (♢)

The word u[∂_{p_{j}}(E_{u}) \ ∂_{Q_{j−1}}(E_{u})] is the portion of u which p_{j} has seen but which the processes in Q_{j−1} have not seen. This is a special case of what we call a residue. Residues Let u be proper, I ⊆ E_{u} an ideal and p ∈ P a process. R(u, p, I) denotes the word u[∂_{p}(E_{u}) \ I] and is called the residue of u at p with respect to I. Observe that any residue of the form R(u, p, I) can equivalently be written R(u, p, ∂_{p}(E_{u}) ∩ I).

Using the notation of residues, we can write the word u[∂_{p_{j}}(E_{u}) \ ∂_{Q_{j−1}}(E_{u})] as R(u, p_{j}, ∂_{Q_{j−1}}(E_{u})). A residue of this form is called a process residue: R(u, p, I) is a process residue if R(u, p, I) = R(u, p, ∂_{P} (E_{u})) for some P ⊆ P. We say that R(u, p, ∂_{P} (E_{u})) is the P -residue of u at p.

Unfortunately, a process residue at p may change due to an action of another process. For instance, if we extend a word u by an action a = q?p, it is clear that R(u, p, ∂_{q}(E_{u})) will not be the same as R(ua, p, ∂_{q}(E_{ua})) since q will get to know about more events from ∂_{p}(u) after receiving the message via the action a. On the other hand, since p does not move on an action of the form q?p, p has no chance to update its q-residue when the action q?p occurs.

However, it turns out that each process can maintain a set of residues based on its primary information such that these primary residues subsume the process residues. The key technical fact which makes this possible is the following.

Lemma 5.5. For any non-empty ideal I, and p, q ∈ P, the maximal events in ∂_{p}(I) ∩ ∂_{q}(I) lie in primary_{p}(I) ∩ primary_{q}(I).

Proof: We show that for each maximal event e in ∂_{p}(I) ∩ ∂_{q}(I), either e ∈ latest(∂_{p}(I)) ∩ unack(∂_{q}(I)) or e ∈ unack(∂_{p}(I)) ∩ latest(∂_{q}(I)).

First suppose that ∂_{p}(I) \ ∂_{q}(I) and ∂_{q}(I) \ ∂_{p}(I) are both nonempty. Let e be a maximal event in ∂_{p}(I) ∩ ∂_{q}(I). Suppose e is an r-event, for some r ∈ P. Since ∂_{p}(I)\∂_{q}(I) and ∂_{q}(I)\∂_{p}(I) are both nonempty, it follows that r ∉ {p, q}. The event e must have ≤-successors in both ∂_{p}(I) and ∂_{q}(I). However, observe that any event f can have at most two immediate ≤-successors—one “internal” successor within the process and, if f is a send event, one “external” successor corresponding to the matching receive event.

Thus, the maximal event e must be a send event, with a <_{rr} successor e_{r} and a <_{rs} successor e_{s}, corresponding to some s ∈ P. Assume that e_{r} ∈ ∂_{q}(I) \ ∂_{p}(I) and e_{s} ∈ ∂_{p}(I) \ ∂_{q}(I). Since the r-successor of e is outside ∂_{p}(I), e = max_{r}(∂_{p}(I)). So e belongs to latest(∂_{p}(I)). On the other hand, e is an unacknowledged r!s event in ∂_{q}(I). Thus, e ∈ unack_{r→s}(∂_{q}(I)), which is part of unack(∂_{q}(I)).

Symmetrically, if e_{r} ∈ ∂_{p}(I) \ ∂_{q}(I) and e_{s} ∈ ∂_{q}(I) \ ∂_{p}(I), we find that e belongs to unack(∂_{p}(I)) ∩ latest(∂_{q}(I)).

We still have to consider the case when ∂_{p}(I) ⊆ ∂_{q}(I) or ∂_{q}(I) ⊆ ∂_{p}(I). Suppose that ∂_{p}(I) ⊆ ∂_{q}(I), so that ∂_{p}(I) ∩ ∂_{q}(I) = ∂_{p}(I). Let e = max_{p}(∂_{q}(I)). Clearly, ∂_{p}(I) = e↓. Consider any r-event f in ∂_{p}(I), where r ∉ {p, q}. Since f < e, f cannot be maximal in ∂_{p}(I). Thus, the only maximal event in ∂_{p}(I) is the p-event e. Since e has a successor in ∂_{q}(I), e must be a send event and is hence in unack(∂_{p}(I)). Thus, e ∈ unack(∂_{p}(I)) ∩ latest(∂_{q}(I)). Symmetrically, if ∂_{q}(I) ⊆ ∂_{p}(I), the unique maximal event e in ∂_{q}(I) belongs to latest(∂_{p}(I)) ∩ unack(∂_{q}(I)). □

Let us call R(u, p, I) a primary residue if I is of the form X↓ for some subset X ⊆ primary_{p}(E_{u}). Clearly, for p, q ∈ P, R(u, p, ∂_{q}(E_{u})), can be rewritten as R(u, p, ∂_{p}(E_{u})∩∂_{q}(E_{u})). So, by the previous result the q-residue R(u, p, ∂_{q}(E_{u})) is a primary residue R(u, p, X↓) for some X ⊆ primary(∂_{p}(E_{u})). Further, the set X can be effectively computed from the primary information of p and q. In fact, it turns out that all process residues can be effectively described in terms of primary residues.

We begin with a simple observation, whose proof we omit.

Proposition 5.6. Let u ∈ Σ^{∗} be proper and p ∈ P. For ideals I, J ⊆ E_{u}, let R(u, p, I) and R(u, p, J) be primary residues such that R(u, p, I) = R(u, p, X_{I}↓) and R(u, p, J) = R(u, p, X_{J}↓) for X_{I}, X_{J} ⊆ primary_{p}(E_{u}). Then R(u, p, I ∪ J) is also a primary residue and R(u, p, I ∪ J) = R(u, p, (X_{I} ∪ X_{J})↓).

Our claim that all process residues can be effectively described in terms of primary residues can then be formulated as follows.

Lemma 5.7. Let u ∈ Σ^{∗} be proper, p ∈ P and Q ⊆ P. Then R(u, p, ∂_{Q}(E_{u})) is a primary residue R(u, p, X↓) for p. Further, the set X ⊆ primary_{p}(E_{u}) can be effectively computed from the information in ⋃_{q∈{p}∪Q} primary_{q}(E_{u}).

Proof: Let Q = {q_{1}, q_{2}, …, q_{k}}. We can rewrite R(u, p, ∂_{Q}(E_{u})) as R(u, p, ⋃_{i∈[1..k]} ∂_{q_{i}}(E_{u})). From Lemma 5.5 it follows that for each i ∈ {1, 2, …, k}, p can compute a set X_{i} ⊆ primary_{p}(E_{u}) from the information in primary_{p}(E_{u})∪ primary_{q_{i}}(E_{u}) such that R(u, p, ∂_{q_{i}}(E_{u})) = R(u, p, X_{i}↓). From Proposition 5.6, it then follows that R(u, p, ∂_{Q}(E_{u})) = R(u, p, ⋃_{i∈{1,2,...,k}} ∂_{q_{i}}(E_{u})) = R(u, p, X↓) where X = ⋃_{i∈{1,2,...,k}} X_{i}. □

6 Updating residues

We now describe how, while reading a word u, each process p maintains the functions f_{w} for each primary residue w of u at p.

Initially, at the empty word u = ε, every primary residue from {R(u, p, X↓)}_{p∈P,X⊆primary(∂_{p}(E_{u}))} is just the empty word ε. So, all primary residues are represented by the identity function Id : {s ↦ s}.

Let u ∈ Σ^{∗} and a ∈ Σ. Assume inductively that every p ∈ P has computed at the end of u the function f_{w} for each primary residue w = R(u, p, X↓), where X ⊆ primary(∂_{p}(E_{u})). We want to compute for each p the corresponding functions after the word ua.

Suppose a is of the form p!q and X ⊆ primary_{p}(E_{ua}). Let e_{a} denote the event corresponding to the new action a. If e_{a} ∈ X, then R(ua, p, X↓) = ε, so we represent the residue by the identity function Id. On the other hand, if a ∉ X, then X ⊆ primary_{p}(E_{u}), so we already have a residue of the form R(u, p, X). We then set R(ua, p, X↓) to be f_{a} ∘ R(u, p, X↓). For r ≠ p, the primary residues are unchanged when going from u to ua.

The case where a is of the form p?q is more interesting. As before, the primary residues are unchanged for r ≠ p. We show how to calculate all the new primary residues for p using the information obtained from q. This will use the following result.

Lemma 6.1. Let u ∈ Σ^{∗} be proper. Let p, q ∈ P and e ∈ E_{u} such that e ∈ primary_{q}(E_{u}) but e ∉ ∂_{p}(E_{u}). Then R(u, p, e↓) is a primary residue R(u, p, X↓) for p. Further, the set X ⊆ primary(∂_{p}(E_{u})) can be effectively computed from the information in primary_{p}(E_{u}) and secondary_{q}(E_{u}).

Proof: Let e be an r-event, r ∈ P and let J = ∂_{p}(E_{u}) ∪ e↓. By construction, max_{p}(J) = max_{p}(E_{u}). On the other hand, max_{r}(J) = e, since e is an r-event and we assumed that e ∉ ∂_{p}(E_{u}).

By Lemma 5.5, the maximal events in ∂_{p}(J) ∩ ∂_{r}(J) lie in primary_{p}(J) ∩ primary_{r}(J). Since max_{p}(J) = max_{p}(E_{u}), primary_{p}(J) = primary_{p}(E_{u}). On the other hand, primary_{r}(J) = primary(e↓), which is a subset of secondary_{q}(E_{u}), since e ∈ primary_{q}(E_{u}).

Thus, the set of maximal events in ∂_{p}(J)∩∂_{r}(J), which is the same as ∂_{p}(E_{u})∩ e↓, is contained in primary_{p}(E_{u}) ∩ primary(e↓). These events are available in primary_{p}(E_{u}) ∪ secondary_{q}(E_{u}). □

Suppose that X ⊆ primary_{p}(E_{ua}). Suppose that X = {x_{1}, x_{2}, …, x_{k}}.

We first argue that for each x_{i} ∈ X, R(u, p, x_{i}↓) is a primary residue R(u, p, Y_{i}↓), where Y_{i} ⊆ primary_{p}(E_{u}). If x_{i} ∈ primary_{p}(E_{u}), then R(u, p, x_{i}↓) is already a primary residue, so we can set Y_{i} = {x_{i}}. If, however, x_{i} ∉ primary_{p}(E_{u}), then x_{i} must have been contributed from primary_{q}(u) through the message received at the action a. We have x_{i} ∈ primary_{q}(E_{u}) but x_{i} ∉ ∂_{p}(E_{u}). Thus, appealing to Lemma 6.1, we can identify Y_{i} ⊆ primary_{p}(E_{u}) such that R(u, p, {x_{i}}↓) = R(u, p, Y_{i}↓).

Since X = ⋃_{i∈{1,2,...,k}} x_{i}, we can appeal to Proposition 5.6 to argue that R(u, p, X↓) is the primary residue R(u, p, Y ↓) where Y = ⋃_{i∈{1,2,...,k}} Y_{i}. We can then set R(ua, p, X↓) = f_{a} ∘ R(u, p, Y ↓).

Thus, after each action that is performed, the process performing the action can effectively update its primary residues using the primary and secondary information available to it.

7 A deterministic message-passing automaton for L

We can now construct a deterministic B-bounded message-passing automaton corresponding to a given regular MSC language L. We first observe that there is a bound B ∈ ℕ such that every word in L is B-bounded.

Proposition 7.1. Let L ⊆ Σ^{∗} be a regular MSC language. There is an effectively computable bound B ∈ ℕ such that every word in L is B-bounded.

Proof: Let A_{L} = (S, Σ, s_{in}, δ, F) be the minimal DFA for L. Recall that we can associate with each live state in S and each channel (p, q) ∈ Chan a channelcapacity function K_{s} : Chan → ℕ. Let B be the maximum value of K_{s}((p, q)) over all live states s and all channels (p, q).

We know that for any word u in L, the run of A_{L} on u visits only live states. Thus, while processing u, no channel’s capacity ever exceeds the bound B. Moreover, since L is ∼-closed, every interleaving v of M_{u} belongs to L and the run of A_{L} on each such interleaving also respects this bound. From Proposition 4.1, we can conclude that in every ideal I ⊆ E_{u}, for any pair p, q of processes, the set unack_{p→q}(I) contains at most B-events. Thus, u is B-bounded. □

We now construct a B-bounded message-passing automaton A = ({A_{p}}_{p∈P}, M, s_{in}, F) for L, where B is the bound derived from the minimal DFA A_{L} for L as described in the preceding proposition.

Recall that A^{B} = ({A_{p}^{B}}_{p∈P}, M^{B}, s_{in}^{B}, F^{B}) is the time-stamping automaton for B-bounded computations, where the state of each component records the primary and secondary information of the component in terms of a consistent set of time-stamps.

– The message alphabet of A is the alphabet M^{B} used by the time-stamping automaton A^{B}.

– In A, a typical state of a component A_{p} is a pair (s_{B}, s_{R}) where s_{B} is a state drawn from A_{p}^{B} and s_{R} is the collection {f_{X} : S → S}_{X⊆primary_{p}(E_{u})} of primary residues of A_{p} at the end of a word u.

– The local transition relation →_{p} of each component A_{p} is as follows:

• For a of the form p!q, the tuple ((s_{B}, s_{R}), a, m, (s′_{B}, s′_{R})) ∈ →_{p} provided (s_{B}, a, m, s′_{B}) ∈ →_{p}^{B} and the residues in s′_{R} are derived from the residues in s_{R} using the time-stamping information in s_{B}, as described in Section 6. Moreover, according to the primary information in s_{B}, it should be the case that |unack_{p→q}(E_{u})| < B for the word u read so far. Otherwise, this send action is disabled.

• For a of the form p?q, the tuple ((s_{B}, s_{R}), a, m, (s′_{B}, s′_{R})) ∈ →_{p} provided (s_{B}, a, m, s′_{B}) ∈ →_{p}^{B} and the residues in s′_{R} are derived from the residues in s_{R} using the time-stamping information in s_{B} and the message m, as described in Section 6.

– In the initial state of A, the local state of each component A_{p} is of the form (s_{B,in}^{p}, s_{R,in}^{p}) where s_{B,in}^{p} is the initial state of A_{p}^{B} and s_{R,in}^{p} records each residue to be the identity function Id.

– The global state {(s_{B}^{p}, s_{R}^{p})}_{p∈P} belongs to the set F of final states if the primary residues stored in the global state record that δ(s_{in}, u) ∈ F for the word u read so far. (This is achieved by evaluating the expression (♢) in Section 5.)

From the analysis of the previous section, it is clear that A accepts precisely the language L. The last clause in the transition relation →_{p} for send actions ensures that A will not admit a run in which unack_{p→q}(E_{u}) grows beyond B events for any input u and any pair of processes p, q. This ensures that every reachable configuration of A is B-bounded. Finally, we observe that A is deterministic because the time-stamping automaton A^{B} is deterministic and the update procedure for residues described in Section 6 is also deterministic.

We have thus succeeded in proving the main result we were after (Theorem 3.2)—namely, that for every regular MSC language L over Σ, there is a deterministic B-bounded message-passing automaton A over Σ such that L(A) = L.

We conclude by providing an upper bound for the size of A, which can be computed by estimating the number of bits required to record the time-stamps and residues which form the local state of a process.

Proposition 7.2. Let n be the number of processes in the system, m be the number of states of the minimal DFA A_{L} for L and B the bound computed from the channel-capacity functions of A_{L}. Then, the number of local states of each component A_{p} is at most 2^{(2^{O(Bn^{2})}m log m)}.

References

1. Alur, R., Holzmann, G.J., and Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools, 17(2) (1996) 70–77.

2. Alur, R., and Yannakakis, M.: Model checking of message sequence charts. Proc. CONCUR’99, LNCS 1664, Springer Verlag (1999) 114–129.

3. Ben-Abdallah, H., and Leue, S.: Syntactic detection of process divergence and nonlocal choice in message sequence charts. Proc. TACAS’97, LNCS 1217, Springer-Verlag (1997) 259–274.

4. Booch, G., Jacobson, I., and Rumbaugh, J.: Unified Modeling Language User Guide. Addison Wesley (1997).

5. Damm, W., and Harel, D.: LCS’s: Breathing life into message sequence charts. Proc. FMOODS’99, Kluwer Academic Publishers (1999) 293–312.

6. Diekert, V., and Rozenberg, G. (Eds.): The book of traces. World Scientific (1995).

7. Harel, D., and Gery, E.: Executable object modeling with statecharts. IEEE Computer, July 1997 (1997) 31–42.

8. Henriksen, J.G., Mukund, M., Narayan Kumar K., and Thiagarajan, P.S.: On message sequence graphs and finitely generated regular MSC languages, to appear in Proc. ICALP 2000, LNCS, Springer-Verlag (2000).

9. Henriksen, J.G., Mukund, M., Narayan Kumar K., and Thiagarajan, P.S.: Regular collections of message sequence charts, to appear in Proc. MFCS 2000, LNCS, Springer-Verlag (2000).

10. Ladkin, P.B., and Leue, S.: Interpreting message flow graphs. Formal Aspects of Computing 7(5) (1975) 473–509.

11. Levin, V., and Peled, D.: Verification of message sequence charts via template matching. Proc. TAPSOFT’97, LNCS 1214, Springer-Verlag (1997) 652–666.

12. Mauw, S., and Reniers, M.A.: High-level message sequence charts, Proc. SDL ’97, Elsevier (1997) 291–306.

13. Mukund, M., Narayan Kumar, K., and Sohoni, M.: Keeping track of the latest gossip in message-passing systems. Proc. Structures in Concurrency Theory (STRICT), Workshops in Computing Series, Springer-Verlag (1995) 249–263.

14. Muscholl, A.: Matching Specifications for Message Sequence Charts. Proc. FOS-SACS’99, LNCS 1578, Springer-Verlag (1999) 273–287.

15. Muscholl, A., Peled, D., and Su, Z.: Deciding properties for message sequence charts. Proc. FOSSACS’98, LNCS 1378, Springer-Verlag (1998) 226–242.

16. Rudolph, E., Graubmann, P., and Grabowski, J.: Tutorial on message sequence charts. In Computer Networks and ISDN Systems—SDL and MSC, Volume 28 (1996).

17. Thomas, W.: Automata on infinite objects. In van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science, Volume B, North-Holland, Amsterdam (1990) 133–191.

18. Thomas, W.: Languages, Automata, and Logic. In Rozenberg, G., and Salomaa, A. (Eds.), Handbook of Formal Language Theory, Vol. III, Springer-Verlag, New York (1997) 389–455.

19. Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O.—Inf. Théor. et Appl., 21 (1987) 99–135.