Significant Diagnostic Counterexamples in Probabilistic Model Checking

TitleSignificant Diagnostic Counterexamples in Probabilistic Model Checking
Publication TypeConference Paper
Year of Publication2008
AuthorsAndrés, ME, D'Argenio, PR, van Rossum, P
Conference NameHardware and Software: Verification and Testing, 4th International Haifa Verification Conference, HVC 2008
PublisherSpringer
ISBN Number978-3-642-01701-8
AbstractThis 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.
DOI10.1007/978-3-642-01702-5_15
PDF (Full text): 
Powered by Drupal