BRICS RS-99-52 Henriksen et al.: Towards a Theory of Regular MSC Languages BRICS

Basic Research in Computer Science

Towards a Theory of Regular MSC Languages

Jesper G. Henriksen Madhavan Mukund K. Narayan Kumar P. S. Thiagarajan

BRICS Report Series RS-99-52

ISSN 0909-0878 December 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Jesper G. Henriksen & Madhavan Mukund &

K. Narayan Kumar & P. S. Thiagarajan. BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/99/52/

Towards a Theory of Regular MSC Languages

Jesper G. Henriksen

BRICS^{∗}, Dept. of Comp. Sci., University of Aarhus, Denmark

            Email: gulmann@brics.dk

Madhavan Mukund, K. Narayan Kumar, P. S. Thiagarajan Chennai Mathematical Institute, Chennai, India

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

December, 1999

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. It is fruitful to have mechanisms for specifying and reasoning about collections of MSCs so that errors can be detected even at the requirements level. We propose, accordingly, a notion of regularity for collections of MSCs and explore its basic properties. In particular, we provide an automata-theoretic characterization of regular MSC languages in terms of finite-state distributed automata called bounded message-passing automata. These automata consist of a set of sequential processes that communicate with each other by sending and receiving messages over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs.

A commonly used technique to generate a collection of MSCs is to use a Message Sequence Graph (MSG). We show that the class of languages arising from the so-called locally synchronized MSGs constitute a proper subclass of the languages which are regular in our sense. In fact, we characterize the locally synchronized MSG languages as the subclass of regular MSC languages that are finitely generated.

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

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 [11, 20]. 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 [4, 10, 20]. In its basic form, an MSC depicts the exchange of messages between the processes of a distributed system along a single partially-ordered 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 the early stages of design. One question that naturally arises in this context is the following: What constitutes a reasonable collection of MSCs on which one can hope to do formal analysis? A related issue is how one should go about representing such collections.

A standard way to generate a collection of MSCs is to use a Hierarchical (or High-level) Message Sequence Chart (HMSC) [14]. 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.

Because of the restrictions on the labelling of HMSCs, we can derive an equivalent Message Sequence Graph (MSG) by flattening out the hierarchical labelling in an HMSC. In other words, an MSG is a graph where each node is labelled by a simple MSC. Like an HMSC, 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, 19].

In [2], Alur and Yannakakis study the restricted class of locally synchronized (or bounded) MSGs. They show that the collection of MSCs generated by a locally synchronized MSG can be represented as a regular string language. As a result, the behaviours captured by a locally synchronized MSG can be, in principle, realized as a finite-state automaton. It is easy to see that not every MSG-definable collection of MSCs is realizable in this sense.

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 and explore its basic properties. 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 is that locally synchronized MSGs define a strict subclass of regular collections of MSCs. A final consequence is that our notion leads to a state-based representation that is one step closer to an implementation than the description of system requirements using MSGs. Stated differently, our work also addresses the issue, raised in [7], of converting inter-process descriptions at the level of requirements, as specified by MSCs, into intra-process executable specifications in terms of a reasonable model of computation.

Yet another motivation for focussing on regularity is that the classical notion of a regular collection of objects has turned out to be very fruitful in a variety of settings including finite (and infinite) strings, trees and restricted partial orders known as Mazurkiewicz traces [8, 23, 24]. 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 which usually induces temporal logics using which one can reason about such collections [23]. 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 [25]. 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 that the set P gives rise to. An MSC in M can be viewed as a labelled partial order in which the labels come from a finite alphabet Σ which is canonically fixed by P. Our proposal for L ⊆ M to be regular is that the collection of all linearizations of all members of L should together constitute a regular subset of Σ^{∗}. A crucial point is that, unlike the classical setting of strings (or trees or Mazurkiewicz traces), the universe M is itself not regular according to our definition. 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 which have yet to be received by q. A language of MSCs 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. The 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 which are concerned with individual MSCs in terms of their semantics and properties [1, 12]. 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 [13, 17, 19] 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 general, the language defined by an MSG is not regular. Conversely, we exhibit a regular MSC language which cannot be represented by an MSG, let alone a locally synchronized MSG. We then characterize the class of regular MSC languages which can be defined by message sequence graphs. We first observe that the MSC languages defined by MSGs are finitely generated. It turns out that there are regular MSC languages which consist of an infinite number of “atomic” MSCs and are hence not finitely generated.

We give a decision procedure to determine when a regular MSC language is finitely generated. Following this, we establish that the class of finitely generated regular MSC languages coincides with the class of languages defined by locally synchronized MSGs. In one direction, this characterization hinges crucially on elements of Mazurkiewicz trace theory [8, 26].

In this paper we confine our attention to finite MSCs. We feel however that our results will serve as a good 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 structured 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 [8]. 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.

We define Message Sequence Graphs in Section 5. We survey the existing body of theory for this class of labelled graphs and bring out the notion of locally synchronized MSGs. In Section 6 we define finitely generated languages and provide an effective procedure to decide whether a regular MSC language is finitely generated. Following this, we establish our characterization result for locally synchronized MSG languages.

2 Regular MSC Languages

Let P = {p, q, r, …} be a finite set of processes (or agents) which communicate with each other through messages via reliable FIFO channels. For each p ∈ P we define Σ_{p} =^{def} {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 =^{def} {e′ | e′ ≤ e}. For p ∈ P and a ∈ Σ, we set E_{p} =^{def} {e | λ(e) ∈ Σ_{p}} and E_{a} =^{def} {e | λ(e) = a}, respectively. For each c ∈ Ch, we define the relation R_{c} =^{def} {(e, e′) | λ(e) = p!q, λ(e′) = q?p and |↓e ∩ E_{p!q}| = |↓e′ ∩ E_{q?p}|}. Since messages are assumed to be read in FIFO fashion, e R_{(p,q)} e′ implies that the message read by q at the receive event e′ is the one sent by p at the send event e. Finally, for each p ∈ P, we define the relation R_{p} =^{def} (E_{p} × E_{p}) ∩ ≤.

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

(1) Each R_{p} is a linear order.

(2) If p ≠ q then |E_{p!q}| = |E_{q?p}|.

(3) ≤ = (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

1Our definition captures the standard partial-order semantics associated with MSCs in, for instance, [1, 20].

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

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

the relation R_{Ch} are displayed as horizontal or downward-sloping directed edges. We illustrate the idea with an example, depicted 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.

Henceforth, we will identify an MSC with its isomorphism class. We let M(P) be the set of MSCs over P. An MSC language is a subset L ⊆ M(P). From now on, whenever there is no confusion we omit P and denote M(P) by M and Σ_{P} by Σ.

We define regular MSC languages in terms of their linearizations. For an MSC M = (E, ≤, λ), we let lin(M) =^{def} {λ(π) | π is a linearization of (E, ≤)}. By abuse of notation, we have used λ to also denote the natural extension of λ to E^{∗}. For an MSC language L ⊆ M, we set lin(L) = ⋃{lin(M) | M ∈ L}. In this sense, the string p!q r!q q?p q?r r!p p?r is one linearization of the MSC in Figure 1.

In the literature (e.g. [1, 18, 19]) 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 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. This is called the causal order of the MSC (as opposed to the visual order). Our results go through with suitable modifications even in the presence of this more generous notion of linearization.

To directly characterize the subsets of Σ^{∗} that correspond to MSC languages, we proceed as follows. Let Com = {(p!q, q?p) | (p, q) ∈ Ch}. 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, lin(M) is a subset of Σ^{∘} and is in fact a ∼-equivalence class over Σ^{∘}.

We define L ⊆ Σ^{∗} to be a string MSC language if there exists an MSC language L ⊆ M(P) such that L = ⋃{lin(M) | M ∈ L}. It is easy to see that L ⊆ Σ^{∗} is a string MSC language iff L is a subset of Σ^{∗} such that every string in L is complete and L is ∼-closed (that is, for each σ ∈ L, if σ ∈ L and σ ∼ σ′ then σ′ ∈ L).

Just as a trace can be identified with its linearizations in Mazurkiewicz trace theory [8], we can identify each MSC with the set of its linearizations. To formalize this, we construct representation maps sm : Σ^{∘}/∼ → M and ms : M → Σ^{∘}/∼ and sketch briefly that these maps are “inverses” of each other.

We first define sm : Σ^{∘} → M. Let σ ∈ Σ^{∘}. Then sm(σ) = (E, ≤, λ), where

• E = {τa | τa ∈ prf(σ)}, where prf(σ) is the set of prefixes of σ. Thus E = prf(σ) − {ε}.

• ≤ = (R_{P} ∪ R_{Ch})^{∗} where R_{P} = ⋃_{p∈P} R_{p}, R_{Ch} = ⋃_{c∈Ch} R_{c}. The constituent relations are defined as follows. For each p ∈ P, (τa, τ′b) ∈ R_{p} iff a, b ∈ Σ_{p} and τa ∈ prf(τ′b). Moreover, for each c ∈ Ch, (τa, τ′b) ∈ R_{c} iff a = p!q and b = q?p for some p, q ∈ P and furthermore |τa|_{a} = |τ′b|_{b}.

• For τa ∈ E, λ(τa) = a.

One can show that σ ∼ σ′ implies sm(σ) = sm(σ′). We can thus extend sm to a map sm′ : Σ^{∘}/∼ → M given by sm′([σ]_{∼}) = sm(σ). Henceforth, we shall write sm to denote both sm and sm′.

Conversely, we define the map ms : M → Σ^{∘}/∼ as: ms(M) = lin(M) and it is not hard to show that ms is well-defined. We can also show that for every τ ∈ Σ^{∘}, ms(sm(σ)) = [σ]_{∼} and for every M ∈ M, sm(ms(M)) = M. This justifies our claim that Σ^{∘}/∼ and M are two equivalent ways of representing the same class of objects. Hence, abusing terminology, we will write “MSC language” to mean “string MSC language”. From the context, it should be clear whether we are working with MSCs from M or complete strings over Σ^{∗}. As a rule of thumb, we will use L to denote the former and L to denote the latter, but this distinction is not always firm.

We can now finally define our notion of a regular collection of MSCs. We will say that L ⊆ M is a regular MSC language if the corresponding string MSC language is a regular subset of Σ^{∗}. Thus, a language L of MSCs is regular in case lin(L) is regular in the classical sense. Note that, unlike the settings of strings (or trees or Mazurkiewicz traces), the universe M is itself not regular according to our definition. This fact has a strong bearing on the automata-theoretic and logical formulations in our work, as will become apparent later.

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 iff we can associate with each live state s ∈ S, a channel-capacity function K_{s} : Ch → ℕ which satisfies the following conditions.

(1) If s ∈ {s_{in}} ∪ F then K_{s}(c) = 0 for every c ∈ Ch.

(2) 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).

(3) 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).

(4) 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}.

Item (4) 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 (4) 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).

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} =^{def} 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. In particular, we have:

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

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

In what follows we assume the terminology and notation developed in the previous section. Recall that the set of processes P determines the communication alphabet Σ and that for p ∈ P, Σ_{p} denotes the actions which process p participates in.

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

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

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

Let σ ∈ Σ^{∗}. A run of A over σ is a map ρ : prf(σ) → Conf_{A} such that ρ(ε) = (s_{in}, χ_{ε}) and for each τa ∈ prf(σ), ρ(τ) ⟹^{a} ρ(τa). The run ρ is accepting if ρ(σ) is a final configuration. We define L(A) =^{def} {σ | A has an accepting run over σ}. It is easy to see that every member of L(A) is complete and L(A) is ∼-closed in the sense that if σ ∈ L(A) and σ ∼ σ′ then σ′ ∈ 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) can grow arbitrarily long. Hence, the set of

[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]

Figure 2: A 3-bounded message-passing automaton.

reachable configurations of this system is 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 message-passing automaton A and a bound B ∈ ℕ, one can decide whether or not A is B-bounded. Figure 2 depicts an example of a 3-bounded message-passing automaton with two components, p and q. The initial state is (s_{1}, t_{1}) and there is only one final state, (s_{2}, t_{3}). (the message alphabet is a singleton and hence omitted). The automaton accepts the infinite set of MSCs L = {M_{i}}_{i=0}^{ω}, where M_{i} is displayed in Figure 3 for i = 2.

This automaton accepts an infinite set of MSCs, none of which can be expressed as the concatenation of two or more non-trivial MSCs. As a result, this MSC language cannot be represented using MSGs, as formulated in [2].

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

This result follows from the definitions and it constitutes the easy half of the characterization we wish to obtain. The second half of our characterization says that every B-bounded regular MSC language can be recognized by a B-bounded message-passing automaton. This is much harder to establish.

Let L ⊆ Σ^{∗} be a regular MSC language. As observed at the end of Section 2, the minimum DFA for L yields a bound B such that L is Bbounded. We first view L as a regular Mazurkiewicz trace language and apply Zielonka’s theorem [26] to obtain a so-called asynchronous automaton Z for L. We then convert Z into the desired B-bounded message-passing automaton A with the property L(A) = L.

[figure: (p); (q); •; p!q; •; q!p; i; •; p!q; •; q?p; i; •; p?q; •; q!p; •; p!q; •; q?p; •; p?q; •; q?p; { ; |; } ; |]

Figure 3: The M_{i}’s accepted by the automaton in Figure 2.

Let {Σ_{c}}_{c∈Ch} be given by Σ_{c} =^{def} {p!q, q?p} for c = (p, q). We let X = P ∪Ch. For a ∈ Σ, we define the locations of a as loc(a) =^{def} {x ∈ X | a ∈ Σ_{x}}. The distributed alphabet {Σ_{x}}_{x∈X} induces the Mazurkiewicz trace alphabet (Σ, I_{X}), where I_{X} = {(a, b) | a, b ∈ Σ, loc(a) ∩ loc(b) = ∅} is an irreflexive and symmetric independence relation. We can then define ≈ ⊆ Σ^{∗} × Σ^{∗} to be the least equivalence relation such that if σ = σ_{1}abσ_{2}, σ′ = σ_{1}baσ_{2} and (a, b) ∈ I_{X} then σ ≈ σ′. We say that L ⊆ Σ^{∗} is a regular (Mazurkiewicz) trace language over (Σ, I_{X}) if L is a regular subset of Σ^{∗} and L is ≈-closed— that is, for each σ ∈ Σ^{∗}, if σ ∈ L and σ ≈ σ′ then σ′ ∈ L.

Let L ⊆ Σ^{∗} be a regular MSC language. It is not difficult to verify that L is a regular trace language over (Σ, I_{X})—the independence relation I_{X} corresponds to the static (context-insensitive) kernel of the context-sensitive independence relation I defined in Section 2.

In order to apply Zielonka’s theorem we need to first introduce asynchronous automata. An asynchronous automaton over the distributed alphabet {Σ_{x}}_{x∈X} is a structure Z = ({S_{x}}_{x∈X}, {⟶_{a}}_{a∈Σ}, s_{in}, F) where each S_{x} is a finite set of local states of the component x. Let S = ∏_{x∈X} S_{x} denote the set of global states of Z. Then s_{in} ∈ S is the global initial state and F ⊆ S is the set of global final states. Let a = p!q. Then ⟶_{a} ⊆ (S_{p}×S_{(p,q)})×(S_{p}×S_{(p,q)}). The pair ((s_{1}, s′_{1}), (s_{2}, s′_{2})) ∈ ⟶_{a} denotes the fact that the p-component in state s_{1}, and the channel (p, q)-component in state s′_{1} can together execute p!q and move to the joint state (s_{2}, s′_{2}). Similarly, for a receive action b = q?p, ⟶_{b} ⊆ (S_{(p,q)} ×S_{q})×(S_{(p,q)} ×S_{q}) defines joint moves of the channel (p, q) and process q when q receives messages from p. To define the global transition relation ⟶ ⊆ S × Σ × S, we let s_{x} denote the xth component of the global state s. Suppose s, s′ ∈ S, a = p!q and c = (p, q). Then (s, a, s′) ∈ ⟶ if ((s_{p}, s_{c}), (s′_{p}, s′_{c})) ∈ ⟶_{a} and s_{x} = s′_{x} for every x ∈ X \ {p, c}. Transitions of the form (s, b, s′) with b = q?p are defined in a similar fashion. The notions of runs and accepting runs are formulated in the obvious way. We let L(Z) be the subset of Σ^{∗} accepted by Z.

Zielonka’s theorem [26] asserts that from a regular trace language L, we can construct a deterministic asynchronous automaton Z such that L(Z) = L. We have already observed that a regular MSC language L ⊆ Σ^{∗} is a regular trace language over (Σ, I_{X}). It follows that from a regular MSC language L ⊆ Σ^{∗} we can effectively construct a deterministic asynchronous automaton Z over the distributed alphabet {Σ_{x}}_{x∈X} such that L = L(Z).

Fix a B-bounded regular MSC language L and let Z = ({S_{x}}_{x∈X}, {⟶_{a}}_{a∈Σ}, s_{in}, F) be a deterministic asynchronous automaton such that L = L(Z). We claim that we can effectively transform Z into a B-bounded message-passing automaton A over Σ such that L(A) = L.

This transformation is complicated by the following fact. In Z, for each pair p, q ∈ P, the actions p!q and q?p are performed by the channel component (p, q) and are hence dependent on each other in all contexts. As a result, the transition relations ⟶_{p!q} and ⟶_{q?p} do not reflect the contextsensitive independence of the actions p!q and q?p, even though the language accepted by Z is a regular MSC language and is hence closed with respect to the context-sensitive independence relation I on Σ. This means that for two inputs σ and σ′ such that σ ∼ σ′, Z will, in general, admit drastically different runs on σ and σ′. On the other hand, the structure of message-passing automata is such that the moves of any message-passing automaton over Σ can be reordered with respect to the independence relation I. This implies that the simulation of Z by A should not depend on the order in which independent occurrences of actions of the form p!q and q?p are linearized in a given input.

To get around this, we simulate the component (p, q) of Z in A using the components p and q such that for each input σ, p and q keep track the moves of (p, q) along a canonical reordering σ′ ∼ σ. This simulation is coordinated using the messages sent from p to q.

The key technical input for this simulation comes from [15] where it is shown how each process p in a message-passing system can use a bounded time-stamping protocol to keep track of the latest information about every other process in the system. The protocol does not add extra messages to the system. This protocol also allows each process p to locally keep track of the messages sent on each channel (p, q) for which p has not received an “acknowledgment”, directly or indirectly, from q. This list of “unacknowledged” messages yields an upper bound for the number of messages currently resident in each outgoing channel from p. (A more detailed description of the time-stamping protocol is presented in Appendix A.)

The desired automaton A will be of the form ({A′_{p}}_{p∈P}, Δ, s′_{in}, F′), where A′_{p} = (S′_{p}, ⇝_{p}). For each process p, each state in S′_{p} is of the form ⟨s_{p}, s̄_{p}, τ_{p}⟩ where s_{p} records a local state of p in Z, s̄_{p} records a local state s_{c} in Z for each incoming channel c = (q, p) at p, and τ is a time-stamp generated by protocol of [15].

The message alphabet is Δ = Ev × T where Ev = ⋃_{a∈Σ} ⟶_{a} and T is the set of time-stamps used by the protocol of [15]. (Recall that ⟶_{a} is the set of a-transitions specified in Z for each a.) The initial state and the final states are defined in the expected manner using the initial and final states of Z.

The transitions of A are arranged as follows. The tuple (⟨s_{p}, \overline{s}_{p}, τ_{p}⟩, p!q, (e, τ), ⟨s′_{p}, \overline{s′}_{p}, τ′_{p}⟩) belongs to the p-local transition relation ⇝_{p} provided the following hold. First, τ = τ′_{p} and τ′_{p} is the time-stamp generated from τ_{p} by the protocol of [15]. Let c = (p, q). The e-component of the message is a move ((s_{p}, s_{c}), (s′_{p}, s′_{c})) ∈ ⟶_{p!q} for some s_{c}, s′_{c} ∈ S_{c}. Finally, according to τ_{p} there are at most B−1 “unacknowledged” messages in the channel c, indicating that sending this message will not violate the B-boundedness of A.

The tuple (⟨s_{p}, \overline{s}_{p}, τ_{p}⟩, p?q, (e, τ′), ⟨s′_{p}, \overline{s′}_{p}, τ′_{p}⟩) belongs to ⇝_{p} provided the following hold. From the time-stamp τ′ on the incoming message, p collects the latest information from each process r ∈ P about new r!p events that have been sent by r but not yet received by p. For each such event, the timestamp τ′ also records the move ((s_{r}, s_{c}), (s′_{r}, s′_{c})) guessed by r when the event occurred. Process p updates the (r, p)-component of \overline{s}_{p} by applying this move guessed by r. If this guess is not permitted by the current state of (r, p) as recorded in \overline{s}_{p}, p gets stuck. If there is more than one such r!p event then p processes each of them in the order in which they were sent. Let the resulting states corresponding to the channel components {(r, p) | r ∈ P} be ŝ_{p}. Let c = (q, p). Now, p simulates the unique p?q move (ŝ_{c}, s_{p}) ⟹^{p?q} (\overline{s}′_{c}, s′_{p}) of Z (recall that Z is deterministic). With this, p has updated the components s_{p} and s̄_{p} of its state to s′_{p} and \overline{s}′_{p}. Finally, it uses the time-stamps τ_{p} and τ′ to generate a new time-stamp τ′_{p} as specified by the protocol of [15].

It is easy to show that L(Z) ⊆ L(A). To show the converse, let σ ∈ L(A) and let ρ be an accepting run of A over σ. From the way A simulates Z, we can show that there is a canonical reordering σ′ ∼ σ such that there is an accepting run ρ′ of A over σ′ where ρ′ is just a reordered version of ρ. The word σ′ has the property that each message is received as soon as possible, subject to causality constraints. For instance, if σ = p!q p!q q?p q?p then σ′ = p!q q?p p!q q?p, and if σ = p!q p!q p!r r?p r!q q?r q?p q?p, then σ′ = σ. In the second example, the messages via r ensure that p will have sent both messages to q before q receives the first one. From ρ′ it is easy to extract an accepting run of Z over σ′. The language accepted by Z is ∼-closed because L is ∼-closed. Consequently, σ is also accepted by Z.

Filling in the details of this proof skeleton leads to the following result.

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.

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

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

The automaton A constructed above is nondeterministic because each send-action requires guessing a move of Z. In [16], a direct construction is presented to generate a deterministic bounded message-passing automaton for each regular MSC language.

4 A Logical Characterization

We formulate a monadic second-order logic which characterizes regular Bbounded 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 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 | ¬φ | φ_{1} ∨ φ_{2} | (∃x)φ | (∃X)φ.

Thus the syntax does not reflect any information about the bound 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 which 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_{φ} =^{def} {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. For convenience, we often use “definable” to mean “MSO(P, B)-definable”. We wish to argue that L ⊆ M(P, B) is definable iff it is a B-bounded regular MSC language. It turns out the techniques used for proving a similar result in the theory of traces [9] 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, to avoid confusion, we will use the predicate symbol ⪯ instead of ≤ and interpret ⪯ as the usual ordering relation over the positions of a structure in Σ^{∗}. Let L = ⋃{lin(M) | M ∈ L_{φ}}. We exhibit a sentence φ̂ in MSO(Σ) such that L = {σ | σ ⊧ φ̂}. The required conclusion will then follow from Büchi’s theorem [5]. Let {K_{0}, K_{1}, …, K_{n}} be the set {K ∈ ℕ^{Ch} | ∀c ∈ Ch. K(c) ≤ B}. Without loss of generality, assume that K_{0}(c) = 0 for every c ∈ Ch. For K ∈ ℕ^{Ch} and c ∈ Ch, let K^{+c} to be the member of ℕ^{Ch} where K^{+c}(c) = K(c) + 1 and K^{+c}(d) = K(d) for all d ≠ c. Similarly, for K ∈ ℕ^{Ch} and c ∈ Ch such that K(c) > 0, K^{−c} is given by K^{−c}(c) = K(c) − 1 and K^{−c}(d) = K(d) for all d ≠ c.

The required sentence φ̂ will be of the form:

(∃X_{K_{0}})(∃X_{K_{1}}) ⋯ (∃X_{K_{n}})(COMP ∧ ||φ||)

where COMP and ||φ|| are defined as follows. We provide these definitions in textual form to enhance readability. They can be easily converted to formulas in MSO(Σ).

First we define COMP to be the conjunction of the following formulas.

(1) Every position x belongs to exactly one of the sets in {X_{K_{0}}, …, X_{K_{n}}}.

(2) If x is the first position then x ∈ X_{K_{0}}.

(3) If x is the last position then Q_{q?p}(x) for some c = (p, q). Moreover x belongs to X_{K_{m}} such that K_{m}(c) = 1 and K_{m}(d) = 0 for d ≠ c.

(4) If y is the successor of x, Q_{p!q}(x), x ∈ X_{K_{i}} and y ∈ X_{K_{j}}, then K_{j} = K_{i}^{+c}, where c = (p, q).

(5) If y is the successor of x, Q_{q?p}(x), x ∈ X_{K_{i}} and y ∈ X_{K_{j}}, then K_{i}(c) > 0 and K_{j} = K_{i}^{−c}, where c = (p, q).

The formula ||φ|| is given inductively as follows:

• ||Q_{a}(x)|| =^{def} Q_{a}(x).

• ||x ∈ X|| =^{def} x ∈ X.

• ||¬φ′|| =^{def} ¬||φ′||.

• ||φ_{1} ∨ φ_{2}|| =^{def} ||φ_{1}|| ∨ ||φ_{2}||.

• ||(∃x)φ′|| =^{def} (∃x)||φ′||.

• ||(∃X)φ′|| =^{def} (∃X)||φ′||.

• Finally, ||x ≤ y|| =^{def} x ⊑ y where we shall first define ⊑ in terms of ⊏· and then define ⊏·. This translation is based on the fact that in an MSC M = (E, ≤, λ), ≤ = (R_{P} ∪ R_{Ch})^{∗}.

The formula x ⊑ y asserts existence of non-empty subsets {p_{1}, p_{2}, …, p_{m}} of processes and {x_{1}, y_{1}, x_{2}, y_{2}, …, x_{m}, y_{m}} of positions such that x = x_{1} and y_{m} = y. Further, x_{i} ⪯ y_{i} and x_{i} and y_{i} are both in Σ_{p_{i}} for 1 ≤ i ≤ m. In addition, y_{i} ⊏· x_{i+1} for 1 ≤ i < m.

The predicate x ⊏· y is given by: x ≺ y and there is a channel c = (p, q) such that Q_{p!q}(x) and Q_{q?p}(y). Further, if x ∈ X_{K_{m}} then there are exactly K_{m}(c) occurrences of the symbol q?p between the positions x and y (and not including y). It is now straightforward to show that φ̂ has the required property. □

Lemma 4.2 Let L ⊆ M(P, B) be a regular MSC language. Then L is definable in MSO(P, B).

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 φ iff 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 and show that the underlying linear order is expressible in MSO(P, B). As a result, we can look for a formula φ̂ which will say “along the canonical linearization of an MSC, the sentence φ is satisfied”. We present below the main ideas and constructions involved in arriving at φ̂.

Throughout what follows, we fix a strict linear order ≺ ⊆ Σ×Σ. Consider an MSC M = (E, ≤, λ). For e ∈ E, let ↑e = {e′ | e ≤ e′}. For events e, e′ ∈ E, we define e co e′ if e ≰ e′ and e′ ≰ e. For X ⊆ E, let λ(X) = {λ(e) | e ∈ X}. Next, suppose that ∅ ≠ Σ′ ⊆ Σ. Then min(Σ′) is the least element of Σ′ under ≺. Finally, suppose e, e′ ∈ E with e co e′. Then Σ_{ee′} = λ(↑e \ ↑e′).

Let M = (E, ≤, λ) be an MSC. Then the ordering relation ≺ induces the ordering relation ≺_{M} ⊆ E × E given by e ≺_{M} e′ if e < e′ or (e co e′ and min(Σ_{ee′}) ≺ min(Σ_{e′e})).

Claim 4.3 Let M = (E, ≤, λ) be an MSC. Then (E, ≺_{M}) is a strict linear order and ≺_{M} is a linearization of ≤.

Proof: Same as the proof of [22, Lemma 15], which asserts an identical result in the setting of (infinite) Mazurkiewicz traces. □

We next exhibit a formula in MSO(P, B) (for any B ∈ ℕ) which captures the relation ≺_{M} for each B-bounded MSC M. First we define the formula min(z_{1}, z_{2}, a) where z_{1} and z_{2} are individual variables and a ∈ Σ via:

min(z_{1}, z_{2}, a) = (∃z)[\begin{matrix}z_{1} ≤ z ∧ ¬(z_{2} ≤ z) ∧ Q_{a}(z)∧ \\ (∀z′) ((z_{1} ≤ z′ ∧ ¬(z_{2} ≤ z′)) ⇒ Q_{a}(z′) ∨ ⋁_{a≺a′} Q_{a′}(z′))] \end{matrix}

The formula Lex(x, y) is now given by:

Lex(x, y) = (x < y) ∨ (co(x, y) ∧ ⋁_{a≺b} min(x, y, a) ∧ min(y, x, b))

where co(x, y) is an abbreviation for ¬(x ≤ y) ∧ ¬(y ≤ x).

Turning now to the proof of Lemma 4.2, 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 = {σ | σ ⊧ φ}. We now define the formula φ̂ = ||φ|| in MSO(P, B) inductively as follows:

||Q_{a}(x)|| = Q_{a}(x) and ||x ⪯ y|| = (x ≤ y ∧ y ≤ x) ∨ Lex(x, y)

The remaining clauses are the natural ones. It is now straightforward to verify that Lφ̂ = L. The key step in the proof is to show the following: Suppose M ∈ M(P, B) and σ is the the linearization of M dictated by ≺_{M}. Then M is a model of φ̂ iff σ is a model of φ. This follows easily by structural induction on φ. The required conclusion can now be derived by exploiting the fact that L is ∼-closed.

Since MSO(Σ) is decidable, it follows that MSO(P, B) is decidable as well. We can now summarize the results characterizing regularity as follows.

Theorem 4.4 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 ∈ ℕ.

5 Message Sequence Graphs

The standard method to describe multiple communication scenarios is to generate collections of MSCs by means of Hierarchical Message Sequence Charts (HMSCs). As described in the introduction, to analyze HMSCs, it suffices to flatten out them out to obtain Message Sequence Graphs (MSGs). As a consequence, henceforth we concentrate on MSGs rather than HMSCs.

An MSG allows the protocol designer to write a finite specification which combines MSCs using basic operations such as branching choice, composition and iteration. Such MSGs are finite directed graphs with designated initial and terminal vertices. Each vertex in an MSG is labelled by an MSC. The edges represent the natural operation of MSC concatenation. The collection of MSCs represented by an MSG consists of all those MSCs obtained by tracing a path in the MSG from an initial vertex to a terminal vertex and concatenating the MSCs that are encountered along the path.

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

[figure: M_{1}; ⟹; M_{2}]

Figure 4: An example MSG.

Formally, the (asynchronous) concatenation of MSCs is defined as follows. 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} yields the MSC M_{1} ∘ M_{2} = (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.

We can now formally define MSGs. 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 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(π) =^{def} 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 | π is a run through G}.

An example of an MSG is depicted in Figure 4. It is not hard to see that the language L defined is not regular. To see this, we note that L projected to {p!q, r!s}^{∗} is {σ ∈ {p!q, r!s}^{∗} | |σ|_{p!q} = |σ|_{r!s} ≥ 1}, which is not a regular string language. (Recall that regular languages are closed under arbitrary projections.)

A number of studies are available which are concerned with individual MSCs in terms of their semantics and properties [1, 12]. The rest of the work in the area consists of checking specific properties of communication scenarios specified as MSGs. We briefly survey these results here.

Muscholl, Peled, and Su [19] investigate various matching problems for MSCs and MSGs, where matching denotes embedding one partial order in another. More specifically, they show that given MSGs G_{1} and G_{2}, it is NPcomplete to decide whether there exist MSCs M_{1} ∈ L(G_{1}) and M_{2} ∈ L(G_{2}) such that M_{1} matches M_{2}. The universal counterpart to this problem— that is, does there exists some M_{1} ∈ L(G_{1}) such that M_{1} matches every M_{2} ∈ L(G_{2})—is also NP-complete.

Muscholl [17] defines “and-or” versions of MSGs, reminiscent of alternating automata. Given an “and-or” MSG G_{1} and a conventional MSG G_{2}, she considers the problem of deciding whether G_{1} admits a run-tree such that each MSC generated by a path in this run-tree matches an MSC in L(G_{2}). She shows that this problem is PSPACE-complete, and moreover that a similar problem of matching LTL-definable properties and MSGs is PSPACE-complete as well.

In [3] Ben-Abdallah and Leue identify and characterize two properties which are intuitively undesirable from an implementation point of view and give algorithms to detect such anomalies. The first of them is that of process divergence signifying that the specification allows some process to have an unbounded number of unreceived messages in its buffer. This can be detected in time linear in the total number of messages in the specification. We will note here that though related, the notion of divergence-freeness is implied by our notion of regularity, but does not coincide with it. Figure 4 provides a simple counter-example, because the language of the MSG is divergence-free but not regular.

The second underspecification detected by Ben-Abdallah and Leue is that of nonlocal choice. Intuitively, this denotes the existence of branching choices where different processes have the possibility of taking conflicting routes in the MSG specification. To prevent such consistency problems, additional messages or history variables have to be introduced into the system. Thus, it is desirable for an MSG to not permit nonlocal choice. Once again, Ben-Abdallah and Leue give an algorithm to detect the existence of nonlocal choice in an MSG which runs in time linear in the total number of messages in the specification. We note that the language of an MSG G might be a regular MSC language and still exhibit nonlocal choice, as the two notions are not related to each other. It is also worth pointing out that the problem

\xymatrix{p \ar[r] & q & p \ar[r] & q \ar[l] \\ r \ar[u] \ar[ur] &  & r \ar[r] & s \ar[l]}

Figure 5: CG_{M} of Figure 1 (left) and CG_{M_{1}∘M_{2}} of Figure 4 (right).

of nonlocal choice is limited to specification formalisms such as MSGs and is not an issue in specifications based on message-passing automata.

Alur and Yannakakis [2] consider model checking problems for systems modeled as MSGs with respect to various semantics. In their setup, automata are used to describe undesirable linearizations. Thus, the property to be checked captures the complement of the intended behaviour. In this framework, the decision problems essentially reduce to checking emptiness for products of automata, as the constituent automata need not be complemented. They show that for synchronous concatenation of MSCs on the paths of the MSG, the problem is coNP-complete, while the problem is undecidable in general for asynchronous concatenation.

Following this negative result, they then define the notion of a locally synchronized MSG. For an MSC M = (E, ≤, λ), let CG_{M}, the communication graph of M, be the directed graph (P, ↦) where:

• P is the set of processes of the system.

• (p, q) ∈ ↦ iff there exists an e ∈ E with λ(e) = p!q.

M is then said to be com-connected if CG_{M} consists of one nontrivial strongly connected component and isolated vertices. An MSC language L ⊆ M is com-connected in case each MSC M ∈ L is com-connected.

The MSG G is locally synchronized^{2} if for every loop π = q⟶q_{1}⟶ ⋯ ⟶q_{n}⟶q, the MSC M(π) is com-connected. In our terminology, we will say that an MSC language L is a locally synchronized MSG-language if there exists a locally synchronized MSG G with L = L(G). Figure 5 illustrates the communication graphs of the example MSCs encountered thus far. It is easy to see that neither M nor M_{1} ∘ M_{2} are com-connected.

Interestingly, Alur and Yannakakis [2] then show that the asynchronous model checking problem becomes PSPACE-complete for locally synchronized MSGs. Clearly, the MSG of Figure 4 is not locally synchronized. This is no coincidence, as it follows as a corollary of their proof sketch [2, Thm. 7] that every locally synchronized MSG-language is indeed regular.

2This notion is called “bounded” in [2]. The terminology “locally synchronized” is taken from [18].

We conclude this section by pointing out that Muscholl and Peled [18] also consider two decision problems related to locally synchronized MSGs. The first such problem is that of checking for race conditions. This essentially consists of checking whether the causal order allows more linearizations than the visual order. Recalling our discussion of linearizations in Section 2 we see that in Figure 1 there is a race on process q between the receive events for the messages from p and r, respectively.

The other problem is to detect confluence of MSG specifications. An MSG G is said to be confluent in case for any two prefixes M_{1}, M_{2} of MSCs in L(G) that are consistent (in the sense that both are prefixes of some common MSC), there does indeed exist such a completed MSC M in L(G) of which both M_{1} and M_{2} is a prefix.

Muscholl and Peled show that both the problem of deciding whether an MSG has race conditions and the problem of checking whether it is confluent are undecidable in general. However, they emphasize the importance of locally synchronized MSGs by additionally proving that both problems are EXPSPACE-complete for locally synchronized MSGs.

6 Finitely Generated Regular MSC Languages

A key feature of MSG languages is that for each such language there is a fixed finite set X of MSCs such that each MSC in the language can be expressed as a concatenation of MSCs (with multiple copies) taken from X. Such languages are said to be finitely generated. In this section we investigate the important connection between MSGs and finitely generated regular MSC languages. More precisely, we characterize the locally synchronized MSGlanguages as precisely constituting the class of MSC languages that are both regular and finitely generated.

Let L_{1}, L_{2} ⊆ M be two sets of MSCs. As usual, L_{1} ∘ L_{2} denotes the pointwise concatenation of L_{1} and L_{2}, as defined out in the previous section. For X ⊆ M, 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}. Now, let L ⊆ M. We say that L is finitely generated if there is a finite set of MSCs X ⊆ M such that L ⊆ X^{⊛}.

We first observe that not every regular MSC language is finitely generated. As an example, the automaton in Figure 2 accepts a regular language which is not finitely generated. By inspection of Figure 3 one readily verifies that none of the MSCs in this language can be expressed as the concatenation of two or more nontrivial MSCs. Hence, this language is not finitely generated.

Our interest in finitely generated languages stems from the fact that these arise naturally from standard high-level descriptions of MSC languages such as message sequence graphs. However, as we saw earlier, Figure 4 provides an example showing that, conversely, not all finitely generated languages are regular.

The first question we address is that of deciding whether a regular MSC language is finitely generated. To do this, we need to introduce atoms. Let M, M′ ∈ M 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 Atoms(M) denote the set {M′ | M′ is an atom and M′ is a component of M}. For an MSC language L ⊆ M, Atoms(L) = ⋃{Atoms(M) | M ∈ L}. It is clear that the question of deciding whether L is finitely generated is equivalent to that of checking whether Atoms(L) is finite.

Theorem 6.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 6.2 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′.

If M is in Comp(L), then there are MSC’s M_{1}, M_{2} such that M_{1}MM_{2} ∈ L. Thus, if w_{1}, w_{2} are some linearizations of M_{1} and M_{2}, then w_{1}ww_{2} is accepted by A. Thus, there is an accepting run s_{in} ⟶^{w_{1}} s ⟶^{w} s′ ⟶^{w_{2}} t. w_{1}, w_{2} and w are complete words as they arise as linearizations of MSCs. Further, s_{in} is a zero-capacity state and thus s and s′ must be zero-capacity states. This proves Claim 6.2.

Claim 6.3 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 M an atom and w be a linearization of M. Suppose w = w_{1}w_{2} for nonempty words w_{1} and w_{2} and s ⟶^{w_{1}} s_{1} ⟶^{w_{2}} s′, where s_{1} is a zerocapacity state. w_{1} and w_{2} are nonempty complete words. Recall that every complete word is the linearization of some MSC. Let M_{1} and M_{2} be the MSCs corresponding to w_{1} and w_{2}. Then, M = M_{1} ∘ M_{2} ∘ M_{3}, where M_{3} is the empty MSC, contradicting the assumption that M is an atom. Thus, the run can have no intermediate zero-capacity state.

Suppose M is not an atom. Then M = M_{1} ∘ M_{2} ∘ M_{3} where at least two of M_{1}, M_{2}, M_{3} are nonempty. Let w_{1}, w_{2} and w_{3} be linearizations of M_{1}, M_{2} and M_{3}. All three are complete words. Thus, there are states s_{1}, s_{2} such that s ⟶^{w_{1}} s_{1} ⟶^{w_{2}} s_{2} ⟶^{w_{3}} s′. Since at least one of these words is nonempty, one of the states s_{1} or s_{2} is a zero-capacity intermediate state. This completes the proof of Claim 6.3.

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 Claims 6.2 and 6.3 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 nontrivial complete prefix. For all such words, we know from Claim 6.3 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. □

We will now bring out the intimate connection between message sequence graphs and finitely generated regular MSC languages. As pointed out earlier, Alur and Yannakakis noted that every locally synchronized MSG-language is regular [2, Thm. 7]. One way to establish this result is — following [6]

— to show that the asynchronous iteration of a com-connected regular MSC language is regular. The proof in [6] is based on grammars. A more direct, automata-theoretic proof of the same result is described in Appendix B.

All languages arising from MSGs are finitely generated, so the language accepted by the message-passing automaton on Figure 2 shows that not all regular MSC languages can be described by MSGs. It turns out that locally synchronized MSGs generate precisely those MSC languages that are both regular and finitely generated.

Theorem 6.4 Let L be an MSC language. Then L is a finitely generated regular MSC language if and only if L is a locally synchronized MSG-language.

Proof Sketch: From the remarks above, it suffices to show that any finitely generated regular MSC language can be accepted by some locally synchronized MSG.

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 .

Fact 6.5 ([8], Sect. 6.3.1)

(1) 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)}.

(2) If w_{1}ww_{2} ∈ LEX , then w ∈ LEX .

(3) If w is not a connected^{3} trace, then ww ∉ LEX .

From (1) 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:

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

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

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

• (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 locally synchronized. 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 com-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 (2) of Fact 6.5, w^{k} ∈ LEX . This means, by (3) of Fact 6.5, 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 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,

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

Figure 6: An non-locally synchronized MSG whose language is regular.

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 locally synchronized.

□

It is easy to see that local synchronicity is not a necessary condition for regularity. Consider the MSG in Figure 6, which is not locally synchronized. It accepts the regular MSC language M_{1} ∘ (M_{1} + M_{2})^{⊛}.

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 6.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 trace-closure of a regular language L ⊆ A^{∗} with respect to a trace alphabet (A, I) is also regular is undecidable [21]. We reduce this problem to the problem of checking whether the MSC language defined by an MSG is regular.

Let Ã = (A_{1}, …, A_{n}) be a distributed alphabet implementing the trace alphabet (A, I) [8]. We will fix a set of processes P and the associated communication alphabet Σ and encode each letter a by an MSC M_{a} over P.

For each i, we create 1+|A_{i}| processes which we will denote by p_{i}, p_{i}^{a_{1}}, p_{i}^{a_{2}}, …, p_{i}^{a_{k}}, where A_{i} = {a_{1}, a_{2}, …, a_{k}}. Suppose now that the letter a appears in the components A_{i_{1}}, A_{i_{2}}, …, A_{i_{k}} of the distributed alphabet Ã with 1 ≤

[figure: (p_{i_{1}}); (p_{i_{1}}^{a}); (p_{i_{2}}); (p_{i_{2}}^{a}); …; (p_{i_{k−1}}); (p_{i_{k−1}}^{a}); (p_{i_{k}}); (p_{i_{k}}^{a}); •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; …]

Figure 7: The MSC M_{a} encoding the letter a ∈ A.

i_{1} < i_{2} < … < i_{k} ≤ n. The MSC M_{a} representing a is then given in Figure 7. It is easy to see 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 Theorem 6.4. 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. □

7 Discussion

In this report, we have first introduced a notion of regularity for collections of MSCs and provided both automata-theoretic and logical characterizations of regular MSC languages. We can summarize these results as follows.

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

(1) L is a regular MSC language.

(2) L is a B-bounded regular MSC language, for some B ∈ ℕ.

(3) There exists a bounded message-passing automaton A such that L(A) = L.

(4) L is MSO(P, B)-definable, for some B ∈ ℕ.

Following this, we have shown that the class of regular MSC languages properly subsumes the class of languages defined by locally synchronized MSGs, as studied in [2]. In fact, we precisely characterize the class of languages definable by locally synchronized MSGs in terms of finitely generated regular MSC languages. One way to phrase our characterization is as follows.

Theorem 7.2 Let L be a regular MSC language. Then L can be described by an MSG if and only if L is finitely generated.

Finally, we have also shown that it is decidable whether a given regular MSC language is finitely generated but it is undecidable, in general, whether a given MSG defines a regular MSC language.

References

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

[2] Alur, R., Yannakakis, M.: Model checking of message sequence charts. Proceedings of the 10th International Conference on Concurrency Theory (CONCUR’99), Lecture Notes in Computer Science 1664, Springer-Verlag (1999) 114–129 [3] Ben-Abdallah, H., Leue, S.: Syntactic detection of process divergence

and non-local choice in message sequence charts. Proceedings of the 3rd Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97), Lecture Notes in Computer Science 1217, Springer-Verlag (1997) 259–274

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

[5] Büchi, J. R.: Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6 (1960) 66–92

[6] Clerbout, M., Latteux, M.: Semi-commutations. Information and Computation 73(1) (1987) 59–74

[7] Damm, W., Harel, D.: LCSs: Breathing life into message sequence charts. Proceedings of the 3rd IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS’99), Kluwer Academic Publishers (1999) 293–312

[8] Diekert, V., Rozenberg, G. (Eds.): The Book of Traces. World Scientific (1995)

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

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

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

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

[13] Levin, V., Peled, D.: Verification of message sequence charts via template matching. Proceedings of the 7th International Conference on Theory and Practice of Software Development (TAPSOFT’97), Lecture Notes in Computer Science 1214, Springer-Verlag (1997) 652–666

[14] Mauw, S., Reniers, M. A.: High-level message sequence charts, Proceedings of the 8th SDL Forum, SDL’97: Time for Testing — SDL, MSC and Trends, Elsevier (1997) 291–306 [15] Mukund, M., Narayan Kumar, K., Sohoni, M.: Keeping track of the lat-

est gossip in message-passing systems. Proceedings of Structures in Concurrency Theory (STRICT), Workshops in Computing Series, Springer-Verlag (1995) 249–263

[16] Mukund, M., Narayan Kumar, K., Sohoni, M.: Synthesizing distributed finite-state systems from MSCs. Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000), Lecture Notes in Computer Science, Springer-Verlag (to appear)

[17] Muscholl, A.: Matching specifications for message sequence charts. Proceedings of the 2nd International Conference on Foundations of Software Science and Computation Structures (FOSSACS’99), Lecture Notes in Computer Science 1578, Springer-Verlag (1999) 273–287

[18] Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. Proceedings of the 24th International Symposium on Mathematical Foundations of Computer Science (MFCS’99), Lecture Notes in Computer Science 1672, Springer-Verlag (1999) 81–91

[19] Muscholl, A., Peled, D., Su, Z.: Deciding properties for message sequence charts. Proceedings of the 1st International Conference on Foundations of Software Science and Computation Structures (FOS-SACS’98), Lecture Notes in Computer Science 1378, Springer-Verlag (1998) 226–242

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

[21] Sakarovitch, J.: The “last” decision problem for rational trace languages. Proceedings of the 1st Latin American Symposium on Theoretical Informatics (LATIN’92), Lecture Notes in Computer Science 583, Springer-Verlag (1992) 460–473

[22] Thiagarajan, P. S., Walukiewicz, I.: An expressively complete linear time temporal logic for Mazurkiewicz traces. Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS’97), IEEE Computer Society Press (1997) 183–194

[23] Thomas, W.: Automata on infinite objects. In van Leeuwen, J. (Ed.): Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier Science Publishers (1990) 133–191 [24] Thomas, W.: Languages, automata, and logic. In Rozenberg, G., Sa-

lomaa, A. (Eds.): Handbook of Formal Language Theory, Volume III, Springer-Verlag (1997) 389–455

[25] Vardi, M. Y., Wolper, P.: An automata-theoretic approach to automatic program verification. Proceedings of the 1st Annual IEEE Symposium on Logic in Computer Science (LICS’86), IEEE Computer Society Press (1986) 332–345

[26] Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O. Informatique Théorique et Applications 21 (1987) 99–135

A Bounded Time-stamps

Partial computations Let u ∈ Σ^{∗} be a complete word and let sm(u) = (E_{u}, ≤_{u}, λ_{u}) be the MSC associated with u. 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. The ideal I ⊆ E_{u} is said to be complete if I is itself an MSC. We denote the set of ideals of M = (E, ≤, λ) by Ideals(M).

Ideals denote consistent partial computations of u—notice that any linearization of an ideal forms a proper word, which we will sometimes refer to as a communication sequence. If an ideal I is complete, then its linearizations are also complete.

We can extend the map sm to the domain of proper words. If u is proper but not complete, sm(u) will not be an MSC because some send events will not have matching receive events. However, it is easy to observe that the labelled partial order sm(u) corresponds to an ideal in the MSC sm(v) for any complete word v which extends u. In this section, we shall work with this extended definition of the map sm. Henceforth, for a proper word u, we shall refer to the labelled partial order sm(u) as M_{u} = (E_{u}, ≤_{u}, λ_{u}). In particular, E_{u} always refers to the set of events associated with the MSC sm(u) generated from a proper word u.

p-views For an ideal I, the ≤-maximum p-event in I is denoted max_{p}(I), provided there is at least one p-event in I. 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 eR_{(p,q)}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 a proper word and let M_{u} = (E_{u}, ≤_{u}, λ_{u}). We say that u is B-bounded, for B ∈ ℕ, if for every pair of processes p, q and for every ideal I ⊆ E_{u}, unack_{p→q}(I) contains at most B events.

The following result is immediate.

Proposition A.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, |w|_{p!q} − |w|_{q?p} ≤ 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 message-passing 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 [15], a protocol is presented for processes to keep track of their primary information during the course of an arbitrary computation.^{4} 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 timestamping mechanism which consistently assigns “names” to events using a bounded set of labels.

4In [15], 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.

Consistent time-stamping Let T be a finite set of labels. For a proper communication sequence u, we say that τ : E_{u} → T is a consistent timestamping of E_{u} by T 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 [15], 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 [15] requires processes to also maintain additional time-stamps, corresponding to secondary information. Though we do not need the details of how the protocol works, for completeness we define secondary information.

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 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 [15] can now be described as follows.

Theorem A.2 For any B ∈ ℕ, we can construct a B-bounded messagepassing automaton A^{B} = ({A_{p}^{B}}_{p∈P}, Δ^{B}, s_{in}^{B}, F^{B}) such that for every Bbounded 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 τ.

B Asynchronous Iteration

In this section, we give an automata-theoretic proof that the asynchronous iteration of a com-connected regular MSC language remains regular. A proof of this result in terms of grammars appears in [6].

We begin with a simple characterization of asynchronous iteration that follows from the definition in Section 6.

Proposition B.1 Let L ⊆ M be an MSC language. The MSC M = (E, ≤, λ) belongs to L^{⊛}, the asynchronous iteration of L, iff there is a sequence of complete ideals ∅ = I_{0} ⊂ I_{1} ⊂ ⋯ ⊂ I_{n} = E such that for each j ∈ {1, 2, …, n}, the partial order I_{j} \ I_{j−1} is isomorphic to some M′ ∈ L.

The ideals I_{0}I_{1} … I_{n} define an L-factorization of M—that is, a factorization of M into MSCs from L.

B.1 An infinite-state automaton for L^{⊛}

Let L be a regular MSC language. From the automata-theoretic characterization of Section 3, it follows that there is a B-bounded message-passing automaton A such that L(A) = L. To construct a (sequential) automaton for L^{⊛}, our strategy will be to guess a factorization of the input and simulate A to verify that each factor belongs to L. We first construct an infinite-state automaton for L^{⊛} for an arbitrary regular MSC language L and then describe the conditions under which we can restrict the automaton for L^{⊛} to be a finite-state device.

The new automaton A^{⊛} that we construct uses natural numbers to label the factors. Since not every process participates in every factor, A^{⊛} records the sequence of factors that each process p ∈ P participates in and ensures that the sequence in which the factors are processed is consistent across the system. In addition, A^{⊛} simulates a copy of A on each factor. Initially, each factor is labelled by the initial configuration of A. The simulation succeeds if the global state associated with each factor is a final configuration of A.

More formally, A^{⊛} = (S′, s′_{in}, ⟶′, F′) where each state in S′ is a pair (μ, ν) with μ : P → ℕ^{∗} and ν : ℕ → Conf_{A} such that μ satisfies the following condition:

• For any pair of processes p and q (not necessarily distinct) and any pair of distinct labels ℓ and ℓ′, if ℓ appears before ℓ′ in μ(p), then ℓ′ does not appear before ℓ in μ(q).

The function μ records the order in which each process observes the Lfactors of the input word. The function ν keeps track of the current configuration of A on each factor.

The initial state s′_{in} of A^{⊛} is the pair (μ_{in}, ν_{in}) where μ_{in}(p) = ε for each process p and ν_{in}(ℓ) = (s_{in}, χ_{ε}) for each ℓ ∈ ℕ (where ε is the empty word and (s_{in}, χ_{ε}) is the initial configuration of A).

A state (μ, ν) of A^{⊛} is in F′ whenever:

• If ℓ appears in μ(p) for some process p, ν(ℓ) is a final configuration of A.

• If ℓ does not appear in μ(p) for any process p, ν(ℓ) = (s_{in}, χ_{ε}).

Consider states (μ, ν) and (μ′, ν′) and a letter a such that a ∈ Σ_{p}. Then, (μ, ν) ⟶^{a}′ (μ′, ν′) provided:

• For q ≠ p, μ′(q) = μ(q).

• Either μ′(p) = μ(p) or μ′(p) = μ(p) · ℓ for some ℓ ∈ ℕ.

• Let the last label in μ′(p) be ℓ. Then, ν(ℓ) ⟹^{a} ν′(ℓ) and for ℓ′ ≠ ℓ, ν′(ℓ′) = ν(ℓ′) (where ⟹ ⊆ Conf_{A} × Σ × Conf_{A} is the global transition relation of A).

The following is easy to verify from the definition of A^{⊛}.

Theorem B.2 Let A be a message-passing automaton for a regular MSC language L. Then, the automaton A^{⊛} accepts the language L^{⊛}.

To describe when we can restrict A^{⊛} to a finite-state device, we extend the definition of A^{⊛} so that each state has one more component. A state of A^{⊛} is now a triple of functions (μ, ν, τ), where μ : P → ℕ^{∗} and ν : ℕ → Conf_{A} are as before. The new component τ : ℕ → 2^{P} specifies the type of each label.

As before, μ records the sequence in which each process observes L-factors while ν keeps track of the current configuration of each factor. The new component τ records the set of processes that participate in each factor.

The states of A^{⊛} are those triples (μ, ν, τ) that satisfy the following conditions:

• For any pair of processes p and q (not necessarily distinct) and any pair of distinct labels ℓ and ℓ′, if ℓ appears before ℓ′ in μ(p), then ℓ′ does not appear before ℓ in μ(q).

• If τ(ℓ) ≠ ∅ then ℓ appears in μ(p) for some p ∈ P. Moreover, if ℓ appears in μ(p) then p ∈ τ(ℓ).

The initial state s′_{in} of the extended version of A^{⊛} is the triple (μ_{in}, ν_{in}, τ_{in}) where μ_{in}(p) = ε for each process p, ν_{in}(ℓ) = (s_{in}, χ_{ε}) for each ℓ ∈ ℕ and τ_{in}(ℓ) = ∅ for each ℓ ∈ ℕ.

A state (μ, ν, τ) of A^{⊛} is in F′ whenever:

• If ℓ appears in μ(p) for some process p, ν(ℓ) is a final configuration of A.

• If ℓ does not appear in μ(p) for any process p, ν(ℓ) = (s_{in}, χ_{ε}).

• If τ(ℓ) = P then ℓ appears in μ(p) for each p ∈ P.

Consider states (μ, ν, τ) and (μ′, ν′, τ′) and a letter a such that a ∈ Σ_{p}. Then, (μ, ν, τ) ⟶^{a}′ (μ′, ν′, τ′) provided:

• For q ≠ p, μ′(q) = μ(q).

• Either μ′(p) = μ(p) or μ′(p) = μ(p) · ℓ for some ℓ ∈ ℕ.

• Let the last label in μ′(p) be ℓ. Then, ν(ℓ) ⟹^{a} ν′(ℓ) and for all ℓ′ ≠ ℓ, ν′(ℓ) = ν(ℓ).

• Let the last label in μ′(p) be ℓ. Then τ′(ℓ) ⊃ {p} and for ℓ′ ≠ ℓ, τ′(ℓ′) = τ(ℓ′). Moreover, if ℓ already appears in μ(q) for some q ∈ P, then τ′(ℓ) = τ(ℓ). (This captures the fact that when ℓ is first used, τ(ℓ) records a nondeterministic guess for the processes which will participate in the factor labelled ℓ and this guess cannot be changed.)

Once again, we can establish that L(A^{⊛}) = L(A)^{⊛}.

B.2 If L is com-connected, L^{⊛} is regular

Recall the definition of a com-connected MSC language from Section 5. The main result we want to prove is the following.

Theorem B.3 Let L be a regular and com-connected MSC language. Then, L^{⊛} is regular.

In the previous section, we saw how to construct an infinite-state automaton A^{⊛} for L^{⊛} from a message-passing automaton A for L. To prove Theorem B.3, we shall argue that if L is com-connected, A^{⊛} can in fact be cut down to a finite-state automaton.

Definition B.4 Let G = (V, E) be a directed graph. For X ⊆ V, define nbd(X), the neighbourhood of X, to be X ∪ {v′ | ∃v ∈ X : (v′, v) ∈ E}.

□

Proposition B.5 Let G = (V, E) be a directed graph such that all nonisolated vertices form a single strongly connected component. Let C ⊆ V be the vertices in this strongly connected component. Then, for any proper subset C′ ⊊ C, nbd(C′) has at least one vertex in C \ C′.

Proof: Suppose that C′ ⊊ C but there is no vertex v ∈ (C \ C′) ∩ nbd(C′). This means there is no path from any vertex in C \ C′ to any vertex in C′. This contradicts the assumption that C is a strongly connected component of G. □

Definition B.6 Consider a state (μ, ν, τ) of the extended automaton A^{⊛} described in the previous section. The label ℓ is said to be dead in (μ, ν, τ) if for every p ∈ τ(ℓ), μ(p) = w · ℓ · w′, where w′ is a nonempty string over ℕ. A label that is not dead is said to be live. □

Lemma B.7 Let A be a message-passing automaton for a com-connected MSC language L. In any state (μ, ν, τ) of A^{⊛} only a bounded number of labels are not dead.

Proof: Let (μ, ν, τ) be a state of A^{⊛} and let p ∈ P. Suppose that μ(p) is of the form u_{0}ℓ_{0}u_{1}ℓ_{1} … ℓ_{k}u_{k}ℓ_{k+1}u_{k+1}, where each u_{i}, i ∈ {0, 1, …, k+1}, is a string over ℕ, τ(ℓ_{0}) = τ(ℓ_{1}) = ⋯ = τ(ℓ_{k+1}) = P and |P | = k. Then, ℓ_{0} must be dead.

Recall that for each ℓ, τ(ℓ) records the set of processes that participate in the factor M_{ℓ} labelled ℓ. Since L is com-connected, τ(ℓ) defines a strongly connected set of processes in CG(M_{ℓ}).

Consider the graph G_{M_{ℓ_{k}}}. Let P_{k} = nbd(p) in this graph. For each process q ∈ P_{k}, there is an edge from q to p in G_{M_{ℓ_{k}}}. Thus, there is at least one action p?q in the factor M_{ℓ_{k}}. Since p has progressed from the factor M_{ℓ_{k}} to the factor M_{ℓ_{k+1}}, the corresponding q-action q!p in M_{ℓ_{k}} must also have occurred already. Thus, q has also observed the factor ℓ_{k} and ℓ_{k} must appear in μ(q) as well.

Let P_{k−1} = nbd(P_{k}) in G_{M_{ℓ_{k}}}. By a similar argument, ℓ_{k−1} must appear in μ(q) for each q ∈ P_{k−1}.

In this vein, we can construct P_{k−2}, P_{k−3}, … such that for each j ∈ {k, k−1, …, 1}, P_{j−1} = nbd(P_{j}) in G_{M_{ℓ_{j}}} and argue that ℓ_{j−1} must appear in μ(q) for each q ∈ P_{j−1}. By Proposition B.5, P_{j−1} \ P_{j} ≠ ∅ and P_{k} ⊂ P_{k−1} ⊂ ⋯ ⊆ P. Recall that |P_{k}| ≥ 2, since p ∈ P_{k} as well as the witness q such that q?p ∈ M_{ℓ_{k}}. Since |P | = k, we must thus have P_{2} = P. In other words, ℓ_{1} appears in μ(q) for each q ∈ P_{2} = P. From Definition B.6, it follows that ℓ_{0} is dead in (μ, ν, τ). □

Let (μ, ν, τ) be a state of A^{⊛}. For any process p and any P ⊆ P, there are at most |P | live labels in μ(p) of type P. Thus, the number of live labels in μ(p) is bounded by |P| · 2^{|P|} and the number of live labels overall in (μ, ν, τ) is bounded by |P|^{2} · 2^{|P|}.

A finite-state version of A^{⊛} From this, we can derive a finite-state version of A^{⊛} when the language accepted by A is com-connected. Instead of using the infinite set of labels ℕ to name factors, we fix a finite set of labels T such that |T | > |P|^{2} · 2^{|P|}. Thus, a state of A^{⊛} now consists of functions (μ, ν, τ) where μ : P → T^{∗}, ν : T → Conf_{A} and τ : T → 2^{P}.

A state of A^{⊛} is a triple (μ, ν, τ) that satisfies the following conditions:

• For any pair of processes p and q (not necessarily distinct) and any pair of distinct labels ℓ and ℓ′, if ℓ appears before ℓ′ in μ(p), then ℓ′ does not appear before ℓ in μ(q).

• If τ(ℓ) ≠ ∅ then ℓ appears in μ(p) for some p ∈ P. Moreover, if ℓ appears in μ(p) then p ∈ τ(ℓ).

• For each p ∈ P, μ(p) contains at most |P | labels of type P for each P ⊆ P.

The last condition ensures that A^{⊛} is finite-state.

In the initial state (μ_{in}, ν_{in}, τ_{in}), μ_{in}(p) = ε for each p ∈ P, ν_{in}(ℓ) = (s_{in}, χ_{ε}) for each ℓ ∈ T and τ(ℓ) = ∅ for each ℓ ∈ T .

Let (μ, ν, τ) and (μ′, ν′, τ′) be two states of A^{⊛} and let a ∈ Σ_{p}. Then (μ, ν, τ) ⟶^{a}′ (μ′, ν′, τ′) provided we can construct an intermediate triple of functions (μ′′, ν′′, τ′′) such that:

• For q ≠ p, μ′′(q) = μ(q).

• Either μ′′(p) = μ(p) or μ′′(p) = μ(p) · ℓ for some ℓ ∈ T .

• Let the last label in μ′′(p) be ℓ. Then, ν(ℓ) ⟹^{a} ν′′(ℓ) and for ℓ′ ≠ ℓ, ν′′(ℓ′) = ν(ℓ′).

• Let the last label in μ′′(p) be ℓ. Then τ′′(ℓ) ⊃ {p} and for ℓ′ ≠ ℓ, τ′′(ℓ′) = τ(ℓ′). Moreover, if ℓ already appears in μ(q) for some q ∈ P, then τ′(ℓ) = τ(ℓ).

For p ∈ P and P ⊆ P, suppose that μ(p) is of the form u_{0}ℓ_{0}u_{1}ℓ_{1} … ℓ_{k}u_{k}ℓ_{k+1}u_{k+1}, where each u_{i}, i ∈ {0, 1, …, k+1}, is a string over T , τ(ℓ_{0}) = τ(ℓ_{1}) = ⋯ = τ(ℓ_{k+1}) = P and |P | = k.

Then, it is the case that ℓ_{0} is dead in (μ′′, ν′′, τ′′) and ν′′(ℓ_{0}) is a final configuration of A. (Observe that since exactly one process moves on each input, at most one dead label is generated with each move).

• (μ′, ν′, τ′) is obtained from (μ′′, ν′′, τ′′) by deleting the dead label ℓ_{0}, if any, from μ(q) for each q ∈ τ′′(ℓ_{0}) and then resetting τ′(ℓ_{0}) = ∅. If there are no dead labels in (μ′′, ν′′, τ′′), then (μ′, ν′, τ′) is the same as (μ′′, ν′′, τ′′).

A state (μ, ν, τ) of A^{⊛} is in F′ provided:

• If ℓ appears in μ(p) for some process p, ν(ℓ) is a final configuration of A.

• If ℓ does not appear in μ(p) for any process p, ν(ℓ) = s_{in}.

• If τ(ℓ) = P then ℓ appears in μ(p) for each p ∈ P.

From Lemma B.7, it is easy to argue that if L is com-connected, then the finite-state version of A^{⊛} accepts L^{⊛}. This completes the proof of Theorem B.3.

Recent BRICS Report Series Publications

RS-99-52 Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, and P. S. Thiagarajan. Towards a Theory of Regular MSC Languages. December 1999. 43 pp.

RS-99-51 Olivier Danvy. Formalizing Implementation Strategies for First-Class Continuations. December 1999. Extended version of an article to appear in Smolka, editor, Programming Languages and Systems: Ninth European Symposium on Programming, ESOP ’00 Proceedings, LNCS 1782, 2000.

RS-99-50 Gerth Stølting Brodal and Srinivasan Venkatesh. Improved Bounds for Dictionary Look-up with One Error. December 1999. 5 pp.

RS-99-49 Alexander A. Ageev and Maxim I. Sviridenko. An Approximation Algorithm for Hypergraph Max k-Cut with Given Sizes of Parts. December 1999. 12 pp.

RS-99-48 Rasmus Pagh. Faster Deterministic Dictionaries. December 1999. 14 pp. Appears in Shmoys, editor, The Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’00 Proceedings, 2000, pages 487–493.

RS-99-47 Peter Bro Miltersen and Vinodchandran N. Variyam. Derandomizing Arthur-Merlin Games using Hitting Sets. December 1999. 21 pp. Appears in Beame, editor, 40th Annual Symposium on Foundations of Computer Science, FOCS ’99 Proceedings, 1999, pages 71–80.

RS-99-46 Peter Bro Miltersen, Vinodchandran N. Variyam, and Osamu Watanabe. Super-Polynomial Versus Half-Exponential Circuit Size in the Exponential Hierarchy. December 1999. 14 pp. Appears in Asano, Imai, Lee, Nakano and Tokuyama, editors, Computing and Combinatorics: 5th Annual International Conference, COCOON ’99 Proceedings, LNCS 1627, 1999, pages 210–220.

RS-99-45 Torben Amtoft. Partial Evaluation for Constraint-Based Program Analyses. December 1999. 13 pp.