[{"oa_version":"Preprint","conference":{"end_date":"2025-03-04","location":"Philadelphia, PA, United States","start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence"},"issue":"25","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","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."}],"status":"public","date_published":"2025-04-11T00:00:00Z","OA_type":"green","language":[{"iso":"eng"}],"volume":39,"page":"26631-26641","article_processing_charge":"No","doi":"10.1609/aaai.v39i25.34865","date_updated":"2026-02-16T12:25:05Z","day":"11","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"author":[{"last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","orcid":"0000-0002-1712-2165"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","orcid":"0000-0002-0163-2152","last_name":"Weininger","full_name":"Weininger, Maximilian"},{"last_name":"Wienhöft","full_name":"Wienhöft, Patrick","first_name":"Patrick"}],"publisher":"Association for the Advancement of Artificial Intelligence","type":"conference","month":"04","scopus_import":"1","oa":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).","publication_status":"published","arxiv":1,"external_id":{"arxiv":["2412.10185"]},"year":"2025","related_material":{"link":[{"url":"https://doi.org/10.5281/zenodo.14385449","relation":"software"}]},"intvolume":"        39","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"19666","ec_funded":1,"publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"OA_place":"repository","citation":{"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>.","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>.","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.","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.","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>","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>"},"title":"Solving robust Markov decision processes: Generic, reliable, efficient","department":[{"_id":"KrCh"}],"quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.10185"}],"date_created":"2025-05-11T22:02:39Z"},{"abstract":[{"text":"The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredient in our approach are Positivstellensätze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state of the art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks.","lang":"eng"}],"corr_author":"1","status":"public","issue":"11","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2025-02-25","location":"Philadelphia, PA, United States","end_date":"2025-03-04"},"oa_version":"Preprint","page":"11158-11166","article_processing_charge":"No","doi":"10.1609/aaai.v39i11.33213","volume":39,"OA_type":"green","date_published":"2025-04-11T00:00:00Z","language":[{"iso":"eng"}],"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"day":"11","date_updated":"2026-02-16T12:24:47Z","type":"conference","publisher":"Association for the Advancement of Artificial Intelligence","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi"},{"last_name":"Karrabi","full_name":"Karrabi, Mehrdad","orcid":"0009-0007-5253-9170","first_name":"Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"last_name":"Motwani","full_name":"Motwani, Harshit J.","first_name":"Harshit J."},{"full_name":"Seeliger, Maximilian","last_name":"Seeliger","first_name":"Maximilian"},{"last_name":"Zikelic","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","acknowledgement":"This work was partially funded by ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12.","scopus_import":"1","oa":1,"month":"04","intvolume":"        39","external_id":{"arxiv":["2412.16226"]},"arxiv":1,"year":"2025","OA_place":"repository","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"ec_funded":1,"_id":"19667","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.16226"}],"date_created":"2025-05-11T22:02:39Z","title":"Quantified linear and polynomial arithmetic satisfiability via template-based skolemization","quality_controlled":"1","department":[{"_id":"KrCh"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. “Quantified Linear and Polynomial Arithmetic Satisfiability via Template-Based Skolemization.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 11, Association for the Advancement of Artificial Intelligence, 2025, pp. 11158–66, doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">10.1609/aaai.v39i11.33213</a>.","ieee":"K. Chatterjee, E. Goharshady, M. Karrabi, H. J. Motwani, M. Seeliger, and D. Zikelic, “Quantified linear and polynomial arithmetic satisfiability via template-based skolemization,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 11, pp. 11158–11166.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Harshit J. Motwani, Maximilian Seeliger, and Dorde Zikelic. “Quantified Linear and Polynomial Arithmetic Satisfiability via Template-Based Skolemization.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:11158–66. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">https://doi.org/10.1609/aaai.v39i11.33213</a>.","ama":"Chatterjee K, Goharshady E, Karrabi M, Motwani HJ, Seeliger M, Zikelic D. Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:11158-11166. doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">10.1609/aaai.v39i11.33213</a>","apa":"Chatterjee, K., Goharshady, E., Karrabi, M., Motwani, H. J., Seeliger, M., &#38; Zikelic, D. (2025). Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 11158–11166). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">https://doi.org/10.1609/aaai.v39i11.33213</a>","short":"K. Chatterjee, E. Goharshady, M. Karrabi, H.J. Motwani, M. Seeliger, D. Zikelic, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 11158–11166.","ista":"Chatterjee K, Goharshady E, Karrabi M, Motwani HJ, Seeliger M, Zikelic D. 2025. Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 11158–11166."}},{"month":"04","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and the Austrian Science Fund (FWF) 10.55776/COE12 grant.","publication_status":"published","scopus_import":"1","oa":1,"arxiv":1,"external_id":{"arxiv":["2412.12228"]},"year":"2025","intvolume":"        39","_id":"19669","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"ec_funded":1,"citation":{"ista":"Chatterjee K, Luo R, Saona Urmeneta RJ, Svoboda J. 2025. Linear equations with min and max operators: Computational complexity. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 11150–11157.","short":"K. Chatterjee, R. Luo, R.J. Saona Urmeneta, J. Svoboda, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 11150–11157.","ama":"Chatterjee K, Luo R, Saona Urmeneta RJ, Svoboda J. Linear equations with min and max operators: Computational complexity. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:11150-11157. doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33212\">10.1609/aaai.v39i11.33212</a>","apa":"Chatterjee, K., Luo, R., Saona Urmeneta, R. J., &#38; Svoboda, J. (2025). Linear equations with min and max operators: Computational complexity. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 11150–11157). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i11.33212\">https://doi.org/10.1609/aaai.v39i11.33212</a>","chicago":"Chatterjee, Krishnendu, Ruichen Luo, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Linear Equations with Min and Max Operators: Computational Complexity.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:11150–57. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i11.33212\">https://doi.org/10.1609/aaai.v39i11.33212</a>.","ieee":"K. Chatterjee, R. Luo, R. J. Saona Urmeneta, and J. Svoboda, “Linear equations with min and max operators: Computational complexity,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 11, pp. 11150–11157.","mla":"Chatterjee, Krishnendu, et al. “Linear Equations with Min and Max Operators: Computational Complexity.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 11, Association for the Advancement of Artificial Intelligence, 2025, pp. 11150–57, doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33212\">10.1609/aaai.v39i11.33212</a>."},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.12228"}],"date_created":"2025-05-11T22:02:40Z","title":"Linear equations with min and max operators: Computational complexity","department":[{"_id":"KrCh"}],"quality_controlled":"1","conference":{"end_date":"2025-03-04","location":"Philadelphia, PA, United States","start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence"},"oa_version":"Preprint","abstract":[{"lang":"eng","text":"We consider a class of optimization problems defined by a system of linear equations with min and max operators. This class of optimization problems has been studied under restrictive conditions, such as, (C1) the halting or stability condition; (C2) the non-negative coefficients condition; (C3) the sum upto 1 condition; and (C4) the only min or only max operator condition. Several seminal results in the literature focus on special cases. For example, turn-based stochastic games correspond to conditions C2 and C3; and Markov decision process to conditions C2, C3, and C4. However, the systematic computational complexity study of all the cases has not been explored, which we address in this work. Some highlights of our results are: with conditions C2 and C4, and with conditions C3 and C4, the problem is NP-complete, whereas with condition C1 only, the problem is in UP intersects coUP. Finally, we establish the computational complexity of the decision problem of checking the respective conditions."}],"corr_author":"1","status":"public","issue":"11","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","date_published":"2025-04-11T00:00:00Z","OA_type":"green","language":[{"iso":"eng"}],"page":"11150-11157","doi":"10.1609/aaai.v39i11.33212","article_processing_charge":"No","volume":39,"date_updated":"2025-05-12T09:42:09Z","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"day":"11","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Luo","full_name":"Luo, Ruichen","first_name":"Ruichen","id":"b391db08-1ffe-11ee-8b67-d18ddcfb5a14"},{"full_name":"Saona Urmeneta, Raimundo J","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","first_name":"Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"last_name":"Svoboda","full_name":"Svoboda, Jakub","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267"}],"publisher":"Association for the Advancement of Artificial Intelligence","type":"conference"},{"intvolume":"     15697","year":"2025","external_id":{"arxiv":["2505.06769"]},"arxiv":1,"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and Austrian Science Fund (FWF) 10.55776/COE12 grant.","publication_status":"published","ddc":["000"],"scopus_import":"1","oa":1,"license":"https://creativecommons.org/licenses/by/4.0/","alternative_title":["LNCS"],"month":"05","date_created":"2025-05-25T22:17:06Z","quality_controlled":"1","department":[{"_id":"KrCh"}],"title":"Value iteration with guessing for Markov chains and Markov decision processes","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"has_accepted_license":"1","citation":{"chicago":"Chatterjee, Krishnendu, Mahdi Jafariraviz, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Value Iteration with Guessing for Markov Chains and Markov Decision Processes.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:217–36. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">https://doi.org/10.1007/978-3-031-90653-4_11</a>.","ieee":"K. Chatterjee, M. Jafariraviz, R. J. Saona Urmeneta, and J. Svoboda, “Value iteration with guessing for Markov chains and Markov decision processes,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 217–236.","mla":"Chatterjee, Krishnendu, et al. “Value Iteration with Guessing for Markov Chains and Markov Decision Processes.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 217–36, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">10.1007/978-3-031-90653-4_11</a>.","ista":"Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. 2025. Value iteration with guessing for Markov chains and Markov decision processes. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 217–236.","short":"K. Chatterjee, M. Jafariraviz, R.J. Saona Urmeneta, J. Svoboda, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 217–236.","ama":"Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. Value iteration with guessing for Markov chains and Markov decision processes. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:217-236. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">10.1007/978-3-031-90653-4_11</a>","apa":"Chatterjee, K., Jafariraviz, M., Saona Urmeneta, R. J., &#38; Svoboda, J. (2025). Value iteration with guessing for Markov chains and Markov decision processes. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 217–236). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">https://doi.org/10.1007/978-3-031-90653-4_11</a>"},"OA_place":"publisher","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031906527"],"issn":["0302-9743"]},"ec_funded":1,"_id":"19740","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","doi":"10.1007/978-3-031-90653-4_11","page":"217-236","volume":15697,"file_date_updated":"2025-06-02T07:31:12Z","OA_type":"hybrid","language":[{"iso":"eng"}],"date_published":"2025-05-01T00:00:00Z","status":"public","abstract":[{"text":"Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.","lang":"eng"}],"corr_author":"1","file":[{"date_created":"2025-06-02T07:31:12Z","checksum":"45da6efbcbed20aada16c48c8e55e2d6","relation":"main_file","success":1,"content_type":"application/pdf","creator":"dernst","file_size":557481,"access_level":"open_access","file_name":"2025_TACAS_Chatterjee.pdf","date_updated":"2025-06-02T07:31:12Z","file_id":"19767"}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Hamilton, ON, Canada","start_date":"2025-05-03","end_date":"2025-05-08"},"oa_version":"Published Version","type":"conference","publisher":"Springer Nature","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Mahdi","last_name":"Jafariraviz","full_name":"Jafariraviz, Mahdi"},{"id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","first_name":"Raimundo J","orcid":"0000-0001-5103-038X","last_name":"Saona Urmeneta","full_name":"Saona Urmeneta, Raimundo J"},{"orcid":"0000-0002-1419-3267","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","full_name":"Svoboda, Jakub"}],"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"day":"01","date_updated":"2025-06-02T07:35:06Z"},{"ec_funded":1,"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031906428"],"issn":["0302-9743"]},"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"19742","title":"Sound statistical model checking for probabilities and expected rewards","quality_controlled":"1","department":[{"_id":"KrCh"}],"date_created":"2025-05-25T22:17:08Z","citation":{"mla":"Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 167–90, doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">10.1007/978-3-031-90643-5_9</a>.","ieee":"C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft, “Sound statistical model checking for probabilities and expected rewards,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190.","chicago":"Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:167–90. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>.","apa":"Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Sound statistical model checking for probabilities and expected rewards. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>","ama":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical model checking for probabilities and expected rewards. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:167-190. doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">10.1007/978-3-031-90643-5_9</a>","short":"C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 167–190.","ista":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound statistical model checking for probabilities and expected rewards. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15696, 167–190."},"has_accepted_license":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"alternative_title":["LNCS"],"oa":1,"scopus_import":"1","acknowledgement":"This work was supported by the DFG through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy) and the TRR 248 (see perspicuous-computing.science, project ID 389792660), by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by the EU under NextGenerationEU projects D53D23008400006 (Smartitude) under MUR PRIN 2022 and PE00000014 (SERICS) under MUR PNRR, by the Interreg North Sea project STORM_SAFE, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy).","ddc":["000"],"publication_status":"published","month":"05","related_material":{"record":[{"id":"19769","status":"public","relation":"research_data"}]},"intvolume":"     15696","external_id":{"arxiv":["2411.00559"]},"arxiv":1,"year":"2025","day":"01","project":[{"name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"date_updated":"2025-06-02T09:45:41Z","type":"conference","author":[{"first_name":"Carlos E.","full_name":"Budde, Carlos E.","last_name":"Budde"},{"last_name":"Hartmanns","full_name":"Hartmanns, Arnd","first_name":"Arnd"},{"last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian"},{"full_name":"Wienhöft, Patrick","last_name":"Wienhöft","first_name":"Patrick"}],"publisher":"Springer Nature","file":[{"content_type":"application/pdf","creator":"dernst","file_size":711271,"file_id":"19770","file_name":"2025_TACAS_Budde.pdf","date_updated":"2025-06-02T09:35:42Z","access_level":"open_access","relation":"main_file","checksum":"d45856b503b1dd4f8f14c3566327225b","date_created":"2025-06-02T09:35:42Z","success":1}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","abstract":[{"lang":"eng","text":"Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results."}],"status":"public","oa_version":"Published Version","conference":{"start_date":"2025-05-03","location":"Hamilton, ON, Canada","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2025-05-08"},"volume":15696,"page":"167-190","doi":"10.1007/978-3-031-90643-5_9","article_processing_charge":"No","OA_type":"hybrid","language":[{"iso":"eng"}],"date_published":"2025-05-01T00:00:00Z","file_date_updated":"2025-06-02T09:35:42Z"},{"has_accepted_license":"1","citation":{"apa":"Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., &#38; Zilken, D. (2025). Fixed point certificates for reachability and expected rewards in MDPs. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 130–151). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>","ama":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. Fixed point certificates for reachability and expected rewards in MDPs. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:130-151. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>","short":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 130–151.","ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Fixed point certificates for reachability and expected rewards in MDPs. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 130–151.","mla":"Chatterjee, Krishnendu, et al. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 130–51, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>.","ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Fixed point certificates for reachability and expected rewards in MDPs,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 130–151.","chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:130–51. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>."},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"department":[{"_id":"KrCh"}],"quality_controlled":"1","title":"Fixed point certificates for reachability and expected rewards in MDPs","date_created":"2025-05-25T22:17:09Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"19743","ec_funded":1,"OA_place":"publisher","publication_identifier":{"isbn":["9783031906527"],"eissn":["1611-3349"],"issn":["0302-9743"]},"year":"2025","arxiv":1,"external_id":{"arxiv":["2501.11467"]},"related_material":{"record":[{"status":"public","relation":"research_data","id":"19771"}]},"intvolume":"     15697","month":"05","oa":1,"scopus_import":"1","alternative_title":["LNCS"],"ddc":["000"],"publication_status":"published","acknowledgement":"This project has received funding from the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12, a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, the DFG RTG 378803395 (ConVeY), the EU’s Horizon 2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement Nos. 101034413 (IST-BRIDGE) and 101008233 (MISSION), and the DFG RTG 2236 (UnRAVeL). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632.","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Tim","full_name":"Quatmann, Tim","last_name":"Quatmann"},{"first_name":"Maximilian","last_name":"Schäffeler","full_name":"Schäffeler, Maximilian"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian"},{"first_name":"Tobias","last_name":"Winkler","full_name":"Winkler, Tobias"},{"first_name":"Daniel","id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3","full_name":"Zilken, Daniel","last_name":"Zilken"}],"publisher":"Springer Nature","type":"conference","date_updated":"2025-06-02T10:55:34Z","day":"01","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"file_date_updated":"2025-06-02T10:49:52Z","language":[{"iso":"eng"}],"date_published":"2025-05-01T00:00:00Z","OA_type":"hybrid","volume":15697,"article_processing_charge":"No","doi":"10.1007/978-3-031-90653-4_7","page":"130-151","oa_version":"Published Version","conference":{"end_date":"2025-05-08","start_date":"2025-05-03","location":"Hamilton, ON, Canada","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","file":[{"success":1,"relation":"main_file","checksum":"64b7f46ef05649b87b827248045c7645","date_created":"2025-06-02T10:49:52Z","file_id":"19772","date_updated":"2025-06-02T10:49:52Z","file_name":"2025_TACAS_ChatterjeeKrish.pdf","access_level":"open_access","file_size":732136,"creator":"dernst","content_type":"application/pdf"}],"status":"public","corr_author":"1","abstract":[{"text":"The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates—lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.","lang":"eng"}]},{"external_id":{"arxiv":["2501.06579"]},"arxiv":1,"year":"2025","intvolume":"     15697","month":"05","ddc":["000"],"acknowledgement":"This work was partially supported by ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12. Petr Novotný is supported by the Czech Science Foundation grant no. GA23-06963S.","publication_status":"published","alternative_title":["LNCS"],"oa":1,"scopus_import":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"citation":{"mla":"Chatterjee, Krishnendu, et al. “Refuting Equivalence in Probabilistic Programs with Conditioning.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 279–300, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Refuting equivalence in probabilistic programs with conditioning,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 279–300.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Refuting Equivalence in Probabilistic Programs with Conditioning.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:279–300. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">https://doi.org/10.1007/978-3-031-90653-4_14</a>.","ama":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. Refuting equivalence in probabilistic programs with conditioning. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:279-300. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>","apa":"Chatterjee, K., Goharshady, E., Novotný, P., &#38; Zikelic, D. (2025). Refuting equivalence in probabilistic programs with conditioning. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 279–300). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">https://doi.org/10.1007/978-3-031-90653-4_14</a>","short":"K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 279–300.","ista":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2025. Refuting equivalence in probabilistic programs with conditioning. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 279–300."},"has_accepted_license":"1","date_created":"2025-05-25T22:17:10Z","title":"Refuting equivalence in probabilistic programs with conditioning","department":[{"_id":"KrCh"}],"quality_controlled":"1","_id":"19744","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031906527"],"eissn":["1611-3349"]},"OA_place":"publisher","ec_funded":1,"date_published":"2025-05-01T00:00:00Z","OA_type":"hybrid","language":[{"iso":"eng"}],"file_date_updated":"2025-06-02T11:13:49Z","page":"279-300","doi":"10.1007/978-3-031-90653-4_14","article_processing_charge":"No","volume":15697,"conference":{"end_date":"2025-05-08","location":"Hamilton, ON, Canada","start_date":"2025-05-03","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"oa_version":"Published Version","abstract":[{"lang":"eng","text":"We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature."}],"corr_author":"1","status":"public","file":[{"success":1,"relation":"main_file","date_created":"2025-06-02T11:13:49Z","checksum":"7dcd85e7e753bfa994c10b3cf9ebc185","file_name":"2025_TACAS_Chatterjee_Goharshadi.pdf","date_updated":"2025-06-02T11:13:49Z","file_id":"19773","access_level":"open_access","creator":"dernst","file_size":532181,"content_type":"application/pdf"}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kafshdar Goharshadi","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","orcid":"0000-0002-8595-0587"},{"last_name":"Novotný","full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"},{"orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","full_name":"Zikelic, Dorde","last_name":"Zikelic"}],"publisher":"Springer Nature","type":"conference","date_updated":"2025-06-02T11:16:13Z","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"day":"01"},{"title":"Sound statistical model checking for probabilities and expected rewards (experimental reproduction package)","department":[{"_id":"KrCh"}],"main_file_link":[{"url":"https://doi.org/10.5281/ZENODO.14602066","open_access":"1"}],"date_created":"2025-06-02T09:37:14Z","type":"research_data_reference","citation":{"short":"C. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, (2025).","ista":"Budde C, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound statistical model checking for probabilities and expected rewards (experimental reproduction package), Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.14602066\">10.5281/ZENODO.14602066</a>.","ama":"Budde C, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical model checking for probabilities and expected rewards (experimental reproduction package). 2025. doi:<a href=\"https://doi.org/10.5281/ZENODO.14602066\">10.5281/ZENODO.14602066</a>","apa":"Budde, C., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Sound statistical model checking for probabilities and expected rewards (experimental reproduction package). Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.14602066\">https://doi.org/10.5281/ZENODO.14602066</a>","ieee":"C. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft, “Sound statistical model checking for probabilities and expected rewards (experimental reproduction package).” Zenodo, 2025.","chicago":"Budde, Carlos, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and Expected Rewards (Experimental Reproduction Package).” Zenodo, 2025. <a href=\"https://doi.org/10.5281/ZENODO.14602066\">https://doi.org/10.5281/ZENODO.14602066</a>.","mla":"Budde, Carlos, et al. <i>Sound Statistical Model Checking for Probabilities and Expected Rewards (Experimental Reproduction Package)</i>. Zenodo, 2025, doi:<a href=\"https://doi.org/10.5281/ZENODO.14602066\">10.5281/ZENODO.14602066</a>."},"publisher":"Zenodo","author":[{"full_name":"Budde, Carlos","last_name":"Budde","first_name":"Carlos"},{"first_name":"Arnd","full_name":"Hartmanns, Arnd","last_name":"Hartmanns"},{"first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian"},{"first_name":"Patrick","full_name":"Wienhöft, Patrick","last_name":"Wienhöft"}],"day":"07","OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"19769","date_updated":"2025-06-02T09:45:41Z","related_material":{"record":[{"id":"19742","status":"public","relation":"used_in_publication"}]},"doi":"10.5281/ZENODO.14602066","article_processing_charge":"No","OA_type":"green","date_published":"2025-01-07T00:00:00Z","year":"2025","oa":1,"abstract":[{"text":"Artifact to reproduce the experimental results presented in the article \"Sound Statistical Model Checking for Probabilities and Expected Rewards\" by Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft (TACAS 2025).\r\n\r\nThe contents include all data and software (formal models, software tools, Python & bash scripts) used in the experimental evaluation presented in sections 3, 4, and 6 of the article. Detailed instructions on how to reproduce the results are bundled in the artifact.","lang":"eng"}],"status":"public","ddc":["000"],"oa_version":"Published Version","month":"01"},{"day":"09","OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-06-02T10:55:35Z","_id":"19771","title":"Artifact: Fixed point certificates for reachability and expected rewards in MDPs","department":[{"_id":"KrCh"}],"date_created":"2025-06-02T10:13:24Z","type":"research_data_reference","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/ZENODO.14626585"}],"citation":{"ama":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. Artifact: Fixed point certificates for reachability and expected rewards in MDPs. 2025. doi:<a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>","apa":"Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., &#38; Zilken, D. (2025). Artifact: Fixed point certificates for reachability and expected rewards in MDPs. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.14626585\">https://doi.org/10.5281/ZENODO.14626585</a>","short":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken, (2025).","ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Artifact: Fixed point certificates for reachability and expected rewards in MDPs, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs</i>. Zenodo, 2025, doi:<a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>.","ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Artifact: Fixed point certificates for reachability and expected rewards in MDPs.” Zenodo, 2025.","chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” Zenodo, 2025. <a href=\"https://doi.org/10.5281/ZENODO.14626585\">https://doi.org/10.5281/ZENODO.14626585</a>."},"publisher":"Zenodo","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Tim","last_name":"Quatmann","full_name":"Quatmann, Tim"},{"last_name":"Schäffeler","full_name":"Schäffeler, Maximilian","first_name":"Maximilian"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881"},{"full_name":"Winkler, Tobias","last_name":"Winkler","first_name":"Tobias"},{"id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3","first_name":"Daniel","last_name":"Zilken","full_name":"Zilken, Daniel"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"oa":1,"abstract":[{"lang":"eng","text":"This artifact allows to review and reproduce the Isabelle proofs and practical experiments from the paper *Fixed Point Certificates for Reachability and Expected Rewards in MDPs*.\r\nThe contents are two-fold:\r\nFirst, the artifact contains a formally verified certificate checker for the certificates presented in the paper.\r\nThe formal Isabelle/HOL proofs of the background theory can be inspected, checked by Isabelle and the code extraction can be retraced.\r\n\r\nSecond, the artifact contains a modified version of the model checking tool `Storm` with support for certificate generation. Together with the provided scripts and benchmark files, this allows to reproduce the experiments from the paper.\r\nAn appropriate subset of the experiments is given to allow a review in a timely manner. In addition, original logfiles from our experiments are provided, allowing a detailed inspection.\r\n\r\nThe package includes convenient installation scripts for [the TACAS 2023 VM](https://doi.org/10.5281/zenodo.7113223) (based on Ubuntu 22.04).\r\nA native installation on Linux or macOS systems (including the newer ARM-based machines) is also possible."}],"status":"public","ddc":["000"],"oa_version":"Published Version","month":"01","related_material":{"record":[{"relation":"used_in_publication","status":"public","id":"19743"}]},"article_processing_charge":"No","doi":"10.5281/ZENODO.14626585","date_published":"2025-01-09T00:00:00Z","OA_type":"green","year":"2025"},{"month":"05","DOAJ_listed":"1","ddc":["000"],"acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.).","publication_status":"published","license":"https://creativecommons.org/licenses/by-nc/4.0/","oa":1,"article_type":"original","scopus_import":"1","external_id":{"pmid":["40417077"]},"year":"2025","intvolume":"         4","related_material":{"record":[{"id":"19903","relation":"dissertation_contains","status":"public"}]},"_id":"19843","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"eissn":["2752-6542"]},"OA_place":"publisher","ec_funded":1,"article_number":"pgaf154","tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","short":"CC BY-NC (4.0)","image":"/images/cc_by_nc.png"},"pmid":1,"citation":{"ista":"Hübner V, Schmid L, Hilbe C, Chatterjee K. 2025. Stable strategies of direct and indirect reciprocity across all social dilemmas. PNAS Nexus. 4(5), pgaf154.","short":"V. Hübner, L. Schmid, C. Hilbe, K. Chatterjee, PNAS Nexus 4 (2025).","ama":"Hübner V, Schmid L, Hilbe C, Chatterjee K. Stable strategies of direct and indirect reciprocity across all social dilemmas. <i>PNAS Nexus</i>. 2025;4(5). doi:<a href=\"https://doi.org/10.1093/pnasnexus/pgaf154\">10.1093/pnasnexus/pgaf154</a>","apa":"Hübner, V., Schmid, L., Hilbe, C., &#38; Chatterjee, K. (2025). Stable strategies of direct and indirect reciprocity across all social dilemmas. <i>PNAS Nexus</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/pnasnexus/pgaf154\">https://doi.org/10.1093/pnasnexus/pgaf154</a>","chicago":"Hübner, Valentin, Laura Schmid, Christian Hilbe, and Krishnendu Chatterjee. “Stable Strategies of Direct and Indirect Reciprocity across All Social Dilemmas.” <i>PNAS Nexus</i>. Oxford University Press, 2025. <a href=\"https://doi.org/10.1093/pnasnexus/pgaf154\">https://doi.org/10.1093/pnasnexus/pgaf154</a>.","ieee":"V. Hübner, L. Schmid, C. Hilbe, and K. Chatterjee, “Stable strategies of direct and indirect reciprocity across all social dilemmas,” <i>PNAS Nexus</i>, vol. 4, no. 5. Oxford University Press, 2025.","mla":"Hübner, Valentin, et al. “Stable Strategies of Direct and Indirect Reciprocity across All Social Dilemmas.” <i>PNAS Nexus</i>, vol. 4, no. 5, pgaf154, Oxford University Press, 2025, doi:<a href=\"https://doi.org/10.1093/pnasnexus/pgaf154\">10.1093/pnasnexus/pgaf154</a>."},"has_accepted_license":"1","date_created":"2025-06-15T22:01:30Z","title":"Stable strategies of direct and indirect reciprocity across all social dilemmas","department":[{"_id":"KrCh"}],"quality_controlled":"1","oa_version":"Published Version","corr_author":"1","abstract":[{"lang":"eng","text":"Social dilemmas are collective-action problems where individual interests are at odds with group interests. Such dilemmas occur frequently at all scales of human interactions. When dealing with collective-action problems, people often act reciprocally. They adjust their behavior to match the previous behavior of the recipient. The literature distinguishes two kinds of reciprocity. According to direct reciprocity, individuals react to their immediate experiences with the recipient. They are more likely to cooperate if the recipient previously cooperated with them. According to indirect reciprocity, individuals react to the recipient’s general behavior, irrespectively of whether or not they benefited directly. In practice, the two kinds of reciprocity are often intertwined; people typically base their decisions on both direct experiences and indirect observations. Yet only recently have researchers begun to explore how the two kinds of reciprocity interact. So far, this research only addresses a single type of social dilemma, the donation game, where the effects of individual behaviors are independent. Instead, here we allow for all pairwise social dilemmas. By applying novel techniques to generalize the theory of zero-determinant strategies, we establish an important proof of principle: In all social dilemmas, socially optimal outcomes can be sustained as an equilibrium, using either direct or indirect reciprocity, or arbitrary mixtures thereof. These results neither require games to be repeated infinitely often, nor that individual opinions are synchronized. In this way, we considerably generalize the scope of models of reciprocity, and we build further bridges between the literatures on direct and indirect reciprocity."}],"status":"public","issue":"5","publication":"PNAS Nexus","file":[{"success":1,"date_created":"2025-06-23T08:09:50Z","checksum":"efd6648db3fc3ea0cdd7155d667e5f11","relation":"main_file","file_size":2551195,"creator":"dernst","access_level":"open_access","file_id":"19867","date_updated":"2025-06-23T08:09:50Z","file_name":"2025_PNASNexus_Huebner.pdf","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"date_published":"2025-05-01T00:00:00Z","OA_type":"gold","file_date_updated":"2025-06-23T08:09:50Z","doi":"10.1093/pnasnexus/pgaf154","article_processing_charge":"Yes","volume":4,"date_updated":"2026-04-07T12:30:56Z","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"day":"01","author":[{"first_name":"Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","orcid":"0009-0001-5009-4987","last_name":"Hübner","full_name":"Hübner, Valentin"},{"full_name":"Schmid, Laura","last_name":"Schmid","orcid":"0000-0002-6978-7329","first_name":"Laura","id":"38B437DE-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0001-5116-955X","first_name":"Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian","last_name":"Hilbe"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"}],"publisher":"Oxford University Press","type":"journal_article"},{"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"title":"Reciprocity and inequality in social dilemmas","date_created":"2025-06-25T13:50:10Z","has_accepted_license":"1","citation":{"ista":"Hübner V. 2025. Reciprocity and inequality in social dilemmas. Institute of Science and Technology Austria.","short":"V. Hübner, Reciprocity and Inequality in Social Dilemmas, Institute of Science and Technology Austria, 2025.","apa":"Hübner, V. (2025). <i>Reciprocity and inequality in social dilemmas</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-19903\">https://doi.org/10.15479/AT-ISTA-19903</a>","ama":"Hübner V. Reciprocity and inequality in social dilemmas. 2025. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-19903\">10.15479/AT-ISTA-19903</a>","chicago":"Hübner, Valentin. “Reciprocity and Inequality in Social Dilemmas.” Institute of Science and Technology Austria, 2025. <a href=\"https://doi.org/10.15479/AT-ISTA-19903\">https://doi.org/10.15479/AT-ISTA-19903</a>.","ieee":"V. Hübner, “Reciprocity and inequality in social dilemmas,” Institute of Science and Technology Austria, 2025.","mla":"Hübner, Valentin. <i>Reciprocity and Inequality in Social Dilemmas</i>. Institute of Science and Technology Austria, 2025, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-19903\">10.15479/AT-ISTA-19903</a>."},"tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","short":"CC BY-NC (4.0)","image":"/images/cc_by_nc.png"},"ec_funded":1,"OA_place":"publisher","publication_identifier":{"issn":["2663-337X"]},"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","_id":"19903","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"19843"},{"status":"public","relation":"part_of_dissertation","id":"15083"},{"id":"19074","relation":"part_of_dissertation","status":"public"}]},"year":"2025","oa":1,"alternative_title":["ISTA Thesis"],"acknowledgement":"The research for this thesis was supported by the European Research Council\r\n(grant agreements No. 863818 and No. 850529), the European Union’s Horizon 2020 research and innovation programme (Marie Skłodowska-Curie grant agreement No. 754411),\r\nthe Austrian Science Fund (grant DOI 10.55776/COE12), the French Agence Nationale\r\nde la Recherche under the Programme d’investissements d’avenir (project reference 17-\r\nEURE-0010) and the Australian Government through the Australian Research Council\r\n(grant No. SR200100005, “Securing Antarctica’s Environmental Future”).","publication_status":"published","ddc":["519"],"month":"06","degree_awarded":"PhD","type":"dissertation","author":[{"orcid":"0009-0001-5009-4987","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","first_name":"Valentin","last_name":"Hübner","full_name":"Hübner, Valentin"}],"publisher":"Institute of Science and Technology Austria","supervisor":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"}],"day":"25","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}],"date_updated":"2026-04-07T12:30:57Z","doi":"10.15479/AT-ISTA-19903","article_processing_charge":"No","page":"157","file_date_updated":"2025-07-09T13:37:00Z","language":[{"iso":"eng"}],"date_published":"2025-06-25T00:00:00Z","file":[{"file_size":6192760,"creator":"vhuebner","access_level":"closed","file_id":"19905","file_name":"Thesis Valentin Hübner source.tar.xz","date_updated":"2025-06-25T13:38:07Z","content_type":"application/x-xz","date_created":"2025-06-25T13:38:07Z","checksum":"794c02f8c82ca59ba6dda3bd7eed871a","relation":"source_file"},{"content_type":"application/pdf","access_level":"open_access","file_id":"19976","file_name":"Thesis Valentin Hübner.pdf","date_updated":"2025-07-09T13:37:00Z","creator":"vhuebner","file_size":4837864,"checksum":"ac56063d81c81e40322b6ff5a8c4912e","date_created":"2025-07-09T13:37:00Z","relation":"main_file"}],"status":"public","corr_author":"1","abstract":[{"lang":"eng","text":"Cooperation, that is, one person paying a cost for another's benefit, is a fundamental principle without which no form of society could exist. The extent to which humans cooperate with each other is also an essential feature that differentiates them from other animals. Cooperation occurs even in the absence of altruistic motivations, when it is selfishly incentivised by the expectation of a future reward. For example, many economic interactions are well described that way. This kind of cooperation requires that people exhibit reciprocal behaviour that acts as a mechanism that rewards cooperation.\r\nWith game-theoretic models, it is possible to formally study potential such mechanisms and under what conditions they can exist. This thesis contributes to this effort by analysing recently introduced models of cooperation that advance on previous work by taking into account the potential for pre-existing inequality among cooperating individuals as well as the different forms that reciprocity can take.\r\nIndividuals may differ both intrinsically, in their abilities, as well as extrinsically, in the amount of resources they have available. Allowing for such differences in a model of cooperation helps to understand how inequality affects the potential for, and outcomes of, cooperation among unequals. In this thesis, it is shown that in the presence of intrinsic inequality, a similar unequal distribution of resources can increase the potential for cooperation. This effect is stronger the smaller the group is in which cooperation takes place. It is also shown that under particular assumptions, if the unequal members of a group vary the size of their contributions to a cooperative effort over time, they can thereby increase their efficiency and improve the collective outcome.\r\nCooperative behaviour in a two-person interaction can be rewarded either by direct reciprocation whenever the same two people interact again, or indirectly by a third party who observed the interaction. In the latter case of indirect reciprocity, individuals are proximally rewarded by a good reputation, which ultimately translates to being rewarded with cooperative behaviour by others. This mechanism can enable selfishly motivated cooperation even in circumstances where individuals are unlikely to meet again, akin to how money facilitates trade. While these two forms of reciprocity have mostly been studied in isolation, this thesis analyses both direct and indirect reciprocity in a general model in order to compare their relative effectiveness under different circumstances. The contribution of this thesis is an extension of previous work regarding a specific kind of interaction, whose parameters allow for convenient mathematical analysis, to the most general set of possible interactions."}],"oa_version":"Published Version"},{"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."}],"status":"public","issue":"25","file":[{"success":1,"relation":"main_file","date_created":"2025-07-08T05:52:26Z","checksum":"3b35befd959a3e37aa9080a64a6afaf3","creator":"dernst","file_size":29525932,"file_name":"2025_PNAS_McAvoy.pdf","file_id":"19972","date_updated":"2025-07-08T05:52:26Z","access_level":"open_access","content_type":"application/pdf"}],"publication":"Proceedings of the National Academy of Sciences","oa_version":"Published Version","article_processing_charge":"Yes (in subscription journal)","doi":"10.1073/pnas.2319927121","volume":122,"language":[{"iso":"eng"}],"OA_type":"hybrid","date_published":"2025-06-24T00:00:00Z","file_date_updated":"2025-07-08T05:52:26Z","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"isi":1,"day":"24","date_updated":"2025-09-30T13:47:14Z","type":"journal_article","publisher":"National Academy of Sciences","author":[{"full_name":"Mcavoy, Alex","last_name":"Mcavoy","first_name":"Alex"},{"first_name":"Udari Madhushani","last_name":"Sehwag","full_name":"Sehwag, Udari Madhushani"},{"orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Hilbe","full_name":"Hilbe, Christian"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"last_name":"Barfuss","full_name":"Barfuss, Wolfram","first_name":"Wolfram"},{"first_name":"Qi","last_name":"Su","full_name":"Su, Qi"},{"last_name":"Leonard","full_name":"Leonard, Naomi Ehrich","first_name":"Naomi Ehrich"},{"first_name":"Joshua B.","full_name":"Plotkin, Joshua B.","last_name":"Plotkin"}],"publication_status":"published","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.).","ddc":["000"],"license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","article_type":"original","scopus_import":"1","oa":1,"month":"06","intvolume":"       122","external_id":{"isi":["001522351900001"],"pmid":["40523172"]},"year":"2025","OA_place":"publisher","publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"article_number":"e2319927121","ec_funded":1,"_id":"19965","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2025-07-06T22:01:23Z","title":"Unilateral incentive alignment in two-agent stochastic games","department":[{"_id":"KrCh"}],"quality_controlled":"1","tmp":{"image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"citation":{"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>.","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>.","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.","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>","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>","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.","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)."},"pmid":1,"has_accepted_license":"1"},{"type":"conference","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Gilbert","full_name":"Gilbert, Seth","first_name":"Seth"},{"first_name":"Stefan","last_name":"Schmid","full_name":"Schmid, Stefan"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","orcid":"0000-0002-1419-3267","last_name":"Svoboda","full_name":"Svoboda, Jakub"},{"first_name":"Michelle X","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","orcid":"0009-0001-3676-4809","full_name":"Yeo, Michelle X","last_name":"Yeo"}],"publisher":"Association for Computing Machinery","isi":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"day":"13","date_updated":"2026-02-16T11:46:51Z","article_processing_charge":"No","doi":"10.1145/3732772.3733544","page":"241-251","file_date_updated":"2025-08-05T07:15:31Z","language":[{"iso":"eng"}],"OA_type":"hybrid","date_published":"2025-06-13T00:00:00Z","status":"public","corr_author":"1","abstract":[{"lang":"eng","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."}],"file":[{"relation":"main_file","date_created":"2025-08-05T07:15:31Z","checksum":"cd628fe54d96e9fc6cc789bb8145422b","success":1,"content_type":"application/pdf","file_size":783297,"creator":"dernst","file_id":"20122","date_updated":"2025-08-05T07:15:31Z","file_name":"2025_PODC_Chatterjee.pdf","access_level":"open_access"}],"publication":"Proceedings of the ACM Symposium on Principles of Distributed Computing","conference":{"name":"PODC: Symposium on Principles of Distributed Computing","location":"Huatulco, Mexico","start_date":"2025-06-16","end_date":"2025-06-20"},"oa_version":"Published Version","date_created":"2025-07-21T08:18:26Z","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2025/745"}],"quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"KrPi"}],"title":"When is liquid democracy possible?: On the manipulation of variance","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"has_accepted_license":"1","citation":{"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.","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.","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>","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>","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.","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>.","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>."},"OA_place":"publisher","publication_identifier":{"isbn":["9798400718854"]},"ec_funded":1,"_id":"20053","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","external_id":{"isi":["001525534800030"]},"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.","ddc":["000"],"publication_status":"published","oa":1,"month":"06"},{"ec_funded":1,"article_number":"pgaf252","publication_identifier":{"eissn":["2752-6542"]},"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"20254","title":"Maintaining diversity in structured populations","department":[{"_id":"KrCh"}],"quality_controlled":"1","date_created":"2025-08-31T22:01:32Z","citation":{"ista":"Brewster DA, Svoboda J, Roscow D, Chatterjee K, Tkadlec J, Nowak MA. 2025. Maintaining diversity in structured populations. PNAS Nexus. 4(8), pgaf252.","short":"D.A. Brewster, J. Svoboda, D. Roscow, K. Chatterjee, J. Tkadlec, M.A. Nowak, PNAS Nexus 4 (2025).","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>","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>","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>.","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>."},"has_accepted_license":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"PlanS_conform":"1","article_type":"original","oa":1,"scopus_import":"1","ddc":["000"],"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.","publication_status":"published","DOAJ_listed":"1","month":"08","intvolume":"         4","external_id":{"arxiv":["2503.09841"]},"arxiv":1,"year":"2025","day":"01","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"APC_amount":"4493,27 EUR","date_updated":"2026-06-11T09:11:17Z","type":"journal_article","publisher":"Oxford University Press","author":[{"first_name":"David A.","full_name":"Brewster, David A.","last_name":"Brewster"},{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","full_name":"Svoboda, Jakub"},{"first_name":"Dylan","full_name":"Roscow, Dylan","last_name":"Roscow"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","last_name":"Tkadlec"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"issue":"8","publication":"PNAS Nexus","file":[{"success":1,"checksum":"8a5e82c6f842e3220ec96028c9374b69","date_created":"2025-09-03T06:20:08Z","relation":"main_file","access_level":"open_access","file_name":"2025_PNASNexus_Brewster.pdf","file_id":"20280","date_updated":"2025-09-03T06:20:08Z","file_size":1086419,"creator":"dernst","content_type":"application/pdf"}],"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."}],"status":"public","oa_version":"Published Version","volume":4,"doi":"10.1093/pnasnexus/pgaf252","article_processing_charge":"Yes","OA_type":"gold","date_published":"2025-08-01T00:00:00Z","language":[{"iso":"eng"}],"file_date_updated":"2025-09-03T06:20:08Z"},{"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"day":"01","date_updated":"2025-09-09T08:21:45Z","type":"conference","author":[{"last_name":"Asadi","full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","first_name":"Ali"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0001-5103-038X","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","first_name":"Raimundo J","full_name":"Saona Urmeneta, Raimundo J","last_name":"Saona Urmeneta"},{"id":"2783031a-7378-11f0-b2d0-f17f1db2ebad","first_name":"Ali","full_name":"Shafiee, Ali","last_name":"Shafiee"}],"publisher":"ML Research Press","status":"public","abstract":[{"lang":"eng","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."}],"corr_author":"1","file":[{"content_type":"application/pdf","creator":"dernst","file_size":307458,"access_level":"open_access","date_updated":"2025-09-09T08:19:41Z","file_id":"20315","file_name":"2025_UAI_AsadiAli.pdf","date_created":"2025-09-09T08:19:41Z","checksum":"1a37ebe7ba73ab6985765bf0d17a0acc","relation":"main_file","success":1}],"publication":"The 41st Conference on Uncertainty in Artificial Intelligence","conference":{"end_date":"2025-07-25","name":"UAI: Conference on Uncertainty in Artificial Intelligence","start_date":"2025-07-21","location":"Rio de Janeiro, Brazil"},"oa_version":"Published Version","article_processing_charge":"No","page":"238-247","volume":286,"file_date_updated":"2025-09-09T08:19:41Z","language":[{"iso":"eng"}],"OA_type":"diamond","date_published":"2025-07-01T00:00:00Z","OA_place":"publisher","publication_identifier":{"eissn":["2640-3498"]},"ec_funded":1,"_id":"20297","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2025-09-07T22:01:34Z","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"quality_controlled":"1","title":"Limit-sure reachability for small memory policies in POMDPs is NP-complete","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"has_accepted_license":"1","citation":{"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.","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.","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.","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.","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.","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."},"publication_status":"published","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.","ddc":["000"],"oa":1,"scopus_import":"1","alternative_title":["PMLR"],"month":"07","intvolume":"       286","year":"2025","arxiv":1,"external_id":{"arxiv":["2412.00941"]}},{"publication_identifier":{"eissn":["2640-3498"]},"OA_place":"publisher","ec_funded":1,"_id":"20299","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2025-09-07T22:01:34Z","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"title":"Lower bound on Howard policy iteration for deterministic Markov Decision Processes","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"has_accepted_license":"1","citation":{"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.","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.","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.","short":"A. Asadi, K. Chatterjee, J. De Raaij, in:, The 41st Conference on Uncertainty in Artificial Intelligence, ML Research Press, 2025, pp. 223–232.","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.","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.","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."},"ddc":["000"],"publication_status":"published","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and Austrian Science Fund (FWF) 10.55776/COE12.\r\n","oa":1,"scopus_import":"1","alternative_title":["PMLR"],"month":"01","intvolume":"       286","year":"2025","arxiv":1,"external_id":{"arxiv":["2506.12254"]},"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"day":"01","date_updated":"2025-09-09T06:31:20Z","type":"conference","publisher":"ML Research Press","author":[{"id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","first_name":"Ali","full_name":"Asadi, Ali","last_name":"Asadi"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Jakob","full_name":"De Raaij, Jakob","last_name":"De Raaij"}],"status":"public","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"}],"corr_author":"1","file":[{"success":1,"relation":"main_file","date_created":"2025-09-09T06:27:59Z","checksum":"4180c81bb6ed3b4f5c7a8e48d06520c6","creator":"dernst","file_size":317097,"file_id":"20313","file_name":"2025_UAI_Asadi.pdf","date_updated":"2025-09-09T06:27:59Z","access_level":"open_access","content_type":"application/pdf"}],"publication":"The 41st Conference on Uncertainty in Artificial Intelligence","conference":{"end_date":"2025-07-25","start_date":"2025-07-21","location":"Rio de Janeiro, Brazil","name":"UAI: Conference on Uncertainty in Artificial Intelligence"},"oa_version":"Published Version","article_processing_charge":"No","page":"223-232","volume":286,"file_date_updated":"2025-09-09T06:27:59Z","OA_type":"diamond","date_published":"2025-01-01T00:00:00Z","language":[{"iso":"eng"}]},{"day":"01","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"date_updated":"2025-09-09T07:17:08Z","type":"conference","author":[{"id":"b391db08-1ffe-11ee-8b67-d18ddcfb5a14","first_name":"Ruichen","full_name":"Luo, Ruichen","last_name":"Luo"},{"first_name":"Sebastian U.","last_name":"Stich","full_name":"Stich, Sebastian U."},{"full_name":"Horváth, Samuel","last_name":"Horváth","first_name":"Samuel"},{"last_name":"Takáč","full_name":"Takáč, Martin","first_name":"Martin"}],"publisher":"ML Research Press","publication":"The 28th International Conference on Artificial Intelligence and Statistics","abstract":[{"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.","lang":"eng"}],"status":"public","oa_version":"Preprint","conference":{"start_date":"2025-05-03","location":"Mai Khao, Thailand","name":"AISTATS: Conference on Artificial Intelligence and Statistics","end_date":"2025-05-05"},"volume":258,"page":"2539-2547","article_processing_charge":"No","date_published":"2025-05-01T00:00:00Z","OA_type":"green","language":[{"iso":"eng"}],"ec_funded":1,"publication_identifier":{"eissn":["2640-3498"]},"OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"20302","title":"Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis","quality_controlled":"1","department":[{"_id":"KrCh"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2501.04443","open_access":"1"}],"date_created":"2025-09-07T22:01:35Z","citation":{"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.","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.","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.","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.","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.","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."},"alternative_title":["PMLR"],"oa":1,"scopus_import":"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.","publication_status":"published","month":"05","intvolume":"       258","external_id":{"arxiv":["2501.04443"]},"arxiv":1,"year":"2025"},{"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).","publication_status":"published","scopus_import":"1","alternative_title":["LNCS"],"month":"10","intvolume":"     16143","year":"2025","publication_identifier":{"isbn":["9783032057914"],"eissn":["1611-3349"],"issn":["0302-9743"]},"ec_funded":1,"_id":"20610","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2025-11-09T23:01:34Z","quality_controlled":"1","department":[{"_id":"KrCh"}],"title":"What are the odds? Improving statistical model checking of Markov decision processes","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>.","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>.","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>","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>","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.","short":"T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Second International Joint Conference on QEST+FORMATS, Springer Nature, 2025, pp. 195–218."},"status":"public","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"}],"publication":"Second International Joint Conference on QEST+FORMATS","conference":{"start_date":"2025-08-26","location":"Aarhus, Denmark","name":"QEST-FORMATS: International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","end_date":"2025-08-28"},"oa_version":"None","doi":"10.1007/978-3-032-05792-1_11","article_processing_charge":"No","page":"195-218","volume":16143,"date_published":"2025-10-02T00:00:00Z","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"day":"02","date_updated":"2025-11-10T08:06:27Z","type":"conference","author":[{"orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","orcid":"0000-0002-0163-2152","last_name":"Weininger","full_name":"Weininger, Maximilian"},{"first_name":"Patrick","full_name":"Wienhöft, Patrick","last_name":"Wienhöft"}],"publisher":"Springer Nature"},{"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783032087065"],"issn":["0302-9743"]},"OA_place":"repository","ec_funded":1,"_id":"20648","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2025-11-16T23:01:24Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2408.03796","open_access":"1"}],"title":"PolyQEnt: A polynomial quantified entailment solver","quality_controlled":"1","department":[{"_id":"KrCh"}],"citation":{"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.","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>.","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>.","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.","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.","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>","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>"},"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).","publication_status":"published","alternative_title":["LNCS"],"scopus_import":"1","oa":1,"month":"10","intvolume":"     16145","external_id":{"arxiv":["2408.03796"]},"arxiv":1,"year":"2025","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"day":"26","date_updated":"2025-11-24T13:11:10Z","type":"conference","publisher":"Springer Nature","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584"},{"last_name":"Kafshdar Goharshadi","full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan"},{"last_name":"Karrabi","full_name":"Karrabi, Mehrdad","orcid":"0009-0007-5253-9170","first_name":"Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"first_name":"Milad","full_name":"Saadat, Milad","last_name":"Saadat"},{"first_name":"Maximilian","full_name":"Seeliger, Maximilian","last_name":"Seeliger"},{"last_name":"Zikelic","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699"}],"corr_author":"1","abstract":[{"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.","lang":"eng"}],"status":"public","publication":"23rd International Symposium on Automated Technology for Verification and Analysis","conference":{"location":"Bengaluru, India","start_date":"2025-10-27","name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2025-10-31"},"oa_version":"Preprint","page":"411-424","article_processing_charge":"No","doi":"10.1007/978-3-032-08707-2_19","volume":16145,"OA_type":"green","language":[{"iso":"eng"}],"date_published":"2025-10-26T00:00:00Z"},{"department":[{"_id":"KrCh"}],"quality_controlled":"1","title":"Stopping criteria for value iteration on concurrent stochastic reachability and safety games","date_created":"2025-11-24T14:23:49Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2505.21087","open_access":"1"}],"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.","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>.","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>.","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.","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>","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>"},"ec_funded":1,"OA_place":"repository","publication_identifier":{"eisbn":["9798331579005"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"20688","year":"2025","external_id":{"arxiv":["2505.21087"]},"arxiv":1,"scopus_import":"1","oa":1,"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).","publication_status":"published","month":"10","type":"conference","author":[{"full_name":"Grobelna, Marta","last_name":"Grobelna","first_name":"Marta"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan"},{"first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","orcid":"0000-0002-0163-2152","full_name":"Weininger, Maximilian","last_name":"Weininger"}],"publisher":"IEEE","day":"09","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"date_updated":"2025-11-26T07:34:19Z","article_processing_charge":"No","doi":"10.1109/lics65433.2025.00049","page":"568-580","language":[{"iso":"eng"}],"OA_type":"green","date_published":"2025-10-09T00:00:00Z","publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","status":"public","corr_author":"1","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"}],"oa_version":"Preprint","conference":{"location":"Singapore, Singapore","start_date":"2025-06-23","name":"LICS: Logic in Computer Science","end_date":"2025-06-26"}}]