---
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. International Journal on Software Tools
for Technology Transfer. 2026. doi:10.1007/s10009-026-00848-y
apa: 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. Springer Nature. https://doi.org/10.1007/s10009-026-00848-y
chicago: Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger.
“The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” International
Journal on Software Tools for Technology Transfer. Springer Nature, 2026.
https://doi.org/10.1007/s10009-026-00848-y.
ieee: A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “The revised practitioner’s
guide to MDP model checking algorithms,” International Journal on Software
Tools for Technology Transfer. 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.” International Journal on Software Tools for Technology Transfer,
Springer Nature, 2026, doi:10.1007/s10009-026-00848-y.
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
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'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '22607'
abstract:
- lang: eng
text: "Farkas established that a system of linear inequalities has a solution if
and only if we cannot obtain a contradiction by taking a linear combination of
the inequalities. We state and formally prove several Farkas-like theorems over
linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the
case when some coefficients are allowed to take \"infinite values\".\r\nCode:
https://github.com/madvorak/duality/tree/v3.2.0"
acknowledgement: "We would like to thank David Bartl and Jasmin Blanchette for frequent
consultations.\r\nWe would also like to express gratitude to Henrik Böving for a
help with generalization\r\nfrom extended rationals to extended linearly ordered
fields and to Andrew Yang for the\r\nproof of Finset.univ_sum_of_zero_when_not.
We would also like to acknowledge Antoine\r\nChambert-Loir, Apurva Nakade, Yaël
Dillies, Richard Copley, Edward van de Meent, Markus\r\nHimmel, Mario Carneiro,
and Kevin Buzzard."
article_number: '14253'
article_processing_charge: Yes (in subscription journal)
article_type: original
arxiv: 1
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
citation:
ama: Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions
-- formally verified. Annals of Formalized Mathematics. 2026;2. doi:10.46298/afm.14253
apa: Dvorak, M., & Kolmogorov, V. (2026). Duality theory in linear optimization
and its extensions -- formally verified. Annals of Formalized Mathematics.
EPI Sciences. https://doi.org/10.46298/afm.14253
chicago: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
and Its Extensions -- Formally Verified.” Annals of Formalized Mathematics.
EPI Sciences, 2026. https://doi.org/10.46298/afm.14253.
ieee: M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its
extensions -- formally verified,” Annals of Formalized Mathematics, vol.
2. EPI Sciences, 2026.
ista: Dvorak M, Kolmogorov V. 2026. Duality theory in linear optimization and its
extensions -- formally verified. Annals of Formalized Mathematics. 2, 14253.
mla: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
and Its Extensions -- Formally Verified.” Annals of Formalized Mathematics,
vol. 2, 14253, EPI Sciences, 2026, doi:10.46298/afm.14253.
short: M. Dvorak, V. Kolmogorov, Annals of Formalized Mathematics 2 (2026).
corr_author: '1'
das_tickbox: '0'
date_created: 2026-07-29T09:06:55Z
date_published: 2026-03-13T00:00:00Z
date_updated: 2026-07-29T10:50:17Z
day: '13'
ddc:
- '500'
department:
- _id: VlKo
- _id: GradSch
doi: 10.46298/afm.14253
external_id:
arxiv:
- '2409.08119'
has_accepted_license: '1'
intvolume: ' 2'
keyword:
- Farkas lemma
- linear programming
- extended reals
- calculus of inductive constructions
language:
- iso: eng
mathsc:
- 68V20
- 15A39
- 90C05
month: '03'
oa_version: Published Version
publication: Annals of Formalized Mathematics
publication_identifier:
eissn:
- 3117-4604
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
record:
- id: '20071'
relation: earlier_version
status: public
researchdata_availability: no
status: public
supplementarymaterial: no
title: Duality theory in linear optimization and its extensions -- formally verified
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
volume: 2
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '20071'
abstract:
- lang: eng
text: Farkas established that a system of linear inequalities has a solution if
and only if we cannot obtain a contradiction by taking a linear combination of
the inequalities. We state and formally prove several Farkas-like theorems over
linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the
case when some coefficients are allowed to take "infinite values".
acknowledgement: We would like to thank David Bartl and Jasmin Blanchette for frequent
consultations. We would also like to express gratitude to Andrew Yang for the proof
of Finset.univ sum of zero when not and to Henrik B¨oving for a help with generalization
from extended rationals to extended linearly ordered fields. We would also like
to acknowledge Antoine Chambert-Loir, Apurva Nakade, Ya¨el Dillies, Richard Copley,
Edward van de Meent, Markus Himmel, Mario Carneiro, and Kevin Buzzard.
article_number: '2409.08119'
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
citation:
ama: Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions
-- formally verified. arXiv. doi:10.48550/arXiv.2409.08119
apa: Dvorak, M., & Kolmogorov, V. (n.d.). Duality theory in linear optimization
and its extensions -- formally verified. arXiv. https://doi.org/10.48550/arXiv.2409.08119
chicago: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
and Its Extensions -- Formally Verified.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2409.08119.
ieee: M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its
extensions -- formally verified,” arXiv. .
ista: Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions
-- formally verified. arXiv, 2409.08119.
mla: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
and Its Extensions -- Formally Verified.” ArXiv, 2409.08119, doi:10.48550/arXiv.2409.08119.
short: M. Dvorak, V. Kolmogorov, ArXiv (n.d.).
corr_author: '1'
date_created: 2025-07-23T11:21:52Z
date_published: 2024-09-12T00:00:00Z
date_updated: 2026-07-29T12:56:51Z
day: '12'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2409.08119
external_id:
arxiv:
- '2409.08119'
keyword:
- Farkas lemma
- linear programming
- extended reals
- calculus of inductive constructions
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2409.08119
month: '09'
oa: 1
oa_version: Preprint
publication: arXiv
publication_status: draft
related_material:
link:
- description: full version of all definitions, statement, and proofs
relation: software
url: https://github.com/madvorak/duality/tree/v3.2
record:
- id: '22607'
relation: later_version
status: public
- id: '21393'
relation: dissertation_contains
status: public
status: public
title: Duality theory in linear optimization and its extensions -- formally verified
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2024'
...