Title: |
Using BDDs to decide CTL |

Authors: |
Will Marrero |

Abstract: |
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 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. |

Keywords: |
CTL, satisfiability, validity, BDDs, tableau |

Full Paper: |
[ps] |