[{"OA_place":"publisher","date_updated":"2026-04-07T09:52:54Z","has_accepted_license":"1","date_published":"2026-03-09T00:00:00Z","day":"09","article_processing_charge":"Yes (in subscription journal)","citation":{"short":"A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, International Journal on Software Tools for Technology Transfer (2026).","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>.","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>.","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.","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."},"department":[{"_id":"KrCh"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"project":[{"name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020","grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"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.","year":"2026","publication_status":"epub_ahead","status":"public","publication_identifier":{"issn":["1433-2779"],"eissn":["1433-2787"]},"doi":"10.1007/s10009-026-00848-y","date_created":"2026-04-05T22:01:32Z","publication":"International Journal on Software Tools for Technology Transfer","quality_controlled":"1","type":"journal_article","related_material":{"record":[{"relation":"software","id":"21668","status":"public"}]},"article_type":"original","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"03","author":[{"first_name":"Arnd","full_name":"Hartmanns, Arnd","last_name":"Hartmanns"},{"first_name":"Sebastian","full_name":"Junges, Sebastian","last_name":"Junges"},{"full_name":"Quatmann, Tim","last_name":"Quatmann","first_name":"Tim"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881","orcid":"0000-0002-0163-2152","first_name":"Maximilian"}],"OA_type":"hybrid","scopus_import":"1","title":"The revised practitioner’s guide to MDP model checking algorithms","abstract":[{"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.","lang":"eng"}],"language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/s10009-026-00848-y"}],"_id":"21661","keyword":["Quantitative model checking","Markov decision process","Linear programming","Value iteration","Policy iteration"],"oa":1,"ec_funded":1,"ddc":["000"],"publisher":"Springer Nature"},{"_id":"20071","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2409.08119","open_access":"1"}],"oa":1,"keyword":["Farkas lemma","linear programming","extended reals","calculus of inductive constructions"],"title":"Duality theory in linear optimization and its extensions -- formally  verified","language":[{"iso":"eng"}],"external_id":{"arxiv":["2409.08119"]},"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\"."}],"month":"09","OA_type":"green","author":[{"id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","full_name":"Dvorak, Martin","last_name":"Dvorak","first_name":"Martin","orcid":"0000-0001-5293-214X"},{"id":"3D50B0BA-F248-11E8-B48F-1D18A9856A87","last_name":"Kolmogorov","full_name":"Kolmogorov, Vladimir","first_name":"Vladimir"}],"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"21393"}],"link":[{"relation":"software","url":"https://github.com/madvorak/duality/tree/v3.2","description":"full version of all definitions, statement, and proofs"}]},"type":"preprint","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa_version":"Preprint","doi":"10.48550/arXiv.2409.08119","publication":"arXiv","arxiv":1,"date_created":"2025-07-23T11:21:52Z","status":"public","publication_status":"draft","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.","year":"2024","corr_author":"1","article_processing_charge":"No","citation":{"ama":"Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions -- formally  verified. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2409.08119\">10.48550/arXiv.2409.08119</a>","mla":"Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization and Its Extensions -- Formally  Verified.” <i>ArXiv</i>, 2409.08119, doi:<a href=\"https://doi.org/10.48550/arXiv.2409.08119\">10.48550/arXiv.2409.08119</a>.","short":"M. Dvorak, V. Kolmogorov, ArXiv (n.d.).","ieee":"M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its extensions -- formally  verified,” <i>arXiv</i>. .","ista":"Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions -- formally  verified. arXiv, 2409.08119.","apa":"Dvorak, M., &#38; Kolmogorov, V. (n.d.). Duality theory in linear optimization and its extensions -- formally  verified. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2409.08119\">https://doi.org/10.48550/arXiv.2409.08119</a>","chicago":"Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization and Its Extensions -- Formally  Verified.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2409.08119\">https://doi.org/10.48550/arXiv.2409.08119</a>."},"article_number":"2409.08119","department":[{"_id":"GradSch"},{"_id":"VlKo"}],"OA_place":"repository","date_updated":"2026-03-27T12:36:59Z","day":"12","date_published":"2024-09-12T00:00:00Z"}]