Using BDDs to Decide CTL
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.
KeywordsCTL satisfiability validity BDDs tableau
- 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
- 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
- 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
- 9.Marrero, W.: Using BDDs to decide CTL. Technical Report 04-005, DePaul University (2004)Google Scholar
- 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