Counterexamples for Timed Probabilistic Reachability
Counterexamples for Timed Probabilistic Reachability
复制标题
DOI：
10.1007/11603009_15
复制
发表时间：
2005-09
期刊：
影响因子：
--
通讯作者：
Husain Aljazzar;H. Hermanns;S. Leue
中科院分区：
文献类型：
--
作者：
Husain Aljazzar;H. Hermanns;S. Leue
无法提供违反定时概率可达性属性的反例限制了连续时间马尔可夫链 (CTMC) 的 CSL 模型检查的实际使用。反例是确定属性违规原因的重要工具，在调试过程中是必需的。我们建议使用显式状态模型检查来确定导致财产违规状态的运行。由于我们对寻找承载大量概率质量的路径感兴趣，因此我们采用定向显式状态模型检查技术来使用各种启发式引导搜索算法（例如最佳优先搜索和 Z*）来查找此类运行。用于计算启发式的估计依赖于 CTMC 的统一。我们将我们的方法应用于 SCSI-2 协议的概率模型。
The inability to provide counterexamples for the violation of timed probabilistic reachability properties constrains the practical use of CSL model checking for continuous time Markov chains (CTMCs). Counterexamples are essential tools in determining the causes of property violations and are required during debugging. We propose the use of explicit state model checking to determine runs leading into property offending states. Since we are interested in finding paths that carry large amounts of probability mass we employ directed explicit state model checking technology to find such runs using a variety of heuristics guided search algorithms, such as Best First search and Z*. The estimates used in computing the heuristics rely on a uniformisation of the CTMC. We apply our approach to a probabilistic model of the SCSI-2 protocol.