Name
Abstract | ||
|---|---|---|
We show that verification techniques for timed automata based on the Alur and Dill region-graph construction can be applied to much more general kinds of systems, including asynchronous untimed systems over unbounded integer variables. We follow this approach in proving that the model-checking problem for the n-process Bakery algorithm is decidable, for any fixed n. We believe this is the first decidability proof for this problem to appear in the literature. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1016/S1571-0661(05)80751-0 | Electronic Notes in Theoretical Computer Science |
Keywords | DocType | Volume |
model checking,real time | Journal | 39 |
Issue | ISSN | Citations |
3 | Electronic Notes in Theoretical Computer Science | 4 |
PageRank | References | Authors |
0.42 | 9 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xiaoqun Du | 1 | 225 | 12.32 |
| C.R. Ramakrishnan | 2 | 24 | 1.47 |
| Scott A. Smolka | 3 | 2959 | 249.22 |