Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL

查看全文 作　　者：Liya [1]Liu;Osman [1]Hasan;Sofiène [1]Tahar

机构地区：[1]Department of Electrical and Computer Engineering, Concordia University

出　　处：《Journal of Computer Science & Technology》索引2013年第28卷第2期,共15页

摘　　要：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. 关键词：离散时间有限状态推理 HOL 马氏链马尔可夫链马尔可夫模型蒙特卡罗模拟

相关文献

参考文献（32）
引证文献（4）
耦合文献（0）

参考文献(32)

引证文献(4)

互联网出版许可证新出网证(渝)字10号全国400电话 - 免长途话费

Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL

参考文献(32)

引证文献(4)

用户提示