A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles

Kavita Ravi, Roderick Bloem, and Fabio Somenzi

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


Detection of fair cycles is an important task of many model checking algorithms. When the transition system is represented symbolically, the standard approach to fair cycle detection is the one of Emerson and Lei. In the last decade variants of this algorithm and an alternative method based on strongly connected component decomposition have been proposed. We present a taxonomy of these techniques and compare the performance of representatives of each major class on a collection of real-life examples. Our results indicate that the Emerson-Lei procedure is the fastest, but other algorithms tend to generate shorter counterexamples.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:39
Maintainer sjohnson@cs.indiana.edu.
Start Conference Manager
Conference Systems