Distributed Explicit Fair Cycle Detection

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ČERNÁ Ivana PELÁNEK Radek

Year of publication 2003
Type Article in Proceedings
Conference SPIN Workshop 2003
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords distributed model checking; cycle detection
Description 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:

You are running an old browser version. We recommend updating your browser to its latest version.