@techreport{atr30,
 author      = {Ralf Wimmer and Alexander Kortus 
                            and Marc Herbstritt 
			    and Bernd Becker},
 title       = {{Symbolic Model Checking for DTMCs with Exact and Inexact Arithmetic}},
 editor      = {Bernd Becker and Werner Damm 
                             and Martin Fr{\"a}nzle 
	                     and Ernst-R{\"u}diger Olderog 
  	                     and Andreas Podelski 
	                     and Reinhard Wilhelm},
 subproject  = {S3},
 year        = {2007},
 month       = aug,
 type        = {Reports of SFB/TR 14 AVACS},
 series      = {ATR},
 number      = "30",
 note        = {ISSN: 1860-9821, {\tt http://www.avacs.org}},
 access      = {open},
 abstract    = {
	In formal verification, \emph{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, numerical 
	instabilities are an additional source for inconsistent
	results.

	In this report, we experimentally analyze the impact
	of inexact floating-point arithmetic on the correctness of the 
	result in the context of probabilistic model checking of
	discrete-time Markov chains. Inexact arithmetic performs
	implicitly \emph{rounding} of values that are generated during the 
	model checking process.

	To enable a direct comparison to the state of the art, which relies on 
	inexact floating-point arithmetic, we have implemented a prototypical 
	probabilistic model checker that provides standard floating-point 
	arithmetic as well as exact arithmetic.

	During our experimental evaluation, we found practical examples where 
	the use of inexact arithmetic produces unacceptable results. Two reasons 
	for these problems are: 
	(1) Rounding can change the structure of the system, and 
	(2) rounding can change the truth-value of sub-formulae. 
	Both issues can result in probabilities that are far away 
	from the correct ones. 

	As a summary, this work reveals the demand for investigating reliable 
	numerical methods within probabilistic model checking.
               },
}