Computation Tree Logic (CTL) has been used quite extensively and
successfully to reason about finite state systems. It can be used
to make assertions about computation paths in a labeled transition
system. 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
system implicitly via Boolean formulas. By translating the problem
into the logic of quantified Boolean formulas, researchers could
represent the model implicitly. They could also make use of
ordered binary decision diagrams (OBDDs) which resulted in enormous
increase in the size of the models that can be checked. In this talk,
I will introduce OBDDS as well as the logic CTL, and I will present a
way to encode the satisfiability algorithms for CTL in terms of Boolean
formulas so that they can be implemented using OBDDs as well.