A Debugging Game for Probabilistic Models
Open Access
- 30 June 2022
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 34 (2), 1-25
- https://doi.org/10.1145/3536429
Abstract
One of the major advantages of model checking over other formal methods is its ability to generate a counterexample when a model does not satisfy is its specification. A counterexample is an error trace that helps to locate the source of the error. Therefore, the counterexample represents a valuable tool for debugging. In Probabilistic Model Checking (PMC), the task of counterexample generation has a quantitative aspect. Unlike the previous methods proposed for conventional model checking that generate the counterexample as a single path ending with a bad state representing the failure, the task in PMC is completely different. A counterexample in PMC is a set of evidences or diagnostic paths that satisfy a path formula, whose probability mass violates the probability threshold. Counterexample generation is not sufficient for finding the exact source of the error. Therefore, in conventional model checking, many debugging techniques have been proposed to act on the counterexamples generated in order to locate the source of the error. In PMC, debugging counterexamples is more challenging, since the probabilistic counterexample consists of multiple paths and it is probabilistic. In this paper, we propose a debugging technique based on stochastic games to analyze probabilistic counterexamples generated for probabilistic models described as Markov chains in PRISM language. The technique is based mainly on the idea of considering the modules composing the system as players of a reachability game, whose actions contribute to the evolution of the game. Through many case studies, we will show that our technique is very effective for systems employing multiple components. The results are also validated by introducing a debugging tool called GEPCX (Game Explainer of Probabilistic Counterexamples).Keywords
This publication has 36 references indexed in Scilit:
- Causes and Explanations: A Structural-Model Approach. Part I: CausesThe British Journal for the Philosophy of Science, 2005
- SOBERACM SIGSOFT Software Engineering Notes, 2005
- Scalable statistical bug isolationACM SIGPLAN Notices, 2005
- Fate and free will in error tracesInternational Journal on Software Tools for Technology Transfer, 2004
- Model-checking algorithms for continuous-time markov chainsIEEE Transactions on Software Engineering, 2003
- Alternating-time temporal logicJournal of the ACM, 2002
- Model-checking continuous-time Markov chainsACM Transactions on Computational Logic, 2000
- A logic for reasoning about time and reliabilityFormal Aspects of Computing, 1994
- Stochastic Petri net models of polling systemsIEEE Journal on Selected Areas in Communications, 1990
- A randomized protocol for signing contractsCommunications of the ACM, 1985