  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.
