Name
Abstract | ||
|---|---|---|
In this paper we report on optimizations for a BDD-based algorithm for the computation of bisimulations. The underlying algorithmic principle is an iterative refinement of a partition of the state space. The proposed optimizations demonstrate that both, taking into account the algorithmic structure of theproblem and the exploitation of the BDD-based representation, are essential to finally obtain an efficient symbolic algorithm for real-world problems. The contributions of this paper are (1) block forwarding to update block refinement as soon as possible, (2) split-driven refinement that over-approximates the set of blocks that must definitely be refined, and (3) block ordering to fix the order of the blocks for the refinement in a clever way. We provide substantial experimental results on examples from different applications and compare them to alternative approaches when possible. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1145/1228784.1228880 | ACM Great Lakes Symposium on VLSI |
Keywords | Field | DocType |
basic algorithm,optimization technique,block forwarding,bdd-based bisimulation computation,efficient symbolic algorithm,bdd-based algorithm,iterative refinement,split-driven refinement,alternative approach,algorithmic structure,bdd-based representation,block refinement,binary decision diagram,bisimulation,state space | Iterative refinement,Symbolic algorithm,Computer science,Algorithm,Bisimulation,State space reduction,Partition (number theory),State space,Computation | Conference |
Citations | PageRank | References |
2 | 0.36 | 17 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ralf Wimmer | 1 | 407 | 34.28 |
| Marc Herbstritt | 2 | 136 | 11.01 |
| Bernd Becker | 3 | 855 | 73.74 |