Markov chains are extensively used in the modeling and analysis of engineering and scientific problems which can be expressed as random processes with the memoryless property. This project advocates the usage of higher-order-logic theorem proving for conducting the analysis of Markov chains. We provide the higher-order-logic formalization of Discrete-time Markov Chains with a finite number of discrete states. We then verify some of their most widely used properties using the HOL4 theorem prover. By building upon these foundational results, we also developed the formalization of classified discrete-time Markov chains and hidden Markov chains in higher-order logic. The above are widely used concepts in the analysis of Markovian models and thus allow us to tackle the formal analysis of a wide range of engineering and scientific systems, including a binary communication channel, the automatic mail quality measurement (AMQM) protocol, a DNA sequence, a least recently used (LRU) stack model and the birth-death process.

HOL Script

Formalization of Discrete-time Markov Chains in HOL

Thesis

[1] Liya Liu, Formalization of Discrete-time Markov Chains in HOL, PhD Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, June 2013.

Publications

Journal Papers

[2] L. Liu, O. Hasan, and S. Tahar: Formal Reasoning about Finite-state Discrete-Time Markov Chains in HOL; Journal of Computer Science and Technology, Springer, Vol. 28, No. 2, March 2013, pp. 231-217.

Conference Papers

[3] L. Liu, V. Aravantinos, O. Hasan, and S. Tahar: On the Formal Analysis of HMM using Theorem Proving; In: S. Merz and J. Pang (Eds.), Formal Methods and Software Engineering, Lecture Notes in Computer Science 8829, Springer Verlag, 2014, pp. 316.331. [Proc. International Conference on Formal Engineering Methods (ICFEM.14), Luxembourg, Luxembourg, November 2014.]

[4] L. Liu, O. Hasan, and S. Tahar: Formal Analysis of Memory Contention in a Multiprocessor System In: J. Iyoda and L. de Moura (Eds.) Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 8195, Springer Verlag, 2013, pp. 195-210. [Proc. of The Brazilian Symposium on Formal Methods (SBMF.13), Brasilia, Brazil, September 2014]

[5] L. Liu, O. Hasan, V. Aravantinos, and S. Tahar: Formal Reasoning about Classified Markov Chains in HOL [In: S. Blazy, C. Paulin-Mohring, D. Pichardie, Interactive Theorem Proving (ITP.13), Lecture Notes in Computer Science 7998, Springer Verlag, 2013, pp. 295-310.]

[6] L. Liu, O. Hasan, and S. Tahar: Formalization of Finite-state Discrete-Time Markov Chains in HOL Automated Technology for Verification and Analysis, Lecture Notes in Computer Sciences 6996, Springer-Verlag, 2011, pp. 90-104. [ Proc. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA.11), Taipei, Taiwan, November 2011.]

Technical Reports

[7] L. Liu, O. Hasan, ans S. Tahar: Formalization of Birth-Death and IID Processes in Higher-order Logic, Technical Report, Department of Electrical and Computer Engineering, Concordia University, November 2016. [35 Pages].

[8] L. Liu, O. Hasan, and S. Tahar: On the Formalization of Continuous-Time Markov Chain in HOL, Technical Report, Department of Electrical and Computer Engineering, Concordia University, April 2013. [12 Pages]

[9] L. Liu, O. Hasan, and S. Tahar: Formalization of Discrete-Time Markov Chain in HOL, Technical Report, Department of Electrical and Computer Engineering, Concordia University, April 2011. [15 Pages]