@inproceedings{wimmer-et-al-mmb-2010,
author = "Ralf Wimmer and Bernd Becker",
title = "Correctness Issues of Symbolic Bisimulation Computation for {Markov} Chains",
year = "2010",
month = mar,
address = "Essen, Germany",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
volume = "5987",
pages = "287--301",
isbn = "978-3-642-12103-6",
booktitle = "Proceedings of the 15\textsuperscript{th} International GI/ITG Conference on
``Measurement, Modelling and Evaluation of Computing Systems'' (MMB)",
editor = "Bruno M{\"u}ller-Clostermann and Klaus Echtle and Erwin Rathgeb",
abstract = "Bisimulation reduction is a classical means to
fight the infamous state space explosion problem, which limits the
applicability of automated methods for verification like model
checking. A signature-based method, originally developed by Blom and
Orzan for labeled transition systems and adapted for Markov chains by
Derisavi, has proved to be very efficient. It is possible to implement it
symbolically using binary decision diagrams such that it is able to
handle very large state spaces efficiently. We will show, however,
that for Markov chains this algorithm suffers from numerical
instabilities, which often result in too large quotient systems. We
will present and experimentally evaluate two different approaches to
avoid these problems: first the usage of rational arithmetic, and
second an approach not only to represent the system structure but also
the transition rates symbolically. In addition, this allows us to
modify their actual values after the quotient computation.",
}