[{"publication_status":"published","file":[{"date_updated":"2026-03-09T12:33:58Z","success":1,"file_name":"2026_OPODIS_Bentert.pdf","file_id":"21419","access_level":"open_access","date_created":"2026-03-09T12:33:58Z","relation":"main_file","file_size":1041334,"creator":"dernst","content_type":"application/pdf","checksum":"a7af114da7c38d2338b4edb922eb27f1"}],"oa":1,"date_created":"2026-03-08T23:01:46Z","ddc":["000"],"day":"07","_id":"21411","OA_type":"gold","conference":{"start_date":"2025-12-03","end_date":"2025-12-05","name":"OPODIS: Conference on Principles of Distributed Systems","location":"Iaşi, Romania"},"title":"Fast re-routing in networks: On the complexity of perfect resilience","publication_identifier":{"isbn":["9783959774093"],"eissn":["1868-8969"]},"year":"2026","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2026-03-09T12:36:11Z","publication":"29th International Conference on Principles of Distributed Systems","month":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Matthias","last_name":"Bentert","full_name":"Bentert, Matthias"},{"full_name":"Ceylan, Esra","last_name":"Ceylan","first_name":"Esra"},{"first_name":"Valentin","orcid":"0009-0001-5009-4987","full_name":"Hübner, Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","last_name":"Hübner"},{"last_name":"Schmid","full_name":"Schmid, Stefan","first_name":"Stefan"},{"first_name":"Jiří","last_name":"Srba","full_name":"Srba, Jiří"}],"doi":"10.4230/LIPIcs.OPODIS.2025.31","citation":{"apa":"Bentert, M., Ceylan, E., Hübner, V., Schmid, S., &#38; Srba, J. (2026). Fast re-routing in networks: On the complexity of perfect resilience. In <i>29th International Conference on Principles of Distributed Systems</i> (Vol. 361). Iaşi, Romania: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31\">https://doi.org/10.4230/LIPIcs.OPODIS.2025.31</a>","short":"M. Bentert, E. Ceylan, V. Hübner, S. Schmid, J. Srba, in:, 29th International Conference on Principles of Distributed Systems, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","mla":"Bentert, Matthias, et al. “Fast Re-Routing in Networks: On the Complexity of Perfect Resilience.” <i>29th International Conference on Principles of Distributed Systems</i>, vol. 361, 31, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31\">10.4230/LIPIcs.OPODIS.2025.31</a>.","ieee":"M. Bentert, E. Ceylan, V. Hübner, S. Schmid, and J. Srba, “Fast re-routing in networks: On the complexity of perfect resilience,” in <i>29th International Conference on Principles of Distributed Systems</i>, Iaşi, Romania, 2026, vol. 361.","ama":"Bentert M, Ceylan E, Hübner V, Schmid S, Srba J. Fast re-routing in networks: On the complexity of perfect resilience. In: <i>29th International Conference on Principles of Distributed Systems</i>. Vol 361. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31\">10.4230/LIPIcs.OPODIS.2025.31</a>","chicago":"Bentert, Matthias, Esra Ceylan, Valentin Hübner, Stefan Schmid, and Jiří Srba. “Fast Re-Routing in Networks: On the Complexity of Perfect Resilience.” In <i>29th International Conference on Principles of Distributed Systems</i>, Vol. 361. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31\">https://doi.org/10.4230/LIPIcs.OPODIS.2025.31</a>.","ista":"Bentert M, Ceylan E, Hübner V, Schmid S, Srba J. 2026. Fast re-routing in networks: On the complexity of perfect resilience. 29th International Conference on Principles of Distributed Systems. OPODIS: Conference on Principles of Distributed Systems, LIPIcs, vol. 361, 31."},"alternative_title":["LIPIcs"],"volume":361,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"intvolume":"       361","status":"public","type":"conference","abstract":[{"lang":"eng","text":"To achieve fast recovery from link failures, most modern communication networks feature fully\r\ndecentralized fast re-routing mechanisms. These re-routing mechanisms rely on pre-installed static re-routing rules at the nodes (the routers), which depend only on local failure information, namely on the failed links incident to the node. Ideally, a network is perfectly resilient: the re-routing rules ensure that packets are always successfully routed to their destinations as long as the source and the destination are still physically connected in the underlying network after the failures. Unfortunately, there are examples where achieving perfect resilience is not possible. Surprisingly, only very little is known about the algorithmic aspect of when and how perfect resilience can be achieved. We investigate the computational complexity of analyzing such local fast re-routing mechanisms. Our main result is a negative one: we show that even checking whether a given set of static re-routing rules ensures perfect resilience is coNP-complete. Additionally, we investigate other fundamental variations of the problem. In particular, we show that our coNP-completeness proof also applies to scenarios where the re-routing rules have specific patterns (known as skipping in the literature). On the positive side, for scenarios where nodes do not have information about the link from which a packet arrived (the so-called in-port), we present a linear-time algorithm to realize perfect resilience whenever possible (which we show can also be determined in linear time). "}],"file_date_updated":"2026-03-09T12:33:58Z","oa_version":"Published Version","language":[{"iso":"eng"}],"article_processing_charge":"No","quality_controlled":"1","OA_place":"publisher","scopus_import":"1","department":[{"_id":"KrCh"}],"acknowledgement":"Matthias Bentert: ERC Horizon 2020 research and innovation programme (grant agreement\r\nNo. 819416) and ERC Consolidator grant AdjustNet (agreement No. 864228).\r\nEsra Ceylan: German Research Foundation (DFG) project ReNO, Schwerpunktprogramm:\r\nResilienz in Vernetzten Welten – Beherrschen von Fehlern, Überlast, Angriffen und dem\r\nUnbekannten (SPP 2378).\r\nStefan Schmid: German Research Foundation (DFG) project ReNO, Schwerpunktprogramm:\r\nResilienz in Vernetzten Welten – Beherrschen von Fehlern, Überlast, Angriffen und dem\r\nUnbekannten (SPP 2378).","date_published":"2026-01-07T00:00:00Z","article_number":"31","has_accepted_license":"1"},{"author":[{"full_name":"Hartmanns, Arnd","last_name":"Hartmanns","first_name":"Arnd"},{"first_name":"Sebastian","last_name":"Junges","full_name":"Junges, Sebastian"},{"full_name":"Quatmann, Tim","last_name":"Quatmann","first_name":"Tim"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian","orcid":"0000-0002-0163-2152"}],"doi":"10.1007/s10009-026-00848-y","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"03","citation":{"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.","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>","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>.","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>.","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).","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>"},"publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"title":"The revised practitioner’s guide to MDP model checking algorithms","publication":"International Journal on Software Tools for Technology Transfer","publisher":"Springer Nature","date_updated":"2026-04-07T09:52:54Z","year":"2026","ddc":["000"],"date_created":"2026-04-05T22:01:32Z","oa":1,"OA_type":"hybrid","ec_funded":1,"_id":"21661","day":"09","publication_status":"epub_ahead","keyword":["Quantitative model checking","Markov decision process","Linear programming","Value iteration","Policy iteration"],"department":[{"_id":"KrCh"}],"scopus_import":"1","has_accepted_license":"1","date_published":"2026-03-09T00:00:00Z","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.","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"OA_place":"publisher","main_file_link":[{"url":"https://doi.org/10.1007/s10009-026-00848-y","open_access":"1"}],"language":[{"iso":"eng"}],"oa_version":"Published Version","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"}],"quality_controlled":"1","article_type":"original","article_processing_charge":"Yes (in subscription journal)","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"related_material":{"record":[{"status":"public","id":"21668","relation":"software"}]},"status":"public","type":"journal_article"},{"acknowledgement":"This work was supported by ERC CoG 863818 (ForMSMArt) and Austrian Science Fund (FWF) 10.55776/COE12. We also thank Hossein Zakerinia for his helpful feedback.","date_published":"2026-03-14T00:00:00Z","arxiv":1,"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"scopus_import":"1","OA_place":"repository","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"quality_controlled":"1","article_processing_charge":"No","oa_version":"Preprint","language":[{"iso":"eng"}],"page":"36137-36145","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2505.04539","open_access":"1"}],"abstract":[{"text":"Robust Markov Decision Processes (RMDPs) generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for ω-regular objectives. The qualitative analysis problem asks whether the objective can be ensured with probability 1. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. Our contributions are twofold. We first present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives. We then report experimental results demonstrating the effectiveness of our oracle-based approach on classical RMDP examples from the literature scaling up to thousands of states.","lang":"eng"}],"status":"public","type":"conference","volume":40,"intvolume":"        40","external_id":{"arxiv":["2505.04539"]},"citation":{"ista":"Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. 2026. Qualitative analysis of ω-regular objectives on robust MDPs. Proceedings of the 40th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 40, 36137–36145.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Ehsan Goharshady, Mehrdad Karrabi, and Ali Shafiee. “Qualitative Analysis of ω-Regular Objectives on Robust MDPs.” In <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, 40:36137–45. Association for the Advancement of Artificial Intelligence, 2026. <a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">https://doi.org/10.1609/aaai.v40i43.40931</a>.","ama":"Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. Qualitative analysis of ω-regular objectives on robust MDPs. In: <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>. Vol 40. Association for the Advancement of Artificial Intelligence; 2026:36137-36145. doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">10.1609/aaai.v40i43.40931</a>","ieee":"A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, and A. Shafiee, “Qualitative analysis of ω-regular objectives on robust MDPs,” in <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36137–36145.","mla":"Asadi, Ali, et al. “Qualitative Analysis of ω-Regular Objectives on Robust MDPs.” <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–45, doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">10.1609/aaai.v40i43.40931</a>.","apa":"Asadi, A., Chatterjee, K., Goharshady, E., Karrabi, M., &#38; Shafiee, A. (2026). Qualitative analysis of ω-regular objectives on robust MDPs. In <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i> (Vol. 40, pp. 36137–36145). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">https://doi.org/10.1609/aaai.v40i43.40931</a>","short":"A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, A. Shafiee, in:, Proceedings of the 40th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–36145."},"month":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1609/aaai.v40i43.40931","author":[{"full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","last_name":"Asadi","first_name":"Ali"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8595-0587","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi"},{"id":"67638922-f394-11eb-9cf6-f20423e08757","full_name":"Karrabi, Mehrdad","last_name":"Karrabi","orcid":"0009-0007-5253-9170","first_name":"Mehrdad"},{"first_name":"Ali","last_name":"Shafiee","full_name":"Shafiee, Ali","id":"2783031a-7378-11f0-b2d0-f17f1db2ebad"}],"publication":"Proceedings of the 40th AAAI Conference on Artificial Intelligence","year":"2026","date_updated":"2026-05-04T11:38:56Z","publisher":"Association for the Advancement of Artificial Intelligence","title":"Qualitative analysis of ω-regular objectives on robust MDPs","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"OA_type":"green","ec_funded":1,"conference":{"start_date":"2026-01-20","end_date":"2026-01-27","name":"AAAI: Conference on Artificial Intelligence","location":"Singapore, Singapore"},"day":"14","_id":"21717","date_created":"2026-04-12T22:01:50Z","oa":1,"issue":"43","publication_status":"published"},{"publication_status":"published","issue":"43","_id":"21722","day":"14","conference":{"start_date":"2026-01-20","end_date":"2026-01-27","location":"Singapore, Singapore","name":"AAAI: Conference on Artificial Intelligence"},"OA_type":"green","ec_funded":1,"date_created":"2026-04-12T22:01:52Z","date_updated":"2026-05-04T11:44:14Z","publisher":"Association for the Advancement of Artificial Intelligence","year":"2026","corr_author":"1","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"title":"Revealing POMDPs: Qualitative and quantitative analysis for parity objectives","external_id":{"arxiv":["2511.13134"]},"citation":{"short":"A. Asadi, K. Chatterjee, D. Lurie, R.J. Saona Urmeneta, in:, Proceedings of the AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2026, pp. 36146–36154.","apa":"Asadi, A., Chatterjee, K., Lurie, D., &#38; Saona Urmeneta, R. J. (2026). Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 40, pp. 36146–36154). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">https://doi.org/10.1609/aaai.v40i43.40932</a>","ieee":"A. Asadi, K. Chatterjee, D. Lurie, and R. J. Saona Urmeneta, “Revealing POMDPs: Qualitative and quantitative analysis for parity objectives,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36146–36154.","mla":"Asadi, Ali, et al. “Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026, pp. 36146–54, doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">10.1609/aaai.v40i43.40932</a>.","chicago":"Asadi, Ali, Krishnendu Chatterjee, David Lurie, and Raimundo J Saona Urmeneta. “Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 40:36146–54. Association for the Advancement of Artificial Intelligence, 2026. <a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">https://doi.org/10.1609/aaai.v40i43.40932</a>.","ama":"Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 40. Association for the Advancement of Artificial Intelligence; 2026:36146-36154. doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">10.1609/aaai.v40i43.40932</a>","ista":"Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. 2026. Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 40, 36146–36154."},"doi":"10.1609/aaai.v40i43.40932","author":[{"last_name":"Asadi","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","full_name":"Asadi, Ali","first_name":"Ali"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"579a6c20-34cf-11f1-acbd-8c2f19cdb4da","full_name":"Lurie, David","last_name":"Lurie","first_name":"David"},{"orcid":"0000-0001-5103-038X","first_name":"Raimundo J","full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","last_name":"Saona Urmeneta"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"03","type":"conference","status":"public","intvolume":"        40","volume":40,"article_processing_charge":"No","quality_controlled":"1","abstract":[{"text":"Partially observable Markov decision processes (POMDPs) are a central model for uncertainty in sequential decision making. The most basic objective is the reachability objective, where a target set must be eventually visited, and the more general parity objectives can model all omega-regular specifications. For such objectives, the computational analysis problems are the following: (a) qualitative analysis that asks whether the objective can be satisfied with probability 1 (almost-sure winning) or probability arbitrarily close to 1 (limit-sure winning); and (b) quantitative analysis that asks for the approximation of the optimal probability of satisfying the objective. For general POMDPs, almost-sure analysis for reachability objectives is EXPTIME-complete, but limit-sure and quantitative analyses for reachability objectives are undecidable; almost-sure, limit-sure, and quantitative analyses for parity objectives are all undecidable. A special class of POMDPs, called revealing POMDPs, has been studied recently in several works, and for this subclass the almost-sure analysis for parity objectives was shown to be EXPTIME-complete. In this work, we show that for revealing POMDPs the limit-sure analysis for parity objectives is EXPTIME-complete, and even the quantitative analysis for parity objectives can be achieved in EXPTIME.","lang":"eng"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2511.13134"}],"language":[{"iso":"eng"}],"page":"36146-36154","oa_version":"Preprint","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"OA_place":"repository","arxiv":1,"date_published":"2026-03-14T00:00:00Z","acknowledgement":"This work was partially supported by the ANRT under the French CIFRE Ph.D program in collaboration between NyxAir and Paris-Dauphine University (Contract: CIFRE N° 2022/0513), by the French Agence Nationale de la Recherche (ANR) under reference ANR-21-CE40-\r\n0020 (CONVERGENCE project), by Austrian Science Fund (FWF) 10.55776/COE12, and by the ERC CoG 863818 (ForM-SMArt) grant.","scopus_import":"1","department":[{"_id":"KrCh"}]},{"OA_type":"closed access","_id":"18529","day":"01","date_created":"2024-11-10T23:02:00Z","issue":"1","publication_status":"published","citation":{"ieee":"Y. Zhang <i>et al.</i>, “Limitation of time promotes cooperation in structured collaboration systems,” <i>IEEE Transactions on Network Science and Engineering</i>, vol. 12, no. 1. IEEE, pp. 4–12, 2025.","mla":"Zhang, Yichao, et al. “Limitation of Time Promotes Cooperation in Structured Collaboration Systems.” <i>IEEE Transactions on Network Science and Engineering</i>, vol. 12, no. 1, IEEE, 2025, pp. 4–12, doi:<a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">10.1109/TNSE.2024.3481434</a>.","apa":"Zhang, Y., Wang, J., Wen, G., Guan, J., Zhou, S., Chen, G., … Perc, M. (2025). Limitation of time promotes cooperation in structured collaboration systems. <i>IEEE Transactions on Network Science and Engineering</i>. IEEE. <a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">https://doi.org/10.1109/TNSE.2024.3481434</a>","short":"Y. Zhang, J. Wang, G. Wen, J. Guan, S. Zhou, G. Chen, K. Chatterjee, M. Perc, IEEE Transactions on Network Science and Engineering 12 (2025) 4–12.","ista":"Zhang Y, Wang J, Wen G, Guan J, Zhou S, Chen G, Chatterjee K, Perc M. 2025. Limitation of time promotes cooperation in structured collaboration systems. IEEE Transactions on Network Science and Engineering. 12(1), 4–12.","chicago":"Zhang, Yichao, Jiasheng Wang, Guanghui Wen, Jihong Guan, Shuigeng Zhou, Guanrong Chen, Krishnendu Chatterjee, and Matjaz Perc. “Limitation of Time Promotes Cooperation in Structured Collaboration Systems.” <i>IEEE Transactions on Network Science and Engineering</i>. IEEE, 2025. <a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">https://doi.org/10.1109/TNSE.2024.3481434</a>.","ama":"Zhang Y, Wang J, Wen G, et al. Limitation of time promotes cooperation in structured collaboration systems. <i>IEEE Transactions on Network Science and Engineering</i>. 2025;12(1):4-12. doi:<a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">10.1109/TNSE.2024.3481434</a>"},"external_id":{"isi":["001385382200040"]},"author":[{"first_name":"Yichao","full_name":"Zhang, Yichao","last_name":"Zhang"},{"first_name":"Jiasheng","last_name":"Wang","full_name":"Wang, Jiasheng"},{"first_name":"Guanghui","last_name":"Wen","full_name":"Wen, Guanghui"},{"first_name":"Jihong","full_name":"Guan, Jihong","last_name":"Guan"},{"full_name":"Zhou, Shuigeng","last_name":"Zhou","first_name":"Shuigeng"},{"full_name":"Chen, Guanrong","last_name":"Chen","first_name":"Guanrong"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Perc","full_name":"Perc, Matjaz","first_name":"Matjaz"}],"doi":"10.1109/TNSE.2024.3481434","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","publication":"IEEE Transactions on Network Science and Engineering","date_updated":"2025-02-27T12:35:48Z","publisher":"IEEE","year":"2025","publication_identifier":{"eissn":["2327-4697"]},"title":"Limitation of time promotes cooperation in structured collaboration systems","quality_controlled":"1","article_type":"original","article_processing_charge":"No","page":"4-12","language":[{"iso":"eng"}],"oa_version":"None","abstract":[{"lang":"eng","text":"Temporal networks are obtained from time-dependent interactions among individuals, whereas the interactions can be emails, phone calls, face-to-face meetings, or work collaboration. In this article, a temporal game framework is established, in which interactions among rational individuals are embedded into two-player games in a time-dependent manner. This allows studying the time-dependent complexity and variability of interactions, and the way they affect prosocial behaviors. Based on this simple mathematical model, it is found that the level of cooperation is promoted when the time of collaboration is equally limited for every individual. This observation is confirmed by a series of systematic human experiments on over 1,400 subjects, forming a foundation for comprehensively describing human temporal interactions in collaboration. The research results reveal an important incentive for human cooperation, leading to a better understanding of a fascinating aspect of human nature in society."}],"status":"public","type":"journal_article","volume":12,"intvolume":"        12","date_published":"2025-01-01T00:00:00Z","isi":1,"department":[{"_id":"KrCh"}],"scopus_import":"1"},{"department":[{"_id":"KrCh"}],"isi":1,"scopus_import":"1","has_accepted_license":"1","article_number":"e2319927121","date_published":"2025-06-24T00:00:00Z","acknowledgement":"We gratefully acknowledge the support from the European Research Council (Starting Grant 850529: E-DIRECT) and the Max Planck Society (C.H.), the European Research Council (Consolidator Grant 863818: ForM-SMArt) (K.C.), the Shanghai Pujiang Program (No. 23PJ1405500) (Q.S.), the Army Research Office (Grant No. W911NF-18-1-0325) (N.E.L.), and the John Templeton Foundation (Grant No. 62281) (J.B.P.).","pmid":1,"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"OA_place":"publisher","language":[{"iso":"eng"}],"oa_version":"Published Version","file_date_updated":"2025-07-08T05:52:26Z","abstract":[{"lang":"eng","text":"Multiagent learning is challenging when agents face mixed-motivation interactions, where conflicts of interest arise as agents independently try to optimize their respective outcomes. Recent advancements in evolutionary game theory have identified a class of “zero-determinant” strategies, which confer an agent with significant unilateral control over outcomes in repeated games. Building on these insights, we present a comprehensive generalization of zero-determinant strategies to stochastic games, encompassing dynamic environments. We propose an algorithm that allows an agent to discover strategies enforcing predetermined linear (or approximately linear) payoff relationships. Of particular interest is the relationship in which both payoffs are equal, which serves as a proxy for fairness in symmetric games. We demonstrate that an agent can discover strategies enforcing such relationships through experience alone, without coordinating with an opponent. In finding and using such a strategy, an agent (“enforcer”) can incentivize optimal and equitable outcomes, circumventing potential exploitation. In particular, from the opponent’s viewpoint, the enforcer transforms a mixed-motivation problem into a cooperative problem, paving the way for more collaboration and fairness in multiagent systems."}],"quality_controlled":"1","article_type":"original","article_processing_charge":"Yes (in subscription journal)","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"volume":122,"intvolume":"       122","type":"journal_article","status":"public","author":[{"first_name":"Alex","last_name":"Mcavoy","full_name":"Mcavoy, Alex"},{"first_name":"Udari Madhushani","full_name":"Sehwag, Udari Madhushani","last_name":"Sehwag"},{"orcid":"0000-0001-5116-955X","first_name":"Christian","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","last_name":"Hilbe"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Wolfram","last_name":"Barfuss","full_name":"Barfuss, Wolfram"},{"first_name":"Qi","last_name":"Su","full_name":"Su, Qi"},{"full_name":"Leonard, Naomi Ehrich","last_name":"Leonard","first_name":"Naomi Ehrich"},{"full_name":"Plotkin, Joshua B.","last_name":"Plotkin","first_name":"Joshua B."}],"doi":"10.1073/pnas.2319927121","month":"06","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ieee":"A. Mcavoy <i>et al.</i>, “Unilateral incentive alignment in two-agent stochastic games,” <i>Proceedings of the National Academy of Sciences</i>, vol. 122, no. 25. National Academy of Sciences, 2025.","mla":"Mcavoy, Alex, et al. “Unilateral Incentive Alignment in Two-Agent Stochastic Games.” <i>Proceedings of the National Academy of Sciences</i>, vol. 122, no. 25, e2319927121, National Academy of Sciences, 2025, doi:<a href=\"https://doi.org/10.1073/pnas.2319927121\">10.1073/pnas.2319927121</a>.","short":"A. Mcavoy, U.M. Sehwag, C. Hilbe, K. Chatterjee, W. Barfuss, Q. Su, N.E. Leonard, J.B. Plotkin, Proceedings of the National Academy of Sciences 122 (2025).","apa":"Mcavoy, A., Sehwag, U. M., Hilbe, C., Chatterjee, K., Barfuss, W., Su, Q., … Plotkin, J. B. (2025). Unilateral incentive alignment in two-agent stochastic games. <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.2319927121\">https://doi.org/10.1073/pnas.2319927121</a>","ista":"Mcavoy A, Sehwag UM, Hilbe C, Chatterjee K, Barfuss W, Su Q, Leonard NE, Plotkin JB. 2025. Unilateral incentive alignment in two-agent stochastic games. Proceedings of the National Academy of Sciences. 122(25), e2319927121.","chicago":"Mcavoy, Alex, Udari Madhushani Sehwag, Christian Hilbe, Krishnendu Chatterjee, Wolfram Barfuss, Qi Su, Naomi Ehrich Leonard, and Joshua B. Plotkin. “Unilateral Incentive Alignment in Two-Agent Stochastic Games.” <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences, 2025. <a href=\"https://doi.org/10.1073/pnas.2319927121\">https://doi.org/10.1073/pnas.2319927121</a>.","ama":"Mcavoy A, Sehwag UM, Hilbe C, et al. Unilateral incentive alignment in two-agent stochastic games. <i>Proceedings of the National Academy of Sciences</i>. 2025;122(25). doi:<a href=\"https://doi.org/10.1073/pnas.2319927121\">10.1073/pnas.2319927121</a>"},"external_id":{"isi":["001522351900001"],"pmid":["40523172"]},"publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"title":"Unilateral incentive alignment in two-agent stochastic games","publication":"Proceedings of the National Academy of Sciences","publisher":"National Academy of Sciences","date_updated":"2025-09-30T13:47:14Z","year":"2025","ddc":["000"],"date_created":"2025-07-06T22:01:23Z","oa":1,"OA_type":"hybrid","ec_funded":1,"_id":"19965","day":"24","issue":"25","file":[{"success":1,"file_name":"2025_PNAS_McAvoy.pdf","file_id":"19972","date_updated":"2025-07-08T05:52:26Z","file_size":29525932,"relation":"main_file","date_created":"2025-07-08T05:52:26Z","access_level":"open_access","creator":"dernst","content_type":"application/pdf","checksum":"3b35befd959a3e37aa9080a64a6afaf3"}],"publication_status":"published"},{"file_date_updated":"2025-08-05T07:15:31Z","abstract":[{"text":"Liquid democracy is a transitive vote delegation mechanism over voting graphs. It enables each voter to delegate their vote(s) to another better-informed voter, with the goal of collectively making a better decision. The question of whether liquid democracy outperforms direct voting has been previously studied in the context of local delegation mechanisms (where voters can only delegate to someone in their neighbourhood) and binary decision problems. It has previously been shown that it is impossible for local delegation mechanisms to outperform direct voting in general graphs. This raises the question: for which classes of graphs do local delegation mechanisms yield good results?\r\nIn this work, we analyse (1) properties of specific graphs and (2) properties of local delegation mechanisms on these graphs, determining where local delegation actually outperforms direct voting. We show that a critical graph property enabling liquid democracy is that the voting outcome of local delegation mechanisms preserves a sufficient amount of variance, thereby avoiding situations where delegation falls behind direct voting1. These insights allow us to prove our main results, namely that there exist local delegation mechanisms that perform no worse and in fact quantitatively better than direct voting in natural graph topologies like complete, random d-regular, and bounded degree graphs, lending a more nuanced perspective to previous impossibility results.","lang":"eng"}],"oa_version":"Published Version","main_file_link":[{"url":"https://eprint.iacr.org/2025/745","open_access":"1"}],"page":"241-251","language":[{"iso":"eng"}],"article_processing_charge":"No","quality_controlled":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","type":"conference","isi":1,"department":[{"_id":"KrCh"},{"_id":"KrPi"}],"acknowledgement":"This work was partially supported by MOE-T2EP20122-0014 (DataDriven Distributed Algorithms), German Research Foundation (DFG) project ReNO (SPP 2378) from 2023-2027, ERC CoG 863818 (ForMSMArt) and Austrian Science Fund (FWF) 10.55776/COE12.","date_published":"2025-06-13T00:00:00Z","has_accepted_license":"1","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"OA_place":"publisher","oa":1,"date_created":"2025-07-21T08:18:26Z","ddc":["000"],"day":"13","_id":"20053","ec_funded":1,"OA_type":"hybrid","conference":{"name":"PODC: Symposium on Principles of Distributed Computing","location":"Huatulco, Mexico","start_date":"2025-06-16","end_date":"2025-06-20"},"publication_status":"published","file":[{"access_level":"open_access","date_created":"2025-08-05T07:15:31Z","relation":"main_file","file_size":783297,"creator":"dernst","content_type":"application/pdf","checksum":"cd628fe54d96e9fc6cc789bb8145422b","success":1,"file_name":"2025_PODC_Chatterjee.pdf","file_id":"20122","date_updated":"2025-08-05T07:15:31Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"06","doi":"10.1145/3732772.3733544","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Seth","last_name":"Gilbert","full_name":"Gilbert, Seth"},{"last_name":"Schmid","full_name":"Schmid, Stefan","first_name":"Stefan"},{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267"},{"full_name":"Yeo, Michelle X","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","last_name":"Yeo","first_name":"Michelle X","orcid":"0009-0001-3676-4809"}],"citation":{"apa":"Chatterjee, K., Gilbert, S., Schmid, S., Svoboda, J., &#38; Yeo, M. X. (2025). When is liquid democracy possible?: On the manipulation of variance. In <i>Proceedings of the ACM Symposium on Principles of Distributed Computing</i> (pp. 241–251). Huatulco, Mexico: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3732772.3733544\">https://doi.org/10.1145/3732772.3733544</a>","short":"K. Chatterjee, S. Gilbert, S. Schmid, J. Svoboda, M.X. Yeo, in:, Proceedings of the ACM Symposium on Principles of Distributed Computing, Association for Computing Machinery, 2025, pp. 241–251.","mla":"Chatterjee, Krishnendu, et al. “When Is Liquid Democracy Possible?: On the Manipulation of Variance.” <i>Proceedings of the ACM Symposium on Principles of Distributed Computing</i>, Association for Computing Machinery, 2025, pp. 241–51, doi:<a href=\"https://doi.org/10.1145/3732772.3733544\">10.1145/3732772.3733544</a>.","ieee":"K. Chatterjee, S. Gilbert, S. Schmid, J. Svoboda, and M. X. Yeo, “When is liquid democracy possible?: On the manipulation of variance,” in <i>Proceedings of the ACM Symposium on Principles of Distributed Computing</i>, Huatulco, Mexico, 2025, pp. 241–251.","ama":"Chatterjee K, Gilbert S, Schmid S, Svoboda J, Yeo MX. When is liquid democracy possible?: On the manipulation of variance. In: <i>Proceedings of the ACM Symposium on Principles of Distributed Computing</i>. Association for Computing Machinery; 2025:241-251. doi:<a href=\"https://doi.org/10.1145/3732772.3733544\">10.1145/3732772.3733544</a>","chicago":"Chatterjee, Krishnendu, Seth Gilbert, Stefan Schmid, Jakub Svoboda, and Michelle X Yeo. “When Is Liquid Democracy Possible?: On the Manipulation of Variance.” In <i>Proceedings of the ACM Symposium on Principles of Distributed Computing</i>, 241–51. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3732772.3733544\">https://doi.org/10.1145/3732772.3733544</a>.","ista":"Chatterjee K, Gilbert S, Schmid S, Svoboda J, Yeo MX. 2025. When is liquid democracy possible?: On the manipulation of variance. Proceedings of the ACM Symposium on Principles of Distributed Computing. PODC: Symposium on Principles of Distributed Computing, 241–251."},"external_id":{"isi":["001525534800030"]},"title":"When is liquid democracy possible?: On the manipulation of variance","publication_identifier":{"isbn":["9798400718854"]},"corr_author":"1","year":"2025","date_updated":"2026-02-16T11:46:51Z","publisher":"Association for Computing Machinery","publication":"Proceedings of the ACM Symposium on Principles of Distributed Computing"},{"issue":"8","file":[{"file_id":"20280","file_name":"2025_PNASNexus_Brewster.pdf","success":1,"date_updated":"2025-09-03T06:20:08Z","content_type":"application/pdf","checksum":"8a5e82c6f842e3220ec96028c9374b69","creator":"dernst","file_size":1086419,"relation":"main_file","access_level":"open_access","date_created":"2025-09-03T06:20:08Z"}],"publication_status":"published","OA_type":"gold","ec_funded":1,"_id":"20254","day":"01","ddc":["000"],"date_created":"2025-08-31T22:01:32Z","oa":1,"publication":"PNAS Nexus","date_updated":"2026-02-16T12:23:19Z","publisher":"Oxford University Press","year":"2025","publication_identifier":{"eissn":["2752-6542"]},"PlanS_conform":"1","title":"Maintaining diversity in structured populations","citation":{"ieee":"D. A. Brewster, J. Svoboda, D. Roscow, K. Chatterjee, J. Tkadlec, and M. A. Nowak, “Maintaining diversity in structured populations,” <i>PNAS Nexus</i>, vol. 4, no. 8. Oxford University Press, 2025.","mla":"Brewster, David A., et al. “Maintaining Diversity in Structured Populations.” <i>PNAS Nexus</i>, vol. 4, no. 8, pgaf252, Oxford University Press, 2025, doi:<a href=\"https://doi.org/10.1093/pnasnexus/pgaf252\">10.1093/pnasnexus/pgaf252</a>.","apa":"Brewster, D. A., Svoboda, J., Roscow, D., Chatterjee, K., Tkadlec, J., &#38; Nowak, M. A. (2025). Maintaining diversity in structured populations. <i>PNAS Nexus</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/pnasnexus/pgaf252\">https://doi.org/10.1093/pnasnexus/pgaf252</a>","short":"D.A. Brewster, J. Svoboda, D. Roscow, K. Chatterjee, J. Tkadlec, M.A. Nowak, PNAS Nexus 4 (2025).","ista":"Brewster DA, Svoboda J, Roscow D, Chatterjee K, Tkadlec J, Nowak MA. 2025. Maintaining diversity in structured populations. PNAS Nexus. 4(8), pgaf252.","chicago":"Brewster, David A., Jakub Svoboda, Dylan Roscow, Krishnendu Chatterjee, Josef Tkadlec, and Martin A. Nowak. “Maintaining Diversity in Structured Populations.” <i>PNAS Nexus</i>. Oxford University Press, 2025. <a href=\"https://doi.org/10.1093/pnasnexus/pgaf252\">https://doi.org/10.1093/pnasnexus/pgaf252</a>.","ama":"Brewster DA, Svoboda J, Roscow D, Chatterjee K, Tkadlec J, Nowak MA. Maintaining diversity in structured populations. <i>PNAS Nexus</i>. 2025;4(8). doi:<a href=\"https://doi.org/10.1093/pnasnexus/pgaf252\">10.1093/pnasnexus/pgaf252</a>"},"external_id":{"arxiv":["2503.09841"]},"author":[{"first_name":"David A.","full_name":"Brewster, David A.","last_name":"Brewster"},{"orcid":"0000-0002-1419-3267","first_name":"Jakub","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda"},{"first_name":"Dylan","full_name":"Roscow, Dylan","last_name":"Roscow"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","first_name":"Josef"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"doi":"10.1093/pnasnexus/pgaf252","month":"08","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"volume":4,"intvolume":"         4","quality_controlled":"1","article_type":"original","article_processing_charge":"Yes","language":[{"iso":"eng"}],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"We examine population structures for their ability to maintain diversity in neutral evolution. We use the general framework of evolutionary graph theory and consider birth–death (bd) and death–birth (db) updating. The population is of size N. Initially all individuals represent different types. The basic question is: what is the time TN until one type takes over the population? This time is known as consensus time in computer science and as total coalescent time in evolutionary biology. For the complete graph, it is known that TN is quadratic in N for db and bd. For the cycle, we prove that TN is cubic in N for db and bd. For the star, we prove that TN is cubic for bd and quasilinear (N log N) for db. For the double star, we show that TN is quartic for bd. We derive upper and lower bounds for all undirected graphs for bd and db. We also show the Pareto front of graphs (of size N = 8) that maintain diversity the longest for bd and db. Further, we show that some graphs that quickly homogenize can maintain high levels of diversity longer than graphs that slowly homogenize. For directed graphs, we give simple contracting star-like structures that have superexponential time scales for maintaining diversity."}],"file_date_updated":"2025-09-03T06:20:08Z","OA_place":"publisher","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"has_accepted_license":"1","date_published":"2025-08-01T00:00:00Z","arxiv":1,"article_number":"pgaf252","acknowledgement":"J.S. and K.C. were supported by the European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12. J.T. was supported by GAČR grant 25-17377S and by Charles Univ. projects UNCE 24/SCI/008 and PRIMUS 24/SCI/012.","DOAJ_listed":"1","department":[{"_id":"KrCh"}],"scopus_import":"1"},{"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"scopus_import":"1","has_accepted_license":"1","date_published":"2025-07-01T00:00:00Z","arxiv":1,"acknowledgement":"This research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12, the support of the French Agence Nationale de la Recherche (ANR) under reference ANR-21-CE40-0020 (CONVERGENCE project), and the ERC CoG 863818 (ForM-SMArt) grant.","OA_place":"publisher","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"language":[{"iso":"eng"}],"page":"238-247","oa_version":"Published Version","file_date_updated":"2025-09-09T08:19:41Z","abstract":[{"text":"A standard model that arises in several applications in sequential decision-making is partially observable Markov decision processes (POMDPs) where a decision-making agent interacts with an uncertain environment. A basic objective in POMDPs is the reachability objective, where given a target set of states, the goal is to eventually arrive at one of them.\r\n\r\nThe limit-sure problem asks whether reachability can be ensured with probability arbitrarily close to 1. In general, the limit-sure reachability problem for POMDPs is undecidable. However, in many practical cases, the most relevant question is the existence of policies with a small amount of memory. In this work, we study the limit-sure reachability problem for POMDPs with a fixed amount of memory. We establish that the computational complexity of the problem is NP-complete.","lang":"eng"}],"quality_controlled":"1","article_processing_charge":"No","intvolume":"       286","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"volume":286,"alternative_title":["PMLR"],"status":"public","type":"conference","author":[{"full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","last_name":"Asadi","first_name":"Ali"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","first_name":"Raimundo J"},{"last_name":"Shafiee","full_name":"Shafiee, Ali","id":"2783031a-7378-11f0-b2d0-f17f1db2ebad","first_name":"Ali"}],"month":"07","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"arxiv":["2412.00941"]},"citation":{"ama":"Asadi A, Chatterjee K, Saona Urmeneta RJ, Shafiee A. Limit-sure reachability for small memory policies in POMDPs is NP-complete. In: <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>. Vol 286. ML Research Press; 2025:238-247.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Raimundo J Saona Urmeneta, and Ali Shafiee. “Limit-Sure Reachability for Small Memory Policies in POMDPs Is NP-Complete.” In <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, 286:238–47. ML Research Press, 2025.","ista":"Asadi A, Chatterjee K, Saona Urmeneta RJ, Shafiee A. 2025. Limit-sure reachability for small memory policies in POMDPs is NP-complete. The 41st Conference on Uncertainty in Artificial Intelligence. UAI: Conference on Uncertainty in Artificial Intelligence, PMLR, vol. 286, 238–247.","apa":"Asadi, A., Chatterjee, K., Saona Urmeneta, R. J., &#38; Shafiee, A. (2025). Limit-sure reachability for small memory policies in POMDPs is NP-complete. In <i>The 41st Conference on Uncertainty in Artificial Intelligence</i> (Vol. 286, pp. 238–247). Rio de Janeiro, Brazil: ML Research Press.","short":"A. Asadi, K. Chatterjee, R.J. Saona Urmeneta, A. Shafiee, in:, The 41st Conference on Uncertainty in Artificial Intelligence, ML Research Press, 2025, pp. 238–247.","mla":"Asadi, Ali, et al. “Limit-Sure Reachability for Small Memory Policies in POMDPs Is NP-Complete.” <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, vol. 286, ML Research Press, 2025, pp. 238–47.","ieee":"A. Asadi, K. Chatterjee, R. J. Saona Urmeneta, and A. Shafiee, “Limit-sure reachability for small memory policies in POMDPs is NP-complete,” in <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, Rio de Janeiro, Brazil, 2025, vol. 286, pp. 238–247."},"publication_identifier":{"eissn":["2640-3498"]},"title":"Limit-sure reachability for small memory policies in POMDPs is NP-complete","publication":"The 41st Conference on Uncertainty in Artificial Intelligence","publisher":"ML Research Press","date_updated":"2025-09-09T08:21:45Z","corr_author":"1","year":"2025","ddc":["000"],"date_created":"2025-09-07T22:01:34Z","oa":1,"conference":{"location":"Rio de Janeiro, Brazil","name":"UAI: Conference on Uncertainty in Artificial Intelligence","start_date":"2025-07-21","end_date":"2025-07-25"},"OA_type":"diamond","ec_funded":1,"_id":"20297","day":"01","file":[{"file_name":"2025_UAI_AsadiAli.pdf","file_id":"20315","success":1,"date_updated":"2025-09-09T08:19:41Z","checksum":"1a37ebe7ba73ab6985765bf0d17a0acc","content_type":"application/pdf","creator":"dernst","access_level":"open_access","date_created":"2025-09-09T08:19:41Z","relation":"main_file","file_size":307458}],"publication_status":"published"},{"OA_place":"publisher","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"scopus_import":"1","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and Austrian Science Fund (FWF) 10.55776/COE12.\r\n","arxiv":1,"date_published":"2025-01-01T00:00:00Z","has_accepted_license":"1","alternative_title":["PMLR"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"intvolume":"       286","volume":286,"status":"public","type":"conference","file_date_updated":"2025-09-09T06:27:59Z","abstract":[{"text":"Deterministic Markov Decision Processes (DMDPs) are a mathematical framework for decision-making where the outcomes and future possible actions are deterministically determined by the current action taken. DMDPs can be viewed as a finite directed weighted graph, where in each step, the controller chooses an outgoing edge. An objective is a measurable function on runs (or infinite trajectories) of the DMDP, and the value for an objective is the maximal cumulative reward (or weight) that the controller can guarantee. We consider the classical mean-payoff (aka limit-average) objective, which is a basic and fundamental objective.\r\n\r\nHoward's policy iteration algorithm is a popular method for solving DMDPs with mean-payoff objectives. Although Howard's algorithm performs well in practice, as experimental studies suggested, the best known upper bound is exponential and the current known lower bound is as follows: For the input size I, the algorithm requires (math formular) iterations, where (math formular) hides the poly-logarithmic factors, i.e., the current lower bound on iterations is sub-linear with respect to the input size. Our main result is an improved lower bound for this fundamental algorithm where we show that for the input size I, the algorithm requires (math formular) iterations.","lang":"eng"}],"oa_version":"Published Version","page":"223-232","language":[{"iso":"eng"}],"article_processing_charge":"No","quality_controlled":"1","title":"Lower bound on Howard policy iteration for deterministic Markov Decision Processes","publication_identifier":{"eissn":["2640-3498"]},"year":"2025","corr_author":"1","publisher":"ML Research Press","date_updated":"2025-09-09T06:31:20Z","publication":"The 41st Conference on Uncertainty in Artificial Intelligence","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","author":[{"first_name":"Ali","last_name":"Asadi","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","full_name":"Asadi, Ali"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"De Raaij","full_name":"De Raaij, Jakob","first_name":"Jakob"}],"citation":{"mla":"Asadi, Ali, et al. “Lower Bound on Howard Policy Iteration for Deterministic Markov Decision Processes.” <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, vol. 286, ML Research Press, 2025, pp. 223–32.","ieee":"A. Asadi, K. Chatterjee, and J. De Raaij, “Lower bound on Howard policy iteration for deterministic Markov Decision Processes,” in <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, Rio de Janeiro, Brazil, 2025, vol. 286, pp. 223–232.","apa":"Asadi, A., Chatterjee, K., &#38; De Raaij, J. (2025). Lower bound on Howard policy iteration for deterministic Markov Decision Processes. In <i>The 41st Conference on Uncertainty in Artificial Intelligence</i> (Vol. 286, pp. 223–232). Rio de Janeiro, Brazil: ML Research Press.","short":"A. Asadi, K. Chatterjee, J. De Raaij, in:, The 41st Conference on Uncertainty in Artificial Intelligence, ML Research Press, 2025, pp. 223–232.","ista":"Asadi A, Chatterjee K, De Raaij J. 2025. Lower bound on Howard policy iteration for deterministic Markov Decision Processes. The 41st Conference on Uncertainty in Artificial Intelligence. UAI: Conference on Uncertainty in Artificial Intelligence, PMLR, vol. 286, 223–232.","ama":"Asadi A, Chatterjee K, De Raaij J. Lower bound on Howard policy iteration for deterministic Markov Decision Processes. In: <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>. Vol 286. ML Research Press; 2025:223-232.","chicago":"Asadi, Ali, Krishnendu Chatterjee, and Jakob De Raaij. “Lower Bound on Howard Policy Iteration for Deterministic Markov Decision Processes.” In <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, 286:223–32. ML Research Press, 2025."},"external_id":{"arxiv":["2506.12254"]},"publication_status":"published","file":[{"file_id":"20313","file_name":"2025_UAI_Asadi.pdf","success":1,"date_updated":"2025-09-09T06:27:59Z","creator":"dernst","checksum":"4180c81bb6ed3b4f5c7a8e48d06520c6","content_type":"application/pdf","date_created":"2025-09-09T06:27:59Z","access_level":"open_access","file_size":317097,"relation":"main_file"}],"oa":1,"date_created":"2025-09-07T22:01:34Z","ddc":["000"],"day":"01","_id":"20299","ec_funded":1,"OA_type":"diamond","conference":{"name":"UAI: Conference on Uncertainty in Artificial Intelligence","location":"Rio de Janeiro, Brazil","start_date":"2025-07-21","end_date":"2025-07-25"}},{"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"OA_place":"repository","date_published":"2025-05-01T00:00:00Z","arxiv":1,"acknowledgement":"The authors thank for the helpful discussions with Eduard Gorbunov, Kumar Kshitij Patel, Anton\r\nRodomanov, and Ali Zindari during the preparation of this work. This work was partially done during the first author’s stays at CISPA and at MBZUAI. The first author also acknowledges ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12.","department":[{"_id":"KrCh"}],"scopus_import":"1","type":"conference","status":"public","intvolume":"       258","volume":258,"alternative_title":["PMLR"],"quality_controlled":"1","article_processing_charge":"No","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2501.04443","open_access":"1"}],"page":"2539-2547","language":[{"iso":"eng"}],"oa_version":"Preprint","abstract":[{"lang":"eng","text":"LocalSGD and SCAFFOLD are widely used methods in distributed stochastic optimization, with numerous applications in machine learning, large-scale data processing, and federated learning. However, rigorously establishing their theoretical advantages over simpler methods, such as minibatch SGD (MbSGD), has proven challenging, as existing analyses often rely on strong assumptions, unrealistic premises, or overly restrictive scenarios.\r\n\r\nIn this work, we revisit the convergence properties of LocalSGD and SCAFFOLD under a variety of existing or weaker conditions, including gradient similarity, Hessian similarity, weak convexity, and Lipschitz continuity of the Hessian. Our analysis shows that (i) LocalSGD achieves faster convergence compared to MbSGD for weakly convex functions without requiring stronger gradient similarity assumptions; (ii) LocalSGD benefits significantly from higher-order similarity and smoothness; and (iii) SCAFFOLD demonstrates faster convergence than MbSGD for a broader class of non-quadratic functions. These theoretical insights provide a clearer understanding of the conditions under which LocalSGD and SCAFFOLD outperform MbSGD."}],"publication":"The 28th International Conference on Artificial Intelligence and Statistics","date_updated":"2025-09-09T07:17:08Z","publisher":"ML Research Press","year":"2025","publication_identifier":{"eissn":["2640-3498"]},"title":"Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis","external_id":{"arxiv":["2501.04443"]},"citation":{"ama":"Luo R, Stich SU, Horváth S, Takáč M. Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis. In: <i>The 28th International Conference on Artificial Intelligence and Statistics</i>. Vol 258. ML Research Press; 2025:2539-2547.","chicago":"Luo, Ruichen, Sebastian U. Stich, Samuel Horváth, and Martin Takáč. “Revisiting LocalSGD and SCAFFOLD: Improved Rates and Missing Analysis.” In <i>The 28th International Conference on Artificial Intelligence and Statistics</i>, 258:2539–47. ML Research Press, 2025.","ista":"Luo R, Stich SU, Horváth S, Takáč M. 2025. Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis. The 28th International Conference on Artificial Intelligence and Statistics. AISTATS: Conference on Artificial Intelligence and Statistics, PMLR, vol. 258, 2539–2547.","short":"R. Luo, S.U. Stich, S. Horváth, M. Takáč, in:, The 28th International Conference on Artificial Intelligence and Statistics, ML Research Press, 2025, pp. 2539–2547.","apa":"Luo, R., Stich, S. U., Horváth, S., &#38; Takáč, M. (2025). Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis. In <i>The 28th International Conference on Artificial Intelligence and Statistics</i> (Vol. 258, pp. 2539–2547). Mai Khao, Thailand: ML Research Press.","mla":"Luo, Ruichen, et al. “Revisiting LocalSGD and SCAFFOLD: Improved Rates and Missing Analysis.” <i>The 28th International Conference on Artificial Intelligence and Statistics</i>, vol. 258, ML Research Press, 2025, pp. 2539–47.","ieee":"R. Luo, S. U. Stich, S. Horváth, and M. Takáč, “Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis,” in <i>The 28th International Conference on Artificial Intelligence and Statistics</i>, Mai Khao, Thailand, 2025, vol. 258, pp. 2539–2547."},"author":[{"first_name":"Ruichen","id":"b391db08-1ffe-11ee-8b67-d18ddcfb5a14","full_name":"Luo, Ruichen","last_name":"Luo"},{"first_name":"Sebastian U.","full_name":"Stich, Sebastian U.","last_name":"Stich"},{"last_name":"Horváth","full_name":"Horváth, Samuel","first_name":"Samuel"},{"last_name":"Takáč","full_name":"Takáč, Martin","first_name":"Martin"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"05","publication_status":"published","conference":{"end_date":"2025-05-05","start_date":"2025-05-03","name":"AISTATS: Conference on Artificial Intelligence and Statistics","location":"Mai Khao, Thailand"},"ec_funded":1,"OA_type":"green","_id":"20302","day":"01","date_created":"2025-09-07T22:01:35Z","oa":1},{"abstract":[{"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.","lang":"eng"}],"page":"195-218","language":[{"iso":"eng"}],"oa_version":"None","article_processing_charge":"No","quality_controlled":"1","alternative_title":["LNCS"],"intvolume":"     16143","volume":16143,"type":"conference","status":"public","scopus_import":"1","department":[{"_id":"KrCh"}],"date_published":"2025-10-02T00:00:00Z","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).","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"date_created":"2025-11-09T23:01:34Z","_id":"20610","day":"02","conference":{"name":"QEST-FORMATS: International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","location":"Aarhus, Denmark","end_date":"2025-08-28","start_date":"2025-08-26"},"ec_funded":1,"publication_status":"published","author":[{"orcid":"0000-0002-1712-2165","first_name":"Tobias","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian","orcid":"0000-0002-0163-2152"},{"last_name":"Wienhöft","full_name":"Wienhöft, Patrick","first_name":"Patrick"}],"doi":"10.1007/978-3-032-05792-1_11","month":"10","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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>.","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>","short":"T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Second International Joint Conference on QEST+FORMATS, Springer Nature, 2025, pp. 195–218.","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>","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_identifier":{"eissn":["1611-3349"],"isbn":["9783032057914"],"issn":["0302-9743"]},"title":"What are the odds? Improving statistical model checking of Markov decision processes","date_updated":"2025-11-10T08:06:27Z","publisher":"Springer Nature","year":"2025","publication":"Second International Joint Conference on QEST+FORMATS"},{"publication_status":"published","conference":{"start_date":"2025-10-27","end_date":"2025-10-31","name":"ATVA: Automated Technology for Verification and Analysis","location":"Bengaluru, India"},"ec_funded":1,"OA_type":"green","_id":"20648","day":"26","date_created":"2025-11-16T23:01:24Z","oa":1,"publication":"23rd International Symposium on Automated Technology for Verification and Analysis","publisher":"Springer Nature","date_updated":"2025-11-24T13:11:10Z","year":"2025","corr_author":"1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783032087065"]},"title":"PolyQEnt: A polynomial quantified entailment solver","external_id":{"arxiv":["2408.03796"]},"citation":{"short":"K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, M. Saadat, M. Seeliger, D. Zikelic, in:, 23rd International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2025, pp. 411–424.","apa":"Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., Saadat, M., Seeliger, M., &#38; Zikelic, D. (2025). PolyQEnt: A polynomial quantified entailment solver. In <i>23rd International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 16145, pp. 411–424). Bengaluru, India: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">https://doi.org/10.1007/978-3-032-08707-2_19</a>","mla":"Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment Solver.” <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:<a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">10.1007/978-3-032-08707-2_19</a>.","ieee":"K. Chatterjee <i>et al.</i>, “PolyQEnt: A polynomial quantified entailment solver,” in <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, Bengaluru, India, 2025, vol. 16145, pp. 411–424.","ama":"Chatterjee K, Goharshady AK, Goharshady E, et al. PolyQEnt: A polynomial quantified entailment solver. In: <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>. Vol 16145. Springer Nature; 2025:411-424. doi:<a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">10.1007/978-3-032-08707-2_19</a>","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and Dorde Zikelic. “PolyQEnt: A Polynomial Quantified Entailment Solver.” In <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, 16145:411–24. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">https://doi.org/10.1007/978-3-032-08707-2_19</a>.","ista":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424."},"doi":"10.1007/978-3-032-08707-2_19","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady"},{"first_name":"Ehsan","orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi"},{"full_name":"Karrabi, Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757","last_name":"Karrabi","first_name":"Mehrdad","orcid":"0009-0007-5253-9170"},{"last_name":"Saadat","full_name":"Saadat, Milad","first_name":"Milad"},{"first_name":"Maximilian","full_name":"Seeliger, Maximilian","last_name":"Seeliger"},{"first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic"}],"month":"10","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","status":"public","intvolume":"     16145","volume":16145,"alternative_title":["LNCS"],"quality_controlled":"1","article_processing_charge":"No","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2408.03796"}],"page":"411-424","oa_version":"Preprint","abstract":[{"lang":"eng","text":"Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is a tool for solving polynomial quantified entailments in which variables on both sides of the implication are real valued or unbounded integers. Our tool provides a unified framework for polynomial quantified entailment problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks shows the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints."}],"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"OA_place":"repository","date_published":"2025-10-26T00:00:00Z","arxiv":1,"acknowledgement":"This work was supported by the following grants: ERC CoG 863818 (ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, ERC StG 101222524 (SPES), the Ethereum Foundation Research Grant FY24-1793, and the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SISSMU-100).","department":[{"_id":"KrCh"}],"scopus_import":"1"},{"type":"conference","status":"public","quality_controlled":"1","article_processing_charge":"No","language":[{"iso":"eng"}],"page":"568-580","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.21087"}],"oa_version":"Preprint","abstract":[{"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.","lang":"eng"}],"project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"OA_place":"repository","arxiv":1,"date_published":"2025-10-09T00:00:00Z","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).","department":[{"_id":"KrCh"}],"scopus_import":"1","publication_status":"published","conference":{"end_date":"2025-06-26","start_date":"2025-06-23","location":"Singapore, Singapore","name":"LICS: Logic in Computer Science"},"OA_type":"green","ec_funded":1,"_id":"20688","day":"09","date_created":"2025-11-24T14:23:49Z","oa":1,"publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","publisher":"IEEE","date_updated":"2025-11-26T07:34:19Z","year":"2025","corr_author":"1","publication_identifier":{"eisbn":["9798331579005"]},"title":"Stopping criteria for value iteration on concurrent stochastic reachability and safety games","external_id":{"arxiv":["2505.21087"]},"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.","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>.","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>","short":"M. Grobelna, J. Kretinsky, M. Weininger, in:, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 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.","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>.","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>"},"doi":"10.1109/lics65433.2025.00049","author":[{"last_name":"Grobelna","full_name":"Grobelna, Marta","first_name":"Marta"},{"first_name":"Jan","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"},{"orcid":"0000-0002-0163-2152","first_name":"Maximilian","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger"}],"month":"10","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"external_id":{"arxiv":["2504.18277"]},"citation":{"mla":"Baier, Christel, et al. “Multiplicative Rewards in Markovian Models.” <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2025, pp. 499–512, doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00044\">10.1109/lics65433.2025.00044</a>.","ieee":"C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Multiplicative rewards in Markovian models,” in <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Singapore, Singapore, 2025, pp. 499–512.","apa":"Baier, C., Chatterjee, K., Meggendorfer, T., &#38; Piribauer, J. (2025). Multiplicative rewards in Markovian models. In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 499–512). Singapore, Singapore: IEEE. <a href=\"https://doi.org/10.1109/lics65433.2025.00044\">https://doi.org/10.1109/lics65433.2025.00044</a>","short":"C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, in:, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp. 499–512.","ista":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2025. Multiplicative rewards in Markovian models. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 499–512.","ama":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Multiplicative rewards in Markovian models. In: <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2025:499-512. doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00044\">10.1109/lics65433.2025.00044</a>","chicago":"Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer. “Multiplicative Rewards in Markovian Models.” In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 499–512. IEEE, 2025. <a href=\"https://doi.org/10.1109/lics65433.2025.00044\">https://doi.org/10.1109/lics65433.2025.00044</a>."},"author":[{"last_name":"Baier","full_name":"Baier, Christel","first_name":"Christel"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"orcid":"0000-0002-1712-2165","first_name":"Tobias","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"first_name":"Jakob","full_name":"Piribauer, Jakob","last_name":"Piribauer"}],"doi":"10.1109/lics65433.2025.00044","month":"10","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","publisher":"IEEE","date_updated":"2025-11-25T07:59:25Z","corr_author":"1","year":"2025","publication_identifier":{"eisbn":["9798331579005"]},"title":"Multiplicative rewards in Markovian models","conference":{"end_date":"2025-06-26","start_date":"2025-06-23","location":"Singapore, Singapore","name":"LICS: Logic in Computer Science"},"OA_type":"green","ec_funded":1,"_id":"20689","day":"09","date_created":"2025-11-24T14:24:00Z","oa":1,"publication_status":"published","date_published":"2025-10-09T00:00:00Z","arxiv":1,"acknowledgement":"This work was partly funded by the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12, the DFG Grant 389792660 as part of TRR 248 (Foundations of Perspicuous Software Systems), the Cluster of Excellence EXC 2050/1 (CeTI, project ID\r\n390696704, as part of Germany’s Excellence Strategy), and by the BMBF (Federal Ministry of Education and Research) in DAAD project 57616814 (SECAI, School of Embedded and\r\nComposite AI) as part of the program Konrad Zuse Schools of Excellence in Artificial Intelligence.","department":[{"_id":"KrCh"}],"scopus_import":"1","OA_place":"repository","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"quality_controlled":"1","article_processing_charge":"No","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2504.18277","open_access":"1"}],"language":[{"iso":"eng"}],"page":"499-512","oa_version":"Preprint","abstract":[{"text":"This paper studies the expected value of multiplicative rewards, where rewards obtained in each step are multiplied (instead of the usual addition), in Markov chains (MCs) and Markov decision processes (MDPs). One of the key differences to additive rewards is that the expected value may diverge to ∞ not only due to recurrent, but also due to transient states.For MCs, computing the value is shown to be possible in polynomial time given an oracle for the comparison of succinctly represented integers (CSRI), which is only known to be solvable in polynomial time subject to number-theoretic conjectures. Interestingly, distinguishing whether the value is ∞ or 0 is at least as hard as CSRI, while determining if it is one of these two can be done in polynomial time. In MDPs, the optimal value can be computed in polynomial space. Further refined complexity results and results on the complexity of optimal schedulers are presented. The techniques developed for MDPs additionally allow to solve the multiplicative variant of the stochastic shortest path problem. Finally, for MCs and MDPs where an absorbing state is reached almost surely, all considered problems are solvable in polynomial time.","lang":"eng"}],"status":"public","type":"conference"},{"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).","arxiv":1,"date_published":"2025-10-09T00:00:00Z","department":[{"_id":"KrCh"}],"scopus_import":"1","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"OA_place":"repository","quality_controlled":"1","article_processing_charge":"No","oa_version":"Preprint","language":[{"iso":"eng"}],"page":"458-471","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.09514"}],"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"}],"type":"conference","status":"public","external_id":{"arxiv":["2505.09514"]},"citation":{"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>.","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>","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.","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.","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>","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.","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>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"10","author":[{"first_name":"Thomas","full_name":"Brihaye, Thomas","last_name":"Brihaye"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Mohr, Stefanie","last_name":"Mohr","first_name":"Stefanie"},{"last_name":"Weininger","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","orcid":"0000-0002-0163-2152"}],"doi":"10.1109/lics65433.2025.00041","publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","year":"2025","corr_author":"1","publisher":"IEEE","date_updated":"2025-11-25T07:59:49Z","title":"Risk-aware Markov decision processes using cumulative prospect theory","publication_identifier":{"eisbn":["9798331579005"]},"ec_funded":1,"OA_type":"green","conference":{"location":"Singapore, Singapore","name":"LICS: Logic in Computer Science","start_date":"2025-06-23","end_date":"2025-06-26"},"day":"09","_id":"20690","date_created":"2025-11-24T14:43:47Z","oa":1,"publication_status":"published"},{"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).","date_published":"2025-01-23T00:00:00Z","arxiv":1,"isi":1,"department":[{"_id":"KrCh"}],"scopus_import":"1","project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"OA_place":"repository","quality_controlled":"1","article_processing_charge":"No","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2410.18293"}],"language":[{"iso":"eng"}],"page":"97-120","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"}],"type":"conference","status":"public","intvolume":"     15530","volume":15530,"alternative_title":["LNCS"],"external_id":{"isi":["001446577100005"],"arxiv":["2410.18293"]},"citation":{"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.","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>.","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>.","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.","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>","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."},"month":"01","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1007/978-3-031-82703-7_5","author":[{"first_name":"Muqsit","full_name":"Azeem, Muqsit","last_name":"Azeem"},{"last_name":"Chakraborty","full_name":"Chakraborty, Debraj","first_name":"Debraj"},{"first_name":"Sudeep","full_name":"Kanav, Sudeep","last_name":"Kanav"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan"},{"first_name":"Mohammadsadegh","last_name":"Mohagheghi","full_name":"Mohagheghi, Mohammadsadegh"},{"full_name":"Mohr, Stefanie","last_name":"Mohr","first_name":"Stefanie"},{"first_name":"Maximilian","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger"}],"publication":"26th International Conference on Verification, Model Checking, and Abstract Interpretation","year":"2025","publisher":"Springer Nature","date_updated":"2025-09-30T10:46:54Z","title":"1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization","publication_identifier":{"isbn":["9783031827020"],"issn":["0302-9743"],"eissn":["1611-3349"]},"OA_type":"green","ec_funded":1,"conference":{"location":"Denver, CO, United States","name":"VMCAI: Verification, Model Checking, and Abstract Interpretation","start_date":"2025-01-20","end_date":"2025-01-21"},"day":"23","_id":"19375","date_created":"2025-03-09T23:01:29Z","oa":1,"publication_status":"published"},{"acknowledgement":"J. M. Křišťan acknowledges the support of the Czech Science Foundation Grant No. 24-12046S. This work was supported by the Grant Agency of the Czech Technical University in Prague, grant No. SGS23/205/OHK3/3T/18. J. Svoboda acknowledges the support of the ERC CoG 863818 (ForM-SMArt) grant.","arxiv":1,"date_published":"2025-02-20T00:00:00Z","scopus_import":"1","department":[{"_id":"KrCh"}],"isi":1,"OA_place":"repository","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"article_processing_charge":"No","quality_controlled":"1","abstract":[{"lang":"eng","text":"In reconfiguration, we are given two solutions to a graph problem, such as Vertex Cover or Dominating Set, with each solution represented by a placement of tokens on vertices of the graph. Our task is to reconfigure one into the other using small steps while ensuring the intermediate configurations of tokens are also valid solutions. The two commonly studied settings are Token Jumping and Token Sliding, which allows moving a single token to an arbitrary or an adjacent vertex, respectively.\r\n\r\nWe introduce new rules that generalize Token Jumping, parameterized by the number of tokens allowed to move at once and by the maximum distance of each move. Our main contribution is identifying minimal rules that allow reconfiguring any possible given solution into any other for Independent Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide an efficient algorithm that finds a corresponding reconfiguration sequence.\r\n\r\nWe further focus on the rule that allows each token to move to an adjacent vertex in a single step. This natural variant turns out to be the minimal rule that guarantees reconfigurability for Vertex Cover. We determine the computational complexity of deciding whether a (shortest) reconfiguration sequence exists under this rule for the three studied problems. While reachability for Vertex Cover is shown to be in P, finding a shortest sequence is shown to be NP-complete. For Independent Set and Dominating Set, even reachability is shown to be PSPACE-complete."}],"oa_version":"Preprint","page":"244-265","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2411.12582","open_access":"1"}],"status":"public","type":"conference","alternative_title":["LNCS"],"intvolume":"     15411","volume":15411,"citation":{"ista":"Křišťan JM, Svoboda J. 2025. Reconfiguration using generalized token jumping. 19th International Conference and Workshops on Algorithms and Computation. WALCOM: International Conference and Workshops on Algorithms and Computation, LNCS, vol. 15411, 244–265.","ama":"Křišťan JM, Svoboda J. Reconfiguration using generalized token jumping. In: <i>19th International Conference and Workshops on Algorithms and Computation</i>. Vol 15411. Springer Nature; 2025:244-265. doi:<a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">10.1007/978-981-96-2845-2_16</a>","chicago":"Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized Token Jumping.” In <i>19th International Conference and Workshops on Algorithms and Computation</i>, 15411:244–65. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">https://doi.org/10.1007/978-981-96-2845-2_16</a>.","mla":"Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized Token Jumping.” <i>19th International Conference and Workshops on Algorithms and Computation</i>, vol. 15411, Springer Nature, 2025, pp. 244–65, doi:<a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">10.1007/978-981-96-2845-2_16</a>.","ieee":"J. M. Křišťan and J. Svoboda, “Reconfiguration using generalized token jumping,” in <i>19th International Conference and Workshops on Algorithms and Computation</i>, Chengdu, China, 2025, vol. 15411, pp. 244–265.","apa":"Křišťan, J. M., &#38; Svoboda, J. (2025). Reconfiguration using generalized token jumping. In <i>19th International Conference and Workshops on Algorithms and Computation</i> (Vol. 15411, pp. 244–265). Chengdu, China: Springer Nature. <a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">https://doi.org/10.1007/978-981-96-2845-2_16</a>","short":"J.M. Křišťan, J. Svoboda, in:, 19th International Conference and Workshops on Algorithms and Computation, Springer Nature, 2025, pp. 244–265."},"external_id":{"isi":["001537885900016"],"arxiv":["2411.12582"]},"month":"02","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"first_name":"Jan Matyáš","full_name":"Křišťan, Jan Matyáš","last_name":"Křišťan"},{"first_name":"Jakub","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda"}],"doi":"10.1007/978-981-96-2845-2_16","year":"2025","date_updated":"2025-09-30T11:14:33Z","publisher":"Springer Nature","publication":"19th International Conference and Workshops on Algorithms and Computation","title":"Reconfiguration using generalized token jumping","publication_identifier":{"isbn":["9789819628445"],"issn":["0302-9743"],"eissn":["1611-3349"]},"day":"20","_id":"19445","ec_funded":1,"OA_type":"green","conference":{"location":"Chengdu, China","name":"WALCOM: International Conference and Workshops on Algorithms and Computation","end_date":"2025-03-02","start_date":"2025-02-28"},"oa":1,"date_created":"2025-03-23T23:01:27Z","publication_status":"published"},{"scopus_import":"1","department":[{"_id":"KrPi"},{"_id":"KrCh"}],"date_published":"2025-04-01T00:00:00Z","acknowledgement":"This work was supported in part by the ERC CoG 863818 (ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, and MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms) grants.","OA_place":"repository","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"abstract":[{"text":"In this work, we explore route discovery in private payment channel networks. We first determine what “ideal\" privacy for a routing protocol means in this setting. We observe that protocols achieving this strong privacy definition exist by leveraging Multi-Party Computation but they are inherently inefficient as they must involve the entire network. We then present protocols with weaker privacy guarantees but much better efficiency (involving only a small fraction of the nodes). The core idea is that both sender and receiver gossip a message which propagates through the network, and the moment any node in the network receives both messages, a path is found. In our first protocol the message is always sent to all neighbouring nodes with a delay proportional to the fees of that edge. In our second protocol the message is only sent to one neighbour chosen randomly with a probability proportional to its degree. We additionally propose a more realistic notion of privacy in order to measure the privacy leakage of our protocols in practice. Our realistic notion of privacy challenges an adversary that join the network with a fixed budget to create channels to guess the sender and receiver of a transaction upon receiving messages from our protocols. Simulations of our protocols on the Lightning network topology (for random transactions and uniform fees) show that 1) forming edges with high degree nodes is a more effective attack strategy for the adversary, 2) there is a tradeoff between the number of nodes involved in our protocols (privacy) and the optimality of the discovered path, and 3) our protocols involve a very small fraction of the network on average.","lang":"eng"}],"language":[{"iso":"eng"}],"main_file_link":[{"url":"https://eprint.iacr.org/2021/1539","open_access":"1"}],"page":"207-223","oa_version":"Submitted Version","article_processing_charge":"No","quality_controlled":"1","alternative_title":["LNCS"],"intvolume":"     15263","volume":15263,"type":"conference","status":"public","author":[{"first_name":"Zeta","last_name":"Avarikioti","full_name":"Avarikioti, Zeta"},{"last_name":"Bastankhah","full_name":"Bastankhah, Mahsa","first_name":"Mahsa"},{"full_name":"Maddah-Ali, Mohammad Ali","last_name":"Maddah-Ali","first_name":"Mohammad Ali"},{"first_name":"Krzysztof Z","orcid":"0000-0002-9139-1654","last_name":"Pietrzak","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","full_name":"Pietrzak, Krzysztof Z"},{"last_name":"Svoboda","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","first_name":"Jakub","orcid":"0000-0002-1419-3267"},{"last_name":"Yeo","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","full_name":"Yeo, Michelle X","first_name":"Michelle X","orcid":"0009-0001-3676-4809"}],"doi":"10.1007/978-3-031-82349-7_15","month":"04","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Avarikioti, Zeta, Mahsa Bastankhah, Mohammad Ali Maddah-Ali, Krzysztof Z Pietrzak, Jakub Svoboda, and Michelle X Yeo. “Route Discovery in Private Payment Channel Networks.” In <i>Computer Security. ESORICS 2024 International Workshops</i>, 15263:207–23. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">https://doi.org/10.1007/978-3-031-82349-7_15</a>.","ama":"Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX. Route discovery in private payment channel networks. In: <i>Computer Security. ESORICS 2024 International Workshops</i>. Vol 15263. Springer Nature; 2025:207-223. doi:<a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">10.1007/978-3-031-82349-7_15</a>","ista":"Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX. 2025. Route discovery in private payment channel networks. Computer Security. ESORICS 2024 International Workshops. ESORICS: European Symposium on Research in Computer Security, LNCS, vol. 15263, 207–223.","short":"Z. Avarikioti, M. Bastankhah, M.A. Maddah-Ali, K.Z. Pietrzak, J. Svoboda, M.X. Yeo, in:, Computer Security. ESORICS 2024 International Workshops, Springer Nature, 2025, pp. 207–223.","apa":"Avarikioti, Z., Bastankhah, M., Maddah-Ali, M. A., Pietrzak, K. Z., Svoboda, J., &#38; Yeo, M. X. (2025). Route discovery in private payment channel networks. In <i>Computer Security. ESORICS 2024 International Workshops</i> (Vol. 15263, pp. 207–223). Bydgoszcz, Poland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">https://doi.org/10.1007/978-3-031-82349-7_15</a>","ieee":"Z. Avarikioti, M. Bastankhah, M. A. Maddah-Ali, K. Z. Pietrzak, J. Svoboda, and M. X. Yeo, “Route discovery in private payment channel networks,” in <i>Computer Security. ESORICS 2024 International Workshops</i>, Bydgoszcz, Poland, 2025, vol. 15263, pp. 207–223.","mla":"Avarikioti, Zeta, et al. “Route Discovery in Private Payment Channel Networks.” <i>Computer Security. ESORICS 2024 International Workshops</i>, vol. 15263, Springer Nature, 2025, pp. 207–23, doi:<a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">10.1007/978-3-031-82349-7_15</a>."},"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031823480"],"issn":["0302-9743"]},"title":"Route discovery in private payment channel networks","date_updated":"2025-11-05T07:52:35Z","publisher":"Springer Nature","year":"2025","publication":"Computer Security. ESORICS 2024 International Workshops","oa":1,"date_created":"2025-04-20T22:01:28Z","_id":"19600","day":"01","conference":{"name":"ESORICS: European Symposium on Research in Computer Security","location":"Bydgoszcz, Poland","start_date":"2024-09-16","end_date":"2024-09-20"},"ec_funded":1,"OA_type":"green","publication_status":"published"},{"publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"title":"Solving robust Markov decision processes: Generic, reliable, efficient","date_updated":"2026-02-16T12:25:05Z","publisher":"Association for the Advancement of Artificial Intelligence","year":"2025","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","doi":"10.1609/aaai.v39i25.34865","author":[{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","first_name":"Tobias","orcid":"0000-0002-1712-2165"},{"first_name":"Maximilian","orcid":"0000-0002-0163-2152","last_name":"Weininger","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881"},{"full_name":"Wienhöft, Patrick","last_name":"Wienhöft","first_name":"Patrick"}],"month":"04","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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.","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>.","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>","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.","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.","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>.","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>"},"external_id":{"arxiv":["2412.10185"]},"publication_status":"published","issue":"25","oa":1,"date_created":"2025-05-11T22:02:39Z","_id":"19666","day":"11","conference":{"end_date":"2025-03-04","start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence","location":"Philadelphia, PA, United States"},"OA_type":"green","ec_funded":1,"OA_place":"repository","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"scopus_import":"1","department":[{"_id":"KrCh"}],"date_published":"2025-04-11T00:00:00Z","arxiv":1,"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).","volume":39,"intvolume":"        39","related_material":{"link":[{"url":"https://doi.org/10.5281/zenodo.14385449","relation":"software"}]},"type":"conference","status":"public","abstract":[{"lang":"eng","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."}],"page":"26631-26641","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2412.10185","open_access":"1"}],"language":[{"iso":"eng"}],"oa_version":"Preprint","article_processing_charge":"No","quality_controlled":"1"}]