What is the best algorithm for MDP model checking?

International Journal on Software Tools for Technology Transfer, vol. 27, pp. 431–437

Abstract

Abstract Computing reachability probabilities and expected rewards for Markov decision processes is a core feature of probabilistic model checkers. Value iteration (VI) is the predominantly implemented approach but occasionally yields vastly incorrect results. Interval iteration (II), sound value iteration (SVI), and optimistic value iteration (OVI) are recently proposed variants of VI that produce sound approximations of the desired values. Hartmanns and Kaminski (CAV (2), pp. 488–511, 2020) empirically compared the three approaches using implementations in the model checker mcsta and a broad selection of benchmarks. They concluded that OVI is faster than II and SVI for the majority of instances. We replicate these research results using implementations in the model checker Storm. The key insight is that OVI still mostly outperforms II and SVI, but the competition becomes tighter.

Authors 1

1. Tim Quatmann corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany