Significant Diagnostic Counterexamples in Probabilistic Model Checking

Simple item page
dc.creatorAndres, Miguel E.
dc.creatorD'Argenio, Pedro
dc.creatorvan Rossum, Peter
dc.date2008-06-06
dc.date.accessioned2026-07-07T09:43:06Z
dc.date.available2026-07-07T09:43:06Z
dc.descriptionThis 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.
dc.identifierhttps://arxiv.org/abs/0806.1139
dc.identifierhttp://arxiv.org/abs/0806.1139
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/162426
dc.subjectLogic in Computer Science
dc.subjectPerformance
dc.subjectB.8; C.4; D.2.4; G.3
dc.titleSignificant Diagnostic Counterexamples in Probabilistic Model Checking
dc.typetext

Files

Collections

arXiv