@InProceedings{ wimmer-et-al-mbmv-2012,
author = "Ralf Wimmer and Bernd Becker and
Nils Jansen and Erika {\'A}brah{\'a}m and
Joost-Pieter Katoen",
title = "Minimal Critical Subsystems as Counterexamples
for {$\omega$}-Regular {DTMC} Properties",
booktitle = "Proceedings of the 15\textsuperscript{th} Workshop
``Methoden und Beschreibungssprachen zur Modellierung
und Verifikation von Schaltungen und Systemen'' (MBMV)",
address = "Kaiserslautern, Germany",
month = mar,
year = "2012",
editor = "Jens Brandt and Klaus Schneider",
publisher = "Kova{\v c}-Verlag",
isbn = "??",
pages = "??--??",
abstract = "We propose a new approach to compute
counterexamples for violated $\omega$-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 $\omega$-regular properties.",
note = "(to appear)",
}