Debugging of Markov Decision Processes (MDPs) Models

Hichem Debbi

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.

In Gregor Gössler and Oleg Sokolsky: Proceedings First Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies (CREST 2016), Eindhoven, The Netherlands, 8th April 2016, Electronic Proceedings in Theoretical Computer Science 224, pp. 25–39.
Published: 26th August 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: