Counterexample generation for stochastic systems using Bounded Model Checking
Final Report Abstract
Model checking is a powerful approach to analyze whether a system model satisfies a given property. If the property is violated, for the correction of the system it is crucial to provide a reason for the violation. For linear properties of discrete models like Kripke structures, counterexamples are system runs which lead to erroneous behavior. For probabilistic models, a counterexample is a set of paths such that each path satisfies a given path property and the probability mass of all paths together exceeds a safe bound. Since state-of-the-art probabilistic model checkers don’t provide such counterexamples, the goal of this project was to 1. improve the available technologies for probabilistic counterexample generation, 2. develop and implement algorithms for more expressive properties and models, and 3. demonstrate the practical applicability of those algorithms on a set of benchmarks. We adapted and extended the industrially highly successful approach of bounded model checking to collect adequate paths of probabilistic models, until the probability threshold is exceeded. We could handle richer models—like Markov chains with costs—and achieved great improvements in scalability and running times by using different solver technologies. Symbolic graph representations allowed us to handle systems with more than 1015 states. Since probabilistic counterexamples might be very large, we investigated alternative representations. The most successful one specifies critical subsystems, a part of the model such that all paths inside it build a counterexample, combined with a hierarchical abstraction technique for the interactive abstraction and concretion of model parts. These approaches are implemented in COMICS, our publicly available open-source tool. We also identified a great potential in compositionality. For models composed by parallel composition, the methods we investigated compute counterexamples on the components instead of the composed model. The composition of the components’ critical subsystems results in a critical subsystem for the composed model. When writing the proposal, we planned to put weight on the improvement of the available algorithms for path search and adapt them to fit optimally for probabilistic models. Due to the support of frequent working visits, we had intensive enriching discussions and worked, besides the planned tasks, also on several other approaches for probabilistic counterexample generation. One of the nicest results aims to further reduce the representation size by the computation of minimal critical subsystems. Most successful was the application of MILP solvers, which was powerful enough to support more expressive models like Markov decision processes (MDPs) which extend DTMCs with nondeterminism, and arbitrary ω-regular properties. The above approaches work on the low-level state-space of probabilistic automata. However, the probabilistic models are usually specified in a high-level language. We extended our work to represent minimal counterexamples in the high-level language, as a part of the high-level model. This has great advantages for system developers, who use counterexamples for bug fixing. We implemented our methods in the COMICS tool, which is devoted to probabilistic counterexample generation, but its model checking functionalities are not as optimized as in other model checking tools. Therefore we are happy that the community acknowledged our achievements and currently inclusions of our methods in the two popular probabilistic model checkers MRMC and PRISM are under development. This underlines the success of our project and the sustainability of our results, and provides tools for highly optimized model checking process combined with the feature of optimized counterexample generation.
Publications
- Symbolic counterexample generation for large discrete-time Markov chains. Science of Computer Programming, 91A:90–114, 2014
Nils Jansen, Ralf Wimmer, Erika Ábráhm, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, and Johann Schuster
- DTMC model checking by SCC reduction. In Proc. of QEST’10, pages 37–46. IEEE Computer Society, 2010
Erika Ábráhm, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, and Bernd Becker
- Counterexample generation for Markov chains using SMT-based bounded model checking. In Proc. of FMOODS/FORTE’11, volume 6722 of LNCS, pages 75–89. Springer-Verlag, June 2011
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, and Erika Ábráhm
- Hierarchical counterexamples for discrete-time Markov chains. In Proc. of ATVA’11, volume 6996 of LNCS, pages 443–452. Springer-Verlag, 2011
Nils Jansen, Erika Ábráhm, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, and Bernd Becker
- Minimal critical subsystems for discrete-time Markov models. In Proc. of TACAS’12, volume 7214 of LNCS, pages 299–314. Springer-Verlag, 2012
Ralf Wimmer, Nils Jansen, Erika Ábráhm, Joost-Pieter Katoen, and Bernd Becker
- Symbolic counterexample generation for discrete-time Markov chains. In Proc. of FACS’12, volume 7684 of LNCS, pages 134–151. Springer-Verlag, 2012
Nils Jansen, Erika Ábráhm, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, and Bernd Becker
- The COMICS tool – Computing minimal counterexamples for DTMCs. In Proc. of ATVA’12, volume 7561 of LNCS, pages 349–353. Springer-Verlag, 2012
Nils Jansen, Erika Ábráhm, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, and Bernd Becker
- Highlevel counterexamples for probabilistic automata. In Proc. of QEST’13, volume 8054 of LNCS, pages 18–33. Springer-Verlag, 2013
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábráhm, Joost-Pieter Katoen, and Bernd Becker
- Minimal counterexamples for linear-time probabilistic verification. Theoretical Computer Science, 549:61–100, 2014
Ralf Wimmer, Nils Jansen, Erika Ábráhm, Joost-Pieter Katoen, and Bernd Becker
(See online at https://doi.org/10.1016/j.tcs.2014.06.020)
