Measure Theory and Markov Chains

Abstract

The future is largely unpredictable. Nondeterminism allows modelling of some phenomena arising in reactive systems, but it does not allow a quantitative estimation of how likely is one event w.r.t. another.We use the term random or probabilistic to denote systems where the quantitative estimation is possible. In this chapter we present well-studied models of probabilistic systems, called random processes and Markov chains in particular. The second come in two flavours, depending on the underlying model of time (discrete or continuous). Their key feature is called the Markov property and it allows us to develop an elegant theoretical setting, where it can be conveniently estimated, e.g., how long a system will sojourn in a given state, or the probability of finding the system in a given state at a given time or in the long run. We conclude the chapter by discussing how bisimilarity equivalences can be extended to Markov chains.

The future is independent of the past, given the present. (Markov property as folklore)