Compositional BDD Construction: A Lazy AlgorithmJ Bradley, N Davies, Compositional BDD Construction: A Lazy Algorithm. CSTR-98-005, Department of Computer Science, University of Bristol. April 1998. PDF, 226 Kbytes.
The efficient Binary Decision Diagram algorithm presented in Brace, Rudell and Bryant 1990 is modified to operate in a lazy or demand-driven fashion. We show how this new approach benefits the area of symbolic model checking by reducing the amount of state-space that needs to be evaluated. The need for a lazy or "delayed" BDD-based manipulation system, specifically to aid the reasoning about symbolic systems, was identified in Bryant 1992 as a method of tackling the state-space explosion problem. Often the model checking of systems only uses a very small part of the BDD (Bryant 1992). This is especially true for the generation of model checking counter-examples (Clarke et al 1994). However the strict nature of traditional BDD algorithms means that the whole BDD-representation of a system has to be evaluated. Since this new technique only evaluates the nodes of the BDD that are required, it can potentially manipulate significantly larger and more complex systems than could be represented before. We give space and time complexity comparisons between the traditional and lazy algorithms and show how it affects the practical evaluation of state-space especially for model checking purposes.