@inproceedings{wimmer-et-al-mmb-2010,
  author = "Ralf Wimmer and Bernd Becker",
  title  = "Correctness Issues of Symbolic Bisimulation Computation for {Markov} Chains",
  year   = "2010",
  address = "Essen, Germany",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "5987",
  pages  = "287--301",
  booktitle = "15th International GI/ITG Conference on ``Measurement, Modelling and Evaluation of Computing Systems''",
  editor = "Bruno M{\"u}ller-Clostermann and Klaus Echtle and Erwin Rathgeb",
  subproject={S3},
  access={restricted},
  bibtex={wimmer.mmb10.bib},
  pdf={wimmer.mmb10.pdf},
  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.",
  note = "(to appear)",
}