[{"type":"journal_article","month":"03","_id":"21661","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.","OA_place":"publisher","date_updated":"2026-04-07T09:52:54Z","quality_controlled":"1","scopus_import":"1","title":"The revised practitioner’s guide to MDP model checking algorithms","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"day":"09","year":"2026","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"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"}],"main_file_link":[{"url":"https://doi.org/10.1007/s10009-026-00848-y","open_access":"1"}],"ddc":["000"],"date_published":"2026-03-09T00:00:00Z","citation":{"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>.","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>","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.","short":"A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, International Journal on Software Tools for Technology Transfer (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.","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>.","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>"},"publisher":"Springer Nature","oa":1,"OA_type":"hybrid","publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"department":[{"_id":"KrCh"}],"oa_version":"Published Version","date_created":"2026-04-05T22:01:32Z","keyword":["Quantitative model checking","Markov decision process","Linear programming","Value iteration","Policy iteration"],"author":[{"last_name":"Hartmanns","full_name":"Hartmanns, Arnd","first_name":"Arnd"},{"first_name":"Sebastian","last_name":"Junges","full_name":"Junges, Sebastian"},{"last_name":"Quatmann","full_name":"Quatmann, Tim","first_name":"Tim"},{"full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","orcid":"0000-0002-0163-2152","last_name":"Weininger","first_name":"Maximilian"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"relation":"software","id":"21668","status":"public"}]},"publication":"International Journal on Software Tools for Technology Transfer","has_accepted_license":"1","ec_funded":1,"article_processing_charge":"Yes (in subscription journal)","doi":"10.1007/s10009-026-00848-y","publication_status":"epub_ahead","article_type":"original"},{"author":[{"full_name":"Toman, Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-9036-063X","last_name":"Toman","first_name":"Viktor"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"9987","relation":"part_of_dissertation"},{"status":"public","id":"10191","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"141"},{"id":"10190","relation":"part_of_dissertation","status":"public"}]},"keyword":["concurrency","verification","model checking"],"date_created":"2021-10-29T20:09:01Z","publication_status":"published","acknowledged_ssus":[{"_id":"SSU"}],"doi":"10.15479/at:ista:10199","article_processing_charge":"No","has_accepted_license":"1","ec_funded":1,"corr_author":"1","publisher":"Institute of Science and Technology Austria","citation":{"apa":"Toman, V. (2021). <i>Improved verification techniques for concurrent systems</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:10199\">https://doi.org/10.15479/at:ista:10199</a>","mla":"Toman, Viktor. <i>Improved Verification Techniques for Concurrent Systems</i>. Institute of Science and Technology Austria, 2021, doi:<a href=\"https://doi.org/10.15479/at:ista:10199\">10.15479/at:ista:10199</a>.","ieee":"V. Toman, “Improved verification techniques for concurrent systems,” Institute of Science and Technology Austria, 2021.","chicago":"Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.” Institute of Science and Technology Austria, 2021. <a href=\"https://doi.org/10.15479/at:ista:10199\">https://doi.org/10.15479/at:ista:10199</a>.","short":"V. Toman, Improved Verification Techniques for Concurrent Systems, Institute of Science and Technology Austria, 2021.","ista":"Toman V. 2021. Improved verification techniques for concurrent systems. Institute of Science and Technology Austria.","ama":"Toman V. Improved verification techniques for concurrent systems. 2021. doi:<a href=\"https://doi.org/10.15479/at:ista:10199\">10.15479/at:ista:10199</a>"},"ddc":["000"],"date_published":"2021-10-31T00:00:00Z","publication_identifier":{"issn":["2663-337X"]},"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"file":[{"file_name":"toman_th_final.pdf","relation":"main_file","content_type":"application/pdf","file_id":"10225","creator":"vtoman","date_created":"2021-11-08T14:12:22Z","checksum":"4f412a1ee60952221b499a4b1268df35","access_level":"open_access","file_size":2915234,"date_updated":"2021-11-08T14:12:22Z"},{"file_size":8616056,"date_updated":"2021-11-09T09:00:50Z","access_level":"closed","file_id":"10226","checksum":"9584943f99127be2dd2963f6784c37d4","creator":"vtoman","date_created":"2021-11-08T14:12:46Z","relation":"source_file","content_type":"application/zip","file_name":"toman_thesis.zip"}],"oa_version":"Published Version","oa":1,"status":"public","year":"2021","day":"31","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","title":"Improved verification techniques for concurrent systems","abstract":[{"text":"The design and verification of concurrent systems remains an open challenge due to the non-determinism that arises from the inter-process communication. In particular, concurrent programs are notoriously difficult both to be written correctly and to be analyzed formally, as complex thread interaction has to be accounted for. The difficulties are further exacerbated when concurrent programs get executed on modern-day hardware, which contains various buffering and caching mechanisms for efficiency reasons. This causes further subtle non-determinism, which can often produce very unintuitive behavior of the concurrent programs. Model checking is at the forefront of tackling the verification problem, where the task is to decide, given as input a concurrent system and a desired property, whether the system satisfies the property. The inherent state-space explosion problem in model checking of concurrent systems causes naïve explicit methods not to scale, thus more inventive methods are required. One such method is stateless model checking (SMC), which explores in memory-efficient manner the program executions rather than the states of the program. State-of-the-art SMC is typically coupled with partial order reduction (POR) techniques, which argue that certain executions provably produce identical system behavior, thus limiting the amount of executions one needs to explore in order to cover all possible behaviors. Another method to tackle the state-space explosion is symbolic model checking, where the considered techniques operate on a succinct implicit representation of the input system rather than explicitly accessing the system. In this thesis we present new techniques for verification of concurrent systems. We present several novel POR methods for SMC of concurrent programs under various models of semantics, some of which account for write-buffering mechanisms. Additionally, we present novel algorithms for symbolic model checking of finite-state concurrent systems, where the desired property of the systems is to ensure a formally defined notion of fairness.","lang":"eng"}],"project":[{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program","grant_number":"665385"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"page":"166","file_date_updated":"2021-11-09T09:00:50Z","_id":"10199","type":"dissertation","month":"10","alternative_title":["ISTA Thesis"],"degree_awarded":"PhD","OA_place":"publisher","supervisor":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"}],"date_updated":"2026-04-08T07:00:31Z"}]