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

• Theoretical Computer Science •     Next Articles

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

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!
Full text



[1] Wu Xindong;. Inductive Learning[J]. , 1993, 8(2): 22 -36 .
[2] Yusuf Fatihu Hamza, Hong-Wei Lin. Conjugate-Gradient Progressive-Iterative Approximation for Loop and Catmull-Clark Subdivision Surface Interpolation[J]. Journal of Computer Science and Technology, 0, (): 1 .
[3] Na Ta, Guo-Liang Li, Jun Hu, Jian-Hua Feng. Location and Trajectory Identification from Microblogs[J]. Journal of Computer Science and Technology, 2019, 34(4): 727 -746 .
[4] Ibrahim S. Alsukayti. Quality of Service Support in RPL Networks: Standing State and Future Prospects[J]. Journal of Computer Science and Technology, 2022, 37(2): 344 -368 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved