  This paper presents a novel technique for counterexample generation in
probabilistic model checking of Markov Chains and Markov Decision Processes.
(Finite) paths in counterexamples are grouped together in witnesses that are
likely to provide similar debugging information to the user. We list five
properties that witnesses should satisfy in order to be useful as debugging
aid: similarity, accuracy, originality, significance, and finiteness. Our
witnesses contain paths that behave similar outside strongly connected
components.
  This papers shows how to compute these witnesses by reducing the problem of
generating counterexamples for general properties over Markov Decision
Processes, in several steps, to the easy problem of generating counterexamples
for reachability properties over acyclic Markov Chains.
