Automata, Languages and Programming, 27th International Colloquium Proceedings: Ugo Montanari, José D. P. Rolim, Emo Welzl(eds.) Springer Lecture Notes in Computer Science 1853 (2000), 675–686.

On Message Sequence Graphs and Finitely Generated Regular MSC Languages

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

1 BRICS, University of Aarhus, Denmark.

                   E-mail: gulmann@brics.dk

2 Chennai Mathematical Institute, Chennai, India.

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

Abstract. Message Sequence Charts (MSCs) are an attractive visual formalism widely used to capture system requirements during the early design stages in domains such as telecommunication software. A standard method to describe multiple communication scenarios is to use message sequence graphs (MSGs). A message sequence graph allows the protocol designer to write a finite specification which combines MSCs using basic operations such as branching choice, composition and iteration. The MSC languages described by MSGs are not necessarily regular in the sense of [HM+99]. We characterize here the class of regular MSC languages that are MSG-definable in terms of a notion called finitely generated MSC languages. We show that a regular MSC language is MSG-definable if and only if it is finitely generated. In fact we show that the subclass of “bounded” MSGs defined in [AY99] exactly capture the class of finitely generated regular MSC languages.

1 Introduction

Message sequence charts (MSCs) are an appealing visual formalism often used to capture system requirements in the early design stages. They are particularly suited for describing scenarios for distributed telecommunication software [RGG96,ITU97]. They also appear in the literature as timing sequence diagrams, message flow diagrams and object interaction diagrams and are used in a number of software engineering methodologies [BJR97,HG97,RGG96]. In its basic form, an MSC depicts a single partially-ordered execution of a distributed system which just describes the exchange of messages between the processes of the system. A collection of MSCs is used to capture the scenarios that a designer might want the system to exhibit (or avoid).

Message Sequence Graphs (MSGs) are a nice mechanism for defining collections of MSCs. An MSG is a finite directed graph with a designated initial vertex and terminal vertex in which each node is labelled by an MSC and the edges represent a natural concatenation operation on MSCs. The collection of MSCs defined by an MSG consists of all those MSCs obtained by tracing a path in the MSG from the initial vertex to the terminal vertex and concatenating the MSCs that are encountered along the path. It is easy to see that this way of defining a collection of MSCs extends smoothly to the case where there are multiple terminal nodes. Throughout what follows we shall assume this extended notion of an MSG (that is, with multiple terminal nodes). For ease of presentation, we shall also not deal with the so called hierarchical MSGs [AY99].

Intuitively, not every MSG-definable collection of MSCs can be realized as a finite-state device. To formalize this idea we have introduced a notion of a regular collection of MSCs and studied its basic properties [HM+99]. Our notion of regularity is independent of the notion of MSGs.

Our main goal in this paper is to pin down the regular MSC languages that can be defined using MSGs. We introduce the notion of an MSC language being finitely generated. From our results, which we detail below, it follows that a regular MSC language is MSG-definable if and only if it is finitely generated. In fact we establish the following results.

As already mentioned, not every MSG defines a regular MSC language. Alur and Yannakakis have identified a syntactic property called boundedness and shown that the set of all linearizations of the MSCs defined by a bounded MSG is a regular string language over an appropriate alphabet of events. It then follows easily that, in the present setting, every bounded MSG defines a finitely generated regular MSC language. One of our main results here is that the converse is also true, namely, every finitely generated regular MSC language can be defined by a bounded MSG. Since every MSG (bounded or otherwise) defines only a finitely generated MSC language, it follows that a regular MSC language is finitely generated if and only if it is MSG-definable and, in fact, if and only if it is bounded MSG-definable.

Since the class of regular MSC languages strictly includes the class of finitely generated regular MSC languages, one could ask when a regular MSC language is finitely generated. We show that this question is decidable. Finally, one can also ask whether a given MSG defines a regular MSC language (and is hence “equivalent” to a bounded MSG). We show that this decision problem is undecidable.

Turning briefly to related literature, a number of studies are available which are concerned with individual MSCs in terms of their semantics and properties [AHP96,LL95]. A variety of algorithms have been developed for MSGs in the literature—for instance, pattern matching [LP97,Mus99,MPS98], detection of process divergence and non-local choice [BL97], and confluence and race conditions [MP99]. A systematic account of the various model-checking problems associated with MSGs and their complexities can be found in [AY99]. Finally, many of our proof techniques make use of results from the theory of Mazurkiewicz traces [DR95].

In the next section we introduce MSCs and regular MSC languages. We then introduce message sequence graphs in Section 3. In Section 4 we define finitely generated MSC languages and provide an effective procedure to decide whether a regular MSC language is finitely generated. Our main result that the class of finitely generated regular MSC languages coincides with the class of bounded

[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}.

MSG-definable languages is then established. Finally, we sketch why the problem of determining if an MSG defines a regular MSC language is undecidable. Due to lack of space, we give here only the main technical constructions and sketches of proofs. All the details are available in [HM+99].

2 Regular MSC Languages

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. 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 communication 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 p-causality relation R_{p} = (E_{p} × E_{p})∩ ≤.

An MSC (over P) is a finite Σ-labelled poset M = (E, ≤, λ) which 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, shown in Figure 1.

Here P = {p, q, r}. For x ∈ P, the events in E_{x} are arranged along the line labelled (x) with earlier (relative to ≤) events appearing above the later 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.

We say that σ ∈ Σ^{∗} is proper if for every prefix τ of σ and every pair (p, q) of processes, |τ|_{p!q} ≥ |τ|_{q?p}. We say that σ is complete if σ is proper and |σ|_{p!q} = |σ|_{q?p} for every pair of processes (p, q). Clearly, any linearization of an MSC is a complete. Conversely, every complete sequence is the linearization of some MSC.

Henceforth, we 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.

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}. As shown in [HM+99], 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 (unique) channel-capacity function K_{s} : Ch → ℕ 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 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}. (Here and elsewhere Com = {(p!q, q?p) | p ≠ q}.)

In the minimal DFA A representing a regular MSC language, if s is a live state and a, b ∈ Σ then we say that a and b are independent at s if (a, b) ∈ Com implies K_{s}((p, q)) > 0 where K is the unique channel-capacity function associated with A and a = p!q and b = q?p.

We conclude this section by introducing the notion of B-bounded MSC languages. Let B ∈ ℕ be a natural number. We say that a word σ in Σ^{∗} is Bbounded 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. It is not difficult to show:

[figure: M_{1}; ⟹; M_{2}; (p); (q); (r); (s); •; •; •; •; •; •; •; •; M_{1}; M_{2}]

Fig. 2. An example MSG.

Proposition 2.1. Let L be a regular MSC language. There is a bound B ∈ ℕ such that L is B-bounded.

3 Message Sequence Graphs

An MSG allows a protocol designer to write in a standard way [ITU97], a finite specification which combines MSCs using operations such as branching choice, composition and iteration. Each node is labelled by an MSC and the edges represent the natural operation of MSC concatenation.

To bring out this concatenation operation, we let M_{1} = (E_{1}, ≤_{1}, λ_{1}) and M_{2} = (E_{2}, ≤_{2}, λ_{2}) be a pair for MSCs such that E_{1} and E_{2} are disjoint. For i ∈ {1, 2}, let R_{c}^{i} and {R_{p}^{i}}_{p∈P} denote the underlying communication and process causality relations in M_{i}. The (asynchronous) concatenation of M_{1} and M_{2}, denoted M_{1} ∘ M_{2}, is the MSC (E, ≤, λ) where E = E_{1} ∪ E_{2}, λ(e) = λ_{i}(e) if e ∈ E_{i}, i ∈ {1, 2}, and ≤ = (R_{P} ∪ R_{Ch})^{∗}, where R_{p} = R_{p}^{1} ∪ R_{p}^{2} ∪ {(e_{1}, e_{2}) | e_{1} ∈ E_{1}, e_{2} ∈ E_{2}, λ(e_{1}) ∈ Σ_{p}, λ(e_{2}) ∈ Σ_{p}} for p ∈ P, and R_{c} = R_{c}^{1} ∪ R_{c}^{2} for c ∈ Com.

A Message Sequence Graph (MSG) is a structure G = (Q, →, Q_{in}, F, Φ), where:

– Q is a finite and nonempty set of states.

– → ⊆ Q × Q.

– Q_{in} ⊆ Q is a set of initial states.

– F ⊆ Q is a set of final states.

– Φ : Q → M_{P} is a (state-)labelling function.

A path π through an MSG G is a sequence q_{0}→q_{1}→ ⋯ →q_{n} such that (q_{i−1}, q_{i}) ∈ → for i ∈ {1, 2, …, n}. The MSC generated by π is M(π) = M_{0} ∘ M_{1} ∘ M_{2} ∘ ⋯ ∘ M_{n}, where M_{i} = Φ(q_{i}). A path π = q_{0}→q_{1}→ ⋯ →q_{n} is a run if q_{0} ∈ Q_{in} and q_{n} ∈ F. The language of MSCs accepted by G is L(G) = {M(π) ∈ M_{P} | π is a run through G}.

An example of an MSG is depicted in Figure 2. It’s not hard to see that the MSC language L defined is not regular in the sense defined in Section 2. To see this, we note that L projected to {p!q, r!s} is not a regular string language.

[figure: (p); (r); (q); •; •; •; •; •; •; •; •; •; •; •; •; •; •]

Fig. 3. The atomic MSC M_{2} of the non-finitely-generated language L_{inf} .

4 Bounded MSGs and Finitely Generated MSC Languages

Let X_{1}, X_{2} ⊆ M_{P} be two sets of MSCs. As usual, X_{1} ∘ X_{2} denotes the pointwise concatenation of X_{1} and X_{2} given by {M | ∃M_{1} ∈ X_{1}, M_{2} ∈ X_{2} : M = M_{1} ∘M_{2}}. For X ⊆ M_{P}, we define X^{0} = {ε}, where ε denotes the empty MSC, and for i ≥ 0, X^{i+1} = X ∘ X^{i}. The asynchronous iteration of X is then defined by X^{⊛} = ⋃_{i≥0} X^{i}.

Let L ⊆ M_{P}. We say that L is finitely generated if there is a finite set of MSCs X ⊆ M_{P} such that L ⊆ X^{⊛}.

We first observe that not every regular MSC language is finitely generated. Let P = {p, q, r}. Consider the regular expression p!q σ^{∗} q?p, where σ is the sequence p!r r?p r!q q?r q!p p?q. This expression describes an infinite set of MSCs L_{inf} = {M_{i}}_{i=0}^{ω}. Figure 3 shows the MSC M_{2}. None of the MSCs in this language can be expressed as the concatenation of two or more non-trivial MSCs. Hence, this language is not finitely generated.

Our interest in finitely generated languages stems from the fact that MSGs can define only finitely generated MSC languages. We now wish to decide whether a regular MSC language is finitely generated. To do this we shall make use of the notion of atoms.

Let M, M′ ∈ M_{P} be nonempty MSCs. Then M′ is a component of M in case there exist M_{1}, M_{2} ∈ M such that M = M_{1}∘M′∘M_{2}. We say that M is an atom if the only component of M is M itself. Thus, an atom is a nonempty message sequence chart that cannot be decomposed into non-trivial subcomponents. For an MSC M we let Comp(M) denote the set {M′ | M′ is a component of M}. We let Atoms(M) denote the set {M′ | M′ is an atom and M′ is a component of M}.

For an MSC language L ⊆ M_{P}, Comp(L) = ⋃{Comp(M) | M ∈ L} and Atoms(L) = ⋃{Atoms(M) | M ∈ L}. It is clear that the question of deciding whether L is finitely generated is equivalent to checking whether Atoms(L) is finite.

Theorem 4.1. Let L be a regular MSC language. It is decidable whether L is finitely generated.

Proof Sketch: Let A = (S, Σ, s_{in}, δ, F) be the minimum DFA for L. From A, we construct a finite family of finite-state automata which together accept the linearizations of the MSCs in Atoms(L). It will then follow that L is finitely generated if and only if each of these automata accepts a finite language. We sketch the details below.

We know that for each live state s ∈ S, we can assign a capacity function K_{s} : Ch → ℕ which counts the number of messages present in each channel when the state s is reached. We say that s is a zero-capacity state if K_{s}(c) = 0 for each channel c. The following claims are easy to prove. Claim 1: Let M be an MSC in Comp(L) (in particular, in Atoms(L)) and w be a linearization of M. Then, there are zero-capacity live states s, s′ in A such

that s ⟶^{w} s′.

Claim 2: Let M be an MSC in Comp(L). M is an atom if and only if for each linearization w of M and each pair (s, s′) of zero-capacity live states in A, if s ⟶^{w} s′ then no intermediate state visited in this run has zero-capacity.

Let us say that two complete words w and w′ are equivalent, written w ∼ w′, if they are linearizations of the same MSC. Suppose s ⟶^{w} s′ and w ∼ w′ . Then it is easy to see that s ⟶^{w′} s′ as well.

With each pair (s, s′) of live zero-capacity states we associate a language L_{At}(s, s′). A word w belongs to L_{At}(s, s′) if and only if w is complete, s ⟶^{w} s′

and for each w′ ∼ w the run s ⟶^{w′} s′ has no zero-capacity intermediate states. From the two claims proved above, each of these languages consists of all the linearizations of some subset of Atoms(L) and the linearizations of each element of Atoms(L) is contained in some L_{At}(s, s′). Thus, it suffices to check for the finiteness of each of these languages.

Let L_{s,s′} be the language of strings accepted by A when we set the initial state to be s and the set of final states to be {s′}. Clearly L_{At}(s, s′) ⊆ L_{s,s′}. We now show how to construct an automaton for for L_{At}(s, s′).

We begin with A and prune the automaton as follows:

– Remove all incoming edges at s and all outgoing edges at s′.

– If t ∉ \{s, s′\} and K_{t} = \overline{0}, remove t and all its incoming and outgoing edges.

– Recursively remove all states that become unreachable as a result of the preceding operation.

Let B be the resulting automaton. B accepts any complete word w on which the run from s to s′ does not visit an intermediate zero-capacity state. Clearly, L_{At}(s, s′) ⊆ L(B). However, L(B) may also contain linearizations of non-atomic MSCs that happen to have no complete prefix. For all such words, we know from Claim 2 that there is at least one equivalent linearization on which the run passes through a zero-capacity state and which would hence be eliminated from L(B). Thus, L_{At}(s, s′) is the ∼-closed subset of L(B) and we need to prune B further to obtain the automaton for L_{At}(s, s′).

Recall that the original DFA A was structurally closed with respect to the independence relation on communication actions in the following sense. Suppose δ(s_{1}, a) = s_{2} and δ(s_{2}, b) = s_{3} with a, b independent at s_{1}. Then, there exists s′_{2} such that δ(s_{1}, b) = s′_{2} and δ(s′_{2}, a) = s_{3}.

To identify the closed subset of L(B), we look for local violations of this “diamond” property and carefully prune transitions. We first blow up the state space into triples of the form (s_{1}, s_{2}, s_{3}) such that there exist a and a′ with δ(s_{1}, a) = s_{2} and δ(s_{2}, a′) = s_{3}. Let S′ denote this set of triples. We obtain a nondeterministic transition relation δ′ = {((s_{1}, s_{2}, s_{3}), a, (t_{1}, t_{2}, t_{3})) | s_{2} = t_{1}, s_{3} = t_{2}, δ(s_{2}, a) = s_{3}}. Set S_{in} = {(s_{1}, s_{2}, s_{3}) ∈ S′ | s_{2} = s_{in}} and F′ = {(s_{1}, s_{f}, s_{2}) ∈ S′ | s_{f} ∈ F }. Let B′ = (S′, Σ, δ′, S_{in}, F′).

Consider any state s_{1} in B such that a and b are independent at s_{1}, δ(s_{1}, a) = s_{2}, δ(s_{2}, b) = s_{3} but there is no s′_{2} such that δ(s_{1}, b) = s′_{2} and δ(s′_{2}, a) = s_{3}. For each such s_{1}, we remove all transitions of the form ((t, s_{0}, s_{1}), a, (s_{0}, s_{1}, t′)) and ((t, s_{2}, s_{3}), b, (s_{2}, s_{3}, t′)) from B′. We then recursively remove all states which become unreachable after this pruning.

Eventually, we arrive at an automaton C such that L(C) = L_{At}(s, s′). Since C is a finite-state automaton, we can easily check whether L(C) is finite. This process is repeated for each pair of live zero-capacity states. □

Alur and Yannakakis [AY99] introduced the notion of boundedness for MSGs. They also showed that the set of all linearizations of the MSCs defined by a bounded MSG is a regular string language. In the present setting this boils down to boundedness of an MSG being a sufficient condition for its MSC language to be regular. To state their condition, we first have to define the notion of connectedness.

Let M = (E, ≤, λ) be an MSC. We let CG_{M}, the communication graph of M, be the directed graph (P, ↦) defined as follows: (p, q) ∈ ↦ if and only if there exists an e ∈ E with λ(e) = p!q. M is connected if CG_{M} consists of one non-trivial strongly connected component and isolated vertices. For an MSC language L ⊆ M_{P} we say that L is connected in case every M ∈ L is connected.

Let G = (Q, →, Q_{in}, F, Φ) be an MSG. A loop in G is a sequence of edges that starts and ends at the same node. We say that G is bounded if for every loop π = q→q_{1}→ ⋯ →q, the MSC M(π) is connected. An MSC language L is a bounded MSG-language if there exists a bounded MSG G with L = L(G).

It is easy to check whether a given MSG is bounded. Clearly, the MSG of Figure 2 is not bounded. One of the main results concerning bounded MSGs shown in [AY99] at once implies:

Lemma 4.2. Every bounded MSG-language is a regular MSC language.

Our main interest in this section is to prove the converse of Lemma 4.2.

Lemma 4.3. Let L be a finitely generated regular MSC language. Then, L is a bounded MSG-language.

Proof Sketch: Suppose L is a regular MSC language accepted by the minimal DFA A = (S, Σ, s_{in}, δ, F). Let Atoms(L) = {a_{1}, a_{2}, …, a_{m}}. For each atom a_{i}, fix a linearization u_{i} ∈ Lin(a_{i}). Define an auxiliary DFA B = (S\overline{0}, Atoms(L), s_{in}, δ̂, F̂) as follows:

– S\overline{0} is the set of states of A which have zero-capacity functions.

– F̂ = F

– δ̂(s, a_{i}) = s′ iff δ(s, u_{i}) = s′ in A. (Note that u, u′ ∈ Lin(a_{i}) implies δ(s, u) = δ(s, u′), so s′ is fixed independent of the choice of u_{i} ∈ Lin(a_{i}).)

Thus, B accepts the (regular) language of atoms corresponding to L(A). We can define a natural independence relation I_{A} on atoms as follows: atoms a_{i} and a_{j} are independent if and only if the set of active processes in a_{i} is disjoint from the set of active processes in a_{j}. (The process p is active in the MSC (E, ≤, λ) if E_{p} is non-empty.)

It follows that L(B) is a regular Mazurkiewicz trace language over the trace alphabet (Atoms(L), I_{A}). As usual, for w ∈ Atoms(L)^{∗}, we let [w] denote the equivalence class of w with respect to I_{A}.

We now fix a strict linear order ≺ on Atoms(L). This induces a (lexicographic) total order on words over Atoms(L). Let Lex ⊆ Atoms(L)^{∗} be given by: w ∈ Lex iff w is the lexicographically least element in [w].

For a trace language L over (Atoms(L), I_{A}), let lex(L) denote the set L∩Lex.

Remark 4.4 ([DR95], Sect. 6.3.1)

(i) If L is a regular trace language over (Atoms(L), I_{A}), then lex(L) is a regular language over Atoms(L). Moreover, L = {[w] | w ∈ lex(L)).

(ii) If w_{1}ww_{2} ∈ Lex, then w ∈ Lex. (iii) If w is not a connected^{1} trace, then ww ∉ Lex.

From (i) we know that lex(L(B)) is a regular language over Atoms(L). Let C = (S′, Atoms(L), s′_{in}, δ′, F′) be the DFA over Atoms(L) obtained by eliminating the (unique) dead state, if any, from the minimal DFA for lex(L(B)). It is easy to see that an MSC M belongs to L if and only if it can be decomposed into a sequence of atoms accepted by C. Using this fact, we can derive an MSG G from C such that L(G) = L. We define G = (Q, →, Q_{in}, F, Φ) as follows:

– Q = S′ × (Atoms(L) ∪ {ε}).

– Q_{in} = {(s′_{in}, ε)}.

1 A trace is said to be connected if, when viewed as a labelled partial order, its Hasse diagram consists of a single connected component. See [DR95] for a more formal definition.

– (s, b)→(s′, b′) iff δ′(s, b′) = s′.

– F′ = F × Atoms(L).

– Φ(s, b) = b.

Clearly G is an MSG and the MSC language that it defines is L. We need to show that G is bounded. To this end, let π = (s, b)→(s_{1}, b_{1})→ ⋯ →(s_{n}, b_{n})→(s, b) be a loop in G. We need to establish that the MSC M(π) = b_{1} ∘⋯∘b_{n} ∘b defined by this loop is connected. Let w = b_{1}b_{2} … b_{n}b.

Consider the corresponding loop s ⟶^{b_{1}} s_{1} ⟶^{b_{2}} ⋯ ⟶^{b_{n}} s_{n} ⟶^{b} s in C. Since every state in C is live, there must be words w_{1}, w_{2} over Atoms(L) such that w_{1}w^{k}w_{2} ∈ lex(L(B)) for every k ≥ 0.

From (ii) of Remark 4.4, w^{k} ∈ Lex. This means, by (iii) of Remark 4.4, that w describes a connected trace over (Atoms(L), I_{A}). From this, it is not difficult to see that the underlying undirected graph of the communication graph CG_{M(π)} = (P, ↦) consists of a single connected component C ⊆ P and isolated processes. We have to argue that the component C is, in fact, strongly connected. We show that if C is not strongly connected, then the regular MSC language L is not B-bounded for any B ∈ ℕ, thus contradicting Proposition 2.1.

Suppose that the underlying graph of C is connected but C not strongly connected. Then, there exist two processes p, q ∈ C such that p ↦ q, but there is no path from q back to p in CG_{M(π)}. For k ≥ 0, let M(π)^{k} = (E, ≤, λ) be the MSC corresponding to the k-fold iteration \underbrace{M(π) ∘ M(π) ∘ ⋯ ∘ M(π)}_{k times}. Since

p ↦ q in CG_{M(π)}, it follows that there are events labelled p!q and q?p in M(π). Moreover, since there is no path from q back to p in CG_{M(π)}, we can conclude that in M(π)^{k}, for each event e with λ(e) = p!q, there is no event labelled q?p in ↓e. This means that M(π)^{k} admits a linearization v′_{k} with a prefix τ′_{k} which includes all the events labelled p!q and excludes all the events labelled q?p, so that |τ|_{p!q} − |τ|_{q?p} ≥ k.

By Proposition 2.1, since L is a regular MSC language, there is be a bound B ∈ ℕ such that every word in L is B-bounded—that is, for each v ∈ L, for each prefix τ of v and for each channel (p, q) ∈ Ch, |τ|_{p!q} − |τ|_{q?p} ≤ B. Recall that w_{1}w^{k}w_{2} ∈ lex(L(B)) for every k ≥ 0. Fix linearizations v_{1} and v_{2} of the atom sequences w_{1} and w_{2}, respectively. Then, for every k ≥ 0, u_{k} = v_{1}v′_{k}v_{2} ∈ L where v′_{k} is the linearization of M(π)^{k} defined earlier. Setting k to be B+1, we find that u_{k} admits a prefix τ_{k} = v_{1}τ′_{k} such that |τ_{k}|_{p!q} − |τ_{k}|_{q?p} ≥ B+1, which contradicts the B-boundedness of L.

Hence, it must be the case that C is a strongly connected component, which establishes that the MSG G we have constructed is bounded. □

Putting together Lemmas 4.2 and 4.3, we obtain the following characterization of MSG-definable regular MSC languages.

Theorem 4.5. Let L be a regular MSC language. Then the following statements are equivalent:

(i) L is finitely generated.

[figure: M; ⟹; M′; (p); (q); (r); (s); •; •; •; •; •; •; •; •; M; M′]

Fig. 4. An non-bounded MSG whose language is regular.

(ii) L is a bounded MSG-language. (iii) L is MSG-definable.

It is easy to see that boundedness is not a necessary condition for regularity. Consider the MSG in Figure 4, which is not bounded. It accepts the regular MSC language M ∘ (M + M′)^{⊛}.

Thus, it would be useful to provide a characterization of the class of MSGs representing regular MSC languages. Unfortunately, the following result shows that there is no (recursive) characterization of this class.

Theorem 4.6. The problem of deciding whether a given MSG represents a regular MSC language is undecidable.

Proof Sketch: It is known that the problem of determining whether the traceclosure of a regular language L ⊆ A^{∗} with respect to a trace alphabet (A, I) is also regular is undecidable [Sak92]. We reduce this problem to the problem of checking whether the MSC language defined by an MSG is regular.

Let (A, I) be a trace alphabet. We fix a set of processes P and the associated communication alphabet Σ and encode each letter a by an MSC M_{a} over P such that the communication graph CG_{M_{a}} is strongly connected. Moreover, if (a, b) ∈ I, then the sets of active processes of M_{a} and M_{b} are disjoint. The encoding ensures that we can construct a finite-state automaton to parse any word over Σ and determine whether it arises as the linearization of an MSC of the form M_{a_{1}} ∘ M_{a_{2}} ∘ ⋯ ∘ M_{a_{k}}. If so, the parser can uniquely reconstruct the corresponding word a_{1}a_{2} … a_{k} over A.

Let A be the minimal DFA corresponding to a regular language L over A. We construct an MSG G from A as described in the proof of Lemma 4.3. Given the properties of our encoding, we can then establish that the MSC language L(G) is regular if and only if the trace-closure of L is regular, thus completing the reduction. □

References

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

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

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

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

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

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

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

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

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

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

[Mus99] Muscholl, A.: Matching specifications for message sequence charts. Proc. FOSSACS’99, LNCS 1578, Springer-Verlag (1999) 273–287.

[MP99] Muscholl, A., and Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. Proc. MFCS’99, LNCS 1672, Springer-Verlag (1999) 81–91.

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

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

[Sak92] Sakarovitch, J.: The “last” decision problem for rational trace languages. Proc. LATIN’92, LNCS 583, Springer-Verlag (1992) 460–473.