Minimal counterexamples for linear-time probabilistic verification
Minimal counterexamples for linear-time probabilistic verification
复制标题
线性时间概率验证的最小反例
DOI：
10.1016/j.tcs.2014.06.020
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Bernd Becker
中科院分区：
文献类型：
--
作者：
Ralf Wimmer;Nils Jansen;Erika Ábráhm;Joost-Pieter Katoen;Bernd Becker
属性违规的反例有许多重要的应用，如支持错误系统的调试和验证大型系统通过反例引导的抽象细化。在本文中，我们提出了使用离散时间马尔可夫链和马尔可夫决策过程的最小临界子系统作为违反ω-正则性质的反例。因此，最小值可以根据状态或转换的数量来定义。这个问题对于马尔可夫决策过程来说是NP完全的。我们将展示如何计算这样的子系统使用混合整数线性规划和评估的实际适用性，在一些实验。他们表明，我们的方法产生的反例比使用现有技术要小得多。
Counterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counterexample-guided abstraction refinement. In this paper, we propose the usage of minimal critical subsystems of discrete-time Markov chains and Markov decision processes as counterexamples for violatedω-regular properties. Minimality can thereby be defined in terms of the number of states or transitions. This problem is known to be NP-complete for Markov decision processes. We show how to compute such subsystems using mixed integer linear programming and evaluate the practical applicability in a number of experiments. They show that our method yields substantially smaller counterexample than using existing techniques.