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

Blaise Genest, Anca Muscholl, Helmut Seidl, Marc Zeitoun

Publikation: Beitrag in Buch/Bericht/KonferenzbandKonferenzbeitragBegutachtung

29 Zitate (Scopus)

Abstract

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.

OriginalspracheEnglisch
TitelAutomata, Languages and Programming - 29th International Colloquium, ICALP 2002, Proceedings
Redakteure/-innenPeter Widmayer, Stephan Eidenbenz, Francisco Triguero, Rafael Morales, Ricardo Conejo, Matthew Hennessy
Herausgeber (Verlag)Springer Verlag
Seiten657-668
Seitenumfang12
ISBN (Print)3540438645, 9783540438649
DOIs
PublikationsstatusVeröffentlicht - 2002
Extern publiziertJa
Veranstaltung29th International Colloquium on Automata, Languages, and Programming, ICALP 2002 - Malaga, Spanien
Dauer: 8 Juli 200213 Juli 2002

Publikationsreihe

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

Konferenz

Konferenz29th International Colloquium on Automata, Languages, and Programming, ICALP 2002
Land/GebietSpanien
OrtMalaga
Zeitraum8/07/0213/07/02

Fingerprint

Untersuchen Sie die Forschungsthemen von „Infinite-state high-level MSCs: Model-checking and realizability“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren