An n log n Algorithm for Online BDD Refinement

Binary decision diagrams are in widespread use in verification systems for the canonical representation of finite functions. Here we consider multivalued BDDs, which represent functions of the form : ^ν →  , where is a finite set of leaves. We study a rather natural online BDD refinement problem: a partition of the leaves of several shared BDDs is gradually refined, and the equivalence of the BDDs under the current partition must be maintained in a discriminator table. We show that it can be solved in O(n log n) time if n bounds both the size of the BDDs and the total size of update operations. Our algorithm is based on an understanding of BDDs as the fixed points of an operator that in each step splits and gathers nodes. We apply our algorithm to show that automata BDD-represented transition functions can be minimized in time O(n · log n), where n is the total number of BDD nodes representing the automaton. This result is not an instance of Hopcroft's classical minimization algorithm, which breaks down for BDD-represented automata because of the BDD path compression property.