Title :
Causal analysis of probabilistic counterexamples
Author :
Debbi, Hichem ; Bourahla, M.
Author_Institution :
Dept. of Comput. Sci., Univ. of M´sila, M´sila, Algeria
Abstract :
In probabilistic model checking (PMC), counterexample generation has a quantitative aspect. The counterexample 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 in PMC, which is the counterexample analysis. We propose an aided-diagnostic method for probabilistic counterexamples based on the notions of causality and responsibility. Given a counterexample for a Probabilistic CTL (PCTL) /CSL (Continuous Stochastic Logic) formula that does not hold over Discreet Time Markov Chain (DTMC)/ Continuous Time Markov Chain (CTMC) model, this method guides the user to the most responsible causes in the counterexample. To evaluate our method, we sue two case studies, the polling server system and the embedded control system.
Keywords :
Markov processes; embedded systems; formal logic; formal verification; probability; CSL; CTMC model; DTMC; PCTL; PMC; accumulative probability mass; aided-diagnostic method; causal analysis; continuous stochastic logic; counterexample generation; discreet time Markov chain; embedded control system; polling server system; probabilistic CTL; probabilistic counterexamples; probabilistic model checking; Computational modeling; Context; Context modeling; Markov processes; Model checking; Probabilistic logic; Causality; Continuous Stochastic Logic (CSL); Probabilistic Computation Tree Logic (PCTL); Probabilistic Counterexample; Probabilistic Model Checking (PMC); Responsibility;
Conference_Titel :
Formal Methods and Models for Codesign (MEMOCODE), 2013 Eleventh IEEE/ACM International Conference on
Conference_Location :
Portland, OR
Print_ISBN :
978-1-4799-0903-2
