@InProceedings{wimmer-et-al-glsvlsi-2007,
  author =    "Ralf Wimmer and Marc Herbstritt and Bernd Becker",
  title =     "Optimization Techniques for BDD-based Bisimulation Minimization",
  booktitle = "Proceedings of the 17\textsuperscript{th} ACM Great Lakes Symposium on VLSI",
  address =   "Stresa, Italy",
  month =     mar,
  year =      "2007",
  editor =    "Hai Zhou and Enrico Macii",
  publisher = "ACM Press",
  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 the
               problem 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."
}