Publication details
Distributed Explicit Fair Cycle Detection
| Basic information | |
|---|---|
| Original title: | Distributed Explicit Fair Cycle Detection |
| Authors: | Ivana Černá, Radek Pelánek |
| Further information | |
|---|---|
| Citation: | ČERNÁ, Ivana and Radek PELÁNEK. Distributed Explicit Fair Cycle
Detection. In SPIN Workshop 2003. Portland (Oregon, USA):
Springer -Verlag, 2003. p. 49-74, 25 pp. ISBN 3-540-40117-2.Export BibTeX@inproceedings{489731, author = {Černá, Ivana and Pelánek, Radek}, address = {Portland (Oregon, USA)}, booktitle = {SPIN Workshop 2003}, keywords = {distributed model checking; cycle detection}, language = {eng}, location = {Portland (Oregon, USA)}, isbn = {3 -540-40117-2},pages = {49 -74},publisher = {Springer -Verlag},title = {Distributed Explicit Fair Cycle Detection}, year = {2003} } |
| Original language: | English |
| Field: | Informatics |
| Type: | Article in Proceedings |
| Keywords: | distributed model checking; cycle detection |
The fair cycle detection problem is at the heart of both LTL and fair CTL model checking. This paper presents a new distributed scalable algorithm for explicit fair cycle detection. Our method combines the simplicity of the distribution of explicitly presented data structure and the features of symbolic algorithm allowing for an efficient parallelisation. If a fair cycle (i.e. counterexample) is detected, then the algorithm produces a cycle, which is in general shorter than that produced by depth-first search based algorithms. Experimental results confirm that our approach outperforms that based on a direct implementation of the best sequential algorithm.
Related projects:
- Automated Verification of Parallel and Distributed Systems
- Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
