Analysis of symbolic SCC hull algorithms

Abstract

The Generalized SCC Hull (GSH) algorithm of [11] can be instantiated to obtain many symbolic algorithms for the detection of fair cycles in a graph.We present a modified GSH with improved convergence properties, and we use it to study—both in theory and experimentally—the performance of various algorithms employed in symbolic model checkers. In particular, we show that the algorithm of Emerson and Lei [4] has optimal complexity among those that can be derived from GSH.We also propose an early termination check that allows the Lockstep algorithm [1] to detect the existence of a fair cycle before an entire SCC has been examined. Our experimental evaluation confirms that no one method dominates the others, and identifies some of the factors that impact run times besides those accounted for by the theoretical analysis.