Open AccessAn n log n Algorithm for Online BDD Refinement
Author(s) -
Nils Klarlund
Publication year - 1995
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v2i29.19931
Subject(s) - boolean function , mathematics , combinatorics , binary decision diagram , algorithm , algebraic number , function (biology) , binary logarithm , discrete mathematics , fixed point , binary number , arithmetic , mathematical analysis , evolutionary biology , biology
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.