Name
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. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/j.jcss.2005.09.007 | Journal of Computer and System Sciences |
Keywords | Field | DocType |
message sequence chart,asynchronous communication,model checking,communication protocol | Model checking,Concurrency,Computer science,Decidability,Theoretical computer science,Communicating automata,Visual notation,Realizability,Communications protocol,Bounded function | Conference |
Volume | Issue | ISSN |
72 | 4 | 0022-0000 |
ISBN | Citations | PageRank |
3-540-43864-5 | 38 | 1.72 |
References | Authors | |
25 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Blaise Genest | 1 | 304 | 25.09 |
| Anca Muscholl | 2 | 1179 | 74.92 |
| Helmut Seidl | 3 | 1468 | 103.61 |
| Marc Zeitoun | 4 | 288 | 24.51 |