@TECHREPORT{AIB200609,
  AUTHOR =        {Tingting Han and Joost-Pieter Katoen},
  TITLE =         {Counterexamples in Probabilistic Model Checking},
  NUMBER =        {AIB200609},
  INSTITUTION =   {Software Modelling and Verification (i2), RWTH Aachen},
  ADDRESS =       {},
  ABSTRACT =      {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.},
  KEYWORDS =      {},
  NOTE =          {},
  MONTH =         {August},
  YEAR  =         {2006},
  AUTHOR1_URL =   {http://www-i2.informatik.rwth-aachen.de/i2/han/},
  AUTHOR1_EMAIL = {tingting.han@cs.rwth-aachen.de},
  AUTHOR2_URL =   {http://www-i2.informatik.rwth-aachen.de/i2/katoen/},
  AUTHOR2_EMAIL = {katoen@cs.rwth-aachen.de},
  PAGES =         {20},
  FILE  =         {},
  URL   =         {},
  CONTACT =       {tingting.han@cs.rwth-aachen.de}
}