Blaise Genest, Anca Muscholl, Helmut Seidl and Marc Zeitoun. Infinite-State High-Level MSCs: Model-Checking and Realizability. In Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan Eidenbenz and Ricardo Conejo, editors, Automata, Languages and Programming, volume 2380 of Lecture Notes in Computer Science, pages 657-668, Malaga, Spain, July 2002. Springer.

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.

Download: PDF Reference: Bibtex The original publication is available at