An n log n algorithm for online BDD refinement

Abstract

Binary Decision Diagrams are in widespread use in verification systems for the canonical representation of finite functions. Here we consider multi-valued BDDs, which represent functions of the form (formula presented), where (formula presented) 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) 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 with 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 algorithm for automaton minimization, which breaks down for BDDs because of their path compression property.