@InProceedings{wimmer-et-al-mbmv-2008,
author = "Ralf Wimmer and Alexander Kortus
and Marc Herbstritt and Bernd Becker",
title = "The Demand for Reliability in Probabilistic Verification",
booktitle = "Proceedings of the 11\textsuperscript{th} GI/ITG/GMM-Workshop
``Methoden und Beschreibungssprachen zur Modellierung
und Verifikation von Schaltungen und Systemen'' (MBMV)",
address = "Freiburg im Breisgau, Germany",
editor = "Christoph Scholl and Stefan Disch",
pages = "99--108",
isbn = "978-3-8322-6962-3",
month = mar,
year = "2008",
publisher = "Shaker Verlag",
abstract = "For formal verification,
reliable results are of utmost importance.
In model checking of digital systems, mainly
incorrect implementations due to logical errors are the source
of wrong results. In probabilistic model checking, however, numerical
instabilities are an additional source for inconsistent
results.\par
First we present an example, for which several state-of-the-art
probabilistic model checking tools give completely wrong
results due to inexact computations. This motivates the
investigation at which points inaccuracies are introduced
during the model checking process. We then give ideas how,
in spite of these inaccuracies, reliable results can be obtained or
at least the user be warned about potential problems:
(1) to introduce a ``degree of belief'' for each sub-formula,
(2) to use exact (rational) arithmetic,
(3) to use interval arithmetic to obtain safe approximations
of the actual probabilities, and (4) to provide certificates
which testify that the result is correct.",
}