@InProceedings{ wimmer-et-al-ddecs-2008,
author = "Ralf Wimmer and
Alexander Kortus and
Marc Herbstritt and
Bernd Becker",
title = "Probabilistic Model Checking and
Reliability of Results",
booktitle = "11\textsuperscript{th} IEEE International
Workshop on Design and Diagnostics of
Electronic Circuits and Systems",
address = "Bratislava, Slovakia",
month = apr,
year = "2008",
pages = "207--212",
isbn = "978-1-4244-2276-0",
publisher = "IEEE Computer Science Press",
editor = "Bernd Straube and
Milo\v{s} Drutarovsk\'y and
Michel Renovell and
Peter Gramata and
M\'aria Fischerov\'a",
abstract = "In formal verification, reliable results are of utmost
importance. In model checking of digital systems, mainly
incorrect implementations of the model checking algorithms
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
We motivate our investigations with an example, for which
several state-of-the-art probabilistic model checking tools
give completely wrong results due to inexact computations.
We then analyze, at which points inaccuracies are introduced
during the model checking process.
We discuss first ideas how, in spite of these inaccuracies,
reliable results can be obtained or at least the user be
warned about potential correctness problems:
(1) usage of exact (rational) arithmetic,
(2) usage of interval arithmetic to obtain safe approximations
of the actual probabilities, (3) provision of certificates
which testify that the result is correct, and (4) integration of
a ``degree of belief'' for each sub-formula into existing model
checking tools.",
}