The two papers “What is the Best Algorithm for MDP Model Checking?” by Tim Quatmann and “The Revised Practitioner’s Guide to MDP Model Checking Algorithms” by Arnd Hartmanns (University of Twente), Sebastian Junges (Radboud University), Tim Quatmann, and Maximilian Weininger (TU Munich, IST Austria) have been accepted in the International Journal on Software Tools for Technology Transfer (Special Issues RRRR 2022 and TACAS 2023, respectively).

Both papers address the current state of the art in MDP model checking. The first paper is a replication study of the experimental results of the paper “Optimistic Value Iteration” by Hartmanns and Kaminski. The second paper contains an extensive practical evaluation of the various MDP model checking algorithms based on Value Iteration, Linear Programming, and Policy iteration.