Name
Abstract | ||
|---|---|---|
We describe the design of (several variants of) a local parallel model-checking algorithm for the alternation-free fragment of the 碌-calculus. It exploits a characterisation of the problem for this fragment in terms of two-player games. For the corresponding winner, our algorithm determines in parallel a winning strategy, which may be employed for debugging the underlying system interactively, and is designed to run on a network of workstations. Depending on the variant, its complexity is linear or quadratic. A prototype implementation within the verification tool Truth shows promising results in practice. |
Year | Venue | Keywords |
|---|---|---|
2002 | SPIN | local parallel model checking,two-player game,local parallel model-checking algorithm,underlying system interactively,verification tool truth,winning strategy,prototype implementation,corresponding winner,alternation-free fragment,model checking |
DocType | ISBN | Citations |
Conference | 3-540-43477-1 | 17 |
PageRank | References | Authors |
0.96 | 17 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Benedikt Bollig | 1 | 427 | 35.02 |
| Martin Leucker | 2 | 1639 | 112.68 |
| Michael Weber | 3 | 240 | 11.93 |