@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.",
}