Distributed Explicit Fair Cycle Detection: Set Based Approach
by
Ivana Černá,
Radek Pelánek,
December 2002, 24 pages.
FIMU-RS-2002-09.
Available as Postscript,
PDF.
Abstract:
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.