Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation
Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation
复制标题
用于概率模型检查的定向启发式反例生成：比较评估
DOI：
10.1145/1808877.1808883
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Stefan Leue
中科院分区：
文献类型：
--
作者：
Husain Aljazzar;Matthias Kuntz;Florian Leitner-Fischer;Stefan Leue
在过去的五年中，概率模型检验的反例生成一直是一个活跃的研究领域。本研究的主要成果是提出了一种新的有向启发式算法，用于有效地生成概率反例，如K * 和XBF。在本文中，我们提出了一个经验评估这些算法的效率和著名的Eppstein算法。我们还将评估应用于Eppstein、K* 和XBF的优化效果。此外，我们将展示如何在模型检查过程中产生的信息可以用来指导搜索反例。这是自动生成启发式函数的第一步。各种算法的实验评估是通过将它们应用于一个案例研究，knwon从文献中的概率模型检查和一个案例研究，从汽车行业。
The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such asK* and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimisations applied to Eppstein,K* and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, knwon from the literature on probabilistic model checking and one case study taken from the automotive industry.
登录
查看更多内容
影响因子：
7.4
作者：
Aljazzar, Husain;Leue, Stefan
通讯作者：
Leue, Stefan
标记马尔可夫链上 PCTL 的 Hintikka 游戏
DOI：
--
发表时间：
2008
期刊：
2008 Fifth International Conference on Quantitative Evaluation of Systems
影响因子：
--
作者：
Harald Fecher;M. Huth;Nir Piterman;Daniel Wagner
通讯作者：
Daniel Wagner
使用概率 FMEA 和概率反例对安全气囊系统进行安全分析
DOI：
10.1109/qest.2009.8
发表时间：
2009
期刊：
2009 Sixth International Conference on the Quantitative Evaluation of Systems
影响因子：
--
作者：
Husain Aljazzar;Manuel Fischer;Lars Grunske;Matthias Kuntz;Florian Leitner-Fischer;Stefan Leue
通讯作者：
Stefan Leue
K*：一种用于查找 k 最短路径的定向即时算法
DOI：
--
发表时间：
2008
期刊：
影响因子：
--
作者：
Husain Aljazzar;S. Leue
通讯作者：
S. Leue
K* ：启发式引导、动态 k 个最短路径搜索
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
Husain Aljazzar;S. Leue
通讯作者：
S. Leue