Formalization of Birth-Death and IID Processes in Higher-order Logic

Technical Report

Abstract
Markov chains are extensively used in modeling and analysis of engineering and scientific problems. 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. Probabilistic model checking has been recently proposed to formally analyze Markovian systems, but it suffers from the inherent state-explosion problem and unacceptable long computation times. To overcome these limitations, in this paper, we develop a framework to formally analyze discrete-time Markov models with finite state-space using higher-order logic theorem proving. The core component of the proposed framework is a higher-order-logic formalization of Discrete-Time Markov Chains (DTMC) and classified DTMCs. The proposed framework is generic enough to be used for extending the library of formal reasoning support for Markovian models and analyzing many real-world stochastic problems. In order to demonstrate the usefulness of our framework to formalize other Markov chain related concepts, we present the formalization of a Discrete-time Birth-Death process and the discrete Independent and Identically Distributed (IID) random process. Moreover, for illustrating the practical utilization of our framework, we use it to formally analyze the performance of a program, which controls a CPU and its connected devices through the system bus, as well as the performance of a data structure in a program.

Files

• Technical Report: PDF File
• HOL Script: HOL Script