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

  • Kavita Ravi
  • Roderick Bloem
  • Fabio Somenzi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)


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.


Model Check Reachable State Strongly Connect Component Seed State Quotient Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    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
  2. [2]
    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
  3. [3]
    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
  4. [4]
    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
  5. [5]
    J.W. de Bakker and D. Scott. A theory of programs. Unpublished notes, IBM Seminar, Vienna, 1969.Google Scholar
  6. [6]
    E. A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8:275–306, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  7. [7]
    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
  8. [8]
    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
  9. [9]
    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
  10. [10]
    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
  11. [11]
    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
  12. [12]
    L. Kantorovitch. The method of successive approximations for functional equations. Acta Mathematica, 71:63–97, 1939.zbMATHCrossRefMathSciNetGoogle Scholar
  13. [13]
    Y. Kesten, A. Pnueli, and L.-o. Raviv. Algorithmic verification of linear temporal logic specifications. In International Colloquium on Automata, Languages, and Programming (ICALP-98), pages 1–16, Berlin, 1998. Springer. LNCS 1443.CrossRefGoogle Scholar
  14. [14]
    R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.Google Scholar
  15. [15]
    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
  16. [16]
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.Google Scholar
  17. [17]
    D. M. R. Park. Fixpoint induction and proofs of program properties. Machine Intelligence, 5, 1970.Google Scholar
  18. [18]
    F. Somenzi. Symbolic state exploration. Electronic Notes in TheoreticalComputer Science, 23, 1999.
  19. [19]
    R. Tarjan. Depth first search and linear graph algorithms. SIAM Journal of Computing, 1:146–160, 1972.zbMATHCrossRefMathSciNetGoogle Scholar
  20. [20]
    A. Tarski. A lattice-theoretic fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.zbMATHMathSciNetGoogle Scholar
  21. [21]
    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
  22. [22]
    H. J. Touati, R. K. Brayton, and R. P. Kurshan. Testing language containment for ω-automata using BDD’s. Information and Computation, 118(1):101–109,April 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  23. [23]
    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
  24. [24]
    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

Copyright information

© Springer-VerlagBerlin Heidelberg 2000

Authors and Affiliations

  • Kavita Ravi
    • 1
  • Roderick Bloem
    • 2
  • Fabio Somenzi
    • 2
  1. 1.Cadence Design SystemsUSA
  2. 2.University of Colorado at BoulderUSA

Personalised recommendations