---
OA_place: publisher
OA_type: hybrid
_id: '21661'
abstract:
- lang: eng
  text: 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.
acknowledgement: "This research was funded by the European Union’s Horizon 2020 research
  and innovation programme under Marie Skłodowska-Curie grant agreements 101008233
  (MISSION)\r\nand 101034413 (IST-BRIDGE), by the Interreg North Sea project STORM_SAFE,
  by a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, by NWO
  VENI grant no. 639.021.754, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy). Experiments
  were performed with computing resources granted by RWTH Aachen University under
  project rwth1632."
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Arnd
  full_name: Hartmanns, Arnd
  last_name: Hartmanns
- first_name: Sebastian
  full_name: Junges, Sebastian
  last_name: Junges
- first_name: Tim
  full_name: Quatmann, Tim
  last_name: Quatmann
- first_name: Maximilian
  full_name: Weininger, Maximilian
  id: 02ab0197-cc70-11ed-ab61-918e71f56881
  last_name: Weininger
  orcid: 0000-0002-0163-2152
citation:
  ama: Hartmanns A, Junges S, Quatmann T, Weininger M. The revised practitioner’s
    guide to MDP model checking algorithms. <i>International Journal on Software Tools
    for Technology Transfer</i>. 2026. doi:<a href="https://doi.org/10.1007/s10009-026-00848-y">10.1007/s10009-026-00848-y</a>
  apa: Hartmanns, A., Junges, S., Quatmann, T., &#38; Weininger, M. (2026). The revised
    practitioner’s guide to MDP model checking algorithms. <i>International Journal
    on Software Tools for Technology Transfer</i>. Springer Nature. <a href="https://doi.org/10.1007/s10009-026-00848-y">https://doi.org/10.1007/s10009-026-00848-y</a>
  chicago: Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger.
    “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” <i>International
    Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2026.
    <a href="https://doi.org/10.1007/s10009-026-00848-y">https://doi.org/10.1007/s10009-026-00848-y</a>.
  ieee: A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “The revised practitioner’s
    guide to MDP model checking algorithms,” <i>International Journal on Software
    Tools for Technology Transfer</i>. Springer Nature, 2026.
  ista: Hartmanns A, Junges S, Quatmann T, Weininger M. 2026. The revised practitioner’s
    guide to MDP model checking algorithms. International Journal on Software Tools
    for Technology Transfer.
  mla: Hartmanns, Arnd, et al. “The Revised Practitioner’s Guide to MDP Model Checking
    Algorithms.” <i>International Journal on Software Tools for Technology Transfer</i>,
    Springer Nature, 2026, doi:<a href="https://doi.org/10.1007/s10009-026-00848-y">10.1007/s10009-026-00848-y</a>.
  short: A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, International Journal
    on Software Tools for Technology Transfer (2026).
date_created: 2026-04-05T22:01:32Z
date_published: 2026-03-09T00:00:00Z
date_updated: 2026-04-07T09:52:54Z
day: '09'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s10009-026-00848-y
ec_funded: 1
has_accepted_license: '1'
keyword:
- Quantitative model checking
- Markov decision process
- Linear programming
- Value iteration
- Policy iteration
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1007/s10009-026-00848-y
month: '03'
oa: 1
oa_version: Published Version
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
  call_identifier: H2020
  grant_number: '101034413'
  name: 'IST-BRIDGE: International postdoctoral program'
publication: International Journal on Software Tools for Technology Transfer
publication_identifier:
  eissn:
  - 1433-2787
  issn:
  - 1433-2779
publication_status: epub_ahead
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '21668'
    relation: software
    status: public
scopus_import: '1'
status: public
title: The revised practitioner’s guide to MDP model checking algorithms
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2026'
...