Symbolic counterexample generation for large discrete-time Markov chains
Symbolic counterexample generation for large discrete-time Markov chains
复制标题
DOI：
10.1016/j.scico.2014.02.001
复制
发表时间：
2014-10-01
影响因子：
1.3
通讯作者：
Schuster, Johann
中科院分区：
文献类型：
--
作者：
Jansen, Nils;Wimmer, Ralf;Schuster, Johann
本文提出了几种不满足PCTL公式的离散时间马尔可夫链（DTMC）的符号反例生成算法。反例是增量生成的子DTMC（的符号表示）。这种渐进式方法的关键是属于反例的路径的符号生成。我们考虑两种方法。首先，我们扩展了有界模型检测，并开发了一个简单的启发式生成高度可能的路径第一。然后，我们补充SAT为基础的方法，通过一个完全（多终端）BOO为基础的技术。所有的符号方法的实施，我们的实验结果表明，大大优于现有的显式技术的可扩展性。特别是，我们基于BDD的方法使用一种称为片段搜索的方法，允许为具有数十亿个状态（最多10（15））的DTMC生成反例。(C)2014爱思唯尔有限公司版权所有。
This paper presents several symbolic counterexample generation algorithms for discrete-time Markov chains (DTMCs) violating a PCTL formula. A counterexample is (a symbolic representation of) a sub-DTMC that is incrementally generated. The crux to this incremental approach is the symbolic generation of paths that belong to the counterexample. We consider two approaches. First, we extend bounded model checking and develop a simple heuristic to generate highly probable paths first. We then complement the SAT-based approach by a fully (multi-terminal) BOO-based technique. All symbolic approaches are implemented, and our experimental results show a substantially better scalability than existing explicit techniques. In particular, our BDD-based approach using a method called fragment search allows for counterexample generation for DTMCs with billions of states (up to 10(15)). (C) 2014 Elsevier B.V. All rights reserved.