## Realizability and Verification of MSC Graphs

*Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis*
Scenario-based specifications such as message sequence charts (MSC)
offer an intuitive and visual way of describing design requirements.
MSC-graphs allow convenient expression of multiple scenarios, and
can be viewed as an early model of the system that can be subjected
to a variety of analyses. Problems such as LTL model checking are known
to be decidable for the class of bounded MSC-graphs.

Our first set of results concerns checking
*realizability* of bounded MSC-graphs.
An MSC-graph is realizable if there is a distributed
implementation that generates precisely the behaviors in the graph.
There are two notions of realizability, *weak* and
*safe*, depending on whether or not
we require the implementation to be deadlock-free.
It is known that for a set of MSCs, weak realizability is coNP-complete
while safe realizability has a polynomial-time solution. We establish that for
bounded MSC-graphs, weak realizability is, surprisingly, undecidable,
while safe is in Expspace.

Our second set of results concerns verification of MSC-graphs.
While checking properties of a graph G, besides verifying
all the scenarios in the set L(G) of MSCs specified by G, it is
desirable to verify all the scenarios in the set L^w(G)---the *closure*
of G, that contains the implied scenarios that any distributed
implementation of G must include.
For checking whether a given MSC
M is a possible behavior, checking M in L(G) is NP-complete, but checking
M in L^w(G) has a quadratic solution.
For temporal logic specifications, considering the closure makes the
verification problem harder: while checking
LTL properties of L(G) is Pspace-complete and checking *local*
properties has polynomial-time solutions,
even for boolean combinations of
local properties of L^w(G), verifying acyclic graphs is coNP-complete
and verifying bounded graphs is undecidable.

*Proceedings of the
13th International
Conference on Computer-Aided Verification*
(CAV'01), 2001.