Constraint-based debugging in probabilistic model checking

A counterexample in model checking is an error trace that represents a valuable tool for debugging. In Probabilistic Model Checking (PMC), the counterexample generation has a quantitative aspect. A probabilistic counterexa mple is a set of diagnostic paths in which a path formula holds, and whose probability mass violates the probability threshold. Comparing to conventional model checking, debugging and analyzing counterexamples in PMC is a very complex task. In this paper, we propose a debugging method for Markov models described in the probabilistic model checker PRISM by analyzing probabilistic counterexamples. The probabilistic counterexample generated is subjected to a set of assertions, which are employed for detecting incorrect behavior of the model, and thus locating the erroneous transitions contributing to the error. Our method has been implemented and tested on many PRISM models of different case studies. The method shows promising results in terms of execution time as well as its efficiency in locating the erroneous transitions.