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.

翻译：我们研究离散时间和连续时间马尔可夫链中每个状态期望访问次数的精确高效计算方法。为在保证计算精度的前提下提升效率，我们将区间迭代与拓扑方法（已知用于可达概率和期望奖励计算）推广至本问题。进一步研究了期望访问时间的应用场景，包括平稳分布的可靠计算以及以到达多个目标状态为条件的期望奖励。在概率模型检测器Storm中实现的算法可扩展至包含数百万个状态的大规模系统。基于定量验证基准集的实验表明，通过期望访问时间计算平稳分布的方法始终优于现有方法——有时甚至会提升数个数量级的性能。