Abstract

Discrete-time Markov chains are an important tool in probabilistic analysis of computer systems. For example they are used to describe the behavior of computer programs with probabilistic choice or the time-dependent distribution of input values. Current formalizations of Markov chains are restricted to a finite state space. We extend this to a countable state space, construct the stochastic process of a Markov chain given a matrix of transition probabilities, and prove the equivalence with the axiomatic definition as stochastic process. Based on this we introduce irreducible, recurrent, and aperiodic classes, generating functions and stationary distributions to analyze Markov chains.

Keywords: Markov chain, probability theory, mathematical analysis, Isabelle/HOL

Analyzing Discrete-Time Markov Chains with Countable State Space in Isabelle/HOL.
Johannes Hölzl.
Draft

The paper references the following work, which uses the formalized Markov chains with infinite state spaces:

Formalizing Probabilistic Noninterference.
Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
Accepted at Certified Programs and Proofs 2013 (CPP '13)

The download contains:

Download

The first section of the generated documents contain an overview the definitions and theorems in the paper related to the theory files.

This verification of Markov chains works with the development version of Isabelle.