An n log n Algorithm for Online BDD Refinement

Nils Klarlund

Abstract


Binary Decision Diagrams are in widespread use in verification systems
for the canonical representation of Boolean functions. A BDD representing
a function phi : B^nu -> N can easily be reduced to its canonical form in
linear time.
In this paper, we consider a natural online BDD refinement problem
and show that it can be solved in O(n log n) if n bounds the size of the
BDD and the total size of update operations.
We argue that BDDs in an algebraic framework should be understood
as minimal fixed points superimposed on maximal fixed points. We propose
a technique of controlled growth of equivalence classes to make the
minimal fixed point calculations be carried out efficiently. Our algorithm
is based on a new understanding of the interplay between the splitting
and growing of classes of nodes.
We apply our algorithm to show that automata with exponentially
large, but implicitly represented alphabets, can be minimized in time
O(n log n), where n is the total number of BDD nodes representing the
automaton.

Full Text:

PDF


DOI: http://dx.doi.org/10.7146/brics.v2i29.19931
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.
OK


ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library