Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL
Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL
复制标题
DOI：
10.1007/s11390-013-1324-6
复制
发表时间：
2013-03
影响因子：
0.7
通讯作者：
Liya Liu;O. Hasan;S. Tahar
中科院分区：
文献类型：
--
作者：
Liya Liu;O. Hasan;S. Tahar
马尔可夫链广泛用于工程和科学系统的不同方面的建模，例如算法的性能和系统的可靠性。已经开发了不同的技术来分析马尔可夫模型，例如，基于马尔可夫链蒙特卡罗模拟，马尔可夫分析器，以及最近的概率模型检查。然而，这些技术要么不能保证准确的分析，要么不能扩展。高阶逻辑定理证明是一种形式化的方法，能够克服上述局限性。然而，它还不够成熟，不能处理各种马尔可夫模型。在本文中，我们提出了一个形式化的离散时间马尔可夫链（DTMC），便于形式化推理的时间齐次有限状态离散时间马尔可夫链。特别地，我们利用高阶逻辑对它的一些重要性质，如联合概率、Chapman-Kolmogorov方程、可逆性等进行了形式化的验证。为了证明我们的工作的有用性，我们分析了两个应用程序：一个简化的二进制通信信道和自动邮件质量测量协议。
Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.