Formalization of Finite-State Discrete-Time Markov Chains in HOL
Formalization of Finite-State Discrete-Time Markov Chains in HOL
复制标题
HOL 中有限状态离散时间马尔可夫链的形式化
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
S. Tahar
中科院分区：
文献类型：
--
作者：
Liya Liu;O. Hasan;S. Tahar
马尔可夫链的数学概念被广泛用于对许多工程和科学问题进行建模和分析。马尔可夫模型通常使用计算机模拟进行分析，近期也使用概率模型检验，但这些方法要么不能保证精确分析，要么不具有可扩展性。作为一种替代方法，我们提议使用高阶逻辑定理证明来推导可描述为马尔可夫链的系统的性质。作为朝着这个目标迈出的第一步，本文介绍了时间齐次有限状态离散时间马尔可夫链的形式化，以及使用HOL定理证明器对其一些基本性质（如联合概率、查普曼 - 科尔莫戈罗夫方程和稳态概率）的形式验证。为了便于说明，我们利用我们的形式化来分析一个简化的二进制通信信道。
The mathematical concept of Markov chains is widely used to model and analyze many engineering and scientific problems. Markovian models are usually analyzed using computer simulation, and more recently using probabilistic model-checking but these methods either do not guarantee accurate analysis or are not scalable. As an alternative, we propose to use higher-order-logic theorem proving to reason about properties of systems that can be described as Markov chains. As the first step towards this goal, this paper presents a formalization of time homogeneous finite-state Discrete-time Markov chains and the formal verification of some of their fundamental properties, such as Joint probabilities, Chapman-Kolmogorov equation and steady state probabilities, using the HOL theorem prover. For illustration purposes, we utilize our formalization to analyze a simplified binary communication channel.