# 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 \(\varphi :\mathbb{B}^\upsilon \to \mathcal{L}\), where \(\mathcal{L}\) 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.

## Keywords

Decision Node Binary Decision Diagram Partial Assignment Current Partition Decision Block## References

- 1.D. Basin and N. Klarlund. Beyond the finite in hardware verification. Submitted. Extended version of: “Hardware verification using monadic second-order logic,”
*CAV '95*, LNCS 939, 1996.Google Scholar - 2.Norbert Blum. An
*o*(*n*log*n*) implementation of the standard mothod for minimizing*n*-state finite automata.*Information Processing Letters*, 1996.Google Scholar - 3.R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams.
*ACM Computing surveys*, 24(3):293–318, September 1992.Google Scholar - 4.A. Cardon and M. Crochemore. Partitioning a graph in
*O*(¦*A*¦log_{2}¦*V*¦).*TCS*, 19:85–98, 1982.Google Scholar - 5.Aarti Gupta.
*Inductive Boolean function manipulation*. PhD thesis, Carnegie Mellon University, 1994. CMU-CS-94-208.Google Scholar - 6.Aarti Gupta and Allan L. Fisher. Representation and symbolic manipulation of linearly inductive boolean functions. In
*Proceedings of the IEEE International Conference on Computer-Aided Design*, pages 192–199. IEEE Computer Society Press, 1993.Google Scholar - 7.J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In
*Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS '95, LNCS 1019*, 1996. Also available through http://www.brics.dk/∼klarlund/MonaFido/papers.html.Google Scholar - 8.J. Hopcroft. An
*n*log*n*algorithm for minimizing states in a finite automaton. In Z. Kohavi and Paz A., editors,*Theory of machines and computations*, pages 189–196. Academic Press, 1971.Google Scholar - 9.D. Lee and M. Yannakakis. Online minimization of transition systems. In
*Proc. STOC*, pages 264–274. ACM, 1992.Google Scholar - 10.H-T. Liaw and C-S. Lin. On the OBDD-representation of general Boolean functions.
*IEEE Trans. on Computers*, C-41(6):661–664, 1992.Google Scholar - 11.R. Paige and R. Tarjan. Three efficient algorithms based on partition refinement.
*SIAM Journal of Computing*, 16(6), 1987.Google Scholar - 12.D. Sieling and I. Wegener. Reduction of OBDDs in linear time.
*IPL*, 48:139–144, 1993.Google Scholar