Original scientific paper
https://doi.org/10.2498/cit.1002115
Generating Diagnoses for Probabilistic Model Checking Using Causality
Hichem Debbi
; Department of Computer Science, University of M'sila, Algeria
Mustapha Bourahla
orcid.org/0000-0002-0691-1417
; Department of Computer Science, University of M'sila, Algeria
Abstract
One of the most major advantages of Model checking over other formal methods of verification, its ability to generate an error trace in case of a specification falsified in the model. We call this trace a counterexample. However, understanding the counterexample is not that easy task, because model checker generates usually multiple counterexamples of long length, what makes the analysis of counterexample time-consuming as well as costly task. Therefore, counterexamples should be small and as indicative as possible to be understood. In probabilistic model checking (PMC) counterexample generation has a quantitative aspect. The counterexample in PMC is a set of paths in which a path formula holds, and their accumulative probability mass violates the probability bound. In this paper, we address the complementary task of counterexample generation which is the counterexample diagnosis in PMC. We propose an aided-diagnostic method for probabilistic counterexamples based on the notion of causality and responsibility. Given a counterexample for a Probabilistic CTL (PCTL) formula that doesn’t hold over Discreet-Time-Markov-Chain (DTMC) model, this method guides the user to the most responsible causes in the counterexample.
Keywords
Probabilistic Model Checking (PMC); Counterexample; Probabilistic Computation Tree Logic (PCTL); Discrete-Time Markov Chain (DTMC); Causality; Responsibility
Hrčak ID:
103375
URI
Publication date:
29.3.2013.
Visits: 1.510 *