Causal Analysis of Probabilistic Counterexamples

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.