Mathematical Foundation of Computer Science (MFCS) 2000, Proceedings: Mogens Nielsen, Branislav Rovan (eds.) Springer Lecture Notes in Computer Science 1893 (2000), 405–414.

Regular Collections of Message Sequence Charts

(Extended Abstract)

Jesper G. Henriksen^{1}, Madhavan Mukund^{2}^{,}^{⋆},
K. Narayan Kumar^{2}^{,}^{⋆}, and P.S. Thiagarajan^{2}

1 BRICS^{⋆⋆}, University of Aarhus, Denmark. Email: gulmann@brics.dk

2 Chennai Mathematical Institute, Chennai, India

           Email: {madhavan,kumar,pst}@smi.ernet.in

Abstract. Message Sequence Charts (MSCs) are an attractive visual formalism used during the early stages of design in domains such as telecommunication software. A popular mechanism for generating a collection of MSCs is a Hierarchical Message Sequence Chart (HMSC). However, not all HMSCs describe collections of MSCs that can be “realized” as a finite-state device. Our main goal is to pin down this notion of realizability. We propose an independent notion of regularity for collections of MSCs and explore its basic properties. In particular, we characterize regular collections of MSCs in terms of finite-state distributed automata called bounded message-passing automata, in which a set of sequential processes communicate with each other asynchronously over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs. It turns out that realizable collections of MSCs as specified by HMSCs constitute a strict subclass of the regular collections of MSCs.

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 [12, 19]. 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, 9, 19]. 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 design errors at an early stage. A natural question in this context is to identify when a collection of MSCs is amenable to formal analysis. A related issue is how to represent such collections.

⋆ Supported in part by IFCPAR Project 2102-1.

⋆⋆

Basic Research in Computer Science, Centre of the Danish National Research Foundation.

A standard way to generate a collection of MSCs is to use a Hierarchical Message Sequence Chart (HMSC) [15]. An HMSC is a finite directed graph in which each node is labelled, in turn, by an HMSC. The labels on the nodes are not permitted to refer to each other. From an HMSC we can derive an equivalent Message Sequence Graph (MSG) [1] by flattening out the hierarchical labelling to obtain a graph where each node is labelled by a simple MSC. An MSG defines a collection of MSCs obtained by concatenating the MSCs labelling each path from an initial vertex to a terminal vertex. Though HMSCs provide more succinct specifications than MSGs, they are only as expressive as MSGs. Thus, one often restricts one’s attention to characterizing structural properties of MSGs rather than of HMSCs [2, 17, 18].

In [2], it is shown that bounded MSGs define reasonable collections of MSCs— the collection of MSCs generated by a bounded MSG can be represented as a regular string language. Thus, behaviours captured by bounded MSGs can, in principle, be realized as finite-state automata. In general, the collection of MSCs defined by an arbitrary MSG is not realizable in this sense. A characterization of the collections of MSCs definable using bounded MSGs is provided in [11].

The main goal of this paper is to pin down this notion of realizability in terms of a notion of regularity for collections of MSCs. One consequence of our study is that our definition of regularity provides a general and robust setting for studying collections of MSCs. A second consequence, which follows from the results in [11], is that bounded MSGs define a strict subclass of regular collections of MSCs. A final consequence is that our notion addresses an important issue raised in [6]; namely, how to convert requirements as specified by MSCs into distributed, state-based specifications.

Another motivation for focussing on regularity is that this notion has turned out to be very fruitful in a variety of contexts including finite (and infinite) strings, trees and restricted partial orders known as Mazurkiewicz traces [7, 21]. In all these settings there is a representation of regular collections in terms of finite-state devices. There is also an accompanying monadic second-order logic that usually induces temporal logics using which one can reason about such collections [21]. One can then develop automated model-checking procedures for verifying properties specified in these temporal logics. In this context, the associated finite-state devices representing the regular collections often play a very useful role [22].

We show here that our notion of regular MSC languages fits in nicely with a related notion of a finite-state device, as also a monadic second-order logic. We fix a finite set of processes P and consider M, the universe of MSCs defined over the set P. An MSC in M can be viewed as a partial order labelled using a finite alphabet Σ that is canonically fixed by P. We say that L ⊆ M is regular if the set of all linearizations of all members of L constitutes a regular subset of Σ^{∗}. A crucial point is that the universe M is itself not regular according to our definition, unlike the classical setting of strings (or trees or Mazurkiewicz traces). This fact has a strong bearing on the automata-theoretic and logical formulations in our work.

It turns out that regular MSC languages can be stratified using the concept of bounds. An MSC is said to be B-bounded for a natural number B if at every “prefix” of the MSC and for every pair of processes (p, q) there are at most B messages that p has sent to q that have yet to be received by q. An MSC language is B-bounded if every member of the language is B-bounded. Fortunately, for every regular MSC language L we can effectively compute a (minimal) bound B such that L is B-bounded. This leads to our automaton model called B-bounded message-passing automata. The components of such an automaton correspond to the processes in P. These components communicate with each other over (potentially unbounded) FIFO channels. We say that a message-passing automaton is B-bounded if, during its operation, it is never the case that a channel contains more than B messages. We establish a precise correspondence between B-bounded message-passing automata and B-bounded regular MSC languages. In a similar vein, we formulate a natural monadic second-order logic MSO(P, B) interpreted over B-bounded MSCs. We then show that B-bounded regular MSC languages are exactly those that are definable in MSO(P, B).

In related work, a number of studies are available that are concerned with individual MSCs in terms of their semantics and properties [1, 13]. As pointed out earlier, a nice way to generate a collection of MSCs is to use an MSG. A variety of algorithms have been developed for MSGs in the literature—for instance, pattern matching [14, 17, 18] and detection of process divergence and non-local choice [3]. A systematic account of the various model-checking problems associated with MSGs and their complexities is given in [2].

In this paper, we confine our attention to finite MSCs. The issues investigated here have, at present, no counterparts in the infinite setting. We feel, however, that our results will serve as a launching pad for a similar account concerning infinite MSCs. This should then lead to the design of appropriate temporal logics and automata-theoretic solutions (based on message-passing automata) to model-checking problems for these logics.

The paper is organized as follows. In the next section we introduce MSCs and regular MSC languages. In Section 3 we establish our automata-theoretic characterization and, in Section 4, the logical characterization. While doing so, we borrow one basic result and a couple of proof techniques from the theory of Mazurkiewicz traces [7]. However, we need to modify some of these techniques in a non-trivial way (especially in the setting of automata) due to the asymmetric flow of information via messages in the MSC setting, as opposed to the symmetric information flow via handshake communication in the trace setting. Due to lack of space, we provide only proof ideas. Detailed proofs are available in [10].

2 Regular MSC Languages

Through the rest of the paper, we fix a finite set of processes (or agents) P and let p, q, r range over P. For each p ∈ P we define Σ_{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.

[figure: (p); (q); (r); •; e_{1}; •; e_{2}; •; e′_{2}; •; e_{3}; •; e′_{1}; •; e′_{3}]

Fig. 1. An example MSC over {p, q, r}.

At our level of abstraction, we shall not be concerned with the actual messages that are sent and received. We will also not deal with the internal actions of the agents. We set Σ = ⋃_{p∈P} Σ_{p} and let a, b range over Σ. We also denote the set of channels by Ch = {(p, q) | p ≠ q} and let c, d range over Ch.

A Σ-labelled poset is a structure M = (E, ≤, λ) where (E, ≤) is a poset and λ : E → Σ is a labelling function. For e ∈ E we define ↓e = {e′ | e′ ≤ e}. For p ∈ P and a ∈ Σ, we set E_{p} = {e | λ(e) ∈ Σ_{p}} and E_{a} = {e | λ(e) = a}, respectively. For each c ∈ Ch, we define the relation R_{c} = {(e, e′) | λ(e) = p!q, λ(e′) = q?p and |↓e ∩ E_{p!q}| = |↓e′ ∩ E_{q?p}|}. Finally, for each p ∈ P, we define the relation R_{p} = (E_{p} × E_{p}) ∩ ≤.

An MSC (over P) is a finite Σ-labelled poset M = (E, ≤, λ) that satisfies the following conditions:

(i) Each R_{p} is a linear order. (ii) If p ≠ q then |E_{p!q}| = |E_{q?p}|. (iii) ≤ = (R_{P} ∪ R_{Ch})^{∗} where R_{P} = ⋃_{p∈P} R_{p} and R_{Ch} = ⋃_{c∈Ch} R_{c}.

In diagrams, the events of an MSC are presented in visual order. The events of each process are arranged in a vertical line and the members of the relation R_{Ch} are displayed as horizontal or downward-sloping directed edges. We illustrate the idea with an example in Figure 1. Here P = {p, q, r}. For x ∈ P, the events in E_{x} are arranged along the line labelled (x) with smaller (relative to ≤) events appearing above the larger events. The R_{Ch}-edges across agents are depicted by horizontal edges—for instance e_{3} R_{(r,q)} e′_{2}. The labelling function λ is easy to extract from the diagram—for example, λ(e′_{3}) = r!p and λ(e_{2}) = q?p.

We define regular MSC languages in terms of their linearizations. For the MSC M = (E, ≤, λ), let Lin(M) = {λ(π) | π is a linearization of (E, ≤)}. By abuse of notation, we have used λ to also denote the natural extension of λ to E^{∗}. The string p!q r!q q?p q?r r!p p?r is a linearization of the MSC in Figure 1.

In the literature [1, 18] one sometimes considers a more generous notion of linearization where two adjacent receive actions in a process corresponding to messages from different senders are deemed to be causally independent. For instance, p!q r!q q?r q?p r!p p?r would also be a valid linearization of the MSC in Figure 1. All our results go through with suitable modifications even in the presence of this more generous notion of linearization.

Henceforth, we will identify an MSC with its isomorphism class. We let M_{P} be the set of MSCs over P. An MSC language L ⊆ M_{P} is said to regular if ⋃{Lin(M) | M ∈ L} is a regular subset of Σ^{∗}. We note that the entire set M_{P} is not regular by this definition.

To directly characterize the subsets of Σ^{∗} that correspond to regular MSC languages, we proceed as follows. Let Com = {(p!q, q?p) | (p, q) ∈ Ch}. For τ ∈ Σ^{∗} and a ∈ Σ, let |τ|_{a} denote the number of times a appears in τ. We say that σ ∈ Σ^{∗} is proper if for every prefix τ of σ and every pair (a, b) ∈ Com, |τ|_{a} ≥ |τ|_{b}. We say that σ is complete if σ is proper and |σ|_{a} = |σ|_{b} for every (a, b) ∈ Com. Next we define a context-sensitive independence relation I ⊆ Σ^{∗} × (Σ × Σ) as follows: (σ, a, b) ∈ I if σab is proper, a ∈ Σ_{p} and b ∈ Σ_{q} for distinct processes p and q, and if (a, b) ∈ Com then |σ|_{a} > |σ|_{b}. Observe that if (σ, a, b) ∈ I then (σ, b, a) ∈ I.

Let Σ^{∘} = {σ | σ ∈ Σ^{∗} and σ is complete}. We then define ∼ ⊆ Σ^{∘} × Σ^{∘} to be the least equivalence relation such that if σ = σ_{1}abσ_{2}, σ′ = σ_{1}baσ_{2} and (σ_{1}, a, b) ∈ I then σ ∼ σ′. It is important to note that ∼ is defined over Σ^{∘} (and not Σ^{∗}). It is easy to verify that for each M ∈ M_{P}, Lin(M) is a subset of Σ^{∘} and is in fact a ∼-equivalence class over Σ^{∘}.

We define L ⊆ Σ^{∗} to be a regular string MSC language if there exists a regular MSC language L ⊆ M_{P} such that L = ⋃{Lin(M) | M ∈ L}. It is easy to see that L ⊆ Σ^{∗} is a regular string MSC language if and only if L is a regular subset of Σ^{∗}, every word in L is complete and L is ∼-closed (that is, for each σ ∈ L, if σ ∈ L and σ ∼ σ′ then σ′ ∈ L). Clearly regular MSC languages and regular string MSC languages represent each other. Hence, abusing terminology, we will write “regular MSC language” to mean “regular string MSC language”. From the context, it should be clear whether we are working with MSCs from M_{P} or complete words over Σ^{∗}.

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. Let A = (S, Σ, s_{in}, δ, F) be the minimal DFA representing L. Then it is not difficult to see that L is a regular MSC language if and only if we can associate with each live state s ∈ S, a channel-capacity function K_{s} : Ch → ℕ that 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 and δ(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

(a, b) ∉ Com or K_{s}((p, q)) > 0, there exists s′_{1} such that δ(s, b) = s′_{1} and δ(s′_{1}, a) = s_{2}.

These conditions can be checked in time linear in the size of δ. We conclude this section by introducing the notion of B-bounded MSC languages. Let B ∈ ℕ be a natural number. We say that a complete word σ is B-bounded if for each prefix τ of σ and for each channel (p, q) ∈ Ch, |τ|_{p!q} − |τ|_{q?p} ≤ B. We say that L ⊆ Σ^{∘} is B-bounded if every word σ ∈ L is B-bounded. Let L be a regular MSC language and let A = (S, Σ, s_{in}, δ, F) be its minimal DFA, as described above, with capacity functions {K_{s}}_{s∈S}. Let B_{L} = max_{s∈S,c∈Ch} K_{s}(c). Then it is easy to see that L is B_{L}-bounded and that B_{L} can be effectively computed from A. Finally, we shall say that the MSC M is B-bounded if every string in Lin(M) is B-bounded. A collection of MSCs is B-bounded if every member of the collection is B-bounded.

3 An Automata-Theoretic Characterization

Recall that the set of processes P determines the communication alphabet Σ and that for p ∈ P, Σ_{p} denotes the actions in which process p participates.

Definition 3.1. A message-passing automaton over Σ is a structure A = ({A_{p}}_{p∈P}, Δ, s_{in}, F) where

– Δ 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} × Δ × 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 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 action p!q and move to the state s′. The message m is, as a result, appended to the queue in channel (p, q). Similarly, the transition (s, p?q, m, s′) signifies that in the state s, the process p can receive the message m from q by executing the action p?q and move to the state s′. The message m is removed from the head of the queue in channel (q, 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 χ : Ch → Δ^{∗} is the channel state that 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:

[figure: (p) :; s_{1}; p!q; ⟹; (q) :; t_{1}; q!p; q?p; ⟹; s_{2}; p!q; t_{2}; q?p; t_{3}; s_{3}; p?q]

Fig. 2. A 3-bounded message-passing automaton.

• 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 c ≠ (q, p), χ′(c) = χ(c).

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

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

Clearly, L(A) need not be regular. Consider, for instance, a message-passing 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) can grow arbitrarily long. 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 ∈ Ch, 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. It is not difficult to show that given a messagepassing automaton A and a bound B ∈ ℕ, one can decide whether A is Bbounded. Figure 2 shows an example of a 3-bounded message-passing automaton with two components, p and q. In this example, the message alphabet is a singleton, and is hence omitted. The initial state is (s_{1}, t_{1}) and there is only one final state, (s_{2}, t_{3}). This automaton accepts an infinite set of MSCs, none of which can be expressed as the concatenation of two or more non-trivial MSCs. It follows easily that the MSC language accepted by this automaton cannot be represented by an MSG.

Lemma 3.2. Let A be a B-bounded automaton over Σ. Then L(A) is a Bbounded regular MSC language.

This result follows from the definitions and it constitutes the easy half of the characterization we wish to obtain. The difficult half is :

Lemma 3.3. Let L ⊆ Σ^{∗} be a B-bounded regular MSC language. Then there exists a B-bounded message-passing automaton A over Σ such that L(A) = L.

The first step in the proof is to view L as a regular Mazurkiewicz trace language over an appropriate alphabet and apply Zielonka’s theorem [23] to obtain an asynchronous automaton recognizing L. The second step, which is the hard part, is to simulate this asynchronous automaton by a B-bounded message passing automaton. This simulation makes crucial use of the technique developed in [16] for locally maintaining the latest information about other processes in a message-passing system.

We say that A is a bounded message-passing automaton if A is B-bounded for some B ∈ ℕ. The main result of this section is an easy consequence of the two previous lemmas.

Theorem 3.4. Let L ⊆ Σ^{∗} be a regular MSC language. Then there exists a bounded message-passing automaton A over Σ such that L(A) = L.

4 A Logical Characterization

We formulate a monadic second-order logic that characterizes regular B-boun-ded MSC languages for each fixed B ∈ ℕ. Thus our logic will be parameterized by a pair (P, B). For convenience, we fix B ∈ ℕ through the rest of the section. As usual, we shall assume a supply of individual variables x, y, …, a supply of set variables X, Y, …, and a family of unary predicate symbols {Q_{a}}_{a∈Σ}. The syntax of the logic is then given by:

MSO(P, B) ::= Q_{a}(x) | x ∈ X | x ≤ y | ¬φ | φ ∨ φ | (∃x)φ | (∃X)φ

Thus the syntax does not reflect any information about B or the structural features of an MSC. These aspects will be dealt with in the semantics. Let M_{P,B} be the set of B-bounded MSCs over P. The formulas of our logic are interpreted over the members of M_{P,B}. Let M = (E, ≤, λ) be an MSC in M_{P,B} and I be an interpretation that assigns to each individual variable a member I(x) in E and to each set variable X a subset I(X) of E. Then M ⊧_{I} φ denotes that M satisfies φ under I. This notion is defined in the expected manner. For instance, M ⊧_{I} Q_{a}(x) if λ(I(x)) = a, M ⊧_{I} x ≤ y if I(x) ≤ I(y) etc. For convenience, we have used ≤ to denote both the predicate symbol in the logic and the corresponding causality relation in the model M.

As usual, φ is a sentence if there are no free occurrences of individual or set variables in φ. With each sentence φ we can associate an MSC language L_{φ} = {M ∈ M_{P,B} | M ⊧ φ}. We say that L ⊆ M_{P,B} is MSO(P, B)-definable if there exists a sentence φ such that L_{φ} = L. We wish to argue that L ⊆ M_{P,B} is MSO(P, B)-definable if and only if it is a B-bounded regular MSC language. It turns out the techniques used for proving a similar result in the theory of traces [8] can be suitably modified to derive our result.

Lemma 4.1. Let φ be a sentence in MSO(P, B). Then L_{φ} is a B-bounded regular MSC language.

Proof Sketch: The fact that L_{φ} is B-bounded follows from the semantics and hence we just need to establish regularity. Consider MSO(Σ), the monadic second-order theory of finite strings in Σ^{∗}. This logic has the same syntax as MSO(P, B) except that the ordering relation is interpreted over the positions of a structure in Σ^{∗}. Let L = ⋃{Lin(M) | M ∈ L_{φ}}. We exhibit a sentence φ̂ in MSO(Σ) such that L = {σ | σ ⊧ φ̂}. The main observation is that the bound B ensures that the family of channel-capacity functions K can be captured by a fixed number of sets, which is used both to assert channel-consistency and to express the partial order of MSCs in terms of the underlying linear order of positions. The required conclusion will then follow from Büchi’s theorem [5]. ⊓ ⊔

Lemma 4.2. Let L ⊆ M_{P,B} be a regular MSC language. Then L is MSO(P, B)- definable.

Proof Sketch: Let L = ⋃{Lin(M) | M ∈ L}. Then L is a regular (string) MSC language over Σ. Hence by Büchi’s theorem [5] there exists a sentence φ in MSO(Σ) such that L = {σ | σ ⊧ φ}. An important property of φ is that one linearization of an MSC satisfies φ if and only if all linearizations of the MSC satisfy φ. We then define the sentence φ̂ = ||φ|| in MSO(P, B) inductively such that the language of MSCs defined by φ̂ is precisely L. The key idea here is to define a canonical linearization of MSCs along the lines of [20] and show that the underlying linear order is expressible in MSO(P, B). We obtain a formula φ̂ that says “along the canonical linearization of an MSC, the sentence φ is satisfied”.

Since MSO(Σ) is decidable, it follows that MSO(P, B) is decidable as well. To conclude, we can summarize the main results of this paper as follows.

Theorem 4.3. Let L ⊆ Σ^{∗}, where Σ is the communication alphabet associated with a set P of processes. Then, the following are equivalent.

(i) L is a regular MSC language. (ii) L is a B-bounded regular MSC language, for some B ∈ ℕ. (iii) There exists a bounded message-passing automaton A such that L(A) = L. (iv) L is MSO(P, B)-definable, for some B ∈ ℕ.

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. Büchi, J. R.: On a decision method in restricted second order arithmetic. Z. Math. Logik Grundlag. Math 6 (1960) 66–92.

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

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

8. Ebinger, W., and Muscholl, A.: Logical definability on infinite traces. Theoretical Computer Science 154(1) (1996) 67–84.

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

10. Henriksen, J. G., Mukund, M., Narayan Kumar, K., and Thiagarajan, P. S.: Towards a theory of regular MSC languages, Report RS-99-52, BRICS, Department of Computer Science, University of Aarhus, Denmark (1999).

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

12. ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1997)

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

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

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

16. 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.

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

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

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

20. Thiagarajan, P. S., and Walukiewicz, I: An expressively complete linear time temporal logic for Mazurkiewicz traces. Proc. IEEE LICS’97 (1997) 183–194.

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

22. Vardi, M. Y., and Wolper, P.: An automata-theoretic approach to automatic program verification. In Proc. IEEE LICS’86 (1986) 332–344.

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