Debugging of Markov Decision Processes (MDPs) Models
This work addresses debugging challenges for users of probabilistic model checking, though it appears incremental as it builds on existing counterexample analysis concepts.
The paper tackles the difficulty of understanding counterexamples in probabilistic model checking for Markov Decision Processes (MDPs) by proposing an aided-diagnostic method based on causality, responsibility, and blame, which guides users to the most relevant parts of the model that caused a violation.
In model checking, a counterexample is considered as a valuable tool for debugging. 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 threshold. However, understanding the counterexample is not an easy task. In this paper we address the task of counterexample analysis for Markov Decision Processes (MDPs). We propose an aided-diagnostic method for probabilistic counterexamples based on the notions of causality, responsibility and blame. Given a counterexample for a Probabilistic CTL (PCTL) formula that does not hold over an MDP model, this method guides the user to the most relevant parts of the model that led to the violation.