---
res:
  bibo_abstract:
  - Model checking undiscounted reachability and expected-reward properties on Markov
    decision processes (MDPs) are key for the verification of systems that act under
    uncertainty. Popular algorithms are policy iteration and variants of value iteration;
    in tool competitions, most participants rely on the latter. These algorithms generally
    need worst-case exponential time. However, the problem can equally be formulated
    as a linear programme, solvable in polynomial time. In this paper, we give a detailed
    overview of today’s state-of-the-art algorithms for MDP model checking with a
    focus on performance and correctness. We highlight their fundamental differences,
    and describe various optimizations and implementation variants. We experimentally
    compare floating-point and exact-arithmetic implementations of all algorithms
    on three benchmark sets using two probabilistic model checkers. 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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Arnd
      foaf_name: Hartmanns, Arnd
      foaf_surname: Hartmanns
  - foaf_Person:
      foaf_givenName: Sebastian
      foaf_name: Junges, Sebastian
      foaf_surname: Junges
  - foaf_Person:
      foaf_givenName: Tim
      foaf_name: Quatmann, Tim
      foaf_surname: Quatmann
  - foaf_Person:
      foaf_givenName: Maximilian
      foaf_name: Weininger, Maximilian
      foaf_surname: Weininger
      foaf_workInfoHomepage: http://www.librecat.org/personId=02ab0197-cc70-11ed-ab61-918e71f56881
    orcid: 0000-0002-0163-2152
  bibo_doi: 10.1007/s10009-026-00848-y
  dct_date: 2026^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/1433-2779
  - http://id.crossref.org/issn/1433-2787
  dct_language: eng
  dct_publisher: Springer Nature@
  dct_subject:
  - Quantitative model checking
  - Markov decision process
  - Linear programming
  - Value iteration
  - Policy iteration
  dct_title: The revised practitioner’s guide to MDP model checking algorithms@
...