[{"file_date_updated":"2026-03-09T12:33:58Z","OA_place":"publisher","alternative_title":["LIPIcs"],"date_updated":"2026-03-09T12:36:11Z","oa_version":"Published Version","volume":361,"publication":"29th International Conference on Principles of Distributed Systems","ddc":["000"],"article_processing_charge":"No","author":[{"full_name":"Bentert, Matthias","last_name":"Bentert","first_name":"Matthias"},{"first_name":"Esra","last_name":"Ceylan","full_name":"Ceylan, Esra"},{"first_name":"Valentin","last_name":"Hübner","full_name":"Hübner, Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","orcid":"0009-0001-5009-4987"},{"full_name":"Schmid, Stefan","first_name":"Stefan","last_name":"Schmid"},{"full_name":"Srba, Jiří","last_name":"Srba","first_name":"Jiří"}],"title":"Fast re-routing in networks: On the complexity of perfect resilience","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2025-12-03","name":"OPODIS: Conference on Principles of Distributed Systems","location":"Iaşi, Romania","end_date":"2025-12-05"},"citation":{"apa":"Bentert, M., Ceylan, E., Hübner, V., Schmid, S., &#38; Srba, J. (2026). Fast re-routing in networks: On the complexity of perfect resilience. In <i>29th International Conference on Principles of Distributed Systems</i> (Vol. 361). Iaşi, Romania: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31\">https://doi.org/10.4230/LIPIcs.OPODIS.2025.31</a>","ama":"Bentert M, Ceylan E, Hübner V, Schmid S, Srba J. Fast re-routing in networks: On the complexity of perfect resilience. In: <i>29th International Conference on Principles of Distributed Systems</i>. Vol 361. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31\">10.4230/LIPIcs.OPODIS.2025.31</a>","ista":"Bentert M, Ceylan E, Hübner V, Schmid S, Srba J. 2026. Fast re-routing in networks: On the complexity of perfect resilience. 29th International Conference on Principles of Distributed Systems. OPODIS: Conference on Principles of Distributed Systems, LIPIcs, vol. 361, 31.","short":"M. Bentert, E. Ceylan, V. Hübner, S. Schmid, J. Srba, in:, 29th International Conference on Principles of Distributed Systems, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","chicago":"Bentert, Matthias, Esra Ceylan, Valentin Hübner, Stefan Schmid, and Jiří Srba. “Fast Re-Routing in Networks: On the Complexity of Perfect Resilience.” In <i>29th International Conference on Principles of Distributed Systems</i>, Vol. 361. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31\">https://doi.org/10.4230/LIPIcs.OPODIS.2025.31</a>.","mla":"Bentert, Matthias, et al. “Fast Re-Routing in Networks: On the Complexity of Perfect Resilience.” <i>29th International Conference on Principles of Distributed Systems</i>, vol. 361, 31, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31\">10.4230/LIPIcs.OPODIS.2025.31</a>.","ieee":"M. Bentert, E. Ceylan, V. Hübner, S. Schmid, and J. Srba, “Fast re-routing in networks: On the complexity of perfect resilience,” in <i>29th International Conference on Principles of Distributed Systems</i>, Iaşi, Romania, 2026, vol. 361."},"day":"07","intvolume":"       361","oa":1,"quality_controlled":"1","doi":"10.4230/LIPIcs.OPODIS.2025.31","license":"https://creativecommons.org/licenses/by/4.0/","_id":"21411","month":"01","publication_status":"published","has_accepted_license":"1","file":[{"date_created":"2026-03-09T12:33:58Z","success":1,"creator":"dernst","file_id":"21419","access_level":"open_access","file_name":"2026_OPODIS_Bentert.pdf","relation":"main_file","checksum":"a7af114da7c38d2338b4edb922eb27f1","file_size":1041334,"content_type":"application/pdf","date_updated":"2026-03-09T12:33:58Z"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","abstract":[{"text":"To achieve fast recovery from link failures, most modern communication networks feature fully\r\ndecentralized fast re-routing mechanisms. These re-routing mechanisms rely on pre-installed static re-routing rules at the nodes (the routers), which depend only on local failure information, namely on the failed links incident to the node. Ideally, a network is perfectly resilient: the re-routing rules ensure that packets are always successfully routed to their destinations as long as the source and the destination are still physically connected in the underlying network after the failures. Unfortunately, there are examples where achieving perfect resilience is not possible. Surprisingly, only very little is known about the algorithmic aspect of when and how perfect resilience can be achieved. We investigate the computational complexity of analyzing such local fast re-routing mechanisms. Our main result is a negative one: we show that even checking whether a given set of static re-routing rules ensures perfect resilience is coNP-complete. Additionally, we investigate other fundamental variations of the problem. In particular, we show that our coNP-completeness proof also applies to scenarios where the re-routing rules have specific patterns (known as skipping in the literature). On the positive side, for scenarios where nodes do not have information about the link from which a packet arrived (the so-called in-port), we present a linear-time algorithm to realize perfect resilience whenever possible (which we show can also be determined in linear time). ","lang":"eng"}],"date_created":"2026-03-08T23:01:46Z","OA_type":"gold","year":"2026","publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959774093"]},"date_published":"2026-01-07T00:00:00Z","article_number":"31","acknowledgement":"Matthias Bentert: ERC Horizon 2020 research and innovation programme (grant agreement\r\nNo. 819416) and ERC Consolidator grant AdjustNet (agreement No. 864228).\r\nEsra Ceylan: German Research Foundation (DFG) project ReNO, Schwerpunktprogramm:\r\nResilienz in Vernetzten Welten – Beherrschen von Fehlern, Überlast, Angriffen und dem\r\nUnbekannten (SPP 2378).\r\nStefan Schmid: German Research Foundation (DFG) project ReNO, Schwerpunktprogramm:\r\nResilienz in Vernetzten Welten – Beherrschen von Fehlern, Überlast, Angriffen und dem\r\nUnbekannten (SPP 2378).","scopus_import":"1","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"status":"public","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"fulldoi":"https://doi.org/10.4230/LIPIcs.OPODIS.2025.31"},{"publication_identifier":{"issn":["1433-2779"],"eissn":["1433-2787"]},"year":"2026","OA_type":"hybrid","date_created":"2026-04-05T22:01:32Z","abstract":[{"text":"Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) are key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear programme, solvable in polynomial time. In this paper, we give a detailed overview of today’s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners—tool builders and users alike.","lang":"eng"}],"publisher":"Springer Nature","has_accepted_license":"1","publication_status":"epub_ahead","month":"03","_id":"21661","fulldoi":"https://doi.org/10.1007/s10009-026-00848-y","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"status":"public","language":[{"iso":"eng"}],"scopus_import":"1","department":[{"_id":"KrCh"}],"acknowledgement":"This research was funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie grant agreements 101008233 (MISSION)\r\nand 101034413 (IST-BRIDGE), by the Interreg North Sea project STORM_SAFE, by a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, by NWO VENI grant no. 639.021.754, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632.","date_published":"2026-03-09T00:00:00Z","type":"journal_article","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Hartmanns, Arnd","last_name":"Hartmanns","first_name":"Arnd"},{"last_name":"Junges","first_name":"Sebastian","full_name":"Junges, Sebastian"},{"full_name":"Quatmann, Tim","last_name":"Quatmann","first_name":"Tim"},{"full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger","first_name":"Maximilian","orcid":"0000-0002-0163-2152"}],"title":"The revised practitioner’s guide to MDP model checking algorithms","article_processing_charge":"Yes (in subscription journal)","ddc":["000"],"publication":"International Journal on Software Tools for Technology Transfer","oa_version":"Published Version","date_updated":"2026-04-07T09:52:54Z","OA_place":"publisher","related_material":{"record":[{"status":"public","relation":"software","id":"21668"}]},"main_file_link":[{"url":"https://doi.org/10.1007/s10009-026-00848-y","open_access":"1"}],"project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"doi":"10.1007/s10009-026-00848-y","keyword":["Quantitative model checking","Markov decision process","Linear programming","Value iteration","Policy iteration"],"quality_controlled":"1","oa":1,"article_type":"original","day":"09","citation":{"ieee":"A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “The revised practitioner’s guide to MDP model checking algorithms,” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2026.","short":"A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, International Journal on Software Tools for Technology Transfer (2026).","chicago":"Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/s10009-026-00848-y\">https://doi.org/10.1007/s10009-026-00848-y</a>.","mla":"Hartmanns, Arnd, et al. “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” <i>International Journal on Software Tools for Technology Transfer</i>, Springer Nature, 2026, doi:<a href=\"https://doi.org/10.1007/s10009-026-00848-y\">10.1007/s10009-026-00848-y</a>.","ista":"Hartmanns A, Junges S, Quatmann T, Weininger M. 2026. The revised practitioner’s guide to MDP model checking algorithms. International Journal on Software Tools for Technology Transfer.","apa":"Hartmanns, A., Junges, S., Quatmann, T., &#38; Weininger, M. (2026). The revised practitioner’s guide to MDP model checking algorithms. <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-026-00848-y\">https://doi.org/10.1007/s10009-026-00848-y</a>","ama":"Hartmanns A, Junges S, Quatmann T, Weininger M. The revised practitioner’s guide to MDP model checking algorithms. <i>International Journal on Software Tools for Technology Transfer</i>. 2026. doi:<a href=\"https://doi.org/10.1007/s10009-026-00848-y\">10.1007/s10009-026-00848-y</a>"}},{"volume":40,"publication":"Proceedings of the 40th AAAI Conference on Artificial Intelligence","article_processing_charge":"No","title":"Qualitative analysis of ω-regular objectives on robust MDPs","author":[{"last_name":"Asadi","first_name":"Ali","full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","last_name":"Kafshdar Goharshadi"},{"orcid":"0009-0007-5253-9170","first_name":"Mehrdad","last_name":"Karrabi","full_name":"Karrabi, Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"full_name":"Shafiee, Ali","id":"2783031a-7378-11f0-b2d0-f17f1db2ebad","last_name":"Shafiee","first_name":"Ali"}],"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2026-01-20","end_date":"2026-01-27","location":"Singapore, Singapore"},"OA_place":"repository","oa_version":"Preprint","date_updated":"2026-09-16T07:27:43Z","intvolume":"        40","oa":1,"quality_controlled":"1","doi":"10.1609/aaai.v40i43.40931","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.04539"}],"citation":{"ieee":"A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, and A. Shafiee, “Qualitative analysis of ω-regular objectives on robust MDPs,” in <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36137–36145.","mla":"Asadi, Ali, et al. “Qualitative Analysis of ω-Regular Objectives on Robust MDPs.” <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–45, doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">10.1609/aaai.v40i43.40931</a>.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Ehsan Goharshady, Mehrdad Karrabi, and Ali Shafiee. “Qualitative Analysis of ω-Regular Objectives on Robust MDPs.” In <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, 40:36137–45. Association for the Advancement of Artificial Intelligence, 2026. <a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">https://doi.org/10.1609/aaai.v40i43.40931</a>.","short":"A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, A. Shafiee, in:, Proceedings of the 40th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–36145.","ista":"Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. 2026. Qualitative analysis of ω-regular objectives on robust MDPs. Proceedings of the 40th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 40, 36137–36145.","ama":"Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. Qualitative analysis of ω-regular objectives on robust MDPs. In: <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>. Vol 40. Association for the Advancement of Artificial Intelligence; 2026:36137-36145. doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">10.1609/aaai.v40i43.40931</a>","apa":"Asadi, A., Chatterjee, K., Goharshady, E., Karrabi, M., &#38; Shafiee, A. (2026). Qualitative analysis of ω-regular objectives on robust MDPs. In <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i> (Vol. 40, pp. 36137–36145). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">https://doi.org/10.1609/aaai.v40i43.40931</a>"},"day":"14","page":"36137-36145","abstract":[{"lang":"eng","text":"Robust Markov Decision Processes (RMDPs) generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for ω-regular objectives. The qualitative analysis problem asks whether the objective can be ensured with probability 1. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. Our contributions are twofold. We first present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives. We then report experimental results demonstrating the effectiveness of our oracle-based approach on classical RMDP examples from the literature scaling up to thousands of states."}],"date_created":"2026-04-12T22:01:50Z","OA_type":"green","year":"2026","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"month":"03","_id":"21717","publication_status":"published","publisher":"Association for the Advancement of Artificial Intelligence","external_id":{"arxiv":["2505.04539"]},"ec_funded":1,"issue":"43","fulldoi":"https://doi.org/10.1609/aaai.v40i43.40931","arxiv":1,"date_published":"2026-03-14T00:00:00Z","acknowledgement":"This work was supported by ERC CoG 863818 (ForMSMArt) and Austrian Science Fund (FWF) 10.55776/COE12. We also thank Hossein Zakerinia for his helpful feedback.","scopus_import":"1","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"language":[{"iso":"eng"}],"status":"public"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2026-01-20","name":"AAAI: Conference on Artificial Intelligence","location":"Singapore, Singapore","end_date":"2026-01-27"},"type":"conference","author":[{"full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","last_name":"Asadi","first_name":"Ali"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"579a6c20-34cf-11f1-acbd-8c2f19cdb4da","full_name":"Lurie, David","first_name":"David","last_name":"Lurie"},{"orcid":"0000-0001-5103-038X","last_name":"Saona Urmeneta","first_name":"Raimundo J","full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"}],"title":"Revealing POMDPs: Qualitative and quantitative analysis for parity objectives","article_processing_charge":"No","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","volume":40,"date_updated":"2026-09-16T07:28:33Z","oa_version":"Preprint","OA_place":"repository","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2511.13134"}],"doi":"10.1609/aaai.v40i43.40932","quality_controlled":"1","oa":1,"intvolume":"        40","page":"36146-36154","day":"14","citation":{"ieee":"A. Asadi, K. Chatterjee, D. Lurie, and R. J. Saona Urmeneta, “Revealing POMDPs: Qualitative and quantitative analysis for parity objectives,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36146–36154.","chicago":"Asadi, Ali, Krishnendu Chatterjee, David Lurie, and Raimundo J Saona Urmeneta. “Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 40:36146–54. Association for the Advancement of Artificial Intelligence, 2026. <a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">https://doi.org/10.1609/aaai.v40i43.40932</a>.","short":"A. Asadi, K. Chatterjee, D. Lurie, R.J. Saona Urmeneta, in:, Proceedings of the AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2026, pp. 36146–36154.","mla":"Asadi, Ali, et al. “Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026, pp. 36146–54, doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">10.1609/aaai.v40i43.40932</a>.","ista":"Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. 2026. Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 40, 36146–36154.","apa":"Asadi, A., Chatterjee, K., Lurie, D., &#38; Saona Urmeneta, R. J. (2026). Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 40, pp. 36146–36154). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">https://doi.org/10.1609/aaai.v40i43.40932</a>","ama":"Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 40. Association for the Advancement of Artificial Intelligence; 2026:36146-36154. doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">10.1609/aaai.v40i43.40932</a>"},"publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"year":"2026","date_created":"2026-04-12T22:01:52Z","OA_type":"green","abstract":[{"text":"Partially observable Markov decision processes (POMDPs) are a central model for uncertainty in sequential decision making. The most basic objective is the reachability objective, where a target set must be eventually visited, and the more general parity objectives can model all omega-regular specifications. For such objectives, the computational analysis problems are the following: (a) qualitative analysis that asks whether the objective can be satisfied with probability 1 (almost-sure winning) or probability arbitrarily close to 1 (limit-sure winning); and (b) quantitative analysis that asks for the approximation of the optimal probability of satisfying the objective. For general POMDPs, almost-sure analysis for reachability objectives is EXPTIME-complete, but limit-sure and quantitative analyses for reachability objectives are undecidable; almost-sure, limit-sure, and quantitative analyses for parity objectives are all undecidable. A special class of POMDPs, called revealing POMDPs, has been studied recently in several works, and for this subclass the almost-sure analysis for parity objectives was shown to be EXPTIME-complete. In this work, we show that for revealing POMDPs the limit-sure analysis for parity objectives is EXPTIME-complete, and even the quantitative analysis for parity objectives can be achieved in EXPTIME.","lang":"eng"}],"external_id":{"arxiv":["2511.13134"]},"publisher":"Association for the Advancement of Artificial Intelligence","publication_status":"published","month":"03","_id":"21722","arxiv":1,"fulldoi":"https://doi.org/10.1609/aaai.v40i43.40932","ec_funded":1,"issue":"43","status":"public","language":[{"iso":"eng"}],"scopus_import":"1","corr_author":"1","department":[{"_id":"KrCh"}],"acknowledgement":"This work was partially supported by the ANRT under the French CIFRE Ph.D program in collaboration between NyxAir and Paris-Dauphine University (Contract: CIFRE N° 2022/0513), by the French Agence Nationale de la Recherche (ANR) under reference ANR-21-CE40-\r\n0020 (CONVERGENCE project), by Austrian Science Fund (FWF) 10.55776/COE12, and by the ERC CoG 863818 (ForM-SMArt) grant.","date_published":"2026-03-14T00:00:00Z"},{"has_accepted_license":"1","publication_status":"published","external_id":{"arxiv":["2603.26215"]},"publisher":"ACM","file":[{"file_name":"2026_ProcACMProgrammingLanguages_Chatterjee.pdf","file_id":"22135","access_level":"open_access","creator":"dernst","date_created":"2026-06-24T06:19:56Z","success":1,"date_updated":"2026-06-24T06:19:56Z","content_type":"application/pdf","checksum":"994bf21d6269dabccf1e1091e02962c5","file_size":858595,"relation":"main_file"}],"month":"06","_id":"22102","publication_identifier":{"eissn":["2475-1421"]},"OA_type":"gold","date_created":"2026-06-21T22:02:59Z","abstract":[{"lang":"eng","text":"Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of є-DP. Our method refutes є-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for є-DP refutation. To the best of our knowledge, our method is the first method for є-DP refutation to offer the following four desirable features: (1) it is fully automated, (2) it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3) it provides soundness guarantees, and (4) it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute є-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods."}],"year":"2026","language":[{"iso":"eng"}],"status":"public","article_number":"218","acknowledgement":"The authors would like to thank Petr Novotný for valuable discussions that helped shape this work.\r\nThis research was supported by the Singapore Ministry of Education (MOE) Academic Research\r\nFund (AcRF) Tier 1 grant (Proposal ID: 25-SIS-SMU-009), Vienna Science and Technology Fund\r\n(WWTF), State of Lower Austria [Grant ID 10.47379/ICT25017], ERC CoG 863818 (ForM-SMArt),\r\nand Austrian Science Fund (FWF) 10.55776/COE12.","date_published":"2026-06-08T00:00:00Z","scopus_import":"1","department":[{"_id":"KrCh"}],"corr_author":"1","supplementarymaterial":"no","arxiv":1,"issue":"PLDI","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"PlanS_conform":"1","fulldoi":"https://doi.org/10.1145/3808296","das_tickbox":"1","date_updated":"2026-09-16T07:36:14Z","oa_version":"Published Version","related_material":{"record":[{"id":"22134","relation":"research_data","status":"public"}]},"researchdata_availability":"yes","OA_place":"publisher","file_date_updated":"2026-06-24T06:19:56Z","article_processing_charge":"Yes","type":"journal_article","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0002-8595-0587","last_name":"Kafshdar Goharshadi","first_name":"Ehsan","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"title":"SuperDP: Differential privacy refutation via supermartingales","publication":"Proceedings of the ACM on Programming Languages","volume":10,"ddc":["000"],"day":"08","article_type":"original","citation":{"ista":"Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 10(PLDI), 218.","apa":"Chatterjee, K., Goharshady, E., &#38; Zikelic, D. (2026). SuperDP: Differential privacy refutation via supermartingales. <i>Proceedings of the ACM on Programming Languages</i>. ACM. <a href=\"https://doi.org/10.1145/3808296\">https://doi.org/10.1145/3808296</a>","ama":"Chatterjee K, Goharshady E, Zikelic D. SuperDP: Differential privacy refutation via supermartingales. <i>Proceedings of the ACM on Programming Languages</i>. 2026;10(PLDI). doi:<a href=\"https://doi.org/10.1145/3808296\">10.1145/3808296</a>","ieee":"K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential privacy refutation via supermartingales,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, no. PLDI. ACM, 2026.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>. ACM, 2026. <a href=\"https://doi.org/10.1145/3808296\">https://doi.org/10.1145/3808296</a>.","short":"K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming Languages 10 (2026).","mla":"Chatterjee, Krishnendu, et al. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, no. PLDI, 218, ACM, 2026, doi:<a href=\"https://doi.org/10.1145/3808296\">10.1145/3808296</a>."},"doi":"10.1145/3808296","keyword":["Static Program Analysis","Differential Privacy","Probabilistic Programming","Martingales"],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"oa":1,"intvolume":"        10","dataavailabilitystatement":"The artifact supporting the findings of this study, which includes the underlying datasets, software\r\ncode, and experiments, is publicly available in Zenodo https://zenodo.org/records/19399862.","quality_controlled":"1"},{"month":"12","_id":"22101","external_id":{"pmid":["41997932"]},"publisher":"Springer Nature","file":[{"access_level":"open_access","file_id":"22136","file_name":"2026_NatureComm_Svoboda.pdf","success":1,"date_created":"2026-06-24T06:50:24Z","creator":"dernst","content_type":"application/pdf","date_updated":"2026-06-24T06:50:24Z","relation":"main_file","file_size":1068919,"checksum":"b660048bb271f24d6763803e247d5c32"}],"has_accepted_license":"1","publication_status":"published","year":"2026","date_created":"2026-06-21T22:02:59Z","OA_type":"gold","abstract":[{"text":"Evolutionary biology examines how the genetic and phenotypic composition\r\nof populations changes over time. An important goal is to determine the\r\nfixation probability of a single advantageous mutant that arises in a homogeneous\r\npopulation of N residents. Many real populations experience environmental\r\ngradients that cause mutations to be beneficial in some spatial\r\nregions but harmful in others. Here, we study the fixation probability of a\r\nmutant placed on a simple one-dimensional spatial structure that experiences\r\nsuch a gradient. The mutant’s fitness varies linearly from1 − s to 1 + s, whereas\r\nthe resident fitness is constant and equal to 1. The existing literature suggests\r\nthat such heterogeneity in the mutant’s fitness should lead to a decrease in its\r\nfixation probability. However, in this work, we find that small, non-negligible\r\ngradients (s < 1=√N) substantially increase the fixation probability,while larger\r\ngradients (s > (log N)/√N) substantially decrease it.Moreover, we quantify the\r\nstrength of this phenomenon analytically and we precisely delimit the range of\r\nthe gradients for which it occurs. Our computer simulations closely match\r\nthose findings. Altogether, our results indicate that subjecting a simple\r\npopulation structure to natural environmental conditions can produce strong\r\ncounterintuitive effects.","lang":"eng"}],"publication_identifier":{"eissn":["2041-1723"]},"department":[{"_id":"KrCh"}],"corr_author":"1","scopus_import":"1","article_number":"5325","acknowledgement":"J.S. and K.C. were supported by the European Research Council (ERC)\r\nCoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/\r\nCOE12. J.T. was supported by GAČR grant 25-17377S and by Charles\r\nUniv. projects UNCE 24/SCI/008 and PRIMUS 24/SCI/012.","date_published":"2026-12-01T00:00:00Z","status":"public","DOAJ_listed":"1","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1038/s41467-026-71777-2","pmid":1,"ec_funded":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png"},"supplementarymaterial":"yes","OA_place":"publisher","file_date_updated":"2026-06-24T06:50:24Z","researchdata_availability":"no","oa_version":"Published Version","date_updated":"2026-09-16T07:36:49Z","das_tickbox":"1","ddc":["000"],"publication":"Nature Communications","volume":17,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","title":"The effect of the fitness gradient on fixation probability","author":[{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","first_name":"Jakub","last_name":"Svoboda"},{"full_name":"Nemati, Hossein","first_name":"Hossein","last_name":"Nemati"},{"last_name":"Tkadlec","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684"},{"full_name":"Kaveh, Kamran","last_name":"Kaveh","first_name":"Kamran"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"}],"article_processing_charge":"Yes","citation":{"ama":"Svoboda J, Nemati H, Tkadlec J, Kaveh K, Chatterjee K. The effect of the fitness gradient on fixation probability. <i>Nature Communications</i>. 2026;17. doi:<a href=\"https://doi.org/10.1038/s41467-026-71777-2\">10.1038/s41467-026-71777-2</a>","apa":"Svoboda, J., Nemati, H., Tkadlec, J., Kaveh, K., &#38; Chatterjee, K. (2026). The effect of the fitness gradient on fixation probability. <i>Nature Communications</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41467-026-71777-2\">https://doi.org/10.1038/s41467-026-71777-2</a>","ista":"Svoboda J, Nemati H, Tkadlec J, Kaveh K, Chatterjee K. 2026. The effect of the fitness gradient on fixation probability. Nature Communications. 17, 5325.","mla":"Svoboda, Jakub, et al. “The Effect of the Fitness Gradient on Fixation Probability.” <i>Nature Communications</i>, vol. 17, 5325, Springer Nature, 2026, doi:<a href=\"https://doi.org/10.1038/s41467-026-71777-2\">10.1038/s41467-026-71777-2</a>.","chicago":"Svoboda, Jakub, Hossein Nemati, Josef Tkadlec, Kamran Kaveh, and Krishnendu Chatterjee. “The Effect of the Fitness Gradient on Fixation Probability.” <i>Nature Communications</i>. Springer Nature, 2026. <a href=\"https://doi.org/10.1038/s41467-026-71777-2\">https://doi.org/10.1038/s41467-026-71777-2</a>.","short":"J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, K. Chatterjee, Nature Communications 17 (2026).","ieee":"J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, and K. Chatterjee, “The effect of the fitness gradient on fixation probability,” <i>Nature Communications</i>, vol. 17. Springer Nature, 2026."},"article_type":"original","day":"01","quality_controlled":"1","dataavailabilitystatement":"Correspondence and requests for materials should be addressed to Krishnendu Chatterjee.","oa":1,"intvolume":"        17","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","doi":"10.1038/s41467-026-71777-2"},{"_id":"22134","related_material":{"record":[{"id":"22102","relation":"used_in_publication","status":"public"}]},"month":"03","OA_place":"repository","has_accepted_license":"1","publisher":"Zenodo","oa_version":"Published Version","date_updated":"2026-09-16T07:36:13Z","abstract":[{"text":"This artifact provides the source code, benchmarks, and scripts necessary to build and reproduce the experimental results for `SuperDP` (Accepted at PLDI 2026). It also includes instructions for running the tool on user-provided inputs.","lang":"eng"}],"OA_type":"green","date_created":"2026-06-24T06:25:29Z","year":"2026","ddc":["000"],"article_processing_charge":"No","title":"SuperDP: Differential Privacy Refutation via Supermartingales","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Kafshdar Goharshadi","first_name":"Ehsan","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587"},{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic"}],"type":"research_data_reference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2026-03-09T00:00:00Z","citation":{"ieee":"K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential Privacy Refutation via Supermartingales.” Zenodo, 2026.","short":"K. Chatterjee, E. Goharshady, D. Zikelic, (2026).","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” Zenodo, 2026. <a href=\"https://doi.org/10.5281/ZENODO.18930113\">https://doi.org/10.5281/ZENODO.18930113</a>.","mla":"Chatterjee, Krishnendu, et al. <i>SuperDP: Differential Privacy Refutation via Supermartingales</i>. Zenodo, 2026, doi:<a href=\"https://doi.org/10.5281/ZENODO.18930113\">10.5281/ZENODO.18930113</a>.","ista":"Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential Privacy Refutation via Supermartingales, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.18930113\">10.5281/ZENODO.18930113</a>.","apa":"Chatterjee, K., Goharshady, E., &#38; Zikelic, D. (2026). SuperDP: Differential Privacy Refutation via Supermartingales. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.18930113\">https://doi.org/10.5281/ZENODO.18930113</a>","ama":"Chatterjee K, Goharshady E, Zikelic D. SuperDP: Differential Privacy Refutation via Supermartingales. 2026. doi:<a href=\"https://doi.org/10.5281/ZENODO.18930113\">10.5281/ZENODO.18930113</a>"},"corr_author":"1","department":[{"_id":"KrCh"}],"day":"09","status":"public","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"oa":1,"fulldoi":"https://doi.org/10.5281/ZENODO.18930113","doi":"10.5281/ZENODO.18930113","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/ZENODO.18930113"}]},{"file_date_updated":"2026-09-17T09:43:28Z","OA_place":"publisher","researchdata_availability":"no","das_tickbox":"0","date_updated":"2026-09-17T09:44:41Z","alternative_title":["LIPIcs"],"oa_version":"Published Version","ddc":["000"],"volume":391,"publication":"37th International Conference on Concurrency Theory","author":[{"first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587"},{"full_name":"Kebis, Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a","last_name":"Kebis","first_name":"Pavol"},{"orcid":"0000-0001-9864-7475","first_name":"Kaushik","last_name":"Mallik","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"}],"title":"Generalized bidding games: Where bidding and stochastic games meet","conference":{"start_date":"2026-09-01","name":"CONCUR: Conference on Concurrency Theory","location":"Liverpool, United Kingdom","end_date":"2026-09-04"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","article_processing_charge":"Yes","citation":{"apa":"Asadi, A., Henzinger, T. A., Goharshady, E., Kebis, P., &#38; Mallik, K. (2026). Generalized bidding games: Where bidding and stochastic games meet. In <i>37th International Conference on Concurrency Theory</i> (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.13</a>","ama":"Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. Generalized bidding games: Where bidding and stochastic games meet. In: <i>37th International Conference on Concurrency Theory</i>. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">10.4230/LIPIcs.CONCUR.2026.13</a>","ista":"Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. 2026. Generalized bidding games: Where bidding and stochastic games meet. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 13:1-13:20.","short":"A. Asadi, T.A. Henzinger, E. Goharshady, P. Kebis, K. Mallik, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","chicago":"Asadi, Ali, Thomas A Henzinger, Ehsan Goharshady, Pavol Kebis, and Kaushik Mallik. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.” In <i>37th International Conference on Concurrency Theory</i>, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.13</a>.","mla":"Asadi, Ali, et al. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.” <i>37th International Conference on Concurrency Theory</i>, vol. 391, 13:1-13:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">10.4230/LIPIcs.CONCUR.2026.13</a>.","ieee":"A. Asadi, T. A. Henzinger, E. Goharshady, P. Kebis, and K. Mallik, “Generalized bidding games: Where bidding and stochastic games meet,” in <i>37th International Conference on Concurrency Theory</i>, Liverpool, United Kingdom, 2026, vol. 391."},"day":"24","quality_controlled":"1","intvolume":"       391","oa":1,"project":[{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"keyword":["Bidding Games","Stochastic Games"],"doi":"10.4230/LIPIcs.CONCUR.2026.13","_id":"22920","month":"08","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"date_updated":"2026-09-17T09:43:28Z","content_type":"application/pdf","checksum":"de9af748d78fa42c173f68a71cbbd8d9","file_size":1175682,"relation":"main_file","file_name":"2026_LIPIcsCONCUR_Asadi.pdf","access_level":"open_access","file_id":"22946","creator":"dernst","date_created":"2026-09-17T09:43:28Z","success":1}],"external_id":{"arxiv":["2606.29420"]},"publication_status":"published","has_accepted_license":"1","year":"2026","abstract":[{"lang":"eng","text":"Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the right to move the token is determined by the current vertex. In traditional bidding games - referred to as pure bidding games - the right to move the token is determined at each step through bidding; here we consider Richman bidding, where the winning player of a bid pays the losing player. The winner is decided based on a temporal or quantitative specification evaluated over the resulting infinite play.\r\nIn this work, we combine turn-based games and pure bidding games into generalized bidding games, with player-1 vertices, player-2 vertices, and bidding vertices. This natural and simple generalization of bidding games has far-reaching consequences. First, we show that, as a model, generalized bidding games are more expressive than pure bidding games, and we provide several applications. Second, and most importantly, we show that generalized Richman bidding games are structurally equivalent to simple stochastic games, a well-studied model: they are linearly interreducible to each other. As was previously known, the special case of pure Richman bidding games corresponds to random-turn games. In other words, generalized bidding games extend pure bidding games in the same way that simple stochastic games extend random-turn games. We use this connection to solve generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff and discounted-sum) specifications. From a computational perspective, we establish that generalized bidding games with parity and mean-payoff specifications retain the best known upper bounds for turn-based games and pure bidding games, namely NP∩coNP.\r\nFinally, we study a repair problem that asks whether bidding vertices can be assigned \"owners\" so as to bring the threshold budget required to win the game below a given target. This problem has direct applications in compositional policy synthesis for multi-objective settings, and we show it to be NP-complete."}],"OA_type":"gold","date_created":"2026-09-13T22:01:53Z","publication_identifier":{"isbn":["9783959774475"],"eissn":["1868-8969"]},"department":[{"_id":"GradSch"},{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","corr_author":"1","date_published":"2026-08-24T00:00:00Z","article_number":"13:1-13:20","acknowledgement":"The research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), ERC-2020-AdG 101020093\r\n(VAMOS), and the RYC2024-049116-I grant funded by MICIU/AEI/10.13039/501100011033 and\r\nESF+.\r\n","status":"public","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"arxiv":1,"supplementarymaterial":"yes"},{"acknowledgement":"The research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), and ERC-2020-AdG 101020093\r\n(VAMOS) grants.","article_number":"12:1-12:23","date_published":"2026-08-24T00:00:00Z","scopus_import":"1","corr_author":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"},{"_id":"ToHe"}],"language":[{"iso":"eng"}],"status":"public","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12","supplementarymaterial":"yes","arxiv":1,"month":"08","_id":"22919","has_accepted_license":"1","publication_status":"published","external_id":{"arxiv":["2607.14877"]},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"success":1,"date_created":"2026-09-17T09:50:00Z","creator":"dernst","access_level":"open_access","file_id":"22947","file_name":"2026_LIPIcsCONCUR_Asadi2.pdf","relation":"main_file","file_size":959234,"checksum":"2e6c55b65d9d7ce436a6f59e81d7ba17","content_type":"application/pdf","date_updated":"2026-09-17T09:50:00Z"}],"date_created":"2026-09-13T22:01:53Z","OA_type":"gold","abstract":[{"lang":"eng","text":"Reachability is the most fundamental logical objective, yet it is notoriously difficult to learn in reinforcement learning settings: even for Markov decision processes, PAC learning of reachability is impossible without additional assumptions. This difficulty also holds in turn-based stochastic games (TBSGs), where two adversarial players interact on a finite state space. In this work, we consider turn-based stochastic games with reachability objectives. For such settings, adversarial learning, in which players are adversarial even in the learning phase, is impossible. Therefore, the goal is to consider learning, in which both players learn the unknown model together. In this spirit, previous literature on PAC learning in TBSGs considers (a) public information shared by both players; and (b) centralized learning, which means that players share the same learning algorithm. In this work, our contribution is two-fold. First, we relax these strong assumptions and ensure learning: (i) with private information not shared with the other player; and (ii) decentralized learning where the players do not share the same learning algorithm. To the best of our knowledge, this work is the first positive result for decentralized and private information learning of TBSGs with reachability objectives. Second, we introduce a game-theoretic generalization of the Expected Conditional Distance (ECD) parameter, which measures the expected length of reaching the target set. We establish a polynomial-sample complexity bound with respect to the number of states, actions, ECD parameter, and inverses of error tolerance and failure probability."}],"year":"2026","publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959774475"]},"citation":{"mla":"Asadi, Ali, et al. “PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance.” <i>37th International Conference on Concurrency Theory</i>, vol. 391, 12:1-12:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12\">10.4230/LIPIcs.CONCUR.2026.12</a>.","chicago":"Asadi, Ali, Krishnendu Chatterjee, and Pavol Kebis. “PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance.” In <i>37th International Conference on Concurrency Theory</i>, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.12</a>.","short":"A. Asadi, K. Chatterjee, P. Kebis, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","ieee":"A. Asadi, K. Chatterjee, and P. Kebis, “PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance,” in <i>37th International Conference on Concurrency Theory</i>, Liverpool, United Kingdom, 2026, vol. 391.","ama":"Asadi A, Chatterjee K, Kebis P. PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. In: <i>37th International Conference on Concurrency Theory</i>. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12\">10.4230/LIPIcs.CONCUR.2026.12</a>","apa":"Asadi, A., Chatterjee, K., &#38; Kebis, P. (2026). PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. In <i>37th International Conference on Concurrency Theory</i> (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.12</a>","ista":"Asadi A, Chatterjee K, Kebis P. 2026. PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 12:1-12:23."},"day":"24","oa":1,"intvolume":"       391","quality_controlled":"1","keyword":["formal methods","games and logic","logical aspects of AI","model checking"],"doi":"10.4230/LIPIcs.CONCUR.2026.12","project":[{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"researchdata_availability":"no","OA_place":"publisher","file_date_updated":"2026-09-17T09:50:00Z","das_tickbox":"0","alternative_title":["LIPIcs"],"date_updated":"2026-09-17T09:51:25Z","oa_version":"Published Version","publication":"37th International Conference on Concurrency Theory","volume":391,"ddc":["000"],"article_processing_charge":"Yes","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CONCUR: Conference on Concurrency Theory","start_date":"2026-09-01","end_date":"2026-09-04","location":"Liverpool, United Kingdom"},"title":"PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance","author":[{"first_name":"Ali","last_name":"Asadi","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","full_name":"Asadi, Ali"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Kebis","first_name":"Pavol","full_name":"Kebis, Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a"}]},{"year":"2026","abstract":[{"lang":"eng","text":"In this note, we recall the history and our motivation behind the development of Strategy Logic and we discuss some of the work that ensued from its introduction."}],"date_created":"2026-09-13T22:01:54Z","OA_type":"gold","publication_identifier":{"isbn":["9783959774475"],"issn":["1868-8969"]},"_id":"22922","month":"08","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"access_level":"open_access","file_id":"22977","file_name":"2026_LIPIcsCONCUR_Chatterjee.pdf","date_created":"2026-09-22T05:53:16Z","success":1,"creator":"dernst","content_type":"application/pdf","date_updated":"2026-09-22T05:53:16Z","relation":"main_file","checksum":"f3995df175701f56a702bdb012e4f710","file_size":517651}],"publication_status":"published","has_accepted_license":"1","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"supplementarymaterial":"no","corr_author":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","date_published":"2026-08-24T00:00:00Z","article_number":"6:1-6:7","acknowledgement":" Krishnendu Chatterjee: Supported in part by the Austrian Science Fund (FWF) COE\r\ngrant 10.55776/COE12 and the ERC CoG 863818 (ForM-SMArt).\r\nThomas A. Henzinger: Supported in part by the ERC AdG 101020093 (VAMOS) and the FWF\r\nSFB grant F8502 (SPyCoDe).\r\nNir Piterman: Supported in part by the Swedish research council (VR) project no. 2025-05419 and\r\nthe Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and\r\nAlice Wallenberg Foundation.\r\nAcknowledgements We thank the jury that our paper introducing Strategy Logic at the Conference\r\non Concurrency Theory (CONCUR) 2007 [10] was chosen for a CONCUR Test-of-Time Award at\r\nCONCUR 2026.","status":"public","language":[{"iso":"eng"}],"ddc":["000"],"volume":391,"publication":"37th International Conference on Concurrency Theory","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Nir","last_name":"Piterman","full_name":"Piterman, Nir"}],"title":"A look back at strategy logic","conference":{"location":"Liverpool, United Kingdom","end_date":"2026-09-04","start_date":"2026-09-01","name":"CONCUR: Conference on Concurrency Theory"},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"Yes","file_date_updated":"2026-09-22T05:53:16Z","OA_place":"publisher","researchdata_availability":"no","alternative_title":["LIPIcs"],"das_tickbox":"0","date_updated":"2026-09-22T05:54:30Z","oa_version":"Published Version","quality_controlled":"1","intvolume":"       391","oa":1,"project":[{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"keyword":["Strategy Logic","Games","Automata"],"doi":"10.4230/LIPIcs.CONCUR.2026.6","citation":{"ista":"Chatterjee K, Henzinger TA, Piterman N. 2026. A look back at strategy logic. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 6:1-6:7.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Piterman, N. (2026). A look back at strategy logic. In <i>37th International Conference on Concurrency Theory</i> (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.6</a>","ama":"Chatterjee K, Henzinger TA, Piterman N. A look back at strategy logic. In: <i>37th International Conference on Concurrency Theory</i>. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6\">10.4230/LIPIcs.CONCUR.2026.6</a>","ieee":"K. Chatterjee, T. A. Henzinger, and N. Piterman, “A look back at strategy logic,” in <i>37th International Conference on Concurrency Theory</i>, Liverpool, United Kingdom, 2026, vol. 391.","short":"K. Chatterjee, T.A. Henzinger, N. Piterman, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Nir Piterman. “A Look Back at Strategy Logic.” In <i>37th International Conference on Concurrency Theory</i>, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.6</a>.","mla":"Chatterjee, Krishnendu, et al. “A Look Back at Strategy Logic.” <i>37th International Conference on Concurrency Theory</i>, vol. 391, 6:1-6:7, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6\">10.4230/LIPIcs.CONCUR.2026.6</a>."},"day":"24"},{"fulldoi":"https://doi.org/10.15479/AT-ISTA-23079","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"status":"public","language":[{"iso":"eng"}],"corr_author":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"acknowledgement":"The research reported in Part I was partially supported by the European Research\r\nCouncil (ERC) Consolidator Grant 863818 (ForM-SMArt), by the Austrian Science Fund\r\n(FWF) 10.55776/COE12, and by the French Agence Nationale de la Recherche (ANR) grant\r\nANR-21-CE40-0020 (CONVERGENCE project). The research reported in Part II is a part of\r\nproject VAMOS, which has received funding from the European Research Council (ERC) under\r\ngrant agreement No.101020093.","doi_confirm":"1","date_published":"2026-10-09T00:00:00Z","publication_identifier":{"issn":["2791-4585"]},"year":"2026","date_created":"2026-10-08T09:07:53Z","abstract":[{"lang":"eng","text":"We study the computational aspects of the two central solution concepts of stochastic games\r\nplayed on finite graphs for an infinite number of steps: the value in two-player zero-sum\r\ngames, and Nash equilibria in multi-player games. In both settings, exact solutions are in\r\ntractable. Fortwo-playerzero-sumconcurrentstochasticgames,valuescanbeirrational,and\r\nthe associated decision problem is SQRT-SUM hard. For multi-player turn-based stochastic\r\ngames,theequilibriumprobabilitiescanbeirrational,anddecidingtheconstrainedexistence\r\nof a Nash equilibrium is undecidable in the presence of memory, and ∃R-complete when the\r\nplayers are restricted to stationary strategies. Hence, in both settings, the natural computational problem is the approximation of the solution within an arbitrary additive error. In\r\nthis thesis, we present improved complexity results and algorithms for such approximation\r\nproblems.\r\nThe first part of the thesis considers two-player zero-sum concurrent stochastic games\r\nwith two classic objectives: (a) stateful-discounted objectives, which are similar to the classic\r\ndiscounted-sum objectives, but states are associated with different discount factors rather\r\nthan a single discount factor; and (b) parity objectives, which are a canonical representation\r\nfor ω-regular objectives. For stateful-discounted objectives, given an ordering of the discount\r\nfactors, the limit value is the limit of the value of the stateful-discounted objectives, as\r\nthe discount factors approach zero according to the given order. The value-approximation\r\nproblem is known to be in EXPSPACE for the limit value of stateful-discounted objectives and\r\nin PSPACEforparityobjectives,andthebest-knownalgorithmsforbothproblemsareatleast\r\nexponential time, with an exponential dependence on the number of states and actions. Our\r\nmain results for the value-approximation problem for the limit value of stateful-discounted\r\nobjectives and parity objectives areas follows: (a)we establish TFNPNP complexity; and (b)we\r\npresent algorithms that improve the dependency on the number of actions in the exponent\r\nfrom linear to logarithmic. In particular, if the number of states is constant, our algorithms\r\nrun in polynomial time.\r\nThe second part of the thesis considers multi-player turn-based stochastic games with\r\nterminal payoffs, where the players are restricted to stationary strategies. We study the\r\napproximate constrained existence problem of Nash equilibria: given a game that has a Nash\r\nequilibrium in which the payoff of every player lies in a given interval, compute a strategy\r\nprofile that is an ε-Nash equilibrium and that satisfies the same constraints up to an additive\r\nerror ε. Our main results are as follows: (a) we present an FNPNP algorithm for the problem;\r\nand(b)we establish that its decision version is NP-hard, already with two players. For the\r\nupperbound,weshowthatifaconstrainedNashequilibriumexists,thenthereexists one\r\nin which the non-zero probabilities are at least an inverse of a double-exponential in the\r\ni\r\ninput size, and that such a strategy profile can be represented, up to an additive error ε, with\r\nfloating-point numbers of polynomial size. We complement the upper bound with a lower\r\nbound on this approach: we present a game with only five players in which every constrained\r\nNash equilibrium requires double-exponentially small probabilities.\r\nThe two parts share a common technical toolkit: bounds on solutions of systems of\r\npolynomial inequalities that arise from real algebraic geometry, the floating-point representation of doubly-exponentially small numbers, and guess-and-verify procedures that resolve\r\nsingle-player games with an NP oracle."}],"file":[{"date_created":"2026-10-09T11:12:08Z","creator":"aasadi","file_id":"23081","access_level":"open_access","file_name":"2026_Asadi_Ali_Thesis.pdf","relation":"main_file","checksum":"c6b368f342409de884eafdd3af7867c5","file_size":694682,"content_type":"application/pdf","date_updated":"2026-10-12T13:13:51Z"},{"content_type":"application/zip","date_updated":"2026-10-09T11:47:47Z","relation":"source_file","file_size":1538723,"checksum":"71ecb0b666438f395a92b395e315f904","access_level":"closed","file_id":"23082","file_name":"2026_Asadi_Ali_Thesis.zip","date_created":"2026-10-09T11:12:56Z","creator":"aasadi"}],"publisher":"Institute of Science and Technology Austria","has_accepted_license":"1","publication_status":"published","supervisor":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"month":"10","_id":"23079","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"},{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"doi":"10.15479/AT-ISTA-23079","oa":1,"page":"83","day":"09","citation":{"short":"A. Asadi, Approximation of Values and Equilibria in Stochastic Games: Complexity and Algorithms, Institute of Science and Technology Austria, 2026.","chicago":"Asadi, Ali. “Approximation of Values and Equilibria in Stochastic Games: Complexity and Algorithms.” Institute of Science and Technology Austria, 2026. <a href=\"https://doi.org/10.15479/AT-ISTA-23079\">https://doi.org/10.15479/AT-ISTA-23079</a>.","mla":"Asadi, Ali. <i>Approximation of Values and Equilibria in Stochastic Games: Complexity and Algorithms</i>. Institute of Science and Technology Austria, 2026, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-23079\">10.15479/AT-ISTA-23079</a>.","ieee":"A. Asadi, “Approximation of values and equilibria in stochastic games: Complexity and algorithms,” Institute of Science and Technology Austria, 2026.","apa":"Asadi, A. (2026). <i>Approximation of values and equilibria in stochastic games: Complexity and algorithms</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-23079\">https://doi.org/10.15479/AT-ISTA-23079</a>","ama":"Asadi A. Approximation of values and equilibria in stochastic games: Complexity and algorithms. 2026. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-23079\">10.15479/AT-ISTA-23079</a>","ista":"Asadi A. 2026. Approximation of values and equilibria in stochastic games: Complexity and algorithms. Institute of Science and Technology Austria."},"type":"dissertation","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","title":"Approximation of values and equilibria in stochastic games: Complexity and algorithms","author":[{"first_name":"Ali","last_name":"Asadi","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","full_name":"Asadi, Ali"}],"article_processing_charge":"No","ddc":["000"],"degree_awarded":"MS","alternative_title":["ISTA Master’s Thesis"],"oa_version":"Published Version","date_updated":"2026-10-16T08:00:45Z","OA_place":"publisher","file_date_updated":"2026-10-12T13:13:51Z","related_material":{"record":[{"relation":"part_of_dissertation","id":"21281","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"17099"}]}},{"file_date_updated":"2026-03-09T11:39:59Z","OA_place":"publisher","oa_version":"Published Version","date_updated":"2026-03-09T11:43:38Z","volume":4,"publication":"TheoretiCS","ddc":["000"],"article_processing_charge":"Yes","title":"Learning algorithms for verification of Markov decision processes","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"first_name":"Marta","last_name":"Kwiatkowska","full_name":"Kwiatkowska, Marta"},{"orcid":"0000-0002-1712-2165","first_name":"Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias"},{"full_name":"Parker, David","last_name":"Parker","first_name":"David"},{"full_name":"Ujma, Mateusz","first_name":"Mateusz","last_name":"Ujma"}],"type":"journal_article","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Brázdil, Tomáš, et al. “Learning Algorithms for Verification of Markov Decision Processes.” <i>TheoretiCS</i>, vol. 4, 10, TheoretiCS Foundation, 2025, doi:<a href=\"https://doi.org/10.46298/theoretics.25.10\">10.46298/theoretics.25.10</a>.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, and Mateusz Ujma. “Learning Algorithms for Verification of Markov Decision Processes.” <i>TheoretiCS</i>. TheoretiCS Foundation, 2025. <a href=\"https://doi.org/10.46298/theoretics.25.10\">https://doi.org/10.46298/theoretics.25.10</a>.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, T. Meggendorfer, D. Parker, M. Ujma, TheoretiCS 4 (2025).","ieee":"T. Brázdil <i>et al.</i>, “Learning algorithms for verification of Markov decision processes,” <i>TheoretiCS</i>, vol. 4. TheoretiCS Foundation, 2025.","ama":"Brázdil T, Chatterjee K, Chmelik M, et al. Learning algorithms for verification of Markov decision processes. <i>TheoretiCS</i>. 2025;4. doi:<a href=\"https://doi.org/10.46298/theoretics.25.10\">10.46298/theoretics.25.10</a>","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2025). Learning algorithms for verification of Markov decision processes. <i>TheoretiCS</i>. TheoretiCS Foundation. <a href=\"https://doi.org/10.46298/theoretics.25.10\">https://doi.org/10.46298/theoretics.25.10</a>","ista":"Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Meggendorfer T, Parker D, Ujma M. 2025. Learning algorithms for verification of Markov decision processes. TheoretiCS. 4, 10."},"day":"01","article_type":"original","intvolume":"         4","oa":1,"quality_controlled":"1","doi":"10.46298/theoretics.25.10","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Rigorous Systems Engineering"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"}],"_id":"21413","month":"04","publication_status":"published","has_accepted_license":"1","file":[{"date_updated":"2026-03-09T11:39:59Z","content_type":"application/pdf","file_size":861607,"checksum":"2ccf563ae577ee08d82baf752292ca7b","relation":"main_file","file_name":"2026_TheoretiCS_Brazdil.pdf","file_id":"21417","access_level":"open_access","creator":"dernst","success":1,"date_created":"2026-03-09T11:39:59Z"}],"publisher":"TheoretiCS Foundation","external_id":{"arxiv":["2403.09184"]},"abstract":[{"text":"We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs).\r\nThe primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors.\r\nThe presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios.\r\nThe first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.","lang":"eng"}],"OA_type":"gold","date_created":"2026-03-08T23:01:46Z","year":"2025","publication_identifier":{"eissn":["2751-4838"]},"date_published":"2025-04-01T00:00:00Z","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement AdG-267989 (QUAREM)*, AdG-246967 (VERIWARE)*, StG-279307 (Graph Games)*\r\n, CoG-863818 (ForM-SMArt), and AdG-834115 (FUN2MODEL), by the EU FP7 project HIERATIC*, by the German Research Foundation (DFG) project 427755713 (GOPro), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE)* , S11407-N23 (RiSE)*\r\n, and P23499-N23* , by the Czech Science Foundation grant No P202/12/P612* and GA23-06963S, by the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant\r\nAgency of Masaryk University, by EPSRC project EP/K038575/1*, and by the Microsoft faculty fellows award*. A preliminary version of this article appeared at ATVA 2014 [33]. The * indicates funding that supported that version.","article_number":"10","scopus_import":"1","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"DOAJ_listed":"1","status":"public","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"PlanS_conform":"1","ec_funded":1,"fulldoi":"https://doi.org/10.46298/theoretics.25.10","arxiv":1},{"publisher":"Zenodo","oa_version":"Published Version","date_updated":"2026-04-07T09:52:55Z","related_material":{"record":[{"relation":"used_for_analysis_in","id":"21661","status":"public"}]},"_id":"21668","month":"03","OA_place":"repository","article_processing_charge":"No","title":"Benchmark data for the revised practitioner's guide to MDP model checking algorithms","author":[{"last_name":"Hartmanns","first_name":"Arnd","full_name":"Hartmanns, Arnd"},{"full_name":"Junges, Sebastian","first_name":"Sebastian","last_name":"Junges"},{"full_name":"Quatmann, Tim","last_name":"Quatmann","first_name":"Tim"},{"orcid":"0000-0002-0163-2152","last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian"}],"type":"research_data_reference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"This artifact allows to review and reproduce the experiments from the paper *A Revised Practitioner's Guide to MDP Model Checking Algorithms*.\r\nThe package contains all original logfiles and derived data used to generate the plots as in the paper. Furthermore, the artifact contains the model checking tools `Storm` and `mcsta` in the version exercised in the paper, the used Docker container, as well as benchmark instances and execution scripts to reproduce the experiments.\r\n\r\nSee also the artifact of the conference paper: https://zenodo.org/records/7509474"}],"date_created":"2026-04-07T09:47:22Z","OA_type":"gold","year":"2025","ddc":["000"],"day":"07","status":"public","date_published":"2025-03-07T00:00:00Z","citation":{"apa":"Hartmanns, A., Junges, S., Quatmann, T., &#38; Weininger, M. (2025). Benchmark data for the revised practitioner’s guide to MDP model checking algorithms. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.14500423\">https://doi.org/10.5281/ZENODO.14500423</a>","ama":"Hartmanns A, Junges S, Quatmann T, Weininger M. Benchmark data for the revised practitioner’s guide to MDP model checking algorithms. 2025. doi:<a href=\"https://doi.org/10.5281/ZENODO.14500423\">10.5281/ZENODO.14500423</a>","ista":"Hartmanns A, Junges S, Quatmann T, Weininger M. 2025. Benchmark data for the revised practitioner’s guide to MDP model checking algorithms, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.14500423\">10.5281/ZENODO.14500423</a>.","chicago":"Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. “Benchmark Data for the Revised Practitioner’s Guide to MDP Model Checking Algorithms.” Zenodo, 2025. <a href=\"https://doi.org/10.5281/ZENODO.14500423\">https://doi.org/10.5281/ZENODO.14500423</a>.","short":"A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, (2025).","mla":"Hartmanns, Arnd, et al. <i>Benchmark Data for the Revised Practitioner’s Guide to MDP Model Checking Algorithms</i>. Zenodo, 2025, doi:<a href=\"https://doi.org/10.5281/ZENODO.14500423\">10.5281/ZENODO.14500423</a>.","ieee":"A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “Benchmark data for the revised practitioner’s guide to MDP model checking algorithms.” Zenodo, 2025."},"department":[{"_id":"KrCh"}],"doi":"10.5281/ZENODO.14500423","main_file_link":[{"url":"https://doi.org/10.5281/ZENODO.14500423","open_access":"1"}],"oa":1,"fulldoi":"https://doi.org/10.5281/ZENODO.14500423"},{"publication_identifier":{"eissn":["2327-4697"]},"year":"2025","date_created":"2024-11-10T23:02:00Z","OA_type":"closed access","abstract":[{"text":"Temporal networks are obtained from time-dependent interactions among individuals, whereas the interactions can be emails, phone calls, face-to-face meetings, or work collaboration. In this article, a temporal game framework is established, in which interactions among rational individuals are embedded into two-player games in a time-dependent manner. This allows studying the time-dependent complexity and variability of interactions, and the way they affect prosocial behaviors. Based on this simple mathematical model, it is found that the level of cooperation is promoted when the time of collaboration is equally limited for every individual. This observation is confirmed by a series of systematic human experiments on over 1,400 subjects, forming a foundation for comprehensively describing human temporal interactions in collaboration. The research results reveal an important incentive for human cooperation, leading to a better understanding of a fascinating aspect of human nature in society.","lang":"eng"}],"external_id":{"isi":["001385382200040"]},"publisher":"IEEE","publication_status":"published","month":"01","_id":"18529","fulldoi":"https://doi.org/10.1109/TNSE.2024.3481434","issue":"1","isi":1,"status":"public","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"scopus_import":"1","date_published":"2025-01-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","author":[{"first_name":"Yichao","last_name":"Zhang","full_name":"Zhang, Yichao"},{"last_name":"Wang","first_name":"Jiasheng","full_name":"Wang, Jiasheng"},{"first_name":"Guanghui","last_name":"Wen","full_name":"Wen, Guanghui"},{"full_name":"Guan, Jihong","first_name":"Jihong","last_name":"Guan"},{"full_name":"Zhou, Shuigeng","last_name":"Zhou","first_name":"Shuigeng"},{"full_name":"Chen, Guanrong","first_name":"Guanrong","last_name":"Chen"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Perc","first_name":"Matjaz","full_name":"Perc, Matjaz"}],"title":"Limitation of time promotes cooperation in structured collaboration systems","article_processing_charge":"No","publication":"IEEE Transactions on Network Science and Engineering","volume":12,"oa_version":"None","date_updated":"2025-02-27T12:35:48Z","doi":"10.1109/TNSE.2024.3481434","quality_controlled":"1","intvolume":"        12","page":"4-12","article_type":"original","day":"01","citation":{"ieee":"Y. Zhang <i>et al.</i>, “Limitation of time promotes cooperation in structured collaboration systems,” <i>IEEE Transactions on Network Science and Engineering</i>, vol. 12, no. 1. IEEE, pp. 4–12, 2025.","mla":"Zhang, Yichao, et al. “Limitation of Time Promotes Cooperation in Structured Collaboration Systems.” <i>IEEE Transactions on Network Science and Engineering</i>, vol. 12, no. 1, IEEE, 2025, pp. 4–12, doi:<a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">10.1109/TNSE.2024.3481434</a>.","short":"Y. Zhang, J. Wang, G. Wen, J. Guan, S. Zhou, G. Chen, K. Chatterjee, M. Perc, IEEE Transactions on Network Science and Engineering 12 (2025) 4–12.","chicago":"Zhang, Yichao, Jiasheng Wang, Guanghui Wen, Jihong Guan, Shuigeng Zhou, Guanrong Chen, Krishnendu Chatterjee, and Matjaz Perc. “Limitation of Time Promotes Cooperation in Structured Collaboration Systems.” <i>IEEE Transactions on Network Science and Engineering</i>. IEEE, 2025. <a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">https://doi.org/10.1109/TNSE.2024.3481434</a>.","ista":"Zhang Y, Wang J, Wen G, Guan J, Zhou S, Chen G, Chatterjee K, Perc M. 2025. Limitation of time promotes cooperation in structured collaboration systems. IEEE Transactions on Network Science and Engineering. 12(1), 4–12.","ama":"Zhang Y, Wang J, Wen G, et al. Limitation of time promotes cooperation in structured collaboration systems. <i>IEEE Transactions on Network Science and Engineering</i>. 2025;12(1):4-12. doi:<a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">10.1109/TNSE.2024.3481434</a>","apa":"Zhang, Y., Wang, J., Wen, G., Guan, J., Zhou, S., Chen, G., … Perc, M. (2025). Limitation of time promotes cooperation in structured collaboration systems. <i>IEEE Transactions on Network Science and Engineering</i>. IEEE. <a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">https://doi.org/10.1109/TNSE.2024.3481434</a>"}},{"isi":1,"ec_funded":1,"fulldoi":"https://doi.org/10.1007/978-3-031-82703-7_5","arxiv":1,"date_published":"2025-01-23T00:00:00Z","acknowledgement":"This research was funded in part by the DFG project 427755713 GOPro, the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement 101034413 (IST-BRIDGE).","scopus_import":"1","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"status":"public","abstract":[{"lang":"eng","text":"Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs.\r\n\r\nThe idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools."}],"OA_type":"green","date_created":"2025-03-09T23:01:29Z","year":"2025","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031827020"],"eissn":["1611-3349"]},"month":"01","_id":"19375","publication_status":"published","publisher":"Springer Nature","external_id":{"arxiv":["2410.18293"],"isi":["001446577100005"]},"intvolume":"     15530","oa":1,"quality_controlled":"1","doi":"10.1007/978-3-031-82703-7_5","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2410.18293"}],"citation":{"apa":"Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr, S., &#38; Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i> (Vol. 15530, pp. 97–120). Denver, CO, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">https://doi.org/10.1007/978-3-031-82703-7_5</a>","ama":"Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In: <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>. Vol 15530. Springer Nature; 2025:97-120. doi:<a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">10.1007/978-3-031-82703-7_5</a>","ista":"Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. 26th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.","short":"M. Azeem, D. Chakraborty, S. Kanav, J. Kretinsky, M. Mohagheghi, S. Mohr, M. Weininger, in:, 26th International Conference on Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2025, pp. 97–120.","chicago":"Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” In <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, 15530:97–120. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">https://doi.org/10.1007/978-3-031-82703-7_5</a>.","mla":"Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, vol. 15530, Springer Nature, 2025, pp. 97–120, doi:<a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">10.1007/978-3-031-82703-7_5</a>.","ieee":"M. Azeem <i>et al.</i>, “1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization,” in <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, Denver, CO, United States, 2025, vol. 15530, pp. 97–120."},"day":"23","page":"97-120","volume":15530,"publication":"26th International Conference on Verification, Model Checking, and Abstract Interpretation","article_processing_charge":"No","title":"1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization","author":[{"first_name":"Muqsit","last_name":"Azeem","full_name":"Azeem, Muqsit"},{"full_name":"Chakraborty, Debraj","last_name":"Chakraborty","first_name":"Debraj"},{"full_name":"Kanav, Sudeep","first_name":"Sudeep","last_name":"Kanav"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881"},{"full_name":"Mohagheghi, Mohammadsadegh","first_name":"Mohammadsadegh","last_name":"Mohagheghi"},{"full_name":"Mohr, Stefanie","last_name":"Mohr","first_name":"Stefanie"},{"first_name":"Maximilian","last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","type":"conference","conference":{"start_date":"2025-01-20","name":"VMCAI: Verification, Model Checking, and Abstract Interpretation","location":"Denver, CO, United States","end_date":"2025-01-21"},"OA_place":"repository","alternative_title":["LNCS"],"oa_version":"Preprint","date_updated":"2025-09-30T10:46:54Z"},{"OA_type":"green","date_created":"2025-03-23T23:01:27Z","abstract":[{"lang":"eng","text":"In reconfiguration, we are given two solutions to a graph problem, such as Vertex Cover or Dominating Set, with each solution represented by a placement of tokens on vertices of the graph. Our task is to reconfigure one into the other using small steps while ensuring the intermediate configurations of tokens are also valid solutions. The two commonly studied settings are Token Jumping and Token Sliding, which allows moving a single token to an arbitrary or an adjacent vertex, respectively.\r\n\r\nWe introduce new rules that generalize Token Jumping, parameterized by the number of tokens allowed to move at once and by the maximum distance of each move. Our main contribution is identifying minimal rules that allow reconfiguring any possible given solution into any other for Independent Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide an efficient algorithm that finds a corresponding reconfiguration sequence.\r\n\r\nWe further focus on the rule that allows each token to move to an adjacent vertex in a single step. This natural variant turns out to be the minimal rule that guarantees reconfigurability for Vertex Cover. We determine the computational complexity of deciding whether a (shortest) reconfiguration sequence exists under this rule for the three studied problems. While reachability for Vertex Cover is shown to be in P, finding a shortest sequence is shown to be NP-complete. For Independent Set and Dominating Set, even reachability is shown to be PSPACE-complete."}],"year":"2025","publication_identifier":{"issn":["0302-9743"],"isbn":["9789819628445"],"eissn":["1611-3349"]},"month":"02","_id":"19445","publication_status":"published","external_id":{"arxiv":["2411.12582"],"isi":["001537885900016"]},"publisher":"Springer Nature","ec_funded":1,"isi":1,"fulldoi":"https://doi.org/10.1007/978-981-96-2845-2_16","arxiv":1,"acknowledgement":"J. M. Křišťan acknowledges the support of the Czech Science Foundation Grant No. 24-12046S. This work was supported by the Grant Agency of the Czech Technical University in Prague, grant No. SGS23/205/OHK3/3T/18. J. Svoboda acknowledges the support of the ERC CoG 863818 (ForM-SMArt) grant.","date_published":"2025-02-20T00:00:00Z","department":[{"_id":"KrCh"}],"scopus_import":"1","language":[{"iso":"eng"}],"status":"public","publication":"19th International Conference and Workshops on Algorithms and Computation","volume":15411,"article_processing_charge":"No","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"start_date":"2025-02-28","name":"WALCOM: International Conference and Workshops on Algorithms and Computation","location":"Chengdu, China","end_date":"2025-03-02"},"type":"conference","author":[{"full_name":"Křišťan, Jan Matyáš","last_name":"Křišťan","first_name":"Jan Matyáš"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","first_name":"Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267"}],"title":"Reconfiguration using generalized token jumping","OA_place":"repository","oa_version":"Preprint","date_updated":"2025-09-30T11:14:33Z","alternative_title":["LNCS"],"oa":1,"intvolume":"     15411","quality_controlled":"1","doi":"10.1007/978-981-96-2845-2_16","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2411.12582","open_access":"1"}],"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"citation":{"ista":"Křišťan JM, Svoboda J. 2025. Reconfiguration using generalized token jumping. 19th International Conference and Workshops on Algorithms and Computation. WALCOM: International Conference and Workshops on Algorithms and Computation, LNCS, vol. 15411, 244–265.","ama":"Křišťan JM, Svoboda J. Reconfiguration using generalized token jumping. In: <i>19th International Conference and Workshops on Algorithms and Computation</i>. Vol 15411. Springer Nature; 2025:244-265. doi:<a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">10.1007/978-981-96-2845-2_16</a>","apa":"Křišťan, J. M., &#38; Svoboda, J. (2025). Reconfiguration using generalized token jumping. In <i>19th International Conference and Workshops on Algorithms and Computation</i> (Vol. 15411, pp. 244–265). Chengdu, China: Springer Nature. <a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">https://doi.org/10.1007/978-981-96-2845-2_16</a>","ieee":"J. M. Křišťan and J. Svoboda, “Reconfiguration using generalized token jumping,” in <i>19th International Conference and Workshops on Algorithms and Computation</i>, Chengdu, China, 2025, vol. 15411, pp. 244–265.","mla":"Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized Token Jumping.” <i>19th International Conference and Workshops on Algorithms and Computation</i>, vol. 15411, Springer Nature, 2025, pp. 244–65, doi:<a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">10.1007/978-981-96-2845-2_16</a>.","short":"J.M. Křišťan, J. Svoboda, in:, 19th International Conference and Workshops on Algorithms and Computation, Springer Nature, 2025, pp. 244–265.","chicago":"Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized Token Jumping.” In <i>19th International Conference and Workshops on Algorithms and Computation</i>, 15411:244–65. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">https://doi.org/10.1007/978-981-96-2845-2_16</a>."},"day":"20","page":"244-265"},{"month":"03","_id":"19499","file":[{"file_name":"2025_PNAS_Muroya.pdf","access_level":"open_access","file_id":"19524","creator":"dernst","success":1,"date_created":"2025-04-07T11:42:22Z","date_updated":"2025-04-07T11:42:22Z","content_type":"application/pdf","file_size":6805668,"checksum":"83501b8a65ee5fdd3f5604fc28eddc22","relation":"main_file"}],"publisher":"National Academy of Sciences","external_id":{"isi":["001459435600001"],"pmid":["40106357"]},"publication_status":"published","has_accepted_license":"1","year":"2025","abstract":[{"lang":"eng","text":"Quantum hardware is inherently fragile and noisy. We find that the accuracy of traditional quantum error correction algorithms can be improved depending on the hardware. Given different hardware specifications, we automatically synthesize hardware-optimal algorithms for parity correction, qubit resetting, and GHZ (Greenberger–Horne–Zeilinger) state preparation. Using stochastic techniques from computer science, our method presents a computational tool to compute exact accuracy guarantees and synthesize optimal algorithms that are often different from traditional ones. We also show that improvements can be gained with respect to the Qiskit transpiler as we compute the hardware-optimal qubit mapping for the GHZ state-preparation problem."}],"date_created":"2025-04-06T22:01:32Z","OA_type":"hybrid","publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"corr_author":"1","scopus_import":"1","date_published":"2025-03-25T00:00:00Z","acknowledgement":"We thank the reviewers. In particular, they inspired us to analyze the reset and state-preparation problems, to compute optimal qubit mappings, and to apply our method to a quantum error correction scheme that includes both bitflip and phaseflip corrections. We also thank Raimundo Saona and Marek Chalupa for their time spent in insightful discussions. This research was partially supported by the European Research Council CoG 863818 (ForM-SMArt) grant.","article_number":"e2419273122","status":"public","language":[{"iso":"eng"}],"pmid":1,"fulldoi":"https://doi.org/10.1073/pnas.2419273122","isi":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png"},"issue":"12","ec_funded":1,"file_date_updated":"2025-04-07T11:42:22Z","OA_place":"publisher","related_material":{"link":[{"relation":"software","url":"https://github.com/smml1996/algorithm_synthesis"},{"description":"News on ISTA website","relation":"press_release","url":"https://ista.ac.at/en/news/hardware-optimal-quantum-algorithms/"}]},"date_updated":"2026-04-28T13:41:14Z","oa_version":"Published Version","ddc":["000"],"volume":122,"publication":"Proceedings of the National Academy of Sciences","title":"Hardware-optimal quantum algorithms","author":[{"id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie","first_name":"Stefanie","last_name":"Muroya Lei"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"}],"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","type":"journal_article","article_processing_charge":"Yes (in subscription journal)","citation":{"ista":"Muroya Lei S, Chatterjee K, Henzinger TA. 2025. Hardware-optimal quantum algorithms. Proceedings of the National Academy of Sciences. 122(12), e2419273122.","ama":"Muroya Lei S, Chatterjee K, Henzinger TA. Hardware-optimal quantum algorithms. <i>Proceedings of the National Academy of Sciences</i>. 2025;122(12). doi:<a href=\"https://doi.org/10.1073/pnas.2419273122\">10.1073/pnas.2419273122</a>","apa":"Muroya Lei, S., Chatterjee, K., &#38; Henzinger, T. A. (2025). Hardware-optimal quantum algorithms. <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.2419273122\">https://doi.org/10.1073/pnas.2419273122</a>","ieee":"S. Muroya Lei, K. Chatterjee, and T. A. Henzinger, “Hardware-optimal quantum algorithms,” <i>Proceedings of the National Academy of Sciences</i>, vol. 122, no. 12. National Academy of Sciences, 2025.","mla":"Muroya Lei, Stefanie, et al. “Hardware-Optimal Quantum Algorithms.” <i>Proceedings of the National Academy of Sciences</i>, vol. 122, no. 12, e2419273122, National Academy of Sciences, 2025, doi:<a href=\"https://doi.org/10.1073/pnas.2419273122\">10.1073/pnas.2419273122</a>.","short":"S. Muroya Lei, K. Chatterjee, T.A. Henzinger, Proceedings of the National Academy of Sciences 122 (2025).","chicago":"Muroya Lei, Stefanie, Krishnendu Chatterjee, and Thomas A Henzinger. “Hardware-Optimal Quantum Algorithms.” <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences, 2025. <a href=\"https://doi.org/10.1073/pnas.2419273122\">https://doi.org/10.1073/pnas.2419273122</a>."},"article_type":"original","day":"25","quality_controlled":"1","intvolume":"       122","oa":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"doi":"10.1073/pnas.2419273122"},{"doi":"10.1007/978-3-031-82349-7_15","main_file_link":[{"url":"https://eprint.iacr.org/2021/1539","open_access":"1"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"oa":1,"intvolume":"     15263","quality_controlled":"1","day":"01","page":"207-223","citation":{"ama":"Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX. Route discovery in private payment channel networks. In: <i>Computer Security. ESORICS 2024 International Workshops</i>. Vol 15263. Springer Nature; 2025:207-223. doi:<a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">10.1007/978-3-031-82349-7_15</a>","apa":"Avarikioti, Z., Bastankhah, M., Maddah-Ali, M. A., Pietrzak, K. Z., Svoboda, J., &#38; Yeo, M. X. (2025). Route discovery in private payment channel networks. In <i>Computer Security. ESORICS 2024 International Workshops</i> (Vol. 15263, pp. 207–223). Bydgoszcz, Poland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">https://doi.org/10.1007/978-3-031-82349-7_15</a>","ista":"Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX. 2025. Route discovery in private payment channel networks. Computer Security. ESORICS 2024 International Workshops. ESORICS: European Symposium on Research in Computer Security, LNCS, vol. 15263, 207–223.","mla":"Avarikioti, Zeta, et al. “Route Discovery in Private Payment Channel Networks.” <i>Computer Security. ESORICS 2024 International Workshops</i>, vol. 15263, Springer Nature, 2025, pp. 207–23, doi:<a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">10.1007/978-3-031-82349-7_15</a>.","short":"Z. Avarikioti, M. Bastankhah, M.A. Maddah-Ali, K.Z. Pietrzak, J. Svoboda, M.X. Yeo, in:, Computer Security. ESORICS 2024 International Workshops, Springer Nature, 2025, pp. 207–223.","chicago":"Avarikioti, Zeta, Mahsa Bastankhah, Mohammad Ali Maddah-Ali, Krzysztof Z Pietrzak, Jakub Svoboda, and Michelle X Yeo. “Route Discovery in Private Payment Channel Networks.” In <i>Computer Security. ESORICS 2024 International Workshops</i>, 15263:207–23. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">https://doi.org/10.1007/978-3-031-82349-7_15</a>.","ieee":"Z. Avarikioti, M. Bastankhah, M. A. Maddah-Ali, K. Z. Pietrzak, J. Svoboda, and M. X. Yeo, “Route discovery in private payment channel networks,” in <i>Computer Security. ESORICS 2024 International Workshops</i>, Bydgoszcz, Poland, 2025, vol. 15263, pp. 207–223."},"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","conference":{"name":"ESORICS: European Symposium on Research in Computer Security","start_date":"2024-09-16","end_date":"2024-09-20","location":"Bydgoszcz, Poland"},"title":"Route discovery in private payment channel networks","author":[{"first_name":"Zeta","last_name":"Avarikioti","full_name":"Avarikioti, Zeta"},{"full_name":"Bastankhah, Mahsa","last_name":"Bastankhah","first_name":"Mahsa"},{"last_name":"Maddah-Ali","first_name":"Mohammad Ali","full_name":"Maddah-Ali, Mohammad Ali"},{"orcid":"0000-0002-9139-1654","last_name":"Pietrzak","first_name":"Krzysztof Z","full_name":"Pietrzak, Krzysztof Z","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","first_name":"Jakub","last_name":"Svoboda"},{"last_name":"Yeo","first_name":"Michelle X","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","full_name":"Yeo, Michelle X","orcid":"0009-0001-3676-4809"}],"publication":"Computer Security. ESORICS 2024 International Workshops","volume":15263,"oa_version":"Submitted Version","date_updated":"2025-11-05T07:52:35Z","alternative_title":["LNCS"],"OA_place":"repository","ec_funded":1,"fulldoi":"https://doi.org/10.1007/978-3-031-82349-7_15","language":[{"iso":"eng"}],"status":"public","acknowledgement":"This work was supported in part by the ERC CoG 863818 (ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, and MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms) grants.","date_published":"2025-04-01T00:00:00Z","scopus_import":"1","department":[{"_id":"KrPi"},{"_id":"KrCh"}],"publication_identifier":{"isbn":["9783031823480"],"eissn":["1611-3349"],"issn":["0302-9743"]},"OA_type":"green","date_created":"2025-04-20T22:01:28Z","abstract":[{"text":"In this work, we explore route discovery in private payment channel networks. We first determine what “ideal\" privacy for a routing protocol means in this setting. We observe that protocols achieving this strong privacy definition exist by leveraging Multi-Party Computation but they are inherently inefficient as they must involve the entire network. We then present protocols with weaker privacy guarantees but much better efficiency (involving only a small fraction of the nodes). The core idea is that both sender and receiver gossip a message which propagates through the network, and the moment any node in the network receives both messages, a path is found. In our first protocol the message is always sent to all neighbouring nodes with a delay proportional to the fees of that edge. In our second protocol the message is only sent to one neighbour chosen randomly with a probability proportional to its degree. We additionally propose a more realistic notion of privacy in order to measure the privacy leakage of our protocols in practice. Our realistic notion of privacy challenges an adversary that join the network with a fixed budget to create channels to guess the sender and receiver of a transaction upon receiving messages from our protocols. Simulations of our protocols on the Lightning network topology (for random transactions and uniform fees) show that 1) forming edges with high degree nodes is a more effective attack strategy for the adversary, 2) there is a tradeoff between the number of nodes involved in our protocols (privacy) and the optimality of the discovered path, and 3) our protocols involve a very small fraction of the network on average.","lang":"eng"}],"year":"2025","publication_status":"published","publisher":"Springer Nature","month":"04","_id":"19600"},{"intvolume":"        39","oa":1,"quality_controlled":"1","doi":"10.1609/aaai.v39i25.34865","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.10185"}],"citation":{"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>.","chicago":"Meggendorfer, Tobias, Maximilian Weininger, and Patrick Wienhöft. “Solving Robust Markov Decision Processes: Generic, Reliable, Efficient.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:26631–41. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i25.34865\">https://doi.org/10.1609/aaai.v39i25.34865</a>.","short":"T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 26631–26641.","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.","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>","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."},"day":"11","page":"26631-26641","volume":39,"publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","article_processing_charge":"No","author":[{"orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer"},{"last_name":"Weininger","first_name":"Maximilian","full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","orcid":"0000-0002-0163-2152"},{"first_name":"Patrick","last_name":"Wienhöft","full_name":"Wienhöft, Patrick"}],"title":"Solving robust Markov decision processes: Generic, reliable, efficient","type":"conference","conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2025-02-25","end_date":"2025-03-04","location":"Philadelphia, PA, United States"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"link":[{"url":"https://doi.org/10.5281/zenodo.14385449","relation":"software"}]},"OA_place":"repository","oa_version":"Preprint","date_updated":"2026-02-16T12:25:05Z","ec_funded":1,"issue":"25","fulldoi":"https://doi.org/10.1609/aaai.v39i25.34865","arxiv":1,"date_published":"2025-04-11T00:00:00Z","acknowledgement":"This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No. 101034413,\r\nthe ERC CoG 863818 (ForM-SMArt), and the DFG through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy) and the TRR 248 (see https://perspicuous-computing.science, project ID 389792660).","department":[{"_id":"KrCh"}],"scopus_import":"1","language":[{"iso":"eng"}],"status":"public","abstract":[{"lang":"eng","text":"Markov decision processes (MDP) are a well-established model for sequential decision-making in the presence of probabilities. In *robust* MDP (RMDP), every action is associated with an *uncertainty set* of probability distributions, modelling that transition probabilities are not known precisely. Based on the known theoretical connection to stochastic games, we provide a framework for solving RMDPs that is generic, reliable, and efficient. It is *generic* both with respect to the model, allowing for a wide range of uncertainty sets, including but not limited to intervals, L1- or L2-balls, and polytopes; and with respect to the objective, including long-run average reward, undiscounted total reward, and stochastic shortest path. It is *reliable*, as our approach not only converges in the limit, but provides precision guarantees at any time during the computation. It is *efficient* because -- in contrast to state-of-the-art approaches -- it avoids explicitly constructing the underlying stochastic game. Consequently, our prototype implementation outperforms existing tools by several orders of magnitude and can solve RMDPs with a million states in under a minute."}],"OA_type":"green","date_created":"2025-05-11T22:02:39Z","year":"2025","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"month":"04","_id":"19666","publication_status":"published","publisher":"Association for the Advancement of Artificial Intelligence","external_id":{"arxiv":["2412.10185"]}},{"project":[{"grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020"}],"doi":"10.1007/978-3-031-90643-5_9","quality_controlled":"1","oa":1,"intvolume":"     15696","page":"167-190","day":"01","citation":{"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>","apa":"Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Sound statistical model checking for probabilities and expected rewards. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>","ista":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound statistical model checking for probabilities and expected rewards. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15696, 167–190.","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>.","chicago":"Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:167–90. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>.","short":"C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 167–190.","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."},"type":"conference","conference":{"location":"Hamilton, ON, Canada","end_date":"2025-05-08","start_date":"2025-05-03","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Sound statistical model checking for probabilities and expected rewards","author":[{"last_name":"Budde","first_name":"Carlos E.","full_name":"Budde, Carlos E."},{"first_name":"Arnd","last_name":"Hartmanns","full_name":"Hartmanns, Arnd"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","first_name":"Tobias","orcid":"0000-0002-1712-2165"},{"full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger","first_name":"Maximilian"},{"full_name":"Wienhöft, Patrick","first_name":"Patrick","last_name":"Wienhöft"}],"article_processing_charge":"No","ddc":["000"],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","volume":15696,"date_updated":"2025-06-02T09:45:41Z","oa_version":"Published Version","alternative_title":["LNCS"],"OA_place":"publisher","file_date_updated":"2025-06-02T09:35:42Z","related_material":{"record":[{"id":"19769","relation":"research_data","status":"public"}]},"arxiv":1,"fulldoi":"https://doi.org/10.1007/978-3-031-90643-5_9","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"status":"public","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"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).","date_published":"2025-05-01T00:00:00Z","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031906428"],"issn":["0302-9743"]},"year":"2025","OA_type":"hybrid","date_created":"2025-05-25T22:17:08Z","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."}],"external_id":{"arxiv":["2411.00559"]},"file":[{"date_updated":"2025-06-02T09:35:42Z","content_type":"application/pdf","file_size":711271,"checksum":"d45856b503b1dd4f8f14c3566327225b","relation":"main_file","file_name":"2025_TACAS_Budde.pdf","access_level":"open_access","file_id":"19770","creator":"dernst","success":1,"date_created":"2025-06-02T09:35:42Z"}],"publisher":"Springer Nature","has_accepted_license":"1","publication_status":"published","_id":"19742","month":"05"}]