Fast parallel algorithms for model checking using BDDs

Binary decision diagrams (BDDs) have recently been used in model checking to verify systems with a large number of states (of the order of 5×10²⁰). Representing both the state space and the state transition graph as BDDs has been demonstrated to alleviate the problem of state space explosion. But there are limitations to this heuristic approach. Even systems of reasonable complexity have many more states. Also, the BDD approach might fail even on some simple systems. The authors propose the use of parallelism to extend the applicability of BDDs in model checking. They present fast algorithms for model checking that employ BDDs. The algorithms presented are much faster than the best known previous algorithms