Sciweavers

CORR
2008
Springer

Significant Diagnostic Counterexamples in Probabilistic Model Checking

13 years 3 months ago
Significant Diagnostic Counterexamples in Probabilistic Model Checking
Abstract. 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 similarly outside strongly connected components. Then, we show 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.
Miguel E. Andrés, Pedro R. D'Argenio, Peter
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Miguel E. Andrés, Pedro R. D'Argenio, Peter van Rossum
Comments (0)