Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate

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, optimistic value iteration and topological approaches developed to compute reachability probabilities and expected rewards and prove all these algorithms to be correct. We further establish that expected visiting times are preserved under backward probabilistic bisimilarity. We study various applications of expected visiting times. The reachability probabilities of multiple bottom strongly connected components (BSCCs) can be obtained by solving a single linear equation system—as opposed to solving an equation system per BSCC. Other applications include the sound computation of the stationary distribution as well as 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.