Generating Diagnoses for Probabilistic Model Checking Using Causality
|
| Title | Generating Diagnoses for Probabilistic Model Checking Using Causality |
| Authors | |
| 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. |
| Publisher | University of Zagreb, University Computing Centre - SRCE |
| Date | 2013-06-04 |
| Source | Journal of Computing and Information Technology Vol 21, No 1 (2013) |
| Rights | CIT. Journal of Computing and Information Technology is an open access journal. Authors who publish with this journal agree to the following terms:Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the works authorship and initial publication in this journal. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journals published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access). |