Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties.
Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen · FreiDok plus (Universitätsbibliothek Freiburg) · 2012
We propose a new approach to compute counterexamples for violated ω-regular properties of discrete-time Markov chains. Whereas most approaches compute a set of system paths as a counterexample, we determine a critical subsystem that already violates the given property. In earlier work methods have been introduced to compute such subsystems for safety properties, based on a search for shortest paths. In this paper we use mixed integer linear programming to determine minimal critical subsystems for arbitrary ω-regular properties.