2024/01/19 by Hannah Mertens, Mertens, Hannah, Joost-Pieter Katoen +5 · 1 citation
Computer Science · Decision Sciences · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Probability (math.PR) #Simulation Techniques and Applications
paper · pdf · doi:10.48550/arxiv.2401.10638
openalex publication_date 2024/01/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.