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