Title: A Practitioner's Guide to MDP Model Checking Algorithms
Authors:
* Arnd Hartmanns (University of Twente)
* Sebastian Junges (Radboud University Nijmegen)
* Tim Quatmann (RWTH Aachen University)
* Maximilian Weininger (Technical University of Munich)
Short summary:
In this paper, we give a detailed overview of today's state-of-the-art algorithms for MDP model checking, including variants of value iteration, policy iteration, and linear programming. We highlight their fundamental differences, and describe various optimisations and implementation variants. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners - tool builders and users alike.
