Exploiting partitioned transition relations for efficient symbolic model checking in CTL
Aleš Časar, Zmago Brezočnik, Tatjana Kapus · 1996
We present an e#cient tool for symbolic state space traversal of #nite state machines. Both algorithms for searching reachable states and for model checking in CTL owe their e#ciency primarily to the use of partitioned transition relations. Partitioning of the relations is fully automatic. Symbolic state space traversal techniques show their superiority over the enumeration based methods when searching reachable states of a FSM. Sets of states and transitions can be represented bycharacteristic functions, and because they are boolean, we can represent them compactly by BDDs. The transition relation of a large circuit may result in a huge BDD that either does not #t into computer memory or leads to unacceptably long computation times. There are several approaches to overcome this problem. We describe the use of partitioned transition relations for an e#cient symbolic state space traversal and model checking in CTL. If the transition relation T of a FSM is represented by a so-called mo...