Advertisement

An n log n algorithm for online BDD refinement

  • Nils Klarlund
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 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. 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. 3.
    R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing surveys, 24(3):293–318, September 1992.Google Scholar
  4. 4.
    A. Cardon and M. Crochemore. Partitioning a graph in OA¦log2¦V¦). TCS, 19:85–98, 1982.Google Scholar
  5. 5.
    Aarti Gupta. Inductive Boolean function manipulation. PhD thesis, Carnegie Mellon University, 1994. CMU-CS-94-208.Google Scholar
  6. 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. 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. 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. 9.
    D. Lee and M. Yannakakis. Online minimization of transition systems. In Proc. STOC, pages 264–274. ACM, 1992.Google Scholar
  10. 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. 11.
    R. Paige and R. Tarjan. Three efficient algorithms based on partition refinement. SIAM Journal of Computing, 16(6), 1987.Google Scholar
  12. 12.
    D. Sieling and I. Wegener. Reduction of OBDDs in linear time. IPL, 48:139–144, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Nils Klarlund
    • 1
  1. 1.AT&T Labs ResearchMurray Hill

Personalised recommendations