Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains

TL;DR

The paper tackles accurate, scalable computation of expected visiting times (EVTs) for finite DTMCs and CTMCs, enabling sound bounds on downstream metrics such as stationary distributions and conditional rewards. It introduces a sound EVT framework based on Interval Iteration and a topological, SCC-wise approach, ensuring $\epsilon$-sound guarantees. EVTs are shown to underpin reductions to stationary distributions and to conditional expectations, with a concrete StormSTORM implementation demonstrating scalability to millions of states and superior performance over prior methods. The results establish EVT-based techniques as a powerful, scalable tool for quantitative verification of probabilistic systems.

Abstract

We study the accurate and efficient computation of the expected number of times each state is visited in discrete- and continuous-time Markov chains. To obtain sound accuracy guarantees efficiently, we lift interval iteration and topological approaches known from the computation of reachability probabilities and expected rewards. We further study applications of expected visiting times, including the sound computation of the stationary distribution and expected rewards conditioned on reaching multiple goal states. The implementation of our methods in the probabilistic model checker Storm scales to large systems with millions of states. Our experiments on the quantitative verification benchmark set show that the computation of stationary distributions via expected visiting times consistently outperforms existing approaches - sometimes by several orders of magnitude.

Figures (2)

• Figure 1: Fast Dice Roller
• Figure 2: Running example DTMC. The individual EVTs are below the states.

Theorems & Definitions (1)

• definition thmcounterdefinition