## Model Checking of Message Sequence Charts

*Rajeev Alur and
Mihalis Yannakakis*
Scenario-based specifications such as message sequence charts (MSC)
offer an intuitive and visual way of describing design requirements.
Such specifications focus on message exchanges among communicating
entities in distributed software systems.
Structured specifications such as MSC-graphs and
Hierarchical MSC-graphs
(HMSC) allow convenient expression of multiple scenarios, and
can be viewed as an early *model* of the system.
In this paper, we present a comprehensive study of the problem
of verifying whether this model
satisfies a temporal requirement given by an automaton,
by developing algorithms for the different cases
along with matching lower bounds.

When the model is given as an MSC, model checking can be done
by constructing a suitable automaton for the linearizations
of the partial order specified by the MSC, and the problem is
coNP-complete. When the model is given by an MSC-graph, we consider two
possible semantics depending on the *synchronous*
or *asynchronous* interpretation of concatenating two MSCs.
For synchronous model checking of MSC-graphs and HMSCs,
we present algorithms whose time complexity is
proportional to the product of the size of the description
and the cost of processing
MSCs at individual vertices. Under the asynchronous interpretation,
we prove undecidability of the model checking problem.
We, then, identify a natural requirement of *boundedness*,
give algorithms to check boundedness,
and establish asynchronous model checking
to be PSPACE-complete for bounded MSC-graphs
and EXPSPACE-complete for bounded HMSCs.

In *Proceedings of the
Tenth International Conference on Concurrency Theory*
(CONCUR'99),
Lecture Notes in Computer Science 1664,
Springer-Verlag, pp. 114--129, 1999.