Realizability of high-level message sequence charts: Closing the gaps

  • Lohrey M
  • 3


    Mendeley users who have this article in their library.
  • 14


    Citations of this article.


We study the notion of safe realizability for high-level message sequence charts (HMSCs) (Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP 2001), Crete (Greece), Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001, pp. 797-808). We show that safe realizability is EXPSPACE-complete for bounded HMSCs but undecidable for the class of all HMSCs. This solves two open problems from Alur et al. Moreover we prove that safe realizability is also EXPSPACE-complete for the larger class of globally-cooperative HMSCs. © 2003 Elsevier B.V. All rights reserved.

Author-supplied keywords

  • Complexity
  • Message sequence charts
  • Verification

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Markus Lohrey

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free