@InProceedings{wimmer-et-al-mbmv-2007,
  author =    "Ralf Wimmer and Marc Herbstritt and Bernd Becker",
  title =     "Forwarding, Splitting, and Block Ordering to Optimize
               {BDD}-based Bisimulation Computation",
  booktitle = "Proceedings of the 10\textsuperscript{th} GI/ITG/GMM-Workshop
               ``Methoden und Beschreibungssprachen zur  Modellierung
               und Verifikation von Schaltungen und Systemen'' (MBMV)",
  address =   "Erlangen, Germany",
  editor =    "Christian Haubelt and J{\"u}rgen Teich",
  pages =     "203--212",
  month =     mar,
  year =      "2007",
  publisher = "Shaker Verlag",
  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) \emph{block forwarding} updates in-situ newly refined 
	blocks of the partition, (2) \emph{split-driven refinement} 
	approximates the blocks that may be refined, and (3) \emph{block ordering} 
	heuristically suggests a good order in which the blocks will be refined.\par
	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.",
  isbn =      "978-3-8322-5956-3",
}