Significant Diagnostic Counterexamples in Probabilistic Model Checking
| Title | Significant Diagnostic Counterexamples in Probabilistic Model Checking |
| Publication Type | Conference Paper |
| Year of Publication | 2008 |
| Authors | Andrés, ME, D'Argenio, PR, van Rossum, P |
| Conference Name | Hardware and Software: Verification and Testing, 4th International Haifa Verification Conference, HVC 2008 |
| Publisher | Springer |
| ISBN Number | 978-3-642-01701-8 |
| 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. |
| DOI | 10.1007/978-3-642-01702-5_15 |
PDF (Full text):
