An nlogn Algorithm for Online BDD Refinement
| Autor: | Nils Klarlund |
|---|---|
| Rok vydání: | 1999 |
| Předmět: |
Discrete mathematics
Control and Optimization Discriminator Computational complexity theory Binary decision diagram Computer Science::Artificial Intelligence Fixed point Automaton Combinatorics Computational Mathematics Computational Theory and Mathematics Hardware_GENERAL Computer Science::Logic in Computer Science Partition (number theory) Canonical form Finite set Algorithm Hardware_LOGICDESIGN Mathematics |
| Zdroj: | Journal of Algorithms. 32:133-154 |
| ISSN: | 0196-6774 |
| DOI: | 10.1006/jagm.1999.1013 |
| Popis: | 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 ?: B??L, where 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(nlogn) 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·logn), 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect