Computation Tree Logic (CTL) has been used quite extensively and successfully to reason about finite state systems. Algorithms have been developed for checking if a particular model satisfies a CTL formula (model checking) as well as for deciding if a CTL formula is valid or satisfiable. Initially, these algorithms explicitly constructed the model being checked or the model demonstrating satisfiability. A major breakthrough in CTL model checking occurred when researchers started representing the model implicitly via Boolean formulas. The use of ordered binary decision diagrams (OBDDs) as an efficient representation for these formulas led to a large jump in the size of the models that can be checked. This paper presents a way to encode the satisfiability algorithms for CTL in terms of Boolean formulas as well, so that symbolic model checking techniques using OBDDs can be exploited.


CTL satisfiability validity BDDs tableau 


  1. 1.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of Logics of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)CrossRefGoogle Scholar
  2. 2.
    Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. MIT Press, Cambridge (1990)Google Scholar
  3. 3.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98, 142–170 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Coudert, O., Madre, J.C., Berthet, C.: Verification of synchronous sequential machines based on symbolic execution. In: Proceedings of Automatic Verification Methods for Finite State Systems, pp. 365–373 (1989)Google Scholar
  5. 5.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35, 677–691 (1986)CrossRefGoogle Scholar
  6. 6.
    Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. In: Proceedings of the ACM Symposium on Theory of Computing, pp. 169–180 (1982)Google Scholar
  7. 7.
    Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design 10, 47–71 (1997)CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16, 1512–1542 (1994)CrossRefGoogle Scholar
  9. 9.
    Marrero, W.: Using BDDs to decide CTL. Technical Report 04-005, DePaul University (2004)Google Scholar
  10. 10.
    Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of the 1st Annual Symposium on Logic in Computer Science, pp. 267–278. IEEE Computer Society Press, Los Alamitos (1986)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Will Marrero
    • 1
  1. 1.DePaul UniversityChicagoUSA

Personalised recommendations