| |
|
|
Fair Cycle Detection: A New Algorithm and a Comparative StudyFabio Somenzi AbstractDetection of fair cycles is a central problem in model checking. For instance, the existence of a cycle in a transition structure supplied with appropriate fairness conditions signals the violation of a linear-time property. Typical fairness constraints impose that certain conditions occur infinitely often during a (non-terminating) computation.When states and transitions are enumerated explicitly, fair cycles can be detected in linear time by enumerating the strongly connected components of the transition structure. However, known symbolic algorithms, which cannot rely on depth-first search, are not linear; the most widely used, due to Emerson and Lei, requires a quadratic number of preimage computations (steps) in the worst case. In this talk we present a new symbolic algorithm for fair cycle detection that requires n log n steps. The new algorithm is based on lockstep search and improves over the strongly-connected component enumeration algorithm of Xie and Beerel. We also present a taxonomy of existing symbolic fair cycle detection algorithms, and compare lockstep search to the algorithm of Emerson and Lei and to other representatives of the major taxa. Our comparison combines complexity analysis with experimental evaluation. Complexity analysis of symbolic algorithms raises some issues that strongly argue in favor of the joint theoretical and experimental approach. Joint work with Roderick Bloem, Hal Gabow, and Kavita Ravi.
Slides. |
| Contact |
| ©2002-2018 U.C. Regents |