›› 2013,Vol. 28 ›› Issue (2): 217-231.doi: 10.1007/s11390-013-1324-6

• Special Section on Selected Paper from NPC 2011 •    下一篇

高阶逻辑HOL4中有限状态离散马可夫链的形式化方法

Liya Liu, Student Member, IEEE, Osman Hasan, and Sofiène Tahar, Student Member, IEEE   

  • 收稿日期:2012-01-06 修回日期:2012-09-11 出版日期:2013-03-05 发布日期:2013-03-05

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

Liya Liu, Student Member, IEEE, Osman Hasan, and Sofiène Tahar, Student Member, IEEE   

  1. Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada
  • Received:2012-01-06 Revised:2012-09-11 Online:2013-03-05 Published:2013-03-05

PDF (PC)

2103

离散马可夫链是具有单步记忆功能的时间和状态均离散的特殊马可夫随机过程。离散马可夫链广泛应用于物理学, 生物学, 社会学和很多不同工程学科领域, 特别是在工程系统的建模, 设计和检验过程中, 使用高阶逻辑马可夫链定理验证方法比使用数值测量, 数值仿真和物理模拟验证方法具有更完备, 更准确和扩展性更强的特征。因此近年来高阶逻辑概率模型和高阶逻辑马可夫链模型的形式化研究成为工程系统建模, 设计和验证方向的热点之一。本文在HOL4高阶逻辑平台上定义了有限状态齐次马可夫链模型, 并且用HOL4高阶逻辑验证它的一些重要性质如:联合分布概率密度函数、查普曼-科尔莫格洛夫等式及可反转性等。作为实用案例, 本文还应用该形式化的马可夫链及其性质分析了简化的二进制通信通道(Binary Communication Channel) 和自动邮件质量测量协议(AMQM protocol), 为形式化的马可夫链的应用提供了技术参考。

Abstract: 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.

[1] Bhattacharya R N, Waymire E C. Stochastic Processes withApplications (1st edition). Wiley-Interscience, 1990.

[2] MacKay D J C. Introduction to Monte Carlo methods. InProc. the NATO Advanced Study Institute on Learning inGraphical Models, Jordan M I (ed.), Kluwer Academic Pub-lishers, 1998, pp.175-204.

[3] Steward W J. Introduction to the Numerical Solution ofMarkov Chain. Princeton University Press, 1994.

[4] Haas P J. Stochastic Petri Nets: Modelling, Stability, Simu-lation. Springer, 2002.

[5] Rutten J, Kwaiatkowska M, Normal G, Parker D. Mathemati-cal techniques for analyzing concurrent and probabilisitcsystems. In CRM Monograph Series, Vol.23, AmericanMathematical Society, 2004.

[6] Baier C, Katoen J. Principles of Model Checking (Represen-tation and Mind Series). MIT Press, 2008.

[7] Gordon M J C. Mechanizing programming logics in higher-order logic. In Current Trends in Hardware Verification andAutomated Theorem Proving, Springer, 1989, pp.387-439.

[8] Liu L, Hasan O, Tahar S. Formalization of finite-statediscrete-time Markov chains in HOL. In Proc. the 9th Int.Conf. Automated Technology for Verification and Analysis,Oct. 2011, pp.90-104.

[9] Knottenbelt W J. Generalised Markovian analysis of timedtransition systems [Master's Thesis]. Department of Com-puter Science, University of Cape Town, South Africa, 1996.

[10] Jonassen H, Tessmer M D, HannumWH. Task Analysis Met-hods for Instructional Design. Lawrence Erlbaum, 1999.

[11] Sczittnick M. MACOM——A tool for evaluating communica-tion systems. In Proc. the 7th Int. Conf. Modelling Tech. and Tools for Comput. Performance Evaluation, May 1994,pp.7-10.

[12] Dingle N J, Harrison P G, Knottenbelt W J. HYDRA ——Hypergraph-based distributed response-time analyser. InProc. Int. Conf. Parallel and Distributed Processing Tech-nique and Applications, June 2003, pp.215-219.

[13] Ciardo G, Muppala J K, Trivedi K S. SPNP: Stochastic Petrinet package. In Proc. the 3rd Workshop on Petri Nets andPerformance Models, Dec. 1989, pp.142-151.

[14] Sen K, Viswanathan M, Agha G. VESTA: A statistical model-checker and analyzer for probabilistic systems. In Proc. the2nd International Conference on the Quantitative Evaluationof Systems, Sept. 2005, pp.251-252.

[15] Baier C, Haverkort B, Hermanns H et al. Model-checkingalgorithms for continuous-time Markov chains. IEEE Trans-actions on Software Engineering, 2003, 29(4): 524-541.

[16] Nedzusiak A. σ-fields and probability. Journal of FormalizedMathematics, 1989, 1, pp.1-6.

[17] Bialas J. The σ-additive measure theory. Journal of Formali-zed Mathematics, 1990, 2, pp.1-7.

[18] Hurd J. Formal verification of probabilistic algorithms [Ph.D.Thesis]. University of Cambridge, UK, 2002.

[19] Hasan O. Formal probabilistic analysis using theorem proving[Ph.D. Thesis]. Concordia University, Canada, 2008.

[20] Hasan O, Abbasi N, Akbarpour B, Tahar S, Akbarpour R.Formal reasoning about expectation properties for continu-ous random variables. In Proc. Formal Methods 2009, Nov.2009, pp.435-450.

[21] Mhamdi T, Hasan O, Tahar S. Formalization of entropy mea-sures in HOL. In Proc. the 2nd Interactive Theorem Proving,Aug. 2011, pp.233-248.

[22] H?olzl J, Heller A. Three chapters of measure theory in Is-abelle/HOL. In Proc. the 2nd Interactive Theorem Proving,Aug. 2011, pp.135-151.

[23] Paulson L C. Isabelle: A Generic Theorem Prover, Springer,1994.

[24] Gordon M J C, Melham T F. Introduction to HOL: A Theo-rem Proving Environment for Higher-Order Logic. Cam-bridge University Press, 1993.

[25] Milner R. A theory of type polymorphism in programming.J. Computer and System Sciences, 1977, 17(3): 348-375.

[26] Harrison J. Theorem Proving with the Real Numbers.Springer, 1998.

[27] Hasan O, Tahar S. Reasoning about conditional probabilitiesin a higher-order-logic theorem prover. Journal of AppliedLogic, 2011, 9(1): 23-40.

[28] Norris J R. Markov Cains. Cambridge University Press, 1999.

[29] Prabhu N U. Stochastic Processes: Basic Theory and Its Ap-plications. World Scientific Publisher, 2007.

[30] Trivedi K S. Probability and Statistics with Reliability, Queu-ing, and Computer Science Applications (2nd edition). JohnWiley & Sons, 2001.

[31] ISO/IEC 18000-7——Information Technology——Radio fre-quency identification for item management——Part 7: Pa-rameters for active air interface communications at 433 MHz,2008.

[32] Nokovic B, Sekerinski E. Analysis of interrogator-tag commu-nication protocols. Technical Report, McMaster University,2010.
No related articles found!
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 吴信东;. Inductive Learning[J]. , 1993, 8(2): 22 -36 .
[2] . [J]. 计算机科学技术学报, 0, (): 1 .
[3] Na Ta, Guo-Liang Li, Jun Hu, Jian-Hua Feng. 微博位置与轨迹识别[J]. 计算机科学技术学报, 2019, 34(4): 727 -746 .
[4] . RPL网络服务质量(QoS)支持：现状及展望[J]. 计算机科学技术学报, 2022, 37(2): 344 -368 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：