TY - GEN
T1 - Infinite-state high-level MSCs
T2 - 29th International Colloquium on Automata, Languages, and Programming, ICALP 2002
AU - Genest, Blaise
AU - Muscholl, Anca
AU - Seidl, Helmut
AU - Zeitoun, Marc
N1 - Funding Information:
✩ Work partly supported by the European Community Research Training Network HPRN-CT-2002-00283 “Games and Automata for Synthesis and Validation” (GAMES) and the ACI Sécurité Informatique 2003-22 (VERSYDIS). * Corresponding author. Current affiliation: LaBRI, Université Bordeaux 1 – CNRS, 351, Cours de la Libération, 33405 Talence cedex, France. E-mail addresses: [email protected] (B. Genest), [email protected] (A. Muscholl), [email protected] (H. Seidl), [email protected] (M. Zeitoun). 1 Current affiliation: IRISA – CNRS, Campus de Beaulieu, 35042 Rennes, France. 2 Current affiliation: TU München, I2, Boltzmannstr. 2, 85748 Garching, Germany.
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84869187985&partnerID=8YFLogxK
U2 - 10.1007/3-540-45465-9_56
DO - 10.1007/3-540-45465-9_56
M3 - Conference contribution
AN - SCOPUS:84869187985
SN - 3540438645
SN - 9783540438649
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 657
EP - 668
BT - Automata, Languages and Programming - 29th International Colloquium, ICALP 2002, Proceedings
A2 - Widmayer, Peter
A2 - Eidenbenz, Stephan
A2 - Triguero, Francisco
A2 - Morales, Rafael
A2 - Conejo, Ricardo
A2 - Hennessy, Matthew
PB - Springer Verlag
Y2 - 8 July 2002 through 13 July 2002
ER -