Deciding Properties for Message Sequence Charts

Anca Muscholl^{1}, Doron Peled^{2} and Zhendong Su^{3}

1 Institut für Informatik, Universität Stuttgart, Breitwiesenstr. 20-22, 70565 Stuttgart, Germany

2 Bell Laboratories, Lucent Technologies, 600 Mountain Av., Murray Hill, NJ 07974,

and Carnegie Mellon University, School of Computer Science, Pittsburgh, PA, 15213-3891, USA 3 EECS Department, University of California, Berkeley, CA 94710-1776, USA

Abstract. Message sequence charts (MSC) are commonly used in designing communication systems. They allow describing the communication skeleton of a system and can be used for finding design errors. First, a specification formalism that is based on MSC graphs, combining finite message sequence charts, is presented. We present then an automatic validation algorithm for systems described using the message sequence charts notation. The validation problem is tightly related to a natural language-theoretic problem over semi-traces (a generalization of Mazurkiewicz traces, which represent partially ordered executions). We show that a similar and natural decision problem is undecidable.

1 Introduction

Message sequence charts (MSC) are a notation widely used for the early design of communication protocols. With its graphical representation, it allows to describe the communication skeleton of a protocol by indicating the messages that are sent between its different processes. Using message sequence charts one can document the features of a system, and the way its parts interact. Although MSCs often do not contain the full information that is needed for implementing the described protocols, they can be used for various analysis purposes. For example, one can use MSCs to search for missing features or incorrect behaviors. It is possible to detect mistakes in the design, e.g., the existence of race conditions [1] or nonlocal choice [2]. Another task that is often done using MSCs is providing ‘feature transparence’, namely upgrading a communication system in a way that all the previous services are guaranteed to be supported.

In recent years MSCs have gained popularity and interest. An international committee (ITU-Z 120 [7]) has been working on developping standards for MSCs. Some tools for displaying MSCs and performing simple checks were developed [1,8]. We model systems of MSCs, allowing a (possibly infinite) family of (finite or infinite) executions. Each execution consists of a finite or infinite set of send and receive events, together with a partial (causal) order between them. Such a system is denoted using MSC graphs, where individual MSCs are combined to form a branching and possibly looping structure. Thus, an MSC graph describes a way of combining partially ordered executions of events.

We suggest in this paper a specification formalism for MSC properties based on directed graphs: each node of the graph consists of a template, which includes a set of communication events, and the causal order between them. We study three alternative semantics for the specification by MSC graphs:

– Using the same semantics as for an MSC system. Namely, each maximal sequence corresponds exactly to one execution.

– With gaps, i.e., as a template, where only part of the events (and the order between them) is specified. Moreover, choices in the specification graph correspond to different possible ways to continue the execution.

– Again with gaps, but with choices corresponding to conjunctions. Namely an execution matching the specification must include all the events in every possible path of the specification, respecting the associated causal orders.

The main focus of this paper is on developping an algorithm for deciding whether there are executions of the checked system of MSCs that match the specification. Such an execution is considered as a ‘bad’ execution and if exists it should be reported as a counter-example for the correctness of the system. For the first semantics we show in Section 5 that the matching problem is undecidable. For the last two problems we provide algorithms and we show them to be NP-complete, see Section 4. In the special case of matching two single MSCs we provide a deterministic polynomial time algorithm, improving the result of [8], see Section 3. The complexity of related problems has been studied for pomset languages [6]. In contrast, in [6] only finite pomset languages are studied (however, over a richer structure).

The matching problem can also be represented as a decision problem for semi-traces [4]. A semi-trace is a set of words that is obtained from some word by means of (not necessarily symmetric) rewriting rules. These rules allow commuting pairs of adjacent letters. A semi-trace language is a set of words closed under these given rewriting rules. We provide a natural transformation from MSCs to semi-traces. This allows explaining our decidability result as a decision problem on rational languages of semi-traces. One surprising consequence of this translation is that it applies in the same way to two rather different communication semantics for a natural subclass of MSCs: that of asynchronous fifo communication and that of synchronous (handshake) communication.

Work is in progress to add the proposed validation framework to a toolset that was developed for manipulating MSCs [1]. This paper concludes with several open problems and suggested work.

2 Charts and MSC Graphs

In this section, we introduce message sequence charts (MSC) and MSC graphs, as well as the matching problem.

Definition 1 (MSC). A message sequence chart M is a quintuple ⟨E, <, L, T, P⟩ where E is a set of events, < ⊆ E × E is an acyclic relation, P is a set of processes, L : E → P is a mapping that associates each event with a process, and T : E → {s, r} is a mapping that describes the type of each event (send or receive).

The order relation < is called the visual ordering of events and it is obtained from the syntactical representation of the chart (e.g. represented according to the standard syntax ITU-Z 120). It is called ‘visual’ since it reflects the graphical representation of MSCs. We distinguish between two types of visual ordering as follows. We let <_{c} = {(e, e′) | T (e) = s , T (e′) = r and e, e′ are the send and receive events of the same message} denote the message ordering. Furthermore, for P ∈ P let E_{P} = {e | e ∈ E ∧ L(e) = P }, i.e., E_{P} is the set of events that belong to process P. We define the relation <_{P} = < ∩ (E_{P} × E_{P}) that represents the ordering between events of P only. Then the visual order < is the union of these orders, i.e., < = <_{c} ∪ (⋃_{P ∈P} <_{P}).

Thus, for two events e and f, we have e < f if and only if one of the following holds:

– e and f are the send and receive event of the same message. In this case, we call e and f a message pair.

– e and f belong to the same process P, with e appearing before f on the process line. This imposes a total order among all events of P, for every process P.

In general, the visual order provides more ordering than intended by the designer. Therefore we associate with every chart a causal structure providing the intended ordering. Causal structures are related to pomsets [11], event structures [9], and traces [5]. A causal structure is obtained from an MSC by means of a given semantics. Formally, the causal structure of an MSC M is a quintuple tr(M) = ⟨E, ≺, L, T, P⟩, where the only component that differs from the definition of an MSC is the relation ≺, called the precedence order of events. For two events e and f, we have e ≺ f if and only if event e must terminate before event f starts. The transitive closure ≺^{∗} of ≺ is called the causal order. Events which are not causally ordered can occur independently of each other.

The precedence order of events is defined by a set of semantic rules. As the semantics used throughout the paper, we give below the set of rules for an architecture with fifo queues. This means that every one-directional communication between two processes is done through a fifo channel. For this architecture we have in the visual order for each message pairs e <_{c} f and e′ <_{c} f′ with e <_{P} e′ and L(f) = L(f′) = P′ also f <_{P′} f′. Then, for two events e and f, let e ≺ f for the fifo semantics if one of the following holds:

1. Two sends from the same process:

T (e) = T (f) = s ∧ e <_{P} f for some process P .

2. A message pair: T (e) = s ∧ T (f) = r ∧ e <_{c} f.

3. Messages ordered by the fifo queue:

T (e) = T (f) = r ∧ e <_{P} f for some process P ∧

∃e′, f′ (e′ <_{c} e ∧ f′ <_{c} f ∧ e′ <_{P′} f′ for some process P′) .

4. A receive precedes a send on the same process line:

T (e) = r ∧ T (f) = s ∧ e <_{P} f for some process P .

Remark 2. For a causal structure O = ⟨E, ≺, L, T, P⟩ we use the usual notation e ↓ for the downward closure of an event e ∈ E w.r.t. the partial order of O, i.e. e ↓= {f ∈ E | f ≺^{∗} e}. The notion of a minimal element e in O is also standard, meaning that e′ ≺^{∗} e implies e′ = e. We denote by min(O) the set of minimal elements of the partial order of O.

Note that the following relation between configurations associated to a message pair holds under the fifo semantics:

Lemma 3. Let e <_{c} f be a message pair. Then we have under the fifo semantics:

f ↓ = e ↓ ∪ {f_{1} ∈ E | T (f_{1}) = r, L(f_{1}) = L(f) and
e_{1} <_{c} f_{1} for e_{1} with e_{1} ⪯ e, T (e_{1}) = s, L(e_{1}) = L(e)} .

2.1 Templates and the Matching Problem

An MSC M matches an MSC N (or is embedded in N) if the chart N respects the causal order on the events specified by M. (Clearly, matching is defined with respect to a given semantics.) The MSC M is called a template MSC and it represents the specification, whereas the MSC N is called a system MSC. For matching M against N it suffices to consider the reduced partial order of M. Moreover, a template is viewed as a possibly partially specified execution of the system. The actual executions may contain additional messages, which may induce additional ordering.

Definition 4 (Matching a template with an MSC). Under a given semantics, a template M with the causal structure tr(M) = ⟨E_{M}, ≺_{M}, L_{M}, T_{M}, P_{M}⟩ matches a chart N with the causal structure tr(N) = ⟨E_{N}, ≺_{N}, L_{N}, T_{N}, P_{N}⟩ if and only if P_{M} ⊆ P_{N} and there exists an injective mapping (called embedding) h : E_{M} → E_{N} such that

– for each e ∈ E_{M}, we have L_{N}(h(e)) = L_{M}(e) and T_{N}(h(e)) = T_{M}(e) (preserving processes and types), and

– if e_{1} ≺_{M} e_{2} then h(e_{1}) ≺_{N} h(e_{2}) (preserving the causal order).

Let P = {P_{1}, …, P_{n}} denote the set of processes. For an event e ∈ E we are often interested in its ‘message type’ msg(e) and we let msg(e) = s_{ij}, if e is a send event from P_{i} to P_{j}, and msg(e) = r_{ij} if e is a receive event of P_{j} from P_{i}, respectively. Let msg(M) = {msg(e) | e ∈ E_{M}}.

Note that under the fifo semantics the injectivity of the embedding is already implied by the two other properties in the definition above. Moreover, under this semantics we have a simpler characterization of embeddings, which takes into account just message types:

Lemma 5. Let M, N denote two MSCs and let h : M → N be a mapping. Then h is an embedding from M to N if and only if the following conditions hold for any two events e, f ∈ E_{M}:

1. If (e, f) is a message pair, then (h(e), h(f)) is also a message pair between the same processes.

2. Let e ≺_{M} f such that (e, f) is not a message pair (thus, e, f are on the same process). Then msg(h(e)) = msg(e), msg(h(f)) = msg(f) and h(e) <_{N} h(f) holds in the visual order <_{N} of N.

Let M denote the class of finite message sequence charts. Let M_{i} = ⟨E_{i}, <_{i} , L_{i}, T_{i}, P_{i}⟩ be two MSCs, i = 1, 2. The (syntactic) concatenation of M_{1} and M_{2}, denoted M_{1}M_{2}, is defined by letting M_{1}M_{2} = ⟨E_{1} ∪^{·} E_{2}, <, L, T, P_{1} ∪ P_{2}⟩ with L|_{E_{i}} = L_{i}, T |_{E_{i}} = T_{i} and < = <_{1} ∪ <_{2} ∪{(e, e′) | e ∈ E_{1}, e′ ∈ E_{2}, L(e) = L(e′)}. Here, E_{1} ∪^{·} E_{2} means the disjoint union of the event sets of M_{1} and M_{2}. The concatenation of an infinite sequence M_{1}, M_{2}, … is defined in an analogous way. Message sequence graphs (MSC graphs, sometimes called high-level MSCs [7]), are used to compose MSCs to larger systems. Equivalently, one can compose MSCs using rational operations, i.e. union, concatenation and iteration. MSC graphs are finite directed graphs where each node of the graph is associated with a finite MSC [1].

Definition 6 (MSC graph). An MSC graph N is a quadruple ⟨S, τ, s_{0}, c⟩ where ⟨S, τ, s_{0}⟩ is a finite, directed graph with states set S, transition relation τ ⊆ S × S and starting state s_{0} ∈ S. The mapping c : S → M assigns to each node a finite MSC.

Let ξ = s_{1}, s_{2}, … be a (possibly infinite) path in N, i.e. (s_{i}, s_{i+1}) ∈ τ for every i. The execution (MSC) defined by ξ is given by c(ξ) = c(s_{1})c(s_{2}) . . ..

In order to distinguish MSC graphs from finite MSCs we denote throughout the paper a finite MSC (not bounded to any MSC graph) as a single MSC.

In an MSC graph N = ⟨S, τ, s_{0}, c⟩, a path ξ is called maximal if it begins with the starting state s_{0} and it is not a proper prefix of another path. Notice that a maximal path can be either infinite or finite. Let also msg(N) = ∪_{s∈S}msg(c(s)).

Fig. 1 shows an example of an MSC graph where the state in the upper left corner is the starting state. Note that the executions of this system are either finite or infinite. Also note that the events of receiving messages of fail and report are not causally ordered.

Definition 7 (Matching paths). Let ξ_{1} and ξ_{2} be two finite or infinite paths in some MSC graphs. Then ξ_{1} matches ξ_{2} if c(ξ_{1}) matches c(ξ_{2}).

Approve Connect  Req service Fail  ^{P2}^{P2}  ^{P2}  ^{P3}^{P3}^{P3}  ^{P1} Report^{P1}  ^{P2}  ^{P3}^{P1}  ^{P1}

Fig. 1. A system MSC graph.

A strongly connected component C of a directed graph ⟨S, τ⟩ is a subset C ⊆ S such that for any u, v ∈ C, there is a nonempty path from u to v. A maximal strongly connected component is a strongly connected component which is maximal w.r.t. set inclusion.

3 Matching a Template

In this section, we consider the problem of matching a single template MSC with an MSC graph. As a first result, we show that we can check whether a template can be embedded into a single MSC in polynomial time. (Recall that we assume that the fifo semantics is used.) This algorithm refines the result of [8], where a PSPACE algorithm was exhibited without specifying the semantics. The present matching algorithm is based on the simple observation that it suffices to match a suitable minimal send event and the corresponding receive event with the first occurrence of a message pair of the same type.

Proposition 8. Let M = ⟨E_{M}, <_{M}, L_{M}, T_{M}, P_{M}⟩, N = ⟨E_{N}, <_{N}, L_{N},T_{N}, P_{N}⟩ be single MSCs. For each event e ∈ min(tr(M)) which is minimal w.r.t. ≺_{M}^{∗} let μ(e) ∈ E_{N} denote the first event in N with msg(e) = msg(μ(e)). Choose e_{0} ∈ min(tr(M)) be such that μ(e_{0}) is minimal within the set {μ(e) | e ∈ min(tr(M))}. Let f_{0}, resp. f′_{0}, denote the corresponding receive events of e_{0}, resp. μ(e_{0}). Let M′ = M \ {e_{0}, f_{0}} and N′ = N \ {g′ ∈ E_{N} | g′ ≺_{N}^{∗} f′_{0}}. Then M matches N if and only if e_{0} is well-defined and M′ matches N′. Moreover, if h′ : M′ → N′ is an embedding of M′ into N′, then h′ ∪ {e_{0} ↦ μ(e_{0}), f_{0} ↦ f′_{0}} is an embedding of M into N.

Proof. Note first that all minimal elements of tr(M) are send events. Suppose that M matches N via h : M → N, where h(e_{0}) ≠ μ(e_{0}) (hence, h(f_{0}) ≠ f′_{0}). Let e′_{0} := μ(e_{0}) and let ĥ be given by ĥ(e_{0}) = e′_{0}, ĥ(f_{0}) = f′_{0} and ĥ(g) = h(g) for every g ∉ {e_{0}, f_{0}}. Now, if e_{0} ≺_{M} g, then h(e_{0}) ≺_{N} h(g) and hence also e′_{0} ≺_{N} h(g), since e′_{0} ≺_{N} h(e_{0}) and e′_{0}, h(e_{0}) have the same message type. A similar argument holds for f_{0} ≺_{M} g, which shows that ĥ is again an embedding from M to N. In order to show that M′ matches N′ it suffices to show that ĥ(E_{M}) ∩ {g′ ∈ E_{N} | g′ ≺_{N}^{∗} f′_{0}} = {e′_{0}, f′_{0}}. Assume the contrary, i.e. there exists g ∈ E_{M} such that ĥ(g) ≺_{N}^{∗} f′_{0} and ĥ(g) ∉ {e′_{0}, f′_{0}}. Since every receive event is preceded by its corresponding send event, we may assume that T_{M}(g) = s, i.e. g is a send event. Let e_{1} ∈ min(tr(M)) be a minimal event with e_{1} ≺_{M}^{∗} g, then ĥ(e_{1}) ≺_{N}^{∗} ĥ(g) ≺_{N}^{∗} f′_{0}. By Lemma 3 we obtain that ĥ(e_{1}) ≺_{N}^{∗} e′_{0}, since e_{1} is a send event. By the definition of μ we have μ(e_{1}) ≺_{N}^{∗} ĥ(e_{1}), hence μ(e_{1}) ≺_{N}^{∗} e′_{0}. Thus, by the choice of e_{0} we obtain μ(e_{1}) = e′_{0}. Therefore, e′_{0} ≺_{N}^{∗} ĥ(g) ≺_{N}^{∗} f′_{0}, which yields e′_{0} = ĥ(g) due to T_{M}(g) = s, contradiction.

Suppose finally that M′ matches N′ via h′ and consider some event g in M′. If e_{0} ≺_{M} g, then we also have e′_{0} ≺_{N} h′(g), since h′ preserves message types and h′(g) ∈ E_{N′}. Similarly, f_{0} ≺_{M} g implies e′_{0} ≺_{N} h′(g), which shows that h′ ∪ {e_{0} ↦ e′_{0}, f_{0} ↦ f′_{0}} is an embedding of M into N.

Remark 9. Proposition 8 yields an embedding algorithm, mapping the events of M in such a way that minimal events are mapped first, to the first event with the same type. This algorithm is of linear complexity if we keep min(tr(M)), resp. {μ(e) | e ∈ min(tr(M))} in two lists. More precisely, note that on each process of M, resp. N, there is at most one event e ∈ min(tr(M)), resp. μ(e). Moreover, we will record for each process of N the event on that process line which is of the form μ(e) for some e ∈ min(tr(M)), if there is one on that process. This additional information is needed in order to update the set of minimal elements of {μ(e) | e ∈ min(tr(M))} in constant time. For the complexity of our algorithm note first that min(tr(M′)) can be updated in constant time, since at most two new minimal events can occur on L(e_{0}) and L(f_{0}). Moreover, for e_{1} ∈ min(tr(M′)) \ min(tr(M)) we can check whether μ(e_{1}) is minimal in {μ(e) | e ∈ min(tr(M′))} in constant time, using the additional information mentioned above. This suffices, since μ(e_{1}) is a send event and every event preceding it in the visual order is a predecessor in the causal order, too. Hence, μ(e_{1}) is not minimal within {μ(e) | e ∈ min(tr(M′))} if and only if its process contains an event μ(e_{2}), e_{2} ∈ min(tr(M′)), such that μ(e_{2}) <_{N′} μ(e_{1}).

Note also that the embedding h suggested by Proposition 8 is actually unique. It is not difficult to show that an event e ∈ E_{M} is mapped by h to e′ ∈ E_{N} if and only if e′ is the minimal event w.r.t. ≺_{N}^{∗} such that e ↓ matches e′ ↓.

In the remaining of this section we consider the exact complexity of matching a template MSC with an MSC graph.

Definition 10 (Matching a template with an MSC graph). A template MSC M matches an MSC graph N if M matches some maximal path of N.

Matching a template against an MSC graph actually requires only paths of bounded length to be checked:

Proposition 11. Let N be an MSC graph and let M be a single template MSC such that M matches N. Then there is a path in N that embeds M and has length at most md, where m is the number of messages in M and d is the maximal length of a simple path in N (i.e. of a path where no node appears twice).

Proposition 11 yields a non-deterministic algorithm for matching a template with an MSC graph which guesses a path in N and verifies that the template matches the graph. The algorithm is polynomial in the size of the template and the number of nodes in the graph. The proposition below shows that matching is also NP-hard.

Proposition 12. Matching a single template MSC with an MSC graph is NPcomplete, even if the graph is acyclic.

Proof. It suffices to show that matching is NP-hard. For this, we reduce the satisfiability problem for formulas in conjunctive normal form (CNF-SAT) to the MSC matching problem.

Consider a formula ⋀_{j=1}^{k} C_{j} with clauses (disjunctions) C_{j} over the variables x_{1}, …, x_{l}. For each clause C_{j} we take two processes, P_{j} and R_{j}. Let m(j) denote a message from P_{j} to R_{j}. Note that the events of different messages m(i), m(j), i ≠ j, are not causally ordered. Then the template M is given as M = m(1) ⋯ m(k). The system graph N = ⟨S, τ, s_{0}, c⟩ contains for each variable x_{i} three states denoted as o_{i}, p_{i} and n_{i}, i.e. S = {o_{i}, p_{i}, n_{i} | 1 ≤ i ≤ l}. Let s_{0} = o_{1}. The edge set is given by τ = {(o_{i}, p_{i}), (o_{i}, n_{i}), (p_{j}, o_{j+1}), (n_{j}, o_{j+1}) | 1 ≤ i ≤ l, 1 ≤ j < l}. The assignment of MSC to states is as follows: for every i, c(o_{i}) = ∅, c(p_{i}) = {m(j) | x_{i} occurs in C_{j}} and c(n_{i}) = {m(j) | x̄_{i} occurs in C_{j}}. That is, c(p_{i}) contains messages associated to all clauses satisfied by x_{i} := true, whereas c(n_{i}) contains messages associated to all clauses satisfied by x_{i} := false. Thus, a maximal path in the MSC graph N corresponds exactly to an assignment of the variables. The single MSC M matches a maximal path of N if and only if the assignment given by the path satisfies all clauses.

4 Matching MSC Graphs

In this section, we discuss our extension of the matching algorithm to deal with MSC graphs. Adopting the same convention for matching two single MSCs, we call one of the MSC graphs the template (MSC) graph. The other graph is called the system (MSC) graph.

The template graph represents a collection of properties (behaviors), each defined by one of its maximal paths. Then for the or-semantics as defined below, the template corresponds to a non-deterministic choice among these behaviors, so an execution of the system needs to contain at least one of the executions

Connect Fail

and

P2

P3

P1

P3

P2

P1

Fig. 2. A template MSC graph.

described by the template. For the and-semantics an execution of the system matches the template if it contains all the executions of the template MSC graph.

Definition 13 (Matching a template graph with a system graph). Let M and N be two MSC graphs.

1. M or-matches N if there exists a maximal path ξ′ of N and a maximal path ξ of M which matches ξ′.

2. M and-matches N if there exists a maximal path ξ′ of N such that all maximal paths ξ of M match ξ′.

Consider the and-graph template in Fig. 2. This template matches the system of Fig. 1, since the system may alternate infinitely often between Connect and Fail.

The next lemmas present some fundamental properties of matching paths of MSC graphs. A subpath ξ′ of a path ξ = s_{0}, s_{1}, … in some graph G is a path of G of the form ξ′ = s_{i_{0}}, s_{i_{1}}, s_{i_{2}}, … with i_{0} < i_{1} < . . .. In this case, we denote ξ a superpath of ξ′.

Lemma 14. Let M, N be two MSC graphs and let ξ_{1}, ξ_{2} denote paths in M, N, resp. Let ξ_{1} match ξ_{2}. Then for every subpath ξ′_{1} of ξ_{1} and every superpath ξ′_{2} of ξ_{2}, ξ′_{1} matches ξ′_{2}.

Proposition 15. Let M, N be two MSC graphs and consider an infinite path ξ in M such that every state from ξ occurs infinitely often in ξ. Let C be the strongly connected component of M induced by the states from ξ. Consider also an infinite path χ in N and let C′ denote the strongly connected component of the states occurring infinitely often in χ. Then the following holds:

1. ξ matches χ if and only if msg(C) ⊆ msg(C′).

2. Let K denote a simple cycle within C and suppose that ξ matches χ. Then K^{ω} matches χ, too (here, K^{ω} denotes the infinite path KK …).

3. Let K̂ be a cycle containing all states from C′. Then ξ matches χ if and only if ξ matches K̂^{ω}.

Proof. Suppose first that ξ matches χ. Then, since embeddings preserve message types, it is easily seen that msg(C) ⊆ msg(C′). For the converse let χ = χ_{0}χ_{1} …, with χ_{i} finite paths such that every χ_{i}, i ≥ 1, contains all states from C′. Also, consider a linearization e_{1}e_{2} … of tr(ξ) satisfying the property that for each i, (e_{2i−1}, e_{2i}) is a message pair. We define an embedding h inductively by mapping (e_{2i−1}, e_{2i}) to events from χ_{i}, i ≥ 1. More precisely, h maps e_{2i−1} to the first event e′ occurring in c(χ_{i}) satisfying msg(e_{2i−1}) = msg(e′). Then, e_{2i} is mapped by h to the corresponding receive event of e′. By Lemma 5 it is easy to check that h preserves the causal order.

The second assertion of the proposition is obtained directly from Lemma 14, whereas the last assertion is a consequence of the first one.

4.1 The Complexity of OR-Matching

The next theorem shows that for or-matching two MSC graphs only finite paths have to be considered for an embedding. More precisely, for the recurrent part of a path only the message types of events are relevant. For a strongly connected component C and a state s we denote below a path from s to some node in C as a path from s to C.

Theorem 16. Let M = ⟨S, τ, s_{0}, c⟩ be a template graph and N = ⟨S′, τ′, s′_{0}, c′⟩ be a system graph. Then M or-matches N if and only if either there exists a finite maximal path of M which matches N, or there exist

– a simple cycle K in M and a simple path ξ from s_{0} to K,

– a strongly connected component C′ of N and a path χ from s′_{0} to C′,

such that ξ matches χ and msg(K) ⊆ msg(C′).

Proof. Suppose that M or-matches N via an infinite maximal path. Then, by Lemma 14 and Proposition 15(2) we also obtain a path of M of the form ξKK … which matches N, where K is a simple cycle and ξ is a simple path from s_{0} to K. Let ρ denote a path in N such that ξK^{ω} matches ρ. Moreover, let χ be a minimal prefix of ρ such that ξ matches χ and the corresponding suffix is a strongly connected component of N. Then, by applying Proposition 15(1), we obtain the result.

For the converse we may use again Proposition 15(1) in order to extend the embedding of ξ into χ to an embedding of ξK^{ω} into a path in N starting with χ.

First note that in Theorem 16 the path χ is in general not simple. But by Proposition 11 its length is bounded by size(ξ) · n, with size(ξ) denoting the number of messages in ξ, and n denoting the number of states in N. Note also that we can require above that C′ is a maximal strongly connected component, due to Lemma 14. Hence, an algorithm based on Theorem 16 would first compute in linear time all maximal strongly connected components of N. Then, for each maximal strongly connected component C′ consider the states s of M with msg(c(s)) ⊆ msg(C′) and the subgraph M_{C′} induced by these states. The algorithm checks whether there is some simple path ξ from s_{0} to some strongly connected component of M_{C′} which matches a path χ from s′_{0} to C′. (The length of χ is bounded by a polynomial in the size of ξ and the size of N.)

The complexity of the above algorithm basically derives from two problems: one consists of finding all simple paths from the initial node to a given subgraph, and the second one is the problem of matching a single template MSC with an MSC graph. Clearly, Theorem 16 directly yields an NP-algorithm for ormatching. Moreover, by Proposition 12 already the case where the template graph is a single node is NP-hard. Hence, we obtain:

Corollary 17. The or-matching problem for MSC graphs is NP-complete.

4.2 The Complexity of AND-Matching

For the and-matching problem we need to deal not only with strongly connected components, but also with states reachable from some strongly connected component. The reason is that some of the events in such states have to be mapped to events belonging to recurrent states in the system graph.

For an MSC graph M = ⟨S, τ, s_{0}, c⟩ let S_{c} ⊆ S denote the set of nodes belonging to some strongly connected component of M. For each state s ∈ S let us partition the events belonging to the single MSC c(s) associated with s in two sets c_{f}(s), c_{ω}(s) as follows. For each event e ∈ c(s) let e ∈ c_{ω}(s) if and only if there exist some state s′ ∈ S_{c}, some event e′ in c(s′) and a path ξ from s′ to s with e′ ≺_{ξ}^{∗} e for the causal order ≺_{ξ}^{∗} associated to the execution of ξ. We denote by E_{ω} the set of events {e | e ∈ c_{ω}(s), s ∈ S}. The set E_{ω} can be computed in polynomial time as follows: let E_{ω} := {e′ | e′ ∈ c(s′), s′ ∈ S_{c}}. Then for every e ∉ E_{ω}, e ∈ c(s), test whether there is some event e′ ∈ E_{ω}, e′ ∈ c(s′), such that s is reachable from s′ through a path ξ and e′ ≺_{ξ} e for the execution of that path. Note that e′ ≺_{ξ} e holds if and only if e′ ≺_{χ} e holds for any other path χ from s′ to s. Moreover, by Lemma 3 the condition e′ ≺_{ξ} e can be checked by examining the message types of e, e′. If the test is positive, then let E_{ω} = E_{ω} ∪ {e}. This step is repeated until no more events can be added. Note also that for every e ∈ c_{ω}(s) and e′ ∈ c(s) with e ≺_{c(s)}^{∗} e′, also e′ ∈ c_{ω}(s) holds. Moreover, for every message pair e_{1} <_{c} e_{2} in c(s) we have e_{1} ∈ c_{f}(s) if and only if e_{2} ∈ c_{f}(s) (this is easily checked using Lemma 3.) The set c_{f}(s) together with the visual order inherited from c(s) is thus a single MSC which we also denote by c_{f}(s) (analogously for c_{ω}(s)). By the previous remarks we have that the causal order of c(s) is the same as the causal order of c_{f}(s)c_{ω}(s). Finally, for s ∈ S_{c} we have c(s) = c_{ω}(s).

Theorem 18. Let M = ⟨S, τ, s_{0}, c⟩ be a template graph and N = ⟨S′, τ′, s′_{0}, c′⟩ be a system graph. Define a mapping ĉ : S → M by letting ĉ(s) = c_{f}(s). Let M̂ = ⟨Ŝ, τ̂, s_{0}, ĉ⟩ denote the MSC graph with states set Ŝ = {s ∈ S | ĉ(s) ≠ ∅} ∪ {s_{0}} and (s, s′) ∈ τ̂ if and only if s, s′ ∈ Ŝ such that ¬(s = s′ = s_{0}) and there is a path s = s_{1}, …, s_{k} = s′ in M satisfying ĉ(s_{i}) = ∅ for all 1 < i < k. Then M and-matches N if and only if there exists a subgraph C′ of N and a path χ from s′_{0} to C′ such that

1. All paths in M̂ match χ.

2. If M contains cycles then msg(E_{ω}) ⊆ msg(C′) and C′ is a strongly connected component of N.

Proof. First, note that the MSC graph M̂ is acyclic (since the only possible loop would be a self-loop of s_{0}, which has been excluded by definition).

Suppose that M and-matches N and consider a path ρ in N such that all maximal paths in M match ρ. If M is acyclic, hence M = M̂, then we are done by choosing an appropriate finite prefix χ of ρ. So suppose that S_{c} ≠ ∅, then ρ must be infinite. Let C′ be the strongly connected component containing exactly the states occurring infinitely often in ρ. Let ξ be a (finite) path from M̂. Then it is easy to verify that there exists a path σ in M such that the causal order of the execution of ξ is a prefix of the causal order of the execution of σ. Hence, ξ matches ρ, too. Let χ be a finite prefix of ρ such that all (finite) paths from M̂ match χ and the corresponding suffix is a strongly connected component of N. Finally, consider an event e in some c_{ω}(s), for some state s. Then there exists for each n ≥ 0 a path ξ from s_{0} to s such that the configuration e ↓ of the occurrence of e in the last node of ξ contains at least n events. Hence, there is some state s′ occurring in ρ infinitely often, such that msg(e) = msg(e′) holds for some event e′ in s′. This concludes one direction of the proof.

Conversely, suppose that M has cycles. Let ξ = s_{0}, s_{1}, … be a maximal (finite or infinite) path in M. Note that the causal order associated to the execution c(ξ) of ξ is identical to the causal order of c_{f}(ξ)c_{ω}(ξ), where c_{f}(ξ) = c_{f}(s_{0})c_{f}(s_{1}) … and c_{ω}(ξ) = c_{ω}(s_{0})c_{ω}(s_{1}) . . .. Moreover, c_{f}(s_{0})c_{f}(s_{1}) … is a finite MSC since there can be only a finite number of nodes s_{i} with c_{f}(s_{i}) ≠ ∅. Also, c_{f}(s_{0})c_{f}(s_{1}) … is the execution of a finite path in M̂, thus it matches χ. Since msg(E_{ω}) ⊆ msg(C′) we obtain similarly to Proposition 15 that the MSC c_{ω}(s_{0})c_{ω}(s_{1}) … matches K̂^{ω}, for some fixed cycle K̂ containing all the states from C′. Thus, ξ matches χK̂^{ω}, which shows the claim.

By the previous theorem we have to consider the problem of and-matching a single MSC against an acyclic MSC graph. The next proposition shows that for and-matching an acyclic graph it suffices to look for a mapping which is an embedding for all the paths (instead of embedding each path separately).

Proposition 19. Let M be an acyclic MSC graph and let N be a single MSC. Then M and-matches N if and only if there exists a mapping g : M → N which is an embedding for all paths in M.

Proof. Suppose that M and-matches N and let g_{ξ} denote an embedding of a maximal path ξ of M in N. Let Ξ denote the set of all maximal paths of M. Define a mapping g : M → N by letting g(e) = max{g_{ξ}(e) | ξ ∈ Ξ, e occurs on ξ}. Note that for a fixed event e the set {g_{ξ}(e) | ξ ∈ Ξ, e occurs on ξ} is totally ordered w.r.t. ≺_{N}^{∗}. This is due to the fifo semantics, since for each e, e′ with msg(e) = msg(e′) we have either e ⪯ e′ or e′ ⪯ e.

We show that g is an embedding for every path ξ ∈ Ξ. If e <_{c} f is a message pair in M, then g(e) <_{c} g(f) holds, due to the fifo semantics. Thus, suppose that e ≺_{ξ} f and e ≮_{c} f both hold, where ≺_{ξ} denotes the causal order associated to the execution of ξ. Let χ ∈ Ξ be a path also containing e, f. Note that we have e ≺_{χ} f due to M being acyclic. Hence, g_{χ}(e) ≺_{N} g_{χ}(f). By the definition of g we finally obtain g(e) ≺_{N} g(f).

The previous proposition shows that there exists a mapping g for matching all paths in M with N. This yields an NP-algorithm for matching an acyclic MSC graph M with a single MSC (note that after guessing the mapping g we test the embedding property for every pair of events e, f with e ≺_{ξ} f for some path ξ). We now show that we can even find a canonical mapping deterministically in polynomial time (similar to Proposition 8).

Proposition 20. Let M = ⟨S, τ, s_{0}, c⟩ be an acyclic MSC graph and let s ∈ S be a source node, i.e. a node without predecessors. Let N = ⟨E_{N}, <_{N}, L_{N}, T_{N}, P_{N}⟩ be a single MSC. Assume that M and-matches N and let h : c(s) → N be defined by

h(e) = e′ if e′ is minimal w.r.t. ≺_{N}^{∗} such that e ↓ matches e′ ↓

Let g : M → N be a mapping which is an embedding for all paths from M in N. We define a mapping g′ : M → N by letting g′|_{c(s)} = h and g′(e) = g(e) for every e ∉ c(s). Then g′ is also a mapping which embeds all paths of M into N.

Proof. It can be easily verified that for every event e ∈ c(s) and every mapping g : M → N which is an embedding for all paths in M (in particular for c(s)) one has h(e) ≺_{N} g(e). Therefore, if e ≺_{ξ}^{∗} f holds for the execution of a nonempty path ξ from s to s′ for two events e, f with e ∈ s and f ∈ s′, then also h(e) ≺_{N} g(f) holds.

Proposition 20 yields a polynomial-time algorithm for matching an acyclic and-graph with an MSC defined by a path. We first determine for each node s and for each event e ∈ c(s) the immediate predecessor events of e (w.r.t. the causal order) located in s and in the nodes preceding s. Then we embed a source node s of M and iterate this procedure with M \ {s}. When processing the current node s events in c(s) are mapped according to the partial order (starting with minimal elements) as suggested by Proposition 8. That is, a suitable event e ∈ min(tr(M)) is mapped to the minimal event e′ of the same type in N, such that e′ ↓ contains all events to which the immediate predecessor events of e were mapped to.

Together with Theorem 18 we obtain an NP-algorithm for the and-matching problem by first guessing a subgraph C′ of the system graph N and a path χ from the starting node of N to some node in C′. Then we verify deterministically that the acyclic MSC graph M̂ defined in Theorem 18 and-matches the single MSC corresponding to χ. Note that due to Proposition 19 we can bound the length of χ by a polynomial in the number of messages in M̂ and the number of nodes in N. Together with Proposition 12 we obtain:

Corollary 21. The and-matching problem for MSC graphs is NP-complete.

5 An Undecidable Problem

The matching problems considered previously were based on the paradigm that templates represent partial specifications of system behaviors. We show below that if we require that templates represent exact behaviors, then the or-matching problem is undecidable.

For the fifo semantics considered in this paper we show first that considering a message pair as a single letter we obtain an isomorphism between the causal orders of a natural subclass of message sequence charts and partial orders of semitraces. Semi-traces are objects known from the algebraic study of concurrency (for a survey on semi-traces see Chapter 12 in [5]).

Formally, assume that P = {P_{1}, …, P_{m}} is the set of processes. We associate an alphabet Σ = {m_{ij} | 1 ≤ i ≠ j ≤ m} and a non-commutation relation SD ⊆ Σ × Σ, SD = {(m_{ij}, m_{ik}) | j ≠ i ≠ k} ∪ {(m_{ij}, m_{jk}) | i ≠ j ≠ k}. The idea underlying SD is to consider in the precedence order the order between sends on the same process and receives ordered by the fifo condition (m_{ij}, m_{ik}), and receives followed by sends on the same process line (m_{ij}, m_{jk}). The complementary relation, SI = (Σ × Σ) \ SD, called semi-commutation relation, yields a rewriting system {ab → ba | (a, b) ∈ SI}, which will be also denoted by SI. A semi-trace [w] is a set of words, [w] = {v ∈ Σ^{∗} | w →^{∗}_{SI} v}. The concatenation of two semi-traces [u], [v] is defined as [u][v] = [uv]. It is an associative operation and the set of all semi-traces over (Σ, SI) together with the concatenation is a monoid with identity 1 = [ϵ], which is denoted (𝕄(Σ, SI), ·, 1). Note also that the relation SD is reflexive. Moreover, [w] = [w′] holds if and only if w can be rewritten into w′ by using symmetric rules only.

In the next proposition we show that a naturally arising subclass of MSCs can be identified with semi-traces. We restrict our consideration to MSCs satisfying the condition that in the visual representation no two message lines intersect. We denote this subclass as ordered MSCs. Clearly, ordered MSCs satisfy the fifo condition on the visual order. Note also that the syntactic concatenation of MSCs induces a concatenation operation for the associated causal orders, which is associative.

Proposition 22. Let M_{o} denote the set of ordered MSCs over the set of processes P = {P_{1}, …, P_{m}} and let (Σ, SI) be defined as above. Then the monoid of causal orders over M is isomorphic to (𝕄(Σ, SI), ·, 1).

Proof. Let M = ⟨E, <, L, T, P⟩ and define a homomorphism h : E_{M}^{∗} → Σ^{∗} by letting h(e) = m_{ij}, if e is a send event from P_{i} to P_{j}, and h(e) = λ if e is a receive event. To M we associate a language t_{M} over Σ^{∗}:

t_{M} = {h(z) | z ∈ E_{M}^{∗} is a linearization of ≺_{M}^{∗}}

Then we can show that t_{M} is a semi-trace over (Σ, SI). For this, we first define a linearization z_{0} ∈ E_{M}^{∗} of M inductively by choosing some message pair (e, f) of M satisfying

– e is minimal w.r.t. the visual order < in M

– for every g ∈ E_{M}: g < f ⇔ g = e

and letting z_{0} = efz′_{0}, where z′_{0} is defined accordingly for M′ := M \ {e, f}. (Note that the existence of e, f as above is due to M being an ordered MSC.) Then we claim that t_{M} = [h(z_{0})], i.e. t_{M} is the semi-trace associated to h(z_{0}). We show this by induction on the length of t_{M}. For lack of space, the details are left to the full version of the paper.

Traces [5] result from in symmetric rewriting rules, i.e. both SI and SD are symmetric relations. For the trace monoid given by the rules ab = ba, cd = dc it is known that one cannot decide for given regular languages L_{1}, L_{2} ⊆ {a, b, c, d}^{∗} whether [L_{1}] ∩ [L_{2}] is empty [3], where [L] = ∪_{u∈L}[u] denotes the closure of L

under →^{∗}_{SI}.

Proposition 23. Let M, N be two MSC graphs. Then it is undecidable whether there exist two maximal paths ξ_{1} in M, ξ_{2} in N such that the associated MSCs m_{1}, m_{2} have the same causal order under the fifo semantics.

Proof. We consider four processes, P = {P_{1}, P_{2}, P_{3}, P_{4}} and we denote by s_{a}, r_{a} a message pair from P_{1} to P_{2}, resp. by s_{b}, r_{b} a message pair from P_{2} to P_{1}. Dually, s_{c}, r_{c} denotes a message pair from P_{3} to P_{4}, whereas s_{d}, r_{d} is a message pair from P_{4} to P_{3}. Then we associate to each letter a, b, c, d an MSC as given by the mapping h, with h(x) = s_{x}r_{x}, for x ∈ {a, b, c, d}. Moreover, h induces a homomorphism from {a, b, c, d}^{∗} to M.

Note that for any word u over {a, b, c, d} the partial order tr(h(u)) consists of two totally ordered sequences, one over events between processes P_{1} and P_{2}, the other over events between P_{3} and P_{4}. Moreover, these total orders are completely independent. Viewed as a mapping from 𝕄(Σ, SI) to tr(M), h is injective. This, together with [3], concludes our proof.

Let us comment our results in the context of semi-trace languages. One cannot decide the emptiness of the intersection of two MSC graphs since given two regular languages L, K ⊆ Σ^{ω} and a semi-commutation relation SI over Σ, the question whether the intersection [L] ∩ [K] is nonempty is undecidable. In contrast, the or-matching problem of Section 4.1 can be expressed as a very particular instance of the above problem. Before going into some details, let us fix notations. For a language L ⊆ Σ^{∗}, we denote by L⊔⊔Σ^{∗} the shuffle of L and Σ^{∗}, i.e. the language {u_{1}v_{1}u_{2}v_{2} ⋯ u_{n}v_{n} | u_{1}u_{2} ⋯ u_{n} ∈ L, v_{i} ∈ Σ^{∗}}. The shuffle L⊔⊔Σ^{ω} for L ⊆ Σ^{∗} ∪ Σ^{ω} is defined analogously.

Formally, the or-matching problem for the semantics with gaps is equivalent to the question whether the intersection [L⊔⊔Σ^{ω}]∩[K] is empty or not, for regular languages L, K ⊆ Σ^{ω}. The crucial point now is that [L⊔⊔Σ^{ω}] has a very particular form. Suppose without loss of generality that L = UV^{ω}, with U, V ⊆ Σ^{∗} regular languages such that every element of V has the same alphabet A ⊆ Σ. Then UV^{ω}⊔⊔Σ^{ω} = (U⊔⊔Σ^{∗}) Inf(A), with Inf(A) = {u ∈ Σ^{ω} | |u|_{a} = ∞, ∀a ∈ A}. Moreover, [UV^{ω}⊔⊔Σ^{ω}] = [(U⊔⊔Σ^{∗})] Inf(A). But it is easy to check that U⊔⊔Σ^{∗} is a very simple regular language, a finite union of languages of the form Σ^{∗}a_{1}Σ^{∗}a_{2}Σ^{∗} ⋯ a_{k}Σ^{∗} for some letters a_{i} ∈ Σ. (This family of languages corresponds exactly to level ‘1/2’ in the concatenation hierarchy of Straubing-Thérien [10]). Finally, [Σ^{∗}a_{1}Σ^{∗}a_{2}Σ^{∗} ⋯ a_{k}Σ^{∗}] = ∪_{a_{i_{1}} ···a_{i_{k}} ∈[a_{1}···a_{k}]}Σ^{∗}a_{i_{1}}Σ^{∗} ⋯ a_{i_{k}}Σ^{∗}.

6 Conclusion

In this paper we presented specification and verification methods for MSCs, which employ languages of partially ordered executions. We were interested in the problem of deciding whether there is an execution of the given MSC system that matches the specification. We considered three alternative semantics and showed that the matching problem under both the or-semantics and the and-semantics is NP-complete. Under a semantics which allows no gaps in the specification the matching problem becomes the intersection of two MSC graphs. We showed that this problem is undecidable. Some open directions for further research include extending the framework by allowing and/or-graphs and negation, expressing the finite occurrence of certain events, and obtaining complementable specification formalisms.

References

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

2. H. Ben-Abdallah and S. Leue. Syntactic detection of process divergence and nonlocal choice in message sequence charts. In E. Brinksma, editor, Proceedings of theTools and Algorithms for the Construction and Analysis of Systems, Third International Workshop, TACAS’97, number 1217 in Lecture Notes in Computer Science, pages 259–274, Enschede, The Netherlands, 1997. Springer.

3. J. Berstel. Transductions and context-free languages. Teubner Studienbücher, Stuttgart, 1979.

4. M. Clerbout and M. Latteux. Partial commutations and faithful rational transductions. Theoretical Computer Science, 34:241–254, 1984.

5. V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.

6. J. Feigenbaum, J. Kahn, and C. Lund. Complexity results for pomset languages. SIAM Journal Disc. Math., 6(3):432–442, 1993.

7. ITU-T Recommendation Z.120, Message Sequence Chart (MSC), March 1993.

8. V. Levin and D. Peled. Verification of message sequence charts via template matching. In TAPSOFT (FASE)’97, Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 652–666, Lille, France, 1997. Springer.

9. M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures and domains, part 1. Theoretical Computer Science, 13:85–108, 1981.

10. J.-E. Pin. Syntactic semigroups. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 1, pages 679–738. Springer, Berlin-Heidelberg-New York, 1997.

11. V. R. Pratt. Modelling concurrency with partial orders. International Journal of Parallel Programming, 15(1):33–71, 1986.