Symbolic Model Checking

The concept of model checking as described in the preceding section is straightforward, but can run into the problem of state explosion. To minimize this problem it would be nice to have a strategy which could replace the direct and explicit handling of all the states with all their possible values and transitions as far as possible by some symbolic representations of whole sets. One of the most efficient and popular method to day to do this is the encoding of the data structures into OBDDs, short for Ordered Binary Decision Diagrams. Originally introduced by Bryant 1986 [47] this concept has been constantly been optimized. But although this method has meanwhile succesfully been used in large industrial projects it is still not completely safe with regarding to occasional exponential growths of the state space.

To introduce the formal concept of OBDDs fully one has to establish some preliminary formal concepts like boolean functions, fixpoint operators, QBFs, Quantified Boolean Formulas, BDT, Binary Decision Tree (which can have redundant subtrees), BDDs, Binary Decision Diagrams (where the redundant subtrees of the BDTs are eliminated), and the ordering of variables in a BDD leading to an OBDDs.