@inProceedings{ wimmer-et-al-qest-2008,
  author =    "Ralf Wimmer and 
               Salem Derisavi and 
	       Holger Hermanns",
  title =     "Symbolic Partition Refinement with Dynamic Balancing of Time and Space",
  booktitle = "5\textsuperscript{th} International Conference
	       on Quantitative Evaluation of Systems (QEST)",
  publisher = "IEEE Computer Science Press",
  year =      "2008",
  month =     sep,
  address =   "Saint-Malo, France",
  pages =     "65--74",
  isbn =      "978-0-7695-3360-5",
  editor =    "Gerardo Rubino",
  abstract =  "Bisimulation minimization is one of the classical means to fight the
	infamous state space explosion problem in verification. Particularly
	in stochastic verification, numerical algorithms are applied, which
	do not scale beyond systems of moderate size. To alleviate this
	problem, symbolic bisimulation minimization has been used
	effectively to reduce very large symbolically represented state
	spaces to moderate size explicit representations.  But even this
	minimization may fail due to time or memory limitations. This paper
	presents a symbolic algorithm which relies on a hybrid symbolic
	partition representation. It dynamically converts between two known
	representations in order to provide a trade-off between
	memory consumption and runtime. The conversion itself is logarithmic
	in the partition size. We show how to apply it for the
	minimization of Markov chains, but the same techniques can be
	adapted in a straightforward way to other models like labeled
	transition systems or interactive Markov chains.",
}