hrcak mascot   Srce   HID

Izvorni znanstveni članak
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 icon orcid.org/0000-0002-0691-1417 ; Department of Computer Science, University of M'sila, Algeria

Puni tekst: engleski, pdf (229 KB) str. 13-22 preuzimanja: 374* citiraj
APA 6th Edition
Debbi, H. i Bourahla, M. (2013). Generating Diagnoses for Probabilistic Model Checking Using Causality. Journal of computing and information technology, 21 (1), 13-22. https://doi.org/10.2498/cit.1002115
MLA 8th Edition
Debbi, Hichem i Mustapha Bourahla. "Generating Diagnoses for Probabilistic Model Checking Using Causality." Journal of computing and information technology, vol. 21, br. 1, 2013, str. 13-22. https://doi.org/10.2498/cit.1002115. Citirano 22.09.2019.
Chicago 17th Edition
Debbi, Hichem i Mustapha Bourahla. "Generating Diagnoses for Probabilistic Model Checking Using Causality." Journal of computing and information technology 21, br. 1 (2013): 13-22. https://doi.org/10.2498/cit.1002115
Harvard
Debbi, H., i Bourahla, M. (2013). 'Generating Diagnoses for Probabilistic Model Checking Using Causality', Journal of computing and information technology, 21(1), str. 13-22. https://doi.org/10.2498/cit.1002115
Vancouver
Debbi H, Bourahla M. Generating Diagnoses for Probabilistic Model Checking Using Causality. Journal of computing and information technology [Internet]. 2013 [pristupljeno 22.09.2019.];21(1):13-22. https://doi.org/10.2498/cit.1002115
IEEE
H. Debbi i M. Bourahla, "Generating Diagnoses for Probabilistic Model Checking Using Causality", Journal of computing and information technology, vol.21, br. 1, str. 13-22, 2013. [Online]. https://doi.org/10.2498/cit.1002115

Sažetak

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.

Ključne riječi
Probabilistic Model Checking (PMC); Counterexample; Probabilistic Computation Tree Logic (PCTL); Discrete-Time Markov Chain (DTMC); Causality; Responsibility

Hrčak ID: 103375

URI
https://hrcak.srce.hr/103375

Posjeta: 507 *