Since 2014
An n log n Algorithm for Online BDD Refinement
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
An n log n Algorithm for Online BDD Refinement
|
|
| Creator |
Klarlund, Nils
|
|
| Description |
Binary Decision Diagrams are in widespread use in verification systemsfor the canonical representation of Boolean functions. A BDD representinga function phi : B^nu -> N can easily be reduced to its canonical form inlinear time.In this paper, we consider a natural online BDD refinement problemand show that it can be solved in O(n log n) if n bounds the size of theBDD and the total size of update operations.We argue that BDDs in an algebraic framework should be understoodas minimal fixed points superimposed on maximal fixed points. We proposea technique of controlled growth of equivalence classes to make theminimal fixed point calculations be carried out efficiently. Our algorithmis based on a new understanding of the interplay between the splittingand growing of classes of nodes.We apply our algorithm to show that automata with exponentiallylarge, but implicitly represented alphabets, can be minimized in timeO(n log n), where n is the total number of BDD nodes representing theautomaton.
|
|
| Publisher |
Aarhus University
|
|
| Contributor |
—
|
|
| Date |
1995-01-29
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion — |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/19931
10.7146/brics.v2i29.19931 |
|
| Source |
BRICS Report Series; No 29 (1995): RS-29 An n log n Algorithm for Online BDD Refinement
BRICS Report Series; No 29 (1995): RS-29 An n log n Algorithm for Online BDD Refinement 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/19931/17585
|
|
| Rights |
Copyright (c) 2015 BRICS Report Series
|
|