Multiple State and Single State Tableaux for Combining Local and Global Nodel Checking

  • Armin Biere
  • Yunshan Zhu
  • Edmund M. Clarke
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)


The verification process of reactive systems in local model checking [2,9,28] and in explicit state model checking [14,16] is on-the-fly. Therefore only those states of a system have to be traversed that are necessary to prove a property. In addition, if the property does not hold, than often only a small subset of the state space has to be traversed to produce a counterexample. Global model checking [8,24] and, in particular, symbolic model checking [6,23] can utilize compact representations of the state space, e.g. BDDs [5], to handle much larger designs than what is possible with local and explicit model checking. We present a new model checking algorithm for LTL that combines both approaches. In essence, it is a generalization of the tableau construction of [2] that enables the use of BDDs but still is on­the­fly.


Model Check Linear Temporal Logic Kripke Structure Strongly Connect Component Symbolic Model Check 
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]
    I. Beer, S. Ben-David, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A. Landver, P. Paanah, Y. Rodeh, G. Ronin, and Y. Wolfsthal. Rulebase: Model checking at IBM. In CVA‘97, number 1254 in LNCS, pages 480–483. Springer-Verlag, 1997.Google Scholar
  2. [2]
    G. Bhat, R. Cleaveland, and O. Grumberg. Efficient on-the-fly model checking for CTL*. In LICS‘95. IEEE Computer Society, 1995.Google Scholar
  3. [3]
    A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS‘99, LNCS. Springer, 1999.Google Scholar
  4. [4]
    J. Bradfield and C. Stirling. Local model checking for infinite state spaces. Theorectical Computer Science, 96:157–174, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [5]
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8), 1986.Google Scholar
  6. [6]
    J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98, 1992.Google Scholar
  7. [7]
    E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking.Formal Methods in System Design, 10:47–71, 1997.CrossRefGoogle Scholar
  8. [8]
    E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs: Workshop, LNCS. Springer, 1981.Google Scholar
  9. [9]
    R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27, 1990.Google Scholar
  10. [10]
    M. Dam. CTL*and ECTL* as fragments of the modal mu-calculus. Theoretical Computer Science, 126, 1994.Google Scholar
  11. [11]
    D. L. Dill. The MurΦ verification system. In CAV‘96, LNCS. Springer, 1996.Google Scholar
  12. [12]
    Y. Dong, X. Du, Y.S. Ramakrishna, C. T. Ramkrishnan, I. V. Ramakrishnan, S. A. Smolka, O. Sokolsky, E. W. Starck, and D. S. Warren. Fighting livelock in the i-protocol: tiA comparative study of verification tools. In TACAS‘99, LNCS. Springer, 1999.Google Scholar
  13. [13]
    E. A. Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back. Science of Computer Programming, 8, 1986.Google Scholar
  14. [14]
    R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proceedings 15th Workshop on Protocol Specification, Testing, and Verification. North-Holland, 1995.Google Scholar
  15. [15]
    T. A. Henzinger, O. Kupferman, and S. Qadeer. From Pre-historic to Post-modern symbolic model checking. In CAV‘98, LNCS. Springer, 1998.Google Scholar
  16. [16]
    G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 5(23) 1997.Google Scholar
  17. [17]
    H. Iwashita and T. Nakata. CTL model checking based on forward state traversal. In ICCAD‘96. ACM, 1996.Google Scholar
  18. [18]
    H. Iwashita, T. Nakata, and F. Hirose. Forward model checking techniques oriented to buggy design. In ICCAD‘97. ACM, 1997.Google Scholar
  19. [19]
    A. Kick. Generierung von Gegenbeispielen und Zeugen bei der Modellprüfung. PhD thesis, Fakultät für Informatik, Universität Karlsruhe, 1996.Google Scholar
  20. [20]
    D. Kozen. Results on the propositional µ-calculus. Theoretical Computer Science, 27, 1983.Google Scholar
  21. [21]
    O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Symposium on Principles of Programming Languages, New York, 1985. ACM.Google Scholar
  22. [22]
    D. E. Long, A. Browne, E. M. Clarke, S. Jha, and W. R. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In CAV‘94, LNCS. Springer, 1994.Google Scholar
  23. [23]
    K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.Google Scholar
  24. [24]
    J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int. Symp. in Programming, 1981.Google Scholar
  25. [25]
    K. Ravi, K. L. McMillan, T. R. Shiple, and F. Somenzi. Approximation and decomposition of binary decision diagrams. In DAC‘98. ACM, 1998.Google Scholar
  26. [26]
    K. Ravi and F. Somenzi. High-density reachability analysis. In ICCAD‘95. ACM, 1995.Google Scholar
  27. [27]
    F. Reffel. Modellprüfung von Unterlogiken von CTL*. Masterthesis, Fakultät für Informatik, Universität Karlsruhe, 1996.Google Scholar
  28. [28]
    C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89, 1991.Google Scholar
  29. [29]
    M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1), 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Armin Biere
    • 2
  • Yunshan Zhu
    • 2
    • 1
  • Edmund M. Clarke
    • 2
  1. 1.Verysys Design Automation, IncFremontUSA
  2. 2.Computer Science DepartmentCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations