Login | Register

Formalization of Discrete-time Markov Chains in HOL


Formalization of Discrete-time Markov Chains in HOL

Liu, Liya (2013) Formalization of Discrete-time Markov Chains in HOL. PhD thesis, Concordia University.

[thumbnail of Liu_PhD_F2013.pdf]
Text (application/pdf)
Liu_PhD_F2013.pdf - Accepted Version


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. Usually, paper-and-pencil proofs, simulation or computer algebra software are used to analyze Markovian models. However, these techniques either are not scalable or do not guarantee accurate results, which are vital in safety-critical systems. To improve the accuracy of the analysis, probabilistic model checking has been recently proposed to formally analyze Markovian systems. However, model checking suffers from the inherent state-explosion problem and thus has a very limited scope in terms of analyzing Markovian models.\newline
\indent In order to overcome the above mentioned limitations, this thesis advocates the usage of higher-order-logic theorem proving for conducting the analysis of Markov chains. We present the higher-order-logic formalization of Discrete-time Markov Chains with finite number of discrete states. We also verify some of their most widely used properties using a theorem prover. These foundations allow us to formally express and reason about Markov chains within the sound core of a theorem prover and thus attain precise results. Moreover, by building upon these foundational results, this thesis also presents the formalization of classified discrete-time Markov chains and hidden Markov chains in higher-order logic. These 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. For illustration purposes, the thesis also presents some applications 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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Liu, Liya
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:May 2013
Thesis Supervisor(s):Tahar, Sofiene
ID Code:977802
Deposited By: LI YA LIU
Deposited On:13 Jan 2014 14:58
Last Modified:18 Jan 2018 17:45
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top