[{"ec_funded":1,"keyword":["Quantitative model checking","Markov decision process","Linear programming","Value iteration","Policy iteration"],"article_type":"original","date_published":"2026-03-09T00:00:00Z","department":[{"_id":"KrCh"}],"month":"03","publication":"International Journal on Software Tools for Technology Transfer","doi":"10.1007/s10009-026-00848-y","status":"public","quality_controlled":"1","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"has_accepted_license":"1","date_updated":"2026-04-07T09:52:54Z","title":"The revised practitioner’s guide to MDP model checking algorithms","article_processing_charge":"Yes (in subscription journal)","related_material":{"record":[{"id":"21668","relation":"software","status":"public"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_type":"hybrid","_id":"21661","scopus_import":"1","ddc":["000"],"author":[{"full_name":"Hartmanns, Arnd","first_name":"Arnd","last_name":"Hartmanns"},{"full_name":"Junges, Sebastian","last_name":"Junges","first_name":"Sebastian"},{"full_name":"Quatmann, Tim","last_name":"Quatmann","first_name":"Tim"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","orcid":"0000-0002-0163-2152","full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian"}],"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"}],"OA_place":"publisher","language":[{"iso":"eng"}],"publisher":"Springer Nature","publication_identifier":{"issn":["1433-2779"],"eissn":["1433-2787"]},"year":"2026","day":"09","date_created":"2026-04-05T22:01:32Z","oa_version":"Published Version","type":"journal_article","fulldoi":"https://doi.org/10.1007/s10009-026-00848-y","oa":1,"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.","citation":{"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>.","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>","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."},"publication_status":"epub_ahead","project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/s10009-026-00848-y"}]},{"abstract":[{"lang":"eng","text":"This artifact allows to review and reproduce the experiments from the paper *A Revised Practitioner's Guide to MDP Model Checking Algorithms*.\r\nThe package contains all original logfiles and derived data used to generate the plots as in the paper. Furthermore, the artifact contains the model checking tools `Storm` and `mcsta` in the version exercised in the paper, the used Docker container, as well as benchmark instances and execution scripts to reproduce the experiments.\r\n\r\nSee also the artifact of the conference paper: https://zenodo.org/records/7509474"}],"OA_place":"repository","department":[{"_id":"KrCh"}],"publisher":"Zenodo","date_published":"2025-03-07T00:00:00Z","month":"03","doi":"10.5281/ZENODO.14500423","year":"2025","day":"07","status":"public","date_updated":"2026-04-07T09:52:55Z","title":"Benchmark data for the revised practitioner's guide to MDP model checking algorithms","date_created":"2026-04-07T09:47:22Z","article_processing_charge":"No","fulldoi":"https://doi.org/10.5281/ZENODO.14500423","oa":1,"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"research_data_reference","related_material":{"record":[{"status":"public","id":"21661","relation":"used_for_analysis_in"}]},"citation":{"ista":"Hartmanns A, Junges S, Quatmann T, Weininger M. 2025. Benchmark data for the revised practitioner’s guide to MDP model checking algorithms, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.14500423\">10.5281/ZENODO.14500423</a>.","apa":"Hartmanns, A., Junges, S., Quatmann, T., &#38; Weininger, M. (2025). Benchmark data for the revised practitioner’s guide to MDP model checking algorithms. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.14500423\">https://doi.org/10.5281/ZENODO.14500423</a>","ieee":"A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “Benchmark data for the revised practitioner’s guide to MDP model checking algorithms.” Zenodo, 2025.","short":"A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, (2025).","chicago":"Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. “Benchmark Data for the Revised Practitioner’s Guide to MDP Model Checking Algorithms.” Zenodo, 2025. <a href=\"https://doi.org/10.5281/ZENODO.14500423\">https://doi.org/10.5281/ZENODO.14500423</a>.","mla":"Hartmanns, Arnd, et al. <i>Benchmark Data for the Revised Practitioner’s Guide to MDP Model Checking Algorithms</i>. Zenodo, 2025, doi:<a href=\"https://doi.org/10.5281/ZENODO.14500423\">10.5281/ZENODO.14500423</a>.","ama":"Hartmanns A, Junges S, Quatmann T, Weininger M. Benchmark data for the revised practitioner’s guide to MDP model checking algorithms. 2025. doi:<a href=\"https://doi.org/10.5281/ZENODO.14500423\">10.5281/ZENODO.14500423</a>"},"_id":"21668","OA_type":"gold","main_file_link":[{"url":"https://doi.org/10.5281/ZENODO.14500423","open_access":"1"}],"ddc":["000"],"author":[{"first_name":"Arnd","last_name":"Hartmanns","full_name":"Hartmanns, Arnd"},{"first_name":"Sebastian","last_name":"Junges","full_name":"Junges, Sebastian"},{"first_name":"Tim","last_name":"Quatmann","full_name":"Quatmann, Tim"},{"first_name":"Maximilian","last_name":"Weininger","orcid":"0000-0002-0163-2152","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881"}]},{"page":"97-120","publisher":"Springer Nature","language":[{"iso":"eng"}],"OA_place":"repository","abstract":[{"text":"Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs.\r\n\r\nThe idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.","lang":"eng"}],"day":"23","year":"2025","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031827020"],"eissn":["1611-3349"]},"type":"conference","arxiv":1,"oa_version":"Preprint","oa":1,"intvolume":"     15530","fulldoi":"https://doi.org/10.1007/978-3-031-82703-7_5","date_created":"2025-03-09T23:01:29Z","project":[{"call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2410.18293","open_access":"1"}],"acknowledgement":"This research was funded in part by the DFG project 427755713 GOPro, the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement 101034413 (IST-BRIDGE).","publication_status":"published","citation":{"mla":"Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, vol. 15530, Springer Nature, 2025, pp. 97–120, doi:<a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">10.1007/978-3-031-82703-7_5</a>.","ama":"Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In: <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>. Vol 15530. Springer Nature; 2025:97-120. doi:<a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">10.1007/978-3-031-82703-7_5</a>","chicago":"Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” In <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, 15530:97–120. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">https://doi.org/10.1007/978-3-031-82703-7_5</a>.","short":"M. Azeem, D. Chakraborty, S. Kanav, J. Kretinsky, M. Mohagheghi, S. Mohr, M. Weininger, in:, 26th International Conference on Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2025, pp. 97–120.","ista":"Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. 26th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.","apa":"Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr, S., &#38; Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i> (Vol. 15530, pp. 97–120). Denver, CO, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">https://doi.org/10.1007/978-3-031-82703-7_5</a>","ieee":"M. Azeem <i>et al.</i>, “1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization,” in <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, Denver, CO, United States, 2025, vol. 15530, pp. 97–120."},"date_published":"2025-01-23T00:00:00Z","alternative_title":["LNCS"],"department":[{"_id":"KrCh"}],"ec_funded":1,"status":"public","doi":"10.1007/978-3-031-82703-7_5","quality_controlled":"1","month":"01","publication":"26th International Conference on Verification, Model Checking, and Abstract Interpretation","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","external_id":{"isi":["001446577100005"],"arxiv":["2410.18293"]},"article_processing_charge":"No","title":"1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization","date_updated":"2025-09-30T10:46:54Z","author":[{"last_name":"Azeem","first_name":"Muqsit","full_name":"Azeem, Muqsit"},{"full_name":"Chakraborty, Debraj","last_name":"Chakraborty","first_name":"Debraj"},{"first_name":"Sudeep","last_name":"Kanav","full_name":"Kanav, Sudeep"},{"orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"},{"last_name":"Mohagheghi","first_name":"Mohammadsadegh","full_name":"Mohagheghi, Mohammadsadegh"},{"full_name":"Mohr, Stefanie","last_name":"Mohr","first_name":"Stefanie"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian"}],"isi":1,"conference":{"location":"Denver, CO, United States","name":"VMCAI: Verification, Model Checking, and Abstract Interpretation","end_date":"2025-01-21","start_date":"2025-01-20"},"OA_type":"green","volume":15530,"_id":"19375","scopus_import":"1"},{"publisher":"Association for the Advancement of Artificial Intelligence","page":"26631-26641","language":[{"iso":"eng"}],"OA_place":"repository","abstract":[{"text":"Markov decision processes (MDP) are a well-established model for sequential decision-making in the presence of probabilities. In *robust* MDP (RMDP), every action is associated with an *uncertainty set* of probability distributions, modelling that transition probabilities are not known precisely. Based on the known theoretical connection to stochastic games, we provide a framework for solving RMDPs that is generic, reliable, and efficient. It is *generic* both with respect to the model, allowing for a wide range of uncertainty sets, including but not limited to intervals, L1- or L2-balls, and polytopes; and with respect to the objective, including long-run average reward, undiscounted total reward, and stochastic shortest path. It is *reliable*, as our approach not only converges in the limit, but provides precision guarantees at any time during the computation. It is *efficient* because -- in contrast to state-of-the-art approaches -- it avoids explicitly constructing the underlying stochastic game. Consequently, our prototype implementation outperforms existing tools by several orders of magnitude and can solve RMDPs with a million states in under a minute.","lang":"eng"}],"day":"11","year":"2025","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"oa":1,"intvolume":"        39","fulldoi":"https://doi.org/10.1609/aaai.v39i25.34865","arxiv":1,"type":"conference","oa_version":"Preprint","date_created":"2025-05-11T22:02:39Z","issue":"25","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2412.10185","open_access":"1"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"publication_status":"published","citation":{"ista":"Meggendorfer T, Weininger M, Wienhöft P. 2025. Solving robust Markov decision processes: Generic, reliable, efficient. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 26631–26641.","apa":"Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Solving robust Markov decision processes: Generic, reliable, efficient. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 26631–26641). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i25.34865\">https://doi.org/10.1609/aaai.v39i25.34865</a>","ieee":"T. Meggendorfer, M. Weininger, and P. Wienhöft, “Solving robust Markov decision processes: Generic, reliable, efficient,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 25, pp. 26631–26641.","chicago":"Meggendorfer, Tobias, Maximilian Weininger, and Patrick Wienhöft. “Solving Robust Markov Decision Processes: Generic, Reliable, Efficient.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:26631–41. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i25.34865\">https://doi.org/10.1609/aaai.v39i25.34865</a>.","short":"T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 26631–26641.","mla":"Meggendorfer, Tobias, et al. “Solving Robust Markov Decision Processes: Generic, Reliable, Efficient.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 25, Association for the Advancement of Artificial Intelligence, 2025, pp. 26631–41, doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34865\">10.1609/aaai.v39i25.34865</a>.","ama":"Meggendorfer T, Weininger M, Wienhöft P. Solving robust Markov decision processes: Generic, reliable, efficient. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:26631-26641. doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34865\">10.1609/aaai.v39i25.34865</a>"},"acknowledgement":"This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No. 101034413,\r\nthe ERC CoG 863818 (ForM-SMArt), and the DFG through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy) and the TRR 248 (see https://perspicuous-computing.science, project ID 389792660).","department":[{"_id":"KrCh"}],"date_published":"2025-04-11T00:00:00Z","ec_funded":1,"quality_controlled":"1","status":"public","doi":"10.1609/aaai.v39i25.34865","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","month":"04","external_id":{"arxiv":["2412.10185"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"link":[{"relation":"software","url":"https://doi.org/10.5281/zenodo.14385449"}]},"article_processing_charge":"No","title":"Solving robust Markov decision processes: Generic, reliable, efficient","date_updated":"2026-02-16T12:25:05Z","conference":{"location":"Philadelphia, PA, United States","name":"AAAI: Conference on Artificial Intelligence","start_date":"2025-02-25","end_date":"2025-03-04"},"author":[{"full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer"},{"orcid":"0000-0002-0163-2152","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","last_name":"Weininger"},{"first_name":"Patrick","last_name":"Wienhöft","full_name":"Wienhöft, Patrick"}],"volume":39,"scopus_import":"1","_id":"19666","OA_type":"green"},{"doi":"10.1007/978-3-031-90643-5_9","status":"public","quality_controlled":"1","month":"05","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","date_published":"2025-05-01T00:00:00Z","department":[{"_id":"KrCh"}],"alternative_title":["LNCS"],"ec_funded":1,"author":[{"full_name":"Budde, Carlos E.","last_name":"Budde","first_name":"Carlos E."},{"full_name":"Hartmanns, Arnd","first_name":"Arnd","last_name":"Hartmanns"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","first_name":"Tobias"},{"first_name":"Maximilian","last_name":"Weininger","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881"},{"full_name":"Wienhöft, Patrick","first_name":"Patrick","last_name":"Wienhöft"}],"ddc":["000"],"conference":{"end_date":"2025-05-08","start_date":"2025-05-03","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Hamilton, ON, Canada"},"OA_type":"hybrid","_id":"19742","scopus_import":"1","volume":15696,"related_material":{"record":[{"status":"public","id":"19769","relation":"research_data"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2025-06-02T09:35:42Z","external_id":{"arxiv":["2411.00559"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"has_accepted_license":"1","date_updated":"2025-06-02T09:45:41Z","article_processing_charge":"No","title":"Sound statistical model checking for probabilities and expected rewards","year":"2025","day":"01","file":[{"file_size":711271,"file_name":"2025_TACAS_Budde.pdf","content_type":"application/pdf","file_id":"19770","creator":"dernst","checksum":"d45856b503b1dd4f8f14c3566327225b","success":1,"date_created":"2025-06-02T09:35:42Z","date_updated":"2025-06-02T09:35:42Z","relation":"main_file","access_level":"open_access"}],"publication_identifier":{"isbn":["9783031906428"],"eissn":["1611-3349"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"publisher":"Springer Nature","page":"167-190","abstract":[{"lang":"eng","text":"Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results."}],"OA_place":"publisher","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020"}],"acknowledgement":"This work was supported by the DFG through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy) and the TRR 248 (see perspicuous-computing.science, project ID 389792660), by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by the EU under NextGenerationEU projects D53D23008400006 (Smartitude) under MUR PRIN 2022 and PE00000014 (SERICS) under MUR PNRR, by the Interreg North Sea project STORM_SAFE, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy).","citation":{"mla":"Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 167–90, doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">10.1007/978-3-031-90643-5_9</a>.","ama":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical model checking for probabilities and expected rewards. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:167-190. doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">10.1007/978-3-031-90643-5_9</a>","chicago":"Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:167–90. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>.","short":"C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 167–190.","apa":"Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Sound statistical model checking for probabilities and expected rewards. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>","ista":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound statistical model checking for probabilities and expected rewards. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15696, 167–190.","ieee":"C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft, “Sound statistical model checking for probabilities and expected rewards,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190."},"publication_status":"published","oa_version":"Published Version","arxiv":1,"type":"conference","intvolume":"     15696","fulldoi":"https://doi.org/10.1007/978-3-031-90643-5_9","oa":1,"date_created":"2025-05-25T22:17:08Z"},{"ddc":["000"],"author":[{"full_name":"Budde, Carlos","first_name":"Carlos","last_name":"Budde"},{"last_name":"Hartmanns","first_name":"Arnd","full_name":"Hartmanns, Arnd"},{"last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias"},{"last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian"},{"full_name":"Wienhöft, Patrick","first_name":"Patrick","last_name":"Wienhöft"}],"main_file_link":[{"url":"https://doi.org/10.5281/ZENODO.14602066","open_access":"1"}],"OA_type":"green","_id":"19769","citation":{"ieee":"C. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft, “Sound statistical model checking for probabilities and expected rewards (experimental reproduction package).” Zenodo, 2025.","apa":"Budde, C., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Sound statistical model checking for probabilities and expected rewards (experimental reproduction package). Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.14602066\">https://doi.org/10.5281/ZENODO.14602066</a>","ista":"Budde C, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound statistical model checking for probabilities and expected rewards (experimental reproduction package), Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.14602066\">10.5281/ZENODO.14602066</a>.","short":"C. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, (2025).","chicago":"Budde, Carlos, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and Expected Rewards (Experimental Reproduction Package).” Zenodo, 2025. <a href=\"https://doi.org/10.5281/ZENODO.14602066\">https://doi.org/10.5281/ZENODO.14602066</a>.","mla":"Budde, Carlos, et al. <i>Sound Statistical Model Checking for Probabilities and Expected Rewards (Experimental Reproduction Package)</i>. Zenodo, 2025, doi:<a href=\"https://doi.org/10.5281/ZENODO.14602066\">10.5281/ZENODO.14602066</a>.","ama":"Budde C, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical model checking for probabilities and expected rewards (experimental reproduction package). 2025. doi:<a href=\"https://doi.org/10.5281/ZENODO.14602066\">10.5281/ZENODO.14602066</a>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"research_data_reference","related_material":{"record":[{"relation":"used_in_publication","id":"19742","status":"public"}]},"oa_version":"Published Version","oa":1,"fulldoi":"https://doi.org/10.5281/ZENODO.14602066","date_created":"2025-06-02T09:37:14Z","title":"Sound statistical model checking for probabilities and expected rewards (experimental reproduction package)","article_processing_charge":"No","date_updated":"2025-06-02T09:45:41Z","status":"public","day":"07","year":"2025","doi":"10.5281/ZENODO.14602066","month":"01","date_published":"2025-01-07T00:00:00Z","publisher":"Zenodo","department":[{"_id":"KrCh"}],"OA_place":"repository","abstract":[{"lang":"eng","text":"Artifact to reproduce the experimental results presented in the article \"Sound Statistical Model Checking for Probabilities and Expected Rewards\" by Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft (TACAS 2025).\r\n\r\nThe contents include all data and software (formal models, software tools, Python & bash scripts) used in the experimental evaluation presented in sections 3, 4, and 6 of the article. Detailed instructions on how to reproduce the results are bundled in the artifact."}]},{"oa_version":"None","type":"conference","intvolume":"     16143","fulldoi":"https://doi.org/10.1007/978-3-032-05792-1_11","date_created":"2025-11-09T23:01:34Z","project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"acknowledgement":"This work was supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 10103441, the ERC Starting Grant DEUCE (101077178) and the DFG through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy) and the DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).","citation":{"ieee":"T. Meggendorfer, M. Weininger, and P. Wienhöft, “What are the odds? Improving statistical model checking of Markov decision processes,” in <i>Second International Joint Conference on QEST+FORMATS</i>, Aarhus, Denmark, 2025, vol. 16143, pp. 195–218.","apa":"Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). What are the odds? Improving statistical model checking of Markov decision processes. In <i>Second International Joint Conference on QEST+FORMATS</i> (Vol. 16143, pp. 195–218). Aarhus, Denmark: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05792-1_11\">https://doi.org/10.1007/978-3-032-05792-1_11</a>","ista":"Meggendorfer T, Weininger M, Wienhöft P. 2025. What are the odds? Improving statistical model checking of Markov decision processes. Second International Joint Conference on QEST+FORMATS. QEST-FORMATS: International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, LNCS, vol. 16143, 195–218.","ama":"Meggendorfer T, Weininger M, Wienhöft P. What are the odds? Improving statistical model checking of Markov decision processes. In: <i>Second International Joint Conference on QEST+FORMATS</i>. Vol 16143. Springer Nature; 2025:195-218. doi:<a href=\"https://doi.org/10.1007/978-3-032-05792-1_11\">10.1007/978-3-032-05792-1_11</a>","mla":"Meggendorfer, Tobias, et al. “What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes.” <i>Second International Joint Conference on QEST+FORMATS</i>, vol. 16143, Springer Nature, 2025, pp. 195–218, doi:<a href=\"https://doi.org/10.1007/978-3-032-05792-1_11\">10.1007/978-3-032-05792-1_11</a>.","short":"T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Second International Joint Conference on QEST+FORMATS, Springer Nature, 2025, pp. 195–218.","chicago":"Meggendorfer, Tobias, Maximilian Weininger, and Patrick Wienhöft. “What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes.” In <i>Second International Joint Conference on QEST+FORMATS</i>, 16143:195–218. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05792-1_11\">https://doi.org/10.1007/978-3-032-05792-1_11</a>."},"publication_status":"published","language":[{"iso":"eng"}],"page":"195-218","publisher":"Springer Nature","abstract":[{"lang":"eng","text":"Markov decision processes (MDPs) are a fundamental model of decision making which exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification assumes exact knowledge of the probabilities that govern the behaviour of an MDP. However, this assumption often is unrealistic, e.g. when modelling cyber-physical systems or biological processes. There, we can employ statistical model checking (SMC) to obtain an estimate of the MDP’s value (e.g. the maximal probability of reaching a goal state) that is close to the true value with high confidence (probably approximately correct). Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: “What are the odds?” However, so far the statistical methods employed by state-of-the-art SMC verification algorithms are quite naive or even compromise the correctness guarantees.\r\n\r\nOur first contribution is to survey, categorize, and analyse statistical methods, identifying those few that are most efficient and that provide suitable guarantees for the verification setting. Secondly, we propose improvements that exploit structural knowledge of the MDP. Both contributions generalize to many types of problem statements as they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that an SMC algorithm has to collect by up to two orders of magnitude."}],"year":"2025","day":"02","publication_identifier":{"issn":["0302-9743"],"isbn":["9783032057914"],"eissn":["1611-3349"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-11-10T08:06:27Z","article_processing_charge":"No","title":"What are the odds? Improving statistical model checking of Markov decision processes","author":[{"last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"},{"last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","orcid":"0000-0002-0163-2152"},{"last_name":"Wienhöft","first_name":"Patrick","full_name":"Wienhöft, Patrick"}],"conference":{"location":"Aarhus, Denmark","start_date":"2025-08-26","end_date":"2025-08-28","name":"QEST-FORMATS: International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"},"_id":"20610","scopus_import":"1","volume":16143,"date_published":"2025-10-02T00:00:00Z","department":[{"_id":"KrCh"}],"alternative_title":["LNCS"],"ec_funded":1,"doi":"10.1007/978-3-032-05792-1_11","status":"public","quality_controlled":"1","month":"10","publication":"Second International Joint Conference on QEST+FORMATS"},{"oa":1,"fulldoi":"https://doi.org/10.1109/lics65433.2025.00049","type":"conference","arxiv":1,"oa_version":"Preprint","date_created":"2025-11-24T14:23:49Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.21087"}],"project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"publication_status":"published","citation":{"ieee":"M. Grobelna, J. Kretinsky, and M. Weininger, “Stopping criteria for value iteration on concurrent stochastic reachability and safety games,” in <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Singapore, Singapore, 2025, pp. 568–580.","ista":"Grobelna M, Kretinsky J, Weininger M. 2025. Stopping criteria for value iteration on concurrent stochastic reachability and safety games. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 568–580.","apa":"Grobelna, M., Kretinsky, J., &#38; Weininger, M. (2025). Stopping criteria for value iteration on concurrent stochastic reachability and safety games. In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 568–580). Singapore, Singapore: IEEE. <a href=\"https://doi.org/10.1109/lics65433.2025.00049\">https://doi.org/10.1109/lics65433.2025.00049</a>","chicago":"Grobelna, Marta, Jan Kretinsky, and Maximilian Weininger. “Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games.” In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 568–80. IEEE, 2025. <a href=\"https://doi.org/10.1109/lics65433.2025.00049\">https://doi.org/10.1109/lics65433.2025.00049</a>.","short":"M. Grobelna, J. Kretinsky, M. Weininger, in:, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp. 568–580.","mla":"Grobelna, Marta, et al. “Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games.” <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2025, pp. 568–80, doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00049\">10.1109/lics65433.2025.00049</a>.","ama":"Grobelna M, Kretinsky J, Weininger M. Stopping criteria for value iteration on concurrent stochastic reachability and safety games. In: <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2025:568-580. doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00049\">10.1109/lics65433.2025.00049</a>"},"acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 GOPro, the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant Agency of Masaryk University, the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 101034413, and the ERC Starting Grant DEUCE (101077178).","publisher":"IEEE","page":"568-580","language":[{"iso":"eng"}],"OA_place":"repository","abstract":[{"lang":"eng","text":"We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be solved by linear or quadratic programming; however, in practice, value iteration (VI) outperforms the other approaches and is the most implemented method. Similarly, for CSGs, this practical performance makes VI an attractive alternative to the standard theoretical solution via the existential theory of reals.VI starts with an under-approximation of the sought values for each state and iteratively updates them, traditionally terminating once two consecutive approximations are ϵ-close. However, this stopping criterion lacks guarantees on the precision of the approximation, which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs: it complements standard VI with a converging sequence of over-approximations and terminates once the over- and under-approximations are ϵ-close."}],"day":"09","corr_author":"1","year":"2025","publication_identifier":{"eisbn":["9798331579005"]},"external_id":{"arxiv":["2505.21087"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Stopping criteria for value iteration on concurrent stochastic reachability and safety games","article_processing_charge":"No","date_updated":"2025-11-26T07:34:19Z","conference":{"location":"Singapore, Singapore","end_date":"2025-06-26","start_date":"2025-06-23","name":"LICS: Logic in Computer Science"},"author":[{"full_name":"Grobelna, Marta","first_name":"Marta","last_name":"Grobelna"},{"orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"},{"last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","orcid":"0000-0002-0163-2152"}],"_id":"20688","scopus_import":"1","OA_type":"green","department":[{"_id":"KrCh"}],"date_published":"2025-10-09T00:00:00Z","ec_funded":1,"quality_controlled":"1","status":"public","doi":"10.1109/lics65433.2025.00049","publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","month":"10"},{"oa":1,"intvolume":"     15697","fulldoi":"https://doi.org/10.1007/978-3-031-90653-4_7","arxiv":1,"type":"conference","oa_version":"Published Version","date_created":"2025-05-25T22:17:09Z","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)"}],"publication_status":"published","citation":{"ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Fixed point certificates for reachability and expected rewards in MDPs,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 130–151.","ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Fixed point certificates for reachability and expected rewards in MDPs. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 130–151.","apa":"Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., &#38; Zilken, D. (2025). Fixed point certificates for reachability and expected rewards in MDPs. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 130–151). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>","mla":"Chatterjee, Krishnendu, et al. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 130–51, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>.","ama":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. Fixed point certificates for reachability and expected rewards in MDPs. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:130-151. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>","short":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 130–151.","chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:130–51. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>."},"acknowledgement":"This project has received funding from the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12, a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, the DFG RTG 378803395 (ConVeY), the EU’s Horizon 2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement Nos. 101034413 (IST-BRIDGE) and 101008233 (MISSION), and the DFG RTG 2236 (UnRAVeL). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632.","page":"130-151","publisher":"Springer Nature","language":[{"iso":"eng"}],"OA_place":"publisher","abstract":[{"lang":"eng","text":"The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates—lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set."}],"file":[{"checksum":"64b7f46ef05649b87b827248045c7645","file_id":"19772","creator":"dernst","success":1,"date_created":"2025-06-02T10:49:52Z","date_updated":"2025-06-02T10:49:52Z","relation":"main_file","access_level":"open_access","file_size":732136,"file_name":"2025_TACAS_ChatterjeeKrish.pdf","content_type":"application/pdf"}],"day":"01","corr_author":"1","year":"2025","publication_identifier":{"isbn":["9783031906527"],"eissn":["1611-3349"],"issn":["0302-9743"]},"external_id":{"arxiv":["2501.11467"]},"file_date_updated":"2025-06-02T10:49:52Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","relation":"research_data","id":"19771"}]},"article_processing_charge":"No","title":"Fixed point certificates for reachability and expected rewards in MDPs","date_updated":"2026-09-16T06:57:17Z","has_accepted_license":"1","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"conference":{"location":"Hamilton, ON, Canada","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2025-05-03","end_date":"2025-05-08"},"ddc":["000"],"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Quatmann, Tim","first_name":"Tim","last_name":"Quatmann"},{"last_name":"Schäffeler","first_name":"Maximilian","full_name":"Schäffeler, Maximilian"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","orcid":"0000-0002-0163-2152","last_name":"Weininger","first_name":"Maximilian"},{"full_name":"Winkler, Tobias","last_name":"Winkler","first_name":"Tobias"},{"first_name":"Daniel","last_name":"Zilken","full_name":"Zilken, Daniel","id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3"}],"volume":15697,"scopus_import":"1","_id":"19743","OA_type":"hybrid","alternative_title":["LNCS"],"department":[{"_id":"KrCh"}],"date_published":"2025-05-01T00:00:00Z","ec_funded":1,"quality_controlled":"1","status":"public","doi":"10.1007/978-3-031-90653-4_7","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","month":"05"},{"date_updated":"2026-09-16T06:57:17Z","date_created":"2025-06-02T10:13:24Z","article_processing_charge":"No","title":"Artifact: Fixed point certificates for reachability and expected rewards in MDPs","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"fulldoi":"https://doi.org/10.5281/ZENODO.14626585","oa":1,"oa_version":"Published Version","related_material":{"record":[{"id":"19743","relation":"used_in_publication","status":"public"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"research_data_reference","_id":"19771","citation":{"short":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken, (2025).","chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” Zenodo, 2025. <a href=\"https://doi.org/10.5281/ZENODO.14626585\">https://doi.org/10.5281/ZENODO.14626585</a>.","ama":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. Artifact: Fixed point certificates for reachability and expected rewards in MDPs. 2025. doi:<a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>","mla":"Chatterjee, Krishnendu, et al. <i>Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs</i>. Zenodo, 2025, doi:<a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>.","ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Artifact: Fixed point certificates for reachability and expected rewards in MDPs.” Zenodo, 2025.","ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Artifact: Fixed point certificates for reachability and expected rewards in MDPs, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>.","apa":"Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., &#38; Zilken, D. (2025). Artifact: Fixed point certificates for reachability and expected rewards in MDPs. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.14626585\">https://doi.org/10.5281/ZENODO.14626585</a>"},"OA_type":"green","main_file_link":[{"url":"https://doi.org/10.5281/ZENODO.14626585","open_access":"1"}],"ddc":["000"],"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Tim","last_name":"Quatmann","full_name":"Quatmann, Tim"},{"full_name":"Schäffeler, Maximilian","first_name":"Maximilian","last_name":"Schäffeler"},{"last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","orcid":"0000-0002-0163-2152"},{"full_name":"Winkler, Tobias","first_name":"Tobias","last_name":"Winkler"},{"last_name":"Zilken","first_name":"Daniel","id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3","full_name":"Zilken, Daniel"}],"abstract":[{"lang":"eng","text":"This artifact allows to review and reproduce the Isabelle proofs and practical experiments from the paper *Fixed Point Certificates for Reachability and Expected Rewards in MDPs*.\r\nThe contents are two-fold:\r\nFirst, the artifact contains a formally verified certificate checker for the certificates presented in the paper.\r\nThe formal Isabelle/HOL proofs of the background theory can be inspected, checked by Isabelle and the code extraction can be retraced.\r\n\r\nSecond, the artifact contains a modified version of the model checking tool `Storm` with support for certificate generation. Together with the provided scripts and benchmark files, this allows to reproduce the experiments from the paper.\r\nAn appropriate subset of the experiments is given to allow a review in a timely manner. In addition, original logfiles from our experiments are provided, allowing a detailed inspection.\r\n\r\nThe package includes convenient installation scripts for [the TACAS 2023 VM](https://doi.org/10.5281/zenodo.7113223) (based on Ubuntu 22.04).\r\nA native installation on Linux or macOS systems (including the newer ARM-based machines) is also possible."}],"OA_place":"repository","department":[{"_id":"KrCh"}],"publisher":"Zenodo","date_published":"2025-01-09T00:00:00Z","month":"01","doi":"10.5281/ZENODO.14626585","year":"2025","day":"09","status":"public"},{"date_updated":"2026-09-16T07:05:13Z","title":"Risk-aware Markov decision processes using cumulative prospect theory","article_processing_charge":"No","external_id":{"arxiv":["2505.09514"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"20690","scopus_import":"1","OA_type":"green","conference":{"location":"Singapore, Singapore","end_date":"2025-06-26","start_date":"2025-06-23","name":"LICS: Logic in Computer Science"},"author":[{"full_name":"Brihaye, Thomas","first_name":"Thomas","last_name":"Brihaye"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Stefanie","last_name":"Mohr","full_name":"Mohr, Stefanie"},{"orcid":"0000-0002-0163-2152","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","last_name":"Weininger"}],"ec_funded":1,"department":[{"_id":"KrCh"}],"date_published":"2025-10-09T00:00:00Z","publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","month":"10","quality_controlled":"1","doi":"10.1109/lics65433.2025.00041","status":"public","date_created":"2025-11-24T14:43:47Z","fulldoi":"https://doi.org/10.1109/lics65433.2025.00041","oa":1,"oa_version":"Preprint","type":"conference","arxiv":1,"citation":{"ieee":"T. Brihaye, K. Chatterjee, S. Mohr, and M. Weininger, “Risk-aware Markov decision processes using cumulative prospect theory,” in <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Singapore, Singapore, 2025, pp. 458–471.","ista":"Brihaye T, Chatterjee K, Mohr S, Weininger M. 2025. Risk-aware Markov decision processes using cumulative prospect theory. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 458–471.","apa":"Brihaye, T., Chatterjee, K., Mohr, S., &#38; Weininger, M. (2025). Risk-aware Markov decision processes using cumulative prospect theory. In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 458–471). Singapore, Singapore: IEEE. <a href=\"https://doi.org/10.1109/lics65433.2025.00041\">https://doi.org/10.1109/lics65433.2025.00041</a>","mla":"Brihaye, Thomas, et al. “Risk-Aware Markov Decision Processes Using Cumulative Prospect Theory.” <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2025, pp. 458–71, doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00041\">10.1109/lics65433.2025.00041</a>.","ama":"Brihaye T, Chatterjee K, Mohr S, Weininger M. Risk-aware Markov decision processes using cumulative prospect theory. In: <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2025:458-471. doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00041\">10.1109/lics65433.2025.00041</a>","short":"T. Brihaye, K. Chatterjee, S. Mohr, M. Weininger, in:, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp. 458–471.","chicago":"Brihaye, Thomas, Krishnendu Chatterjee, Stefanie Mohr, and Maximilian Weininger. “Risk-Aware Markov Decision Processes Using Cumulative Prospect Theory.” In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 458–71. IEEE, 2025. <a href=\"https://doi.org/10.1109/lics65433.2025.00041\">https://doi.org/10.1109/lics65433.2025.00041</a>."},"publication_status":"published","acknowledgement":"This project has received funding from the Fonds de la Recherche Scientifique - FNRS under grant No. T.0027.21, the Belgian National Lottery; the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12; the DFG project 427755713, GOPro, and the DFG research training group GRK 2428 Continuous Verification of Cyber-Physical Systems\r\n(ConVeY); the EU’s Horizon 2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement No. 101034413 (IST-BRIDGE) and the ERC Starting Grant DEUCE (101077178).","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.09514"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"},{"grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"}],"abstract":[{"text":"Cumulative prospect theory (CPT) is the first theory for decision-making under uncertainty that combines full theoretical soundness and empirically realistic features [1], [Page 2]. While CPT was originally considered in one-shot settings for risk-aware decision-making, we consider CPT in sequential decision-making. The most fundamental and well-studied models for sequential decision-making are Markov chains (MCs), and their generalization Markov decision processes (MDPs). The complexity theoretic study of MCs and MDPs with CPT is a fundamental problem that has not been addressed in the literature.Our contributions are as follows: First, we present an alternative viewpoint for the CPT-value of MCs and MDPs. This allows us to establish a connection with multi-objective reachability analysis and conclude the strategy complexity result that memoryless randomized strategies are necessary and sufficient for optimality. Second, based on this connection, we provide an algorithm for computing the CPT-value in MDPs with infinite-horizon objectives. We show that the problem is in EXPTIME and fixed-parameter tractable. Moreover, we provide a polynomial-time algorithm for the special case of MCs.","lang":"eng"}],"OA_place":"repository","language":[{"iso":"eng"}],"page":"458-471","publisher":"IEEE","publication_identifier":{"eisbn":["9798331579005"]},"corr_author":"1","year":"2025","day":"09"},{"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031676949"],"issn":["0302-9743"]},"year":"2024","day":"01","abstract":[{"lang":"eng","text":"The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today’s active areas and tomorrow’s challenges in tool-focused research for quantitative verification."}],"OA_place":"repository","language":[{"iso":"eng"}],"page":"90-146","publisher":"Springer Nature","citation":{"ista":"Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550, 90–146.","apa":"Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E. M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In <i>TOOLympics Challenge 2023</i> (Vol. 14550, pp. 90–146). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">https://doi.org/10.1007/978-3-031-67695-6_4</a>","ieee":"R. Andriushchenko <i>et al.</i>, “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report,” in <i>TOOLympics Challenge 2023</i>, 2024, vol. 14550, pp. 90–146.","short":"R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A. Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer, J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters, L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer Nature, 2024, pp. 90–146.","chicago":"Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” In <i>TOOLympics Challenge 2023</i>, 14550:90–146. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">https://doi.org/10.1007/978-3-031-67695-6_4</a>.","mla":"Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” <i>TOOLympics Challenge 2023</i>, vol. 14550, Springer Nature, 2024, pp. 90–146, doi:<a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">10.1007/978-3-031-67695-6_4</a>.","ama":"Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In: <i>TOOLympics Challenge 2023</i>. Vol 14550. Springer Nature; 2024:90-146. doi:<a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">10.1007/978-3-031-67695-6_4</a>"},"publication_status":"published","acknowledgement":"The authors are ordered alphabetically. This work was supported by DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075 (CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA), by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006 (SMARTITUDE), and by NWO VENI grant 639.021.754.","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.2405.13583"}],"date_created":"2024-12-01T23:01:53Z","intvolume":"     14550","fulldoi":"https://doi.org/10.1007/978-3-031-67695-6_4","oa":1,"oa_version":"Preprint","arxiv":1,"type":"conference","publication":"TOOLympics Challenge 2023","month":"11","quality_controlled":"1","doi":"10.1007/978-3-031-67695-6_4","status":"public","department":[{"_id":"KrCh"}],"alternative_title":["LNCS"],"date_published":"2024-11-01T00:00:00Z","_id":"18600","scopus_import":"1","volume":14550,"OA_type":"green","isi":1,"author":[{"first_name":"Roman","last_name":"Andriushchenko","full_name":"Andriushchenko, Roman"},{"last_name":"Bork","first_name":"Alexander","full_name":"Bork, Alexander"},{"full_name":"Budde, Carlos E.","last_name":"Budde","first_name":"Carlos E."},{"last_name":"Češka","first_name":"Milan","full_name":"Češka, Milan"},{"full_name":"Grover, Kush","last_name":"Grover","first_name":"Kush"},{"full_name":"Hahn, Ernst Moritz","first_name":"Ernst Moritz","last_name":"Hahn"},{"first_name":"Arnd","last_name":"Hartmanns","full_name":"Hartmanns, Arnd"},{"first_name":"Bryant","last_name":"Israelsen","full_name":"Israelsen, Bryant"},{"full_name":"Jansen, Nils","last_name":"Jansen","first_name":"Nils"},{"full_name":"Jeppson, Joshua","first_name":"Joshua","last_name":"Jeppson"},{"last_name":"Junges","first_name":"Sebastian","full_name":"Junges, Sebastian"},{"full_name":"Köhl, Maximilian A.","first_name":"Maximilian A.","last_name":"Köhl"},{"last_name":"Könighofer","first_name":"Bettina","full_name":"Könighofer, Bettina"},{"last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan"},{"last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"},{"last_name":"Parker","first_name":"David","full_name":"Parker, David"},{"first_name":"Stefan","last_name":"Pranger","full_name":"Pranger, Stefan"},{"full_name":"Quatmann, Tim","last_name":"Quatmann","first_name":"Tim"},{"full_name":"Ruijters, Enno","last_name":"Ruijters","first_name":"Enno"},{"last_name":"Taylor","first_name":"Landon","full_name":"Taylor, Landon"},{"first_name":"Matthias","last_name":"Volk","full_name":"Volk, Matthias"},{"full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","last_name":"Weininger"},{"last_name":"Zhang","first_name":"Zhen","full_name":"Zhang, Zhen"}],"date_updated":"2025-09-08T14:45:11Z","title":"Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report","article_processing_charge":"No","external_id":{"isi":["001434957500004"],"arxiv":["2405.13583"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"file_date_updated":"2024-08-12T08:39:12Z","external_id":{"isi":["001307897000016"],"arxiv":["2405.03885"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_updated":"2025-09-08T08:53:55Z","article_processing_charge":"Yes (in subscription journal)","title":"Playing games with your PET: Extending the Partial Exploration Tool to stochastic games","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"has_accepted_license":"1","conference":{"location":"Montreal, Canada","name":"CAV: Computer Aided Verification","end_date":"2024-07-27","start_date":"2024-07-24"},"isi":1,"author":[{"first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian"}],"ddc":["000"],"_id":"17402","scopus_import":"1","volume":14683,"department":[{"_id":"KrCh"}],"alternative_title":["LNCS"],"date_published":"2024-07-01T00:00:00Z","ec_funded":1,"quality_controlled":"1","doi":"10.1007/978-3-031-65633-0_16","status":"public","publication":"36th International Conference on Computer Aided Verification","month":"07","intvolume":"     14683","fulldoi":"https://doi.org/10.1007/978-3-031-65633-0_16","oa":1,"oa_version":"Published Version","type":"conference","arxiv":1,"date_created":"2024-08-09T11:24:54Z","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","call_identifier":"H2020"}],"citation":{"apa":"Meggendorfer, T., &#38; Weininger, M. (2024). Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. In <i>36th International Conference on Computer Aided Verification</i> (Vol. 14683, pp. 359–372). Montreal, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-65633-0_16\">https://doi.org/10.1007/978-3-031-65633-0_16</a>","ista":"Meggendorfer T, Weininger M. 2024. Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. 36th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 14683, 359–372.","ieee":"T. Meggendorfer and M. Weininger, “Playing games with your PET: Extending the Partial Exploration Tool to stochastic games,” in <i>36th International Conference on Computer Aided Verification</i>, Montreal, Canada, 2024, vol. 14683, pp. 359–372.","short":"T. Meggendorfer, M. Weininger, in:, 36th International Conference on Computer Aided Verification, Springer Nature, 2024, pp. 359–372.","chicago":"Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games.” In <i>36th International Conference on Computer Aided Verification</i>, 14683:359–72. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-65633-0_16\">https://doi.org/10.1007/978-3-031-65633-0_16</a>.","ama":"Meggendorfer T, Weininger M. Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. In: <i>36th International Conference on Computer Aided Verification</i>. Vol 14683. Springer Nature; 2024:359-372. doi:<a href=\"https://doi.org/10.1007/978-3-031-65633-0_16\">10.1007/978-3-031-65633-0_16</a>","mla":"Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games.” <i>36th International Conference on Computer Aided Verification</i>, vol. 14683, Springer Nature, 2024, pp. 359–72, doi:<a href=\"https://doi.org/10.1007/978-3-031-65633-0_16\">10.1007/978-3-031-65633-0_16</a>."},"publication_status":"published","acknowledgement":"M. Weininger has received funding from the EU’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101034413.","language":[{"iso":"eng"}],"publisher":"Springer Nature","page":"359-372","abstract":[{"lang":"eng","text":"We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic games, based on a recent unified framework for sound value iteration algorithms. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability/safety and mean payoff. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools."}],"file":[{"success":1,"checksum":"c888231d0a47b55786b7b4c0f02216bb","file_id":"17419","creator":"dernst","access_level":"open_access","date_updated":"2024-08-12T08:39:12Z","relation":"main_file","date_created":"2024-08-12T08:39:12Z","content_type":"application/pdf","file_name":"2024_CAV_Meggendorfer.pdf","file_size":368487}],"year":"2024","corr_author":"1","day":"01","publication_identifier":{"isbn":["9783031656323"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031656330"]}},{"publication_status":"published","citation":{"ieee":"J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value iteration on stochastic games with quantitative objectives,” in <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Boston, MA, United States, 2023, vol. 2023.","ista":"Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2023.","apa":"Kretinsky, J., Meggendorfer, T., &#38; Weininger, M. (2023). Stopping criteria for value iteration on stochastic games with quantitative objectives. In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (Vol. 2023). Boston, MA, United States: IEEE. <a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">https://doi.org/10.1109/LICS56636.2023.10175771</a>","short":"J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2023.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Vol. 2023. IEEE, 2023. <a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">https://doi.org/10.1109/LICS56636.2023.10175771</a>.","mla":"Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, vol. 2023, IEEE, 2023, doi:<a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">10.1109/LICS56636.2023.10175771</a>.","ama":"Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration on stochastic games with quantitative objectives. In: <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Vol 2023. IEEE; 2023. doi:<a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">10.1109/LICS56636.2023.10175771</a>"},"acknowledgement":"This research was funded in part by DFG projects 383882557 “SUV” and 427755713 “GOPro”.","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2304.09930","open_access":"1"}],"date_created":"2023-08-06T22:01:10Z","oa":1,"intvolume":"      2023","fulldoi":"https://doi.org/10.1109/LICS56636.2023.10175771","type":"conference","arxiv":1,"oa_version":"Preprint","publication_identifier":{"issn":["1043-6871"],"isbn":["9798350335873"]},"day":"01","year":"2023","corr_author":"1","abstract":[{"lang":"eng","text":"A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution."}],"publisher":"IEEE","language":[{"iso":"eng"}],"volume":2023,"scopus_import":"1","_id":"13967","isi":1,"conference":{"start_date":"2023-06-26","end_date":"2023-06-29","name":"LICS: Logic in Computer Science","location":"Boston, MA, United States"},"author":[{"first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","orcid":"0000-0002-0163-2152","last_name":"Weininger","first_name":"Maximilian"}],"article_processing_charge":"No","title":"Stopping criteria for value iteration on stochastic games with quantitative objectives","date_updated":"2026-08-12T06:39:58Z","external_id":{"isi":["001036707700042"],"arxiv":["2304.09930"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"38th Annual ACM/IEEE Symposium on Logic in Computer Science","month":"07","quality_controlled":"1","status":"public","doi":"10.1109/LICS56636.2023.10175771","department":[{"_id":"KrCh"}],"date_published":"2023-07-01T00:00:00Z"}]