A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles
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 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 counter-examples.
KeywordsModel Check Reachable State Strongly Connect Component Seed State Quotient Graph
Unable to display preview. Download preview PDF.
- R. Bloem, H. N. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in n log n symbolic steps. In these proceedings.Google Scholar
- R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eighth Conference on Computer Aided Verification (CAV’96), pages 428–432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.Google Scholar
- J. R. Büchi. On a decision method in restricted second order arithmetic. In Proceedings of the 1960 International Congress on Logic,Methodology, and Philosophy of Science, pages 1–11. Stanford University Press, 1962.Google Scholar
- E. Clarke, O. Grumberg, K. McMillan, and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the Design Automation Conference, pages 427–432, San Francisco, CA, June 1995.Google Scholar
- J.W. de Bakker and D. Scott. A theory of programs. Unpublished notes, IBM Seminar, Vienna, 1969.Google Scholar
- E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposiumof Logic in Computer Science, pages 267–278, June 1986.Google Scholar
- R. H. Hardin, Z. Har’El, and R. P. Kurshan. COSPAN. In Eighth Conference on Computer Aided Verification (CAV’ 96), pages 423–427. Springer-Verlag, 1996. LNCS 1102.Google Scholar
- R. H. Hardin, R. P. Kurshan, S. K. Shukla, and M. Y. Vardi. A new heuristic for bad cycle detection using BDDs. In O. Grumberg, editor, Ninth Conference on Computer Aided Verification (CAV’97), pages 268–278. Springer-Verlag, Berlin, 1997. LNCS 1254.Google Scholar
- R. Hojati, R. K. Brayton, and R. P. Kurshan. BDD-based debugging of designs using language containment and fair CTL. In C. Courcoubetis, editor, Fifth Conference on Computer Aided Verification (CAV’ 93), pages 41–58. Springer-Verlag, Berlin, 1993. LNCS 697.Google Scholar
- R. Hojati, H. Touati, R. P. Kurshan, and R. K. Brayton. Efficient ωregular language containment. In Computer Aided Verification, pages 371–382,Montréal, Canada, June 1992.Google Scholar
- R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.Google Scholar
- O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages,New Orleans, January 1985.Google Scholar
- K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.Google Scholar
- D. M. R. Park. Fixpoint induction and proofs of program properties. Machine Intelligence, 5, 1970.Google Scholar
- F. Somenzi. Symbolic state exploration. Electronic Notes in TheoreticalComputer Science, 23, 1999. http://www.elsevier.nl/locate/entcs/volume23.html.
- H. J. Touati, R. K. Brayton, and R. P. Kurshan. Testing language containment for ω-automata using BDD’s. In 1991 International Workshop on Formal Methods in VLSI Design, Miami, FL, January 1991.Google Scholar
- M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposiumon Logic in Computer Science, pages 322–331, Cambridge, UK, June 1986.Google Scholar
- A. Xie and P. A. Beerel. Implicit enumeration of strongly connected components. In Proceedings of the International Conference on Computer-AidedDesign, pages 37–40, San Jose, CA, November 1999.Google Scholar