Counterexamples in Probabilistic Model Checking

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 singlesource (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 (hopconstrained) k shortest paths problem.

• Type: Conference
• Year: 2007
• Where: TACAS
• Authors: Tingting Han, Joost-Pieter Katoen
• Keywords: Algorithms, Paper Considers Algorithms, Shortest Path Algorithms, Shortest Paths, TACAS 2007