Abstract

Classified Markov chains have been extensively applied to model and analyze various stochastic systems in many engineering and scientific domains. Traditionally, the analysis of these systems has been conducted using computer simulations and, more recently, also proba- bilistic model-checking. However, these methods either cannot guarantee accurate analysis or are not scalable due to the unacceptable computa- tion times. As an alternative approach, this paper proposes to reason about classified Markov chains using HOL theorem proving. We provide a formalization of discrete-time Markov chains with finite state space in higher-order logic and the formal verification of some of their widely used properties, such as irreducibility and aperiodicity. To illustrate the use- fulness of the proposed approach in analyzing real-world applications, we present the formal analysis of a generic LRU (least recently used) stack model.

HOL Code

Foundational Formalization

• dtmcBasic.sml (This file contains formalization of DTMC)
• integerSumScript.sml (This file contains the theorems related integer summation)
• setUsefulScript.sml (This file contains the underlying subtheorems)
• cond_probScript.sml (This file contains the useful condition probability theorems)
• gcd_of_setScript.sml (This file contains the formalization of the greatest common divisor of a set and four useful lemmas)
• classified_dtmc.sml (This file contains the formalization of classified DTMCs)

Application

Formal Analysis of LRU Stack Model

• LRUApp.sml (This file contains the formal verification of a LRU stack model)

LRU (Least Recently Used) Model

Least Recently Used (LRU) stack model describes a behavior of reference strings, which has the probability of referencing a given page i at time t to depend on the pages referenced in the closest past. However, this model may be a poor model of practical reference strings for some program. In [1], authors assumed the distance string for referencing a page is a sequence of independent identically distributed (IID) random variables in their LRU stack model, which was described as an irreducible & aperiodic DTMC [2]. The model of the LRU stack model is described in the following figure.


Main References

[1] B.Avi-Itzhak and D. P. Heyman. Approximate Queuing Models for Multiprogramming Computer Systems. Operations Research, 21(6):pp. 1212 - 1230, 1973.
[2] K. S. Trivedi. Probability and Statistics with Reliability, Queuing and Computer Science Applications. John Wiley & Sons, 2002.