Formal Reasoning about Classified Markov Chains in HOL
Formal Reasoning about Classified Markov Chains in HOL
复制标题
HOL 中分类马尔可夫链的形式化推理
DOI：
10.1007/978-3-642-39634-2_22
复制
发表时间：
2013
影响因子：
--
通讯作者：
S. Tahar
中科院分区：
文献类型：
--
作者：
Liya Liu;O. Hasan;Vincent Aravantinos;S. Tahar
分类马尔可夫链在许多工程和科学领域广泛应用于各种随机系统的建模和分析。传统上，这些系统的分析是使用计算机模拟进行的，最近也使用概率模型检查。然而，这些方法要么不能保证准确的分析，要么由于不可接受的计算时间而无法扩展。作为一种替代方法，本文提出使用HOL定理证明对分类马尔可夫链进行推理。给出了高阶逻辑中有限状态空间的分类离散马尔可夫链的形式化，并对其一些常用性质进行了形式化验证。为了说明所提出方法的有效性，我们提出了一个通用LRU（最近最少使用）堆栈模型的形式化分析。
Classified Markov chains have been extensively applied to model and analyze various stochastic systems in many engineering and scientific domains. Traditionally, the analysis of these systems has been conducted using computer simulations and, more recently, also probabilistic model-checking. However, these methods either cannot guarantee accurate analysis or are not scalable due to the unacceptable computation times. As an alternative approach, this paper proposes to reason about classified Markov chains using HOL theorem proving. We provide a formalization of classified discrete-time Markov chains with finite state space in higher-order logic and the formal verification of some of their widely used properties. To illustrate the usefulness of the proposed approach, we present the formal analysis of a generic LRU (least recently used) stack model.
马尔可夫链的交互式验证：两个分布式协议案例研究
DOI：
10.4204/eptcs.103.2
发表时间：
2012
期刊：
影响因子：
--
作者：
Johannes Hölzl;Tobias Nipkow
通讯作者：
Tobias Nipkow