The following technical report is available from http://aib.informatik.rwth-aachen.de:
Counterexamples in Probabilistic Model Checking Tingting Han, Joost-Pieter Katoen AIB 2006-09
This paper considers algorithms and complexity results for the generation of counterexamples in model checking of probabilistic until-formulae in discrete-time Markov chains (DTMCs). It is shown that finding the strongest evidence (i.e, the most probable path) that violates a (bounded) until-formula can be found in polynomial time using single-source (hop-constrained) shortest path algorithms. We also show that computing the smallest counterexample that is mostly deviating from the required probability bound can be found in a pseudo-polynomial time complexity by adopting a certain class of algorithms for the (hop-constrained) $k$ shortest paths problem.