Correct approximation of stationary distributions (Q6535371)

Calculating the invariant distribution for a discrete-time Markov chain is a classical problem, stated as ``\(\pi P = \pi\)'', where \(P\) is the transition matrix and \(\pi\) is the invariant distribution (to be found). This is simply a set of linear equations and, rearranging, the equation becomes ``\(\pi \Delta = 0\)'', where \(\Delta := I - P\) is the Laplacian. In other words, this is a (left-)eigenvector problem. Solving this does not scale well to large systems, and iterative solutions are desired.\N\NThe article shows how current model checkers, such as PRISM, may yield significantly incorrect results, often when iterative methods converge very slowly. The authors even exhibit an example of this slow convergence on a model with only four states.\N\NThe contributions can be summarised as follows.\N\begin{itemize}\N\item [\S3.] A characterisation of the invariant distribution is provided, which allows provably correct approximations.\N\N\item [\S4.] A general framework for approximating the invariant distribution is introduced.\N\N\item [\S5.] Variants of the framework are evaluated experimentally.\N\N\item [\S6.] A minimal example demonstrating the incorrectness of PRISM is provided.\N\end{itemize}\NThe approached used in this article is novel, and utilises recent advancements in \textit{partial exploration} and \textit{mean payoff}.\N\begin{itemize}\N\item Essential, the idea behind \textit{partial exploration} is to omit parts of the system which can be proved to be irrelevant -- e.g., due to having a very small invariant mass -- and focussing on the important areas. This, of course, is an approximation, the error of which must be controlled.\N\N\item \textit{Mean payoff} is specified by a Markov chain and a reward function on the state space, and corresponds to the average reward across a path. It can be computed by solving a set of linear equations, but here a value-iteration approach is used.\N\end{itemize}\N\NFor the entire collection see [Zbl 1525.68003].