Extended Directed Search for Probabilistic Timed Reachability
Extended Directed Search for Probabilistic Timed Reachability
复制标题
DOI：
10.1007/11867340_4
复制
发表时间：
2006-09
期刊：
影响因子：
--
通讯作者：
Husain Aljazzar;S. Leue
中科院分区：
文献类型：
--
作者：
Husain Aljazzar;S. Leue
现有的随机系统数值模型检查器能够有效地分析随机模型。然而，它们不能提供调试信息的事实限制了它们的实际使用。在前期工作中，我们提出了一种选择诊断轨迹的方法，用功能模型检查的说法，通常称为故障轨迹或反例，用于离散时间和连续时间马尔可夫链上的概率时间可达性。我们应用定向显式状态搜索算法（如Z *）来确定具有大量概率的诊断轨迹。在本文中，我们将这种方法扩展到确定携带大概率质量的轨迹集，因为随机系统的性质通常不被单个轨迹所违反，而是被那些轨迹的集合所违反。为此，我们扩展了现有的启发式引导搜索算法，以便它们选择轨迹集。结果以马尔可夫链的形式提供。这种诊断马尔可夫链不仅是诊断和调试的必要工具，而且还允许从下面近似求解时间可达概率。在特殊情况下，它们还提供了真实的反例，可用于显示对给定属性的违反。我们的算法已经在随机模型检查器PRISM中实现。我们使用一些案例研究来说明我们的方法的适用性。
Current numerical model checkers for stochastic systems can efficiently analyse stochastic models. However, the fact that they are unable to provide debugging information constrains their practical use. In precursory work we proposed a method to select diagnostic traces, in the parlance of functional model checking commonly referred to as failure traces or counterexamples, for probabilistic timed reachability properties on discrete-time and continuous-time Markov chains. We applied directed explicit-state search algorithms, like Z∗, to determine a diagnostic trace which carries large amount of probability. In this paper we extend this approach to determining sets of traces that carry large probability mass, since properties of stochastic systems are typically not violated by single traces, but by collections of those. To this end we extend existing heuristics guided search algorithms so that they select sets of traces. The result is provided in the form of a Markov chain. Such diagnostic Markov chains are not just essential tools for diagnostics and debugging but, they also allow the solution of timed reachability probability to be approximated from below. In particular cases, they also provide real counterexamples which can be used to show the violation of the given property. Our algorithms have been implemented in the stochastic model checker PRISM. We illustrate the applicability of our approach using a number of case studies.