Title | ||
---|---|---|
Forwarding, Splitting, and Block Ordering to Optimize BDD-based Bisimulation Computation. |
Abstract | ||
---|---|---|
In this paper we present optimizations for a BDD-based algorithm for the computation of several types of bisimulations which play an important role for minimisation of large systems thus enabling their verification. The basic principle of the algorithm is partition refinement. Our proposed optimizations take this refinement-structure as well as the usage of BDDs for the representation of the system into account: (1) block forwarding updates in-situ newly refined blocks of the partition, (2) split-driven refinement approximates the blocks that may be refined, and (3) block ordering heuristically suggests a good order in which the blocks will be refined. We provide substantial experimental results on examples from different applications and compare them to alternative approaches. 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 | Venue | Field |
---|---|---|
2007 | MBMV | Heuristic,Algorithm,Minimisation (psychology),Bisimulation,Partition (number theory),Partition refinement,Mathematics,Computation |
DocType | Citations | PageRank |
Conference | 2 | 0.40 |
References | Authors | |
11 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ralf Wimmer | 1 | 407 | 34.28 |
Marc Herbstritt | 2 | 136 | 11.01 |
B. Becker | 3 | 191 | 21.44 |