Model checking and transitive-closure logic

  • Neil Immerman
  • Moshe Y. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


We give a linear-time algorithm to translate any formula from computation tree logic (CTL or CTL*) into an equivalent expression in a variable-confined fragment of transitive-closure logic FO(TC). Traditionally, CTL and CTL* have been used to express queries for model checking and then translated into μ-calculus for symbolic evaluation. Evaluation of μ-calculus formulas is, however, complete for time polynomial in the (typically huge) number of states in the Kripke structure. Thus, this is often not feasible, not parallelizable, and efficient incremental strategies are unlikely to exist. By contrast, evaluation of any formula in FO(TC) requires only NSPACE[logn]. This means that the space requirements are manageable, the entire computation is parallelizable, and efficient dynamic evaluation is possible.


Model Check Temporal Logic Boolean Variable Linear Temporal Logic Kripke Structure 
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.


  1. [BBG94]
    I. Beer, S. Ben-David, D. Geist, R. Gewirtzman and M. Yoel, “Methodology and System for Practical Formal Verification of Reactive Hardware,” in Computer Aided Verification, Proc. 6th Int. Conference, D. L. Dill, ed., LNCS 818, 1994, Springer-Verlag, 182–193.Google Scholar
  2. [BVW94]
    O. Bernholtz, M.Y. Vardi and P. Wolper, “An Automata-Theoretic Approach to Branching-Time Model Checking,” in Computer Aided Verification, Proc. 6th Int. Conference, D. L. Dill, ed., LNCS 818, 1994, Springer-Verlag, 142–155.Google Scholar
  3. [BCM92]
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and L.J. Hwang, “Symbolic Model Checking: 1020 States and Beyond,” Information and Computation 98(2) (1992), 142–170.Google Scholar
  4. [CE81]
    E.M. Clarke and E.A. Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” in Proc. Workshop on Logic of Programs, LNCS 131, 1981, Springer-Verlag, 52–71.Google Scholar
  5. [CES86]
    E.M. Clarke, E.A. Emerson and A.P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,” ACM Transactions on Programming Languages and Systems, 8(2) (1986), 244–263.Google Scholar
  6. [EF95]
    H.-D. Ebbinghaus, J. Flum, Finite Model Theory 1995, Springer 1995.Google Scholar
  7. [Eme90]
    E.A. Emerson, “Temporal and modal logic,” in Handbook of theoretical computer science, 1990, 997–1072.Google Scholar
  8. [Eme97]
    E. A. Emerson, “Model Checking and the Mu-Calculus,” in Descriptive Complexity and Finite Models, N. Immerman and Ph. Kolaitis, eds., 1997, American Mathematical Society.Google Scholar
  9. [EL86]
    E.A. Emerson and C.-L. Lei, “Efficient Model Checking in Fragments of the Propositional mu-Calculus,” Proc. 1st Symp. on Logic in Computer Science (1986), 267–278.Google Scholar
  10. [EVW97]
    K. Etessami, M.Y. Vardi, and T. Wilke, “First-Order Logic with Two Variables and Unary Temporal Logic,” Proc. 12th IEEE Symp. on Logic in Computer Science, July 1997.Google Scholar
  11. [I86]
    N. Immerman, “Relational Queries Computable in Polynomial Time,” Information and Control, 68 (1986), 86–104.Google Scholar
  12. [I87]
    N. Immerman, “Languages That Capture Complexity Classes,” SIAM J. Comput. 16(4) (1987), 760–778.Google Scholar
  13. [I88]
    N. Immerman, “Nondeterministic Space is Closed Under Complementation,” SIAM J. Comput. 17(5) (1988), 935–938.Google Scholar
  14. [I89]
    N. Immerman, “Descriptive and Computational Complexity,” in Computational Complexity Theory, ed. J. Hartmanis, Lecture Notes for AMS Short Course on Computational Complexity Theory, Proc. Symp. in Applied Math. 38, American Mathematical Society (1989), 75–91.Google Scholar
  15. [I89a]
    N. Immerman, Expressibility and Parallel Complexity, SIAM J. of Comput 18 (1989), 625–638.Google Scholar
  16. [I91]
    N. Immerman, “DSPACE[n k]=VAR[k+1],” Sixth IEEE Structure in Complexity Theory Symp. (July, 1991), 334–340.Google Scholar
  17. [Koz83]
    D. Kozen, “Results on the Propositional μ-Calculus,” Theoretical Computer Science, 27 (1983), 333–354.Google Scholar
  18. [LR96]
    R. Lassaigne and M. de Rougemont, Logique et Complexité, 1996, Hermes.Google Scholar
  19. [LP85]
    O. Lichtenstein and A. Pnueli, “Checking that Finite State Concurrent Programs Satisfy their Linear Specification” Proc. 12th ACM Symp. on Principles of Programming Languages (1985), 97–107.Google Scholar
  20. [McM93]
    K. McMillan, Symbolic Model Checking, 1993, Kluwer. [Ott] M. Otto, private communication.Google Scholar
  21. [PI94]
    S. Patnaik and N. Immerman, “Dyn-FO: A Parallel, Dynamic Complexity Class,” Proc. ACM Symp. on Principles of Database Systems (1994), 210–221.Google Scholar
  22. [QS81]
    J.P. Queille and J. Sifakis, “Specification and Verification of Concurrent Systems in Cesar,” Proc. 5th Int'l Symp. on Programming, LNCS 137, 1981, Springer-Verlag, 337–351.Google Scholar
  23. [TBK95]
    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, 1995.Google Scholar
  24. [Var82]
    M.Y. Vardi, “Complexity of Relational Query Languages,” ACM Symp. Theory Of Comput. (1982), 137–146.Google Scholar
  25. [Var97]
    M.Y. Vardi, “Why is Modal Logic So Robustly Decidable?” in Descriptive Complexity and Finite Models, N. Immerman and Ph. Kolaitis, eds., 1997, American Mathematical Society.Google Scholar
  26. [VW84]
    M.Y. Vardi and P. Wolper, “Yet Another Process Logic,” in Logics of Programs, LNCS 164, 1984, Springer-Verlag, 501–512.Google Scholar
  27. [VW86]
    M.Y. Vardi and P. Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” Proc. 1st Symp. on Logic in Computer Science (1986), 322–331.Google Scholar
  28. [VW94]
    M.Y. Vardi and P. Wolper, “Reasoning about Infinite Computations,” Information and Computation 115(1) (1994), 1–37.Google Scholar
  29. [Ya90]
    M. Yannakakis, “Graph-theoretic methods in database theory”, Proc. 9th ACM Symp. on Principles of Database Systems, 230–242, 1990.Google Scholar
  30. [ZSS94]
    S. Zhang, S.A. Smolka, and O. Sokolsky, “On the Parallel Complexity of Model Checking in the Modal μ-Calculus,” Proc. 9th IEEE Symp. on Logic in Computer Science, 1994, 154–163.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Neil Immerman
    • 1
  • Moshe Y. Vardi
    • 2
  1. 1.Computer Science Dept.University of MassachusettsAmherst
  2. 2.Computer Science Dept.Rice UniversityHouston

Personalised recommendations