# Model checking and transitive-closure logic

## Abstract

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[log*n*]. This means that the space requirements are manageable, the entire computation is parallelizable, and efficient dynamic evaluation is possible.

## Keywords

Model Check Temporal Logic Boolean Variable Linear Temporal Logic Kripke Structure## References

- [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 - [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 - [BCM92]J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and L.J. Hwang, “Symbolic Model Checking: 10
^{20}States and Beyond,”*Information and Computation*98(2) (1992), 142–170.Google Scholar - [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 - [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 - [EF95]H.-D. Ebbinghaus, J. Flum,
*Finite Model Theory*1995, Springer 1995.Google Scholar - [Eme90]E.A. Emerson, “Temporal and modal logic,” in
*Handbook of theoretical computer science*, 1990, 997–1072.Google Scholar - [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 - [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 - [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 - [I86]N. Immerman, “Relational Queries Computable in Polynomial Time,”
*Information and Control*, 68 (1986), 86–104.Google Scholar - [I87]N. Immerman, “Languages That Capture Complexity Classes,”
*SIAM J. Comput*. 16(4) (1987), 760–778.Google Scholar - [I88]N. Immerman, “Nondeterministic Space is Closed Under Complementation,”
*SIAM J. Comput*. 17(5) (1988), 935–938.Google Scholar - [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 - [I89a]N. Immerman,
*Expressibility and Parallel Complexity, SIAM J. of Comput***18**(1989), 625–638.Google Scholar - [I91]N. Immerman, “DSPACE[
*n*^{k}]=VAR[*k*+1],”*Sixth IEEE Structure in Complexity Theory Symp*. (July, 1991), 334–340.Google Scholar - [Koz83]D. Kozen, “Results on the Propositional
*μ*-Calculus,”*Theoretical Computer Science*, 27 (1983), 333–354.Google Scholar - [LR96]R. Lassaigne and M. de Rougemont,
*Logique et Complexité*, 1996, Hermes.Google Scholar - [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 - [McM93]K. McMillan,
*Symbolic Model Checking*, 1993, Kluwer. [Ott] M. Otto, private communication.Google Scholar - [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 - [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 - [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 - [Var82]M.Y. Vardi, “Complexity of Relational Query Languages,”
*ACM Symp. Theory Of Comput*. (1982), 137–146.Google Scholar - [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 - [VW84]M.Y. Vardi and P. Wolper, “Yet Another Process Logic,” in
*Logics of Programs*, LNCS 164, 1984, Springer-Verlag, 501–512.Google Scholar - [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 - [VW94]M.Y. Vardi and P. Wolper, “Reasoning about Infinite Computations,”
*Information and Computation*115(1) (1994), 1–37.Google Scholar - [Ya90]M. Yannakakis, “Graph-theoretic methods in database theory”,
*Proc. 9th ACM Symp. on Principles of Database Systems*, 230–242, 1990.Google Scholar - [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