Matching Specifications for Message Sequence Charts

Anca Muscholl

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

Abstract. Message sequence charts (MSC) are widely used in the early design of communication protocols. They allow describing the communication skeleton of a system. We consider a basic verification task for MSC graphs, the matching problem via MSC templates. We characterize the complexity of checking properties which are expressible by andor templates, resp. by LTL formulas. Both problems are shown to be PSPACE-complete.

1 Introduction

Message sequence charts (MSC) are an ITU-standardized notation which is widely used for the early design of communication protocols. They describe in a graphical way how message passing is supposed to be performed between concurrent processes. Although MSCs 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 detect mistakes in the design, like race conditions [1] or non-local choice [2]. Some tools for performing basic verification tasks have been developed, [1, 3].

The problem considered in this paper is to verify certain properties of MSC graphs by means of template (MSC) graphs. Matching a template graph with a system graph means that a specific set of executions in the template is required to occur in an execution of the system, such that the causal order of events is preserved. The occurrence of executions is meant as an embedding, i.e. it allows gaps. (Actually, determining the existence of an exact mapping is easily seen to be undecidable, [7]). Two semantics have been already considered for template graphs, or-graphs resp. and-graphs, [7].

Here we focuss on specifications (templates) given as and-or MSC graphs, which can be seen as alternating transition systems with an associated causal order related to Mazurkiewicz traces, [5]. Like alternating automata on ω-words [10], it is more convenient to translate specifications into and-or MSC graphs than just or-graphs. The matching problem for and-or template graphs is shown to be PSPACE-complete. However, our proof shows somewhat surprisingly that and-or templates are not more expressive than or-templates (or and-templates). And-or MSC templates just provide a more succinct representation of specifications. They express properties given by shuffle ideals (of finite sets) and liveness conditions. We also consider the problem of specifying templates by LTL formulas, that is by matching the causal orders of sequences which satisfy a given formula. For this semantics we show that deciding the existence of a matching is PSPACE-complete, too. The paper is organized as follows: Sect. 2 gives basic notions and definitions, in Sect. 3 we consider the and-or matching problem, and Sect. 4 deals with the matching problem for LTL specifications.

2 Preliminaries

Definition 1 (MSC). A message sequence chart M = (E, <, P, L, T) is given by a poset (E, <) of events, a set P of processes, a mapping L : E → P that associates each event with a process, and a mapping T : E → {s, r} that describes the type of each event (send or receive).

The partial order < is called the visual order of events and it is obtained from the syntactical representation of the chart (e.g. represented according to the standard syntax ITU-Z 120). The visual order is induced by an acyclic relation <_{c} ∪ (⋃_{P ∈P} <_{P}) that is explained in the following. First, there is a one-to-one correspondence between send events, E ∩ T^{−1}(s), and receive events, E ∩ T^{−1}(r). Let M denote the graph of this correspondence, i.e. the set of messages. Then we have e <_{c} f for every message (e, f) ∈ M (message ordering). Secondly, for every process P ∈ P the set E ∩ L^{−1}(P) is totally ordered by <_{P} (process line ordering).

In general, the visual order provides more ordering than intended by the designer. Therefore every chart has an associated causal structure providing the intended ordering [1]. Causal structures are related to pomsets [9], event structures [8], and Mazurkiewicz traces [4]. A causal structure is obtained from a chart by means of a given semantics, which depends on the system architecture. Formally, the causal structure of a chart M = (E, <, P, L, T) is given as tr(M) = (E, ≺, P, L, T), where the only difference between M and tr(M) is the poset (E, ≺), with ≺ denoting the causal order. The partial order ≺ is generated by a so-called precedence relation ≺·, which depends on the implementation. The meaning is that for any two events e and f, we have e≺·f if and only if event e must terminate before event f starts.

As the semantics used throughout the paper, we define the precedence relation 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 first impose the following constraint on the visual order: For any messages (e, f), (e′, f′) ∈ M with e <_{P} e′ and L(f) = L(f′) = P′ for some P, P′ ∈ P we require that f <_{P′} f′. Let e, f ∈ E be two events. Then e≺·f for the fifo semantics if one of the following holds:

1. A send preceded by some event on the same process:

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

2. Message ordering: 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′) .

Slightly abusing the notation, we identify tr(M) with the set of all linearizations of the causal order of tr(M). We also write tr(α) for a sequence α ∈ E^{∞} and mean by that the set of all linearizations of the causal order associated with α.

Given two charts M_{i} = (E_{i}, <_{i}, P, L_{i}, T_{i}) over the same set of processes we define their product as the chart M_{1}M_{2} = (E_{1} ∪^{·} E_{2}, <, P, L_{1} ∪^{·} L_{2}, T_{1} ∪^{·} T_{2}), where < = <_{1} ∪ <_{2} ∪ ⋃_{P ∈P}(E_{1} ∩ L^{−1}(P)) × (E_{2} ∩ L^{−1}(P)).

Definition 2 (MSC graph). An MSC graph N = (S, τ, s_{0}, c, P) is given as a finite, directed graph (S, τ, s_{0}) with state set S, transition relation τ ⊆ S × S, source state s_{0} ∈ S, together with a mapping c associating each state s with a finite chart c(s) over the process set P.

Let ξ = s_{1}, s_{2}, … be a (possibly infinite) path in N, i.e. (s_{i}, s_{i+1}) ∈ τ for every i. The chart defined by ξ is given as c(ξ) = c(s_{1})c(s_{2}) . . .. We denote by tr(ξ) the causal structure associated with c(ξ), resp. by ≺_{ξ} the associated causal order.

A maximal path of N is a path in the graph which starts with the source state and is either infinite or it ends in a sink state.

In order to simplify the presentation we assume that in an MSC graph N every state s ∈ S is associated with a single event. This is no restriction, due to the following observation: If α = α_{1} ⋯ α_{k} denotes any topological sorting of the visual order of a chart M, then tr(α) = tr(M). Let M = c(s) for a state s ∈ S. We can replace s by a sequence of states s = s_{0} →^{α_{1}} s_{1} →^{α_{2}} ⋯ s_{k} and add transitions from s_{k} to all successors of s.

Definition 3 (Matching). Under a given semantics, a template M with the causal structure tr(M) = (E_{M}, ≺_{M}, L_{M}, T_{M}, P_{M}) matches an MSC 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),

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

– if e <_{c} f then h(e) <_{c} h(f) (preserving messages).

A path ξ_{1} in a graph M matches a path ξ_{2} in a graph N if the chart c(ξ_{1}) matches the chart c(ξ_{2}).

Under the fifo semantics it suffices to consider only the type and the location of events. Let P = {P_{1}, …, P_{m}} be the set of processes and let E = {s_{ij}, r_{ij} | 1 ≤ i ≠ j ≤ m}. The set E consists of abstract events and is related to any set of events E by means of a mapping ev : E → E. Consider a message (e, f) ∈ M with L(e) = P_{i}, L(f) = P_{j}. Then we let ev(e) = s_{ij} and ev(f) = r_{ij}. Let χ be a path in an MSC graph, then msg(χ) ⊆ E denotes the set {ev(e) | e occurs in c(χ)}. The mapping ev extends to a homomorphism ev : E^{∞} → E^{∞}. Assume that α is a topological sorting of c(χ). Let ev(χ) ∈ E^{∞} = E^{∗} ∪ E^{ω} denote the (finite or infinite) sequence of abstract events ev(α).

For the remaining of the paper we will refer to the elements of E simply as events. All notions introduced so far, e.g. precedence rules, causal order, matchings, can be transferred to the events in E.

3 And-Or MSC Graphs

An and-or MSC graph M = (S, τ, s_{0}, c, S_{∧}, S_{∨}, P) is given as an MSC graph where the set of states is partitioned in two sets, the set of and-states S_{∧} and the set of or-states S_{∨}.

Definition 4 (And-or MSC graphs). Let M = (S, τ, s_{0}, c, S_{∧}, S_{∨}, P) be an and-or MSC graph. A run R of M is a tree R = (X, →, x_{0}, ℓ, ev) with root x_{0} and nodes labelled by states, ℓ : X → S, such that:

1. x → y in R implies that (ℓ(x), ℓ(y)) ∈ τ.

2. Every node x ∈ X with ℓ(x) = s ∈ S_{∨} has one successor in R, if {s′ | τ(s, s′)} ≠ ∅, otherwise it has no successor.

3. Every node x ∈ X with ℓ(x) = s ∈ S_{∧} has exactly k successors in R, all labelled differently, where k = |{s′ | τ(s, s′)}|.

Moreover, ev : X → E labels each node x by the event ev(e), where e = c(ℓ(x)).

A run R is called maximal if all leaves are labelled by states without any successors in M and the root is labelled by the source state.

An and-or MSC graph is an example for alternating transition systems. It can be used for specifying scenarios between a component of a system and the environment. Here, the moves of the environment are modelled as usually as universal moves, i.e. the component is required to meet its specification no matter how the environment behaves. Consider for example the and-or graph in Fig. 1, where state N_{1} is an and-state and N_{2}, N_{3} are or-states. For simplicity, the states are labelled by messages, not by single events. The MSC graph expresses that there are infinitely many connections requested by P_{2} (from P_{1}), and all of them are either successful or P_{2} gets into an infinite loop requesting a connection. Moreover, each time when process P_{2} requests a connection, it expects (several) data transmissions from P_{3}.

Definition 5 (And-or matching). Given a template M as an and-or MSC graph and a system N as an MSC graph. We say that the template matches the system if there is some maximal run R of M and a maximal path χ of N such that every path in R matches χ.

P_{1}  P_{2} P_{1}  P_{2}  P_{2}  P_{3} connect-req connect  data N_{1} N_{2}  N_{3} s_{1} r_{1} s_{2}  r_{2}  s_{3} r_{3}

Fig. 1. An and-or MSC graph.

Consider again the and-or template graph M of the above example. In every maximal run of M the and-node N_{1} occurs infinitely often. Therefore, a maximal run of M matches an MSC N only if N contains infinitely many events of the same type as s_{1}, r_{1}. This holds also for s_{2}, r_{2}, since every maximal run of M includes paths N_{1}^{k}N_{2} for every k, and we have r_{1}≺·s_{2}≺·r_{2}. The situation differs for node N_{3}. We might have a maximal run where N_{3} occurs on every path just once, before N_{2}. But we do not have any events e in N_{1}, f in N_{3} such that e≺·f. Hence, s_{3} for example can be mapped for each occurrence of the node N_{3} in the run of M to the same event in the MSC N. (The specification given by M is in some sense incomplete, it does not correspond to the intuition given above). Moreover, the combination between states occurring infinitely often and dependency between events makes matching for and-or templates to a quite complex task.

3.1 The Complexity of And-Or Matching

Our main result is that matching and-or template graphs is PSPACE-complete. Thus, and-or matching appears to be computationally more difficult than matching or-templates, resp. and-templates. The latter problems have been shown to be NP-complete, [7].

The next proposition gives the lower bound for the and-or matching problem.

Proposition 1. The problem whether an and-or template graph matches a system graph is PSPACE-hard.

Proof. We give a reduction from TQBF, i.e. the question whether a quantified Boolean formula is true or not. Suppose that Q_{0}x_{0} ⋯ Q_{l}x_{l} F (x_{0}, …, x_{l}) is in prenex normal form, with Q_{i} ∈ {∃, ∀} and F a quantifier-free formula in 3-CNF. That is, F = C_{1} ∧ ⋯ ∧ C_{m}, with C_{j} denoting disjunctions of at most three literals. For simplifying notations, the graphs M, N described below are such that states are labelled by charts (instead of events). Recall that this can be easily translated to a labelling by events.

Let the set of processes be P = {P_{i}, P′_{i}, R_{i}, R′_{i} | 0 ≤ i ≤ l}. Let also p_{i} (resp. p′_{i}) denote a message from P_{i} to P′_{i} (resp. from P′_{i} to P_{i}). Analogously, let n_{i} resp. n′_{i} denote a message from R_{i} to R′_{i}, resp. from R′_{i} to R_{i}. The system graph N (see also Fig. 2) is the single MSC p′_{1}p_{1}n′_{1}n_{1} ⋯ p′_{l}p_{l}n′_{l}n_{l}. Note that the events e with L(e) ∈ {P_{i}, P′_{i}} are totally ordered in the causal order. Similarly, all events e with L(e) ∈ {R_{i}, R′_{i}} are totally ordered.

P_{i}  P′_{i}  R_{i}  R′_{i} p′_{i}  n′_{i} p_{i}  n_{i}

Fig. 2. The system graph.

The template graph M = (S, τ, s_{0}, c, S_{∨}, S_{∧}) is given by the vertex set

S = {s_{i}, s_{i}^{+}, s_{i}^{−} | 0 ≤ i ≤ l} ∪ {t_{i}, t_{i,1}, t_{i,2}, t_{i,3} | 1 ≤ i ≤ m} ∪ {t} ,

and the transition relation τ ⊆ S × S:

\begin{matrix}τ = \{(s_{i}, s_{i}^{+}), (s_{i}, s_{i}^{−}), (s_{j}^{+}, s_{j+1}), (s_{j}^{−}, s_{j+1}) | 0 ≤ i, j ≤ l, j ≠ l\} ∪ \\ \{(s_{l}^{+}, t), (s_{l}^{−}, t)\} ∪ \{(t, t_{i}) | 1 ≤ i ≤ m\} ∪ \{(t_{i}, t_{i,1}), (t_{i}, t_{i,2}), (t_{i}, t_{i,3}) | 1 ≤ i ≤ m\} \end{matrix}

For s ∈ S we define s ∈ S_{∧} if and only if either s = s_{i} and Q_{i} = ∀, or s = t. That is, the nodes s_{i}, 0 ≤ i < l, are of type corresponding to the quantifier Q_{i}. Moreover, the node t is an and-node corresponding to the conjunction of the clauses. All remaining nodes are or-nodes. The states s_{i}^{+}, s_{i}^{−} are labelled by single messages (see also Fig. 3):

c(s) = \{ \begin{matrix}p_{i} & for s = s_{i}^{+}, 0 ≤ i ≤ l \\ n_{i} & for s = s_{i}^{−}, 0 ≤ i ≤ l \end{matrix}

Let C_{j} = x_{j,1} ∨ x_{j,2} ∨ x_{j,3} be a clause. If x_{j,1} = x_{k} is a positive literal then let c(t_{j,1}) = n′_{k}. For a negative literal x_{j,1} = x̄_{k} we let c(t_{j,1}) = p′_{k}. The definition of c(t_{j,2}), c(t_{j,3}) is similar, depending on x_{j,2} resp. x_{j,3}. For example, in Fig. 3 we represented the clause x_{1} ∨ x̄_{2} ∨ x_{3}. All remaining states are labelled by ∅.

…  ⋮⋮ p_{0} n_{0}  p_{l} n_{l} (Q_{0})  (Q_{l})  (∀)  (∃)  n′_{1} p′_{2} n′_{3}

Fig. 3. The template graph.

There is a natural bijection between the assignments σ : {x_{1}, …, x_{n}} → {t, f} for F and the paths from s_{0} to t in M. Formally, if s_{i}^{+} belongs to a path then x_{i} is assigned the value t, whereas if s_{i}^{−} belongs to a path, then x_{i} is assigned the value f. It is not difficult to verify that a run R of M matches the system chart N if and only if every path in R from s_{0} to t defines an accepting assignment for F. Hereby, we choose for every clause a leaf corresponding to a true literal. The (easy) proof is left to the reader.

3.2 Matching and-or templates in PSPACE

Showing the lower bound for the and-or matching problem was quite straightforward, which is not the case with the upper bound. Actually, it is a priori not clear why it would be possible to restrict the and-or matching problem to a finite instance of matching. The aim of the next propositions is to give a decomposition of maximal runs in an and-or template graph in two parts. The first part is a polynomially bounded tree, all paths of which have to be matched against a finite path in the system. The remaining part is the so-called recurrent part, for which only (abstract) events have to be recorded, all of which have to occur in a loop of the system graph.

Let x = x_{1}, …, x_{k} = y be a path in a run R = (X, →, x_{0}, ℓ, ev). We write x ≺ y whenever the event ev(x) precedes causally the event ev(y) in the sequence ev(x_{1}) ⋯ ev(x_{k}). Let y ↓= {x ∈ X | x ≺ y}.

Definition 6. Let R = (X, →, x_{0}, ℓ, ev) be a run in an and-or MSC graph M. Let X_{e} = {x ∈ X | ev(x) = e}. We define a set of events E_{fin}(R) ⊆ E as

E_{fin}(R) = {e ∈ E | max{|x↓ | | x ∈ X_{e}} < ∞} .

By X_{fin}(R) ⊆ X we denote the subset of vertices X_{fin}(R) = {x ↓| ev(x) ∈ E_{fin}(R)}.

Intuitively, E_{fin}(R) ⊆ E contains all events which require an exact matching for the corresponding nodes x (resp. paths from x ↓), i.e. for nodes x with ev(x) ∈ E_{fin}(R). Equivalently, for nodes x with events from E \ E_{fin}(R) the only information needed is ev(x) ∈ E. Consider again the and-or template of Fig. 1. We have E_{fin}(R) ⊆ {s_{32}, r_{32}} for every maximal run R of M. Put it another way, s_{21} ∉ E_{fin}(R), since N_{1} has to repeat infinitely often on some path of the run. Moreover, s_{12} ∉ E_{fin}(R) since every maximal run includes paths N_{1}^{k}N_{2} for every k and r_{1}≺·s_{2}. The situation differs for node N_{3}. We might have a maximal run where N_{3} occurs on every path just once, before N_{2}. Since there is no dependence from N_{1} to N_{3} all events e with ev(e) = s_{32} can be mapped to the same event on the system path (similarly for ev(e) = r_{32}). Thus, node N_{2} represents the bounded part, which has to be matched exactly against the system.

Notations: Let M = (S, τ, s_{0}, c, S_{∧}, S_{∨}) be an and-or graph and consider a run R = (X, →, x_{0}, ℓ, ev). Let ρ = (x_{1}, x_{2}, …) be a sequence of vertices from X, then ℓ(ρ) denotes the sequence of states (ℓ(x_{1}), ℓ(x_{2}), …) ∈ S^{∞}. For x ∈ X we denote by R_{x} the subtree of R with root x and by π(x) the path (x_{0}, …, x_{k}) from x_{0} to x = x_{k}. By π_{fin}(x) we denote the subsequence (x_{i_{1}}, …, x_{i_{l}}) of π(x) containing exactly the vertices from X_{fin}(R). (I.e. we have x_{j} ∈ X_{fin}(R) if and only if j = i_{m} for some m.) More generally, for a (finite or infinite) path ρ in R we denote by π_{fin}(ρ) the subsequence of vertices of ρ belonging to X_{fin}(R).

Remark 1. Note that for any path ρ in R the subsequence π_{fin}(ρ) is finite. Moreover, there exists a sequence of events α ∈ (E \ E_{fin}(R))^{∞} such that ev(ρ) and ev(π_{fin}(ρ))α define the same causal structure, i.e. tr(ev(ρ)) = tr(ev(π_{fin}(ρ))α).

Lemma 1. Let M be an and-or template graph and consider a run R′ of M. Let e ∈ E_{fin}(R′). Then there exists a run R = (X, →, x_{0}, ℓ, ev) of M satisfying the following conditions:

1. Every path of R is a subpath of some path in R′.

2. Let x, y, z ∈ X be such that x ∈ X_{e} and y, z ∈ x↓. Then ℓ(y) = ℓ(z) implies y = z.

3. We have E_{fin}(R′) ⊆ E_{fin}(R). Moreover, if R′ is maximal, then R is maximal, too.

The previous lemma says that it suffices to consider maximal runs R where for every path ρ the subsequence π_{fin}(ρ) has length at most |S|, with S denoting the set of states of M.

Lemma 2. Let M be an MSC and let χ be a loop in an MSC graph such that msg(M) ⊆ msg(χ). Then M matches χ^{ω}.

Lemma 3. Let R be a run in an and-or template graph M and let N be a system graph. Then R matches N if and only if R matches some path in N of the form χ_{0}χ_{1}^{ω}, where χ_{0} is a finite path and χ_{1} is a (possibly empty) loop.

Lemma 4. Let R = (X, →, x_{0}, ℓ, ev) be a run in an and-or template graph M and let χ = χ_{0}χ_{1}^{ω} be a path in a system graph N such that R matches χ. Then we have

1. (E \ E_{fin}(R)) ⊆ msg(χ_{1})

2. Every path ρ in R is such that π_{fin}(ρ) matches χ_{0}χ_{1}^{|S|}.

The proposition below says that it is sufficient to consider maximal runs R such that any two vertices x, y ∈ X_{fin}(R) which are such that the subpaths π_{fin}(x) and π_{fin}(y) have the same sequence of state labels also have equal subtrees. We assume in the following w.l.o.g. that the source state of the template has no incoming edges, thus the root x_{0} of a run R belongs to X_{fin}(R).

Proposition 2. Let M be an and-or template graph and consider a run R of M. Then a run R′ = (X, →, x_{0}, ℓ, ev) of M exists such that:

1. For all vertices x, y ∈ X_{fin}(R′) with ℓ(π_{fin}(x)) = ℓ(π_{fin}(y)) we have R′_{x} = R′_{y}.

2. For every path ρ′ in R′, the causal structure tr(π_{fin}(ρ′)) is equal to tr(π_{fin}(ρ)), for some path ρ in R.

3. If R satisfies Lemma 1, then R′ satisfies Lemma 1, too. Moreover, if R is maximal, then R′ is also maximal and we have finally E_{fin}(R) ⊆ E_{fin}(R′).

Proof. Consider a maximal run R satisfying Lem. 1. We assume that R does not satisfy the first condition of the statement and we consider two vertices x, y from X_{fin}(R) with ℓ(π_{fin}(x)) = ℓ(π_{fin}(y)), but R_{x} ≠ R_{y}. Clearly, x, y are incomparable w.r.t. the successor relation in R, since they are labelled by the same state. We claim that the run R′ obtained from R by replacing R_{y} by a copy of R_{x} satisfies Conds. (2) and (3) of the statement. To see this, note that for every maximal path ρ′ in R′ containing y there is a corresponding maximal path ρ in R containing x such that ℓ(π_{fin}(ρ)) = ℓ(π_{fin}(ρ′)) (here π_{fin} is meant w.r.t. R.) Moreover, the nodes in ρ \ π_{fin}(ρ) (resp. in ρ′ \ π_{fin}(ρ′)) are labelled by events from E \ E_{fin}(R).

For subtrees R′ of R we define m(R′) as

m(R′) = max{|π_{fin}(ρ)| | ρ is a path in R′} .

Note that m(R′) is defined w.r.t. R, i.e. π_{fin}(ρ) is given by R. We show below by induction on m(R′) how to obtain a run R̂ satisfying the requirement of the proposition with regard to X_{fin}(R). This means that any two vertices x, y of R̂ with ℓ(π_{fin}(x)) = ℓ(π_{fin}(y)) will have equal subtrees. However, we will obtain E_{fin}(R) ⊆ E_{fin}(R̂). If E_{fin}(R) = E_{fin}(R̂) then we are done, since in this case π_{fin}(ρ) as given by R is the same as π_{fin}(ρ) as given by R̂. Otherwise we repeat the construction with R̂. After at most |E| steps we obtain the desired run.

For defining R̂ we consider all vertices x ∈ X_{fin}(R) at depth 1, i.e. π_{fin}(x) = (x_{0}, x) has length 1. Suppose that x is labelled by s ∈ S and let us choose some fixed vertex x_{s} of this kind, for each possible s. Consider the subtree R_{x_{s}} rooted at x_{s}. Clearly, m(R_{x_{s}}) < m(R). By induction we may assume that any two vertices y, z in R_{x_{s}} with ℓ(π_{fin}(y)) = ℓ(π_{fin}(z)) have equal subtrees. We can replace all subtrees R_{x} for x with π_{fin}(x) = (x_{0}, x), ℓ(x) = s, by R_{x_{s}} and obtain the desired run R̂.

The next proposition gives the characterization for deciding the existence of a matching from an and-or graph into an MSC graph.

Proposition 3. Let M be an and-or template graph and let N be a system graph. Let S denote the set of states of M. Then M matches N if and only if there exist

1. A set of events G ⊆ E of M.

2. A path χ in N to a strongly connected component C of N with G ⊆ msg(C).

3. A tree T_{0} = (X, →, x_{0}, ℓ, ev) labelled by ℓ : X → S, ev : X → E, such that for any two distinct nodes x, y ∈ X which are either siblings or comparable in T_{0}, ℓ(x) ≠ ℓ(y). Moreover, every path of T_{0} matches the path χ in N.

4. A maximal run R of M such that for every maximal path ρ of R we have tr(ev(ρ)) = tr(ev(ξ)α), where ξ is a maximal path in T_{0} and α ∈ G^{∞}.

Proof. By Lem. 3, 4 and Prop. 2 we can assume that we have a maximal run R = (X, →, x_{0}, ℓ, ev) of M which satisfies the first condition of Prop. 2 and matches a path χχ_{1}^{ω} in N. Let C denote the strongly connected component represented by χ_{1}. Let G = E \ E_{fin}(R), then G ⊆ msg(χ_{1}) by Lem. 4. By assumption, the root x_{0} of R belongs to X_{fin}(R). Define first a tree T′_{0} = (X_{fin}(R), →, ℓ, x_{0}) by letting x → y in T′_{0} whenever there is a path x → x_{1} → ⋯ → x_{k} → y in R with x_{i} ∉ X_{fin}(R) for every i. The tree T_{0} is now defined by identifying two vertices x, y in T′_{0} whenever ℓ(π(x)) = ℓ(π(y)). By Cond. (1) of Prop. 2 this step is welldefined. By Rem. 1 every maximal path ρ in R has the same causal structure as ev(π_{fin}(ρ))α, for some α ∈ G^{∞}. Moreover, π_{fin}(ρ) is a maximal path in T_{0}.

Remark 2. The length of the path χ in the previous proposition can be bounded by a polynomial in |S| and |S′|, where S′ is the set of states of N.

The next lemma implies that we can check the last condition of Prop. 3 in PSPACE.

Lemma 5. Let M = (S, τ, s_{0}, c, S_{∧}, S_{∨}, P) be an and-or template graph. Suppose that we are given a state r ∈ S, a set L ⊆ S of sink states in M and a set of events I(s) ⊆ E for each s ∈ L, as well as a set G ⊆ E. Then we can check in PSPACE whether a maximal run R = (X, →, x_{0}, ℓ, ev) of M exists satisfying the following conditions:

1. State r labels the root x_{0} of R.

2. For every state s ∈ L there is at least one leaf labelled by s. Moreover, every non-leaf node x is labelled by ev(x) ∈ G.

3. For every path y →^{+} x in R to a leaf x with ℓ(x) = s we have either ev(y) ∈ I(s) or y = x_{0}.

Theorem 1. There is a PSPACE algorithm for deciding whether an and-or template graph M matches a system graph N.

Proof. We have to check in PSPACE the existence of T_{0}, R, G, χ, C as in Prop. 3. Clearly, G ⊆ E and C can be guessed and stored. By Rem. 2 the path χ can also be stored. The problem arises with T_{0}, since the size of T_{0} might be exponential (however, the depth and the degree of T_{0} are linear in |S|, hence we can store paths of T_{0}.) The main idea is to guess the tree T_{0} implicitly, in a DFS traversal where we store together with the current path also the (ordered sequence of) siblings of the intermediate nodes. Using Lem. 5 it is sufficient to verify the existence of a suitable run R piecewise, along with the DFS traversal.

The (nondeterministic) PSPACE algorithm works as follows (see also Fig. 4). Assume that the current path in T_{0} is s_{0}, …, s_{k}, k < |S|, and that we also stored the (ordered) sequence L_{i} of siblings of s_{i} in T_{0}, 1 ≤ i < k. Moreover, we guessed sets of events I(s) ⊆ E for all s ∈ L_{i+1} and we verified the existence of maximal runs satisfying Lem. 5 with r = s_{i}, L = L_{i+1}, G. If k < |S| then we can either proceed with DFS and guess s_{k+1}, L_{k+1}, …, or s_{k} is a leaf in T_{0} and we apply Lem. 5 with L = ∅. Furthermore we verify that (s_{0}, …, s_{k}) is downward closed w.r.t. the causal order in the run built so far by using Lem. 5. For this, we use the sets I(s_{i}). Using Lem. 5 we checked that a suitable run with root s_{i−1} exists s.t. every node on the path from s_{i−1} to s_{i} is labelled by an event from I(s_{i}). Thus, it suffices to check for each i < j ≤ k and each e′ ∈ I(s_{i}) that e′≺· ev(s_{j}) is not satisfied. Finally, we verify that the path (s_{0}, …, s_{k}) matches χ and then we backtrack in the DFS traversal.

3.3 Specifying Properties by And-Or Templates

Consider a template given as an and-or MSC graph M. We want to determine the set of event sequences L(M) ⊆ E^{∞} which are described by M. That is, we let α ∈ L(M) if α = ev(χ) for some path χ in a system graph such that there is a matching of some maximal run of M into the path χ. Prop. 3 gives us the basic description of the set L(M) as a finite union over languages L(M, T_{0}, G) ⊆ E^{∞}, where T_{0} is a tree labelled by states of M and G ⊆ E is a set of events of M. Let α ∈ L(M, T_{0}, G) if

– every event e ∈ G occurs infinitely often in α, and

– every path of T_{0} matches α.

For any language F ⊆ E^{∗} we denote by F ⊔⊔E^{∗} the shuffle ideal generated by F, i.e. F ⊔⊔E^{∗} = {v_{0}u_{1}v_{1} ⋯ u_{n}v_{n} | u_{1} ⋯ u_{n} ∈ F, v_{i} ∈ E^{∗}}. For subsets G ⊆ E

s_{0}I(s_{1}) s_{1} I(s_{2}) s_{2}⋮ s_{k} ⋮ I(s_{k}) L_{1} L_{2} L_{k}
Fig. 4. Guessing the maximal run R, resp. the path (s_{0}, …, s_{k}) in T_{0}.

we denote by inf(G) the set of sequences α ∈ E^{∞} where every event e ∈ G occurs infinitely often. For α ∈ E^{∞} we denote below by tr(α) ⊆ E^{∞} the set of linearizations of the causal order of α. Let tr(F) = ∪_{α∈F} tr(α).

Proposition 4. Let M be an and-or MSC template graph over the event set E. The language L(M) associated with the template M has the form

⋃_{F,G}(F ⊔⊔E^{∗})inf(G) ,

where F ⊆ E^{∗} is a finite set, tr(F) = F and G ⊆ E.

Proof. Any language L(M, T_{0}, G) as described above is a (finite) intersection of languages of the form (tr(α)⊔⊔E^{∗})inf(G), where α is such that tr(α) ⊆ tr(β) for some path χ in T_{0} with β = ev(χ). Let α, β ∈ E^{∗}, G, H ⊆ E. Then we have

(tr(α)⊔⊔E^{∗})inf(G) ∩ (tr(β)⊔⊔E^{∗})inf(H) = (Γ ⊔⊔E^{∗})inf(G ∪ H) ,

where Γ contains all sequences γ of minimal length such that for some α′ ∈ tr(α), β′ ∈ tr(β), both α′, β′ are subwords of γ. Moreover, it is not hard to check that Γ can be chosen s.t. tr(Γ) = Γ.

4 Matching LTL Properties

In this section we consider properties (templates) specified by linear temporal logic. Our LTL formulas define finite or infinite strings over the alphabet E = {s_{ij}, r_{ij} | 1 ≤ i ≠ j ≤ m} of events. They are built over atomic propositions P_{e}, e ∈ E, using the temporal operators X (nexttime) and U (until), and the Boolean connectives ∧, ∨, ¬.

Definition 7 (LTL Matching Problem). Given a template M as an LTL formula ϕ and a system N as an MSC graph. We say that the template M matches the system N if there is some sequence of events α ∈ E^{ω} such that α ⊧ ϕ and α matches some maximal path in N.

Theorem 2. The LTL matching problem is PSPACE-complete.

We will show the above theorem in a more general setting using automata. Recall that every state of the system graph N is labelled by a single event. Thus we can easily associate to N a nondeterministic Büchi automaton A_{N} of the same size such that L(A_{N}) consists of all maximal executions of N. On the other hand it is well-known how to associate to every LTL formula ϕ an alternating Büchi automaton with O(|ϕ|) states accepting exactly the sequences satisfying ϕ, see e.g. [10]. Moreover, for every alternating Büchi automaton with n states there is an equivalent nondeterministic Büchi automaton with 2^{O(n)} states which can be built off-line using only O(n) space, see [6]. We are thus led to a language-theoretical formulation of the LTL matching problem:

The matching problem for alternating automata: Given an alternating Büchi automaton A_{M} and a nondeterministic Büchi automaton A_{N} over E. Then we ask whether some sequences α ∈ L(A_{M}), β ∈ L(A_{N}) exist such that α matches β.

Proposition 5. The matching problem for alternating automata is PSPACEcomplete.

Proof. Due to the PSPACE-hardness of the satisfiability problem for LTL it suffices to show the upper bound. Let A_{M} denote an alternating Büchi automaton and let B_{M} = (Q, E, q_{0}, δ, F) denote an equivalent nondeterministic Büchi automaton as given by [6]. Let A_{N} = (Q′, E, q′_{0}, δ′, F′) denote the nondeterministic Büchi automaton representing the system. By an immediate modification and extension of Lem. 3 we note that M matches N if and only if final states f ∈ F, f′ ∈ F′ exist such that

– for some paths π = (q_{0}, …, q_{k} = f) in B_{M}, resp. π′ = (q′_{0}, …, q′_{l} = f′) in A_{N}, the execution of π matches the execution of π′, i.e. ev(π) matches ev(π′), and – some loops ρ around f, resp. ρ′ around f′ exist satisfying msg(ρ) ⊆ msg(ρ′).

Clearly, we can choose π of length k ≤ |Q|. But since |Q| ∈ 2^{O(n)} we cannot guess π directly. On the other hand, we have to match π against π′ and this means that we have to consider permutations, due to the causal order of the events. To overcome these problems we consider below the shape of π and π′ in more details and exploit the fact that matching allows gaps.

We denote by C_{1}, C_{2}, …, C_{m} the maximal strongly connected components of the subgraph of A_{N} induced by π′. Thus, π′ = π′_{1} ⋯ π′_{m}, such that w.l.o.g. π′_{i} induces C_{i}. The components C_{i} are naturally ordered, and we write C_{i} < C_{j} for i < j.

Consider some mapping μ matching π into π′. We decompose π into maximal segments π_{i}, π = π_{1} ⋯ π_{r}, such that for every segment π_{i} all events of ev(π_{i}) are matched by μ into the same component π′_{j}, for some j. Let C(i) ∈ {1, …, m} denote the component C_{j} with μ(e) ∈ π′_{j} for all events e in ev(π_{i}). Note that for every 1 ≤ i < j ≤ r, C(i) > C(j) implies that e ⊀ e′ for all events e, e′ with e occurring in ev(π_{i}), resp. e′ occurring in ev(π_{j}). Otherwise, by the definition of matchings, we would require that μ(e) ≺ μ(e′), contradicting C(i) > C(j). The second basic observation is that every segment π_{i} matches any path ρ_{i} in C(i) which visits every state of C(i) sufficiently often. Therefore, we claim that a path π in B_{M} matches some path π′ in A_{N} if and only if

– some maximal strongly connected components C_{1}, …, C_{m} exist in A_{N} with q′_{0} ∈ C_{1}, as well as transitions from C_{i} to C_{i+1} for all i,

– π can be decomposed as π = π_{1} ⋯ π_{r} such that for every i some component C(i) ∈ {C_{1}, …, C_{m}} exists such that msg(π_{i}) ⊆ msg(C(i)),

– for every 1 ≤ i < j ≤ r with C(i) > C(j) we have e ⊀ e′ for all events e, e′ occurring in ev(π_{i}), resp. in ev(π_{j}).

We already showed one direction of the claim. For the converse, assume that C_{i}, π_{j}, C(k) exist as above. Let ρ_{k} denote the subpath of π consisting of all segments π_{i} with C(i) = C_{k}. Since msg(ρ_{k}) ⊆ msg(C_{k}) and C_{k} is strongly connected, we can determine a path ρ′_{k} looping in C_{k} such that ρ_{k} matches ρ′_{k} (via some mapping μ). Moreover, ρ′_{k} can be chosen such that ρ′ = ρ′_{1} ⋯ ρ′_{m} is a path in A_{N}. Finally the last condition above yields that π matches ρ′. This is seen by noting that for any events e, e′ occurring in ev(ρ_{i}), resp. ev(ρ_{j}), e ≺ e′ implies i < j, hence also μ(e) ≺ μ(e′).

The PSPACE algorithm on input A_{M}, A_{N} works as follows. First we guess m ≤ |Q′| strongly connected components C_{1}, …, C_{m} of A_{N}, such that q′_{0} ∈ C_{1} and there exist edges from C_{i} to C_{i+1}, for all i. We guess the path π in B_{M} and its decomposition π = π_{1} ⋯ π_{r} on-line. The only information which is (temporarily) stored concerns event types, which are required in order to check that e ⊀ e′ for all events e, e′ occurring in ev(ρ_{i}), resp. ev(ρ_{j}), satisfying i < j and C(i) > C(j). For this step, we have to record at most m subsets of E. More precisely, assume that E_{1}, …, E_{m} ⊆ E are initially empty. Along with guessing π_{i} and some C(i) = C_{k} we store msg(π_{i}) ⊆ E and check that for no events e ∈ E_{j}, e′ ∈ msg(π_{i}) we have e≺·e′, whenever C_{k} < C_{j} (i.e. k < j). Then we add msg(π_{i}) to E_{k}. Moreover, we verify that msg(π_{i}) ⊆ msg(C(i)).

5 Conclusion

In this paper we characterized the complexity of matching template MSCs which are given as and-or graphs, resp. by LTL formulas. Under these semantics the matching problem becomes PSPACE-complete. However, our proofs show that the increased complexity (compared with previously investigated template semantics, e.g. or-graphs) is due rather to a more succinct representation than to more expressiveness. This leads to the question whether using negations resp. requiring that certain events occur only finitely often might increase the expressiveness.

Acknowledgments. The referees are kindly acknowledged for the careful reading and the suggestions for improving the presentation of the paper.

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 the Tools 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. H. Ben-Abdallah and S. Leue. Mesa: Support for scenario-based design of concurrent systems. In B. Steffen, editor, Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 4th International Conference, TACAS’98, number 1384 in Lecture Notes in Computer Science, pages 118–135, Lisbon, Portugal, 1998. Springer.

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

5. A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.

6. S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321–330, 1984.

7. A. Muscholl, D. Peled, and Z. Su. Deciding properties of message sequence charts. In M. Nivat, editor, Proceedings of the 1st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’98), Lisbon, Portugal, 1998, number 1378 in Lecture Notes in Computer Science, pages 226–242, Berlin-Heidelberg-New York, 1998. Springer.

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

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

10. M. Y. Vardi. An automata-theoretic approach to linear-temporal logic. In F. Moller and G. Birtwistle, editors, Logics for concurrency, number 1043 in Lecture Notes in Computer Science, pages 238–266, Berlin-Heidelberg-New York, 1996. Springer.