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.
