Paper in Journal on Automated Reasoning

The paper “Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate” by Hannah Mertens, Tim Quatmann, Tobias Winkler and Joost-Pieter Katoen has been accepted for publication in the Journal of Automated Reasoning. This paper presents several numerical algorithms to compute expected visiting times (aka: occupation times) in DTMCs and CTMCs, and aplies them to efficiently and accurately computing stationary distributions. The paper extends the TACAS 2024 paper with a correspondence to backward probabilistic bisimilarity, a discussion on MDPs, and detailed proofs.