Realizability and Verification of MSC Graphs

Rajeev Alur, Kousha Etessami, Mihalis Yannakakis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 E upxpspace. 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 ∈ L(G) is NP-complete, but checking M ∈ 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 P upspace-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. .
Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publication28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages12
ISBN (Electronic) 978-3-540-48224-6
ISBN (Print) 978-3-540-42287-7
Publication statusPublished - 2001


Dive into the research topics of 'Realizability and Verification of MSC Graphs'. Together they form a unique fingerprint.

Cite this