Infinite-state high-level MSCs: Model-checking and realizability

Blaise Genest, Anca Muscholl, Helmut Seidl, Marc Zeitoun

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

29 Scopus citations


We consider three natural classes of infinite-state HMSCs: globally-cooperative, locally-cooperative and local-choice HMSCs. We show first that model-checking for globally-cooperative and locally-cooperative HMSCs has the same complexity as for the class of finite-state (bounded) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient in space than for locally-cooperative HMSCs. We also show that locally-cooperative and local-choice HMSCs can be always implemented by communicating finite states machines, provided we allow some additional (bounded) message data. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.

Original languageEnglish
Title of host publicationAutomata, Languages and Programming - 29th International Colloquium, ICALP 2002, Proceedings
EditorsPeter Widmayer, Stephan Eidenbenz, Francisco Triguero, Rafael Morales, Ricardo Conejo, Matthew Hennessy
PublisherSpringer Verlag
Number of pages12
ISBN (Print)3540438645, 9783540438649
StatePublished - 2002
Externally publishedYes
Event29th International Colloquium on Automata, Languages, and Programming, ICALP 2002 - Malaga, Spain
Duration: 8 Jul 200213 Jul 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2380 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference29th International Colloquium on Automata, Languages, and Programming, ICALP 2002


Dive into the research topics of 'Infinite-state high-level MSCs: Model-checking and realizability'. Together they form a unique fingerprint.

Cite this