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 Wimmer140734.28
Marc Herbstritt213611.01
B. Becker319121.44