[{"year":"2026","day":"08","PlanS_conform":"1","file":[{"success":1,"file_id":"22135","file_name":"2026_ProcACMProgrammingLanguages_Chatterjee.pdf","file_size":858595,"content_type":"application/pdf","date_updated":"2026-06-24T06:19:56Z","creator":"dernst","access_level":"open_access","checksum":"994bf21d6269dabccf1e1091e02962c5","date_created":"2026-06-24T06:19:56Z","relation":"main_file"}],"status":"public","publication_status":"published","date_updated":"2026-06-24T06:39:37Z","article_type":"original","publisher":"Association for Computing Machinery","intvolume":"        10","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"keyword":["Static Program Analysis","Differential Privacy","Probabilistic Programming","Martingales"],"has_accepted_license":"1","OA_type":"gold","researchdata_availability":"yes","corr_author":"1","ddc":["000"],"date_published":"2026-06-08T00:00:00Z","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi","first_name":"Ehsan"},{"last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"OA_place":"publisher","issue":"PLDI","language":[{"iso":"eng"}],"quality_controlled":"1","oa":1,"oa_version":"Published Version","department":[{"_id":"KrCh"}],"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.","supplementarymaterial":"no","date_created":"2026-06-21T22:02:59Z","doi":"10.1145/3808296","related_material":{"record":[{"id":"22134","relation":"research_data","status":"public"}]},"_id":"22102","das_tickbox":"1","publication_identifier":{"eissn":["2475-1421"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"06","type":"journal_article","scopus_import":"1","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.","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>. Association for Computing Machinery. <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, Association for Computing Machinery, 2026, 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. Association for Computing Machinery, 2026.","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>","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2026. <a href=\"https://doi.org/10.1145/3808296\">https://doi.org/10.1145/3808296</a>."},"arxiv":1,"external_id":{"arxiv":["2603.26215"]},"article_processing_charge":"Yes","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"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."}],"publication":"Proceedings of the ACM on Programming Languages","volume":10,"ec_funded":1,"file_date_updated":"2026-06-24T06:19:56Z","title":"SuperDP: Differential privacy refutation via supermartingales","article_number":"218"},{"month":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-06-24T06:39:38Z","type":"research_data_reference","publisher":"Zenodo","citation":{"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>","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>.","short":"K. Chatterjee, E. Goharshady, D. Zikelic, (2026).","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>.","ieee":"K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential Privacy Refutation via Supermartingales.” Zenodo, 2026.","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>","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>."},"main_file_link":[{"url":"https://doi.org/10.5281/ZENODO.18930113","open_access":"1"}],"doi":"10.5281/ZENODO.18930113","date_created":"2026-06-24T06:25:29Z","status":"public","related_material":{"record":[{"id":"22102","relation":"used_in_publication","status":"public"}]},"_id":"22134","oa":1,"oa_version":"Published Version","department":[{"_id":"KrCh"}],"OA_place":"repository","year":"2026","day":"09","title":"SuperDP: Differential Privacy Refutation via Supermartingales","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","last_name":"Kafshdar Goharshadi"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde"}],"abstract":[{"lang":"eng","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."}],"corr_author":"1","OA_type":"green","date_published":"2026-03-09T00:00:00Z","ddc":["000"],"article_processing_charge":"No","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"}},{"title":"Qualitative analysis of ω-regular objectives on robust MDPs","publication":"Proceedings of the 40th AAAI Conference on Artificial Intelligence","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."}],"volume":40,"ec_funded":1,"conference":{"name":"AAAI: Conference on Artificial Intelligence","location":"Singapore, Singapore","start_date":"2026-01-20","end_date":"2026-01-27"},"article_processing_charge":"No","page":"36137-36145","external_id":{"arxiv":["2505.04539"]},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"arxiv":1,"month":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","scopus_import":"1","citation":{"ista":"Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. 2026. Qualitative analysis of ω-regular objectives on robust MDPs. Proceedings of the 40th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 40, 36137–36145.","apa":"Asadi, A., Chatterjee, K., Goharshady, E., Karrabi, M., &#38; Shafiee, A. (2026). Qualitative analysis of ω-regular objectives on robust MDPs. In <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i> (Vol. 40, pp. 36137–36145). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">https://doi.org/10.1609/aaai.v40i43.40931</a>","short":"A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, A. Shafiee, in:, Proceedings of the 40th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–36145.","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>.","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>","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>."},"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.","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.04539"}],"date_created":"2026-04-12T22:01:50Z","doi":"10.1609/aaai.v40i43.40931","_id":"21717","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"oa_version":"Preprint","oa":1,"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"OA_place":"repository","issue":"43","quality_controlled":"1","language":[{"iso":"eng"}],"author":[{"first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","last_name":"Kafshdar Goharshadi"},{"first_name":"Mehrdad","last_name":"Karrabi","orcid":"0009-0007-5253-9170","full_name":"Karrabi, Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"last_name":"Shafiee","first_name":"Ali","id":"2783031a-7378-11f0-b2d0-f17f1db2ebad","full_name":"Shafiee, Ali"}],"OA_type":"green","date_published":"2026-03-14T00:00:00Z","intvolume":"        40","date_updated":"2026-05-04T11:38:56Z","publisher":"Association for the Advancement of Artificial Intelligence","status":"public","publication_status":"published","year":"2026","day":"14"},{"quality_controlled":"1","language":[{"iso":"eng"}],"issue":"43","OA_place":"repository","department":[{"_id":"KrCh"}],"oa_version":"Preprint","_id":"21722","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"doi":"10.1609/aaai.v40i43.40932","date_created":"2026-04-12T22:01:52Z","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.","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2511.13134"}],"citation":{"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>","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.","ieee":"A. Asadi, K. Chatterjee, D. Lurie, and R. J. Saona Urmeneta, “Revealing POMDPs: Qualitative and quantitative analysis for parity objectives,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36146–36154.","mla":"Asadi, Ali, et al. “Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026, pp. 36146–54, doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">10.1609/aaai.v40i43.40932</a>.","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>","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>."},"scopus_import":"1","type":"conference","month":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"conference":{"start_date":"2026-01-20","end_date":"2026-01-27","location":"Singapore, Singapore","name":"AAAI: Conference on Artificial Intelligence"},"external_id":{"arxiv":["2511.13134"]},"article_processing_charge":"No","page":"36146-36154","ec_funded":1,"volume":40,"abstract":[{"lang":"eng","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."}],"publication":"Proceedings of the AAAI Conference on Artificial Intelligence","title":"Revealing POMDPs: Qualitative and quantitative analysis for parity objectives","day":"14","year":"2026","publication_status":"published","status":"public","publisher":"Association for the Advancement of Artificial Intelligence","date_updated":"2026-05-04T11:44:14Z","intvolume":"        40","date_published":"2026-03-14T00:00:00Z","OA_type":"green","corr_author":"1","author":[{"first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"David","last_name":"Lurie","full_name":"Lurie, David","id":"579a6c20-34cf-11f1-acbd-8c2f19cdb4da"},{"id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","full_name":"Saona Urmeneta, Raimundo J","orcid":"0000-0001-5103-038X","last_name":"Saona Urmeneta","first_name":"Raimundo J"}]},{"has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"intvolume":"        17","author":[{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267","first_name":"Jakub","last_name":"Svoboda"},{"full_name":"Nemati, Hossein","last_name":"Nemati","first_name":"Hossein"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","first_name":"Josef"},{"first_name":"Kamran","last_name":"Kaveh","full_name":"Kaveh, Kamran"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"}],"ddc":["000"],"date_published":"2026-12-01T00:00:00Z","corr_author":"1","researchdata_availability":"no","OA_type":"gold","file":[{"access_level":"open_access","date_created":"2026-06-24T06:50:24Z","checksum":"b660048bb271f24d6763803e247d5c32","relation":"main_file","content_type":"application/pdf","date_updated":"2026-06-24T06:50:24Z","file_size":1068919,"creator":"dernst","file_id":"22136","file_name":"2026_NatureComm_Svoboda.pdf","success":1}],"day":"01","year":"2026","publisher":"Springer Nature","article_type":"original","date_updated":"2026-06-24T07:53:53Z","status":"public","publication_status":"published","pmid":1,"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"external_id":{"pmid":["41997932"]},"article_processing_charge":"Yes","title":"The effect of the fitness gradient on fixation probability","article_number":"5325","file_date_updated":"2026-06-24T06:50:24Z","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":"Nature Communications","ec_funded":1,"volume":17,"department":[{"_id":"KrCh"}],"DOAJ_listed":"1","oa_version":"Published Version","oa":1,"language":[{"iso":"eng"}],"quality_controlled":"1","OA_place":"publisher","scopus_import":"1","citation":{"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.","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>","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>.","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.","short":"J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, K. Chatterjee, Nature Communications 17 (2026).","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>.","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>"},"dataavailabilitystatement":"Correspondence and requests for materials should be addressed to Krishnendu Chatterjee.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"12","type":"journal_article","date_created":"2026-06-21T22:02:59Z","doi":"10.1038/s41467-026-71777-2","_id":"22101","publication_identifier":{"eissn":["2041-1723"]},"das_tickbox":"0","supplementarymaterial":"yes","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."},{"file":[{"content_type":"application/pdf","date_updated":"2025-12-29T09:36:50Z","file_size":2308124,"creator":"dernst","access_level":"open_access","relation":"main_file","date_created":"2025-12-29T09:36:50Z","checksum":"dd50b62a1efc28c0133fe9c11dbee53c","success":1,"file_id":"20860","file_name":"2025_PNAS_Svoboda.pdf"}],"year":"2025","day":"15","date_updated":"2026-05-20T08:13:17Z","publisher":"National Academy of Sciences","article_type":"original","status":"public","publication_status":"published","pmid":1,"has_accepted_license":"1","intvolume":"       122","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"author":[{"last_name":"Svoboda","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"}],"OA_type":"hybrid","corr_author":"1","APC_amount":"3003,56 EUR","date_published":"2025-12-15T00:00:00Z","ddc":["000"],"oa_version":"Published Version","oa":1,"department":[{"_id":"KrCh"}],"OA_place":"publisher","issue":"51","quality_controlled":"1","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"12","type":"journal_article","scopus_import":"1","citation":{"chicago":"Svoboda, Jakub, and Krishnendu Chatterjee. “Promoters of Cooperation in Evolutionary Games.” <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences, 2025. <a href=\"https://doi.org/10.1073/pnas.2524109122\">https://doi.org/10.1073/pnas.2524109122</a>.","ama":"Svoboda J, Chatterjee K. Promoters of cooperation in evolutionary games. <i>Proceedings of the National Academy of Sciences</i>. 2025;122(51):e2524109122. doi:<a href=\"https://doi.org/10.1073/pnas.2524109122\">10.1073/pnas.2524109122</a>","mla":"Svoboda, Jakub, and Krishnendu Chatterjee. “Promoters of Cooperation in Evolutionary Games.” <i>Proceedings of the National Academy of Sciences</i>, vol. 122, no. 51, National Academy of Sciences, 2025, p. e2524109122, doi:<a href=\"https://doi.org/10.1073/pnas.2524109122\">10.1073/pnas.2524109122</a>.","ieee":"J. Svoboda and K. Chatterjee, “Promoters of cooperation in evolutionary games,” <i>Proceedings of the National Academy of Sciences</i>, vol. 122, no. 51. National Academy of Sciences, p. e2524109122, 2025.","short":"J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences 122 (2025) e2524109122.","apa":"Svoboda, J., &#38; Chatterjee, K. (2025). Promoters of cooperation in evolutionary games. <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.2524109122\">https://doi.org/10.1073/pnas.2524109122</a>","ista":"Svoboda J, Chatterjee K. 2025. Promoters of cooperation in evolutionary games. Proceedings of the National Academy of Sciences. 122(51), e2524109122."},"acknowledgement":"J.S. and K.C. were supported by the European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12.","date_created":"2025-12-28T23:01:26Z","doi":"10.1073/pnas.2524109122","publication_identifier":{"eissn":["1091-6490"]},"_id":"20857","external_id":{"pmid":["41397136"]},"article_processing_charge":"Yes (in subscription journal)","page":"e2524109122","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"title":"Promoters of cooperation in evolutionary games","publication":"Proceedings of the National Academy of Sciences","abstract":[{"lang":"eng","text":"Evolutionary games provide a flexible mathematical framework for many problems in biology and social evolution. Prisoners’ dilemma, and in particular, the important special case of donation games, represents social dilemmas where cooperation is mutually beneficial, yet defection is preferred by selfish agents. In evolutionary games on networks, the agents interact over a population structure. The existence of population structures that promote cooperative behavior is a fascinating and active research topic. Previous research establishes structures promoting cooperation in the limit of weak selection where the benefit-to-cost ratio β exceeds 1.5. The existence of such structures for medium and strong selection for 1 < ß < 2 and for weak selection for 1 < ß < 1.5 has been a long-standing open question. First, we answer the open questions in the affirmative: For every selection strength and every ß > 1, we construct networks promoting cooperation. Second, we present a robustness result with respect to β and selection strength: Our structures promote cooperation for a range of these parameter values rather than specific parameter values. Finally, we supplement our theoretical results with simulation results on small population structures that show the effectiveness of our construction over well-studied population structures."}],"volume":122,"ec_funded":1,"file_date_updated":"2025-12-29T09:36:50Z"},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"has_accepted_license":"1","ddc":["000"],"date_published":"2025-07-30T00:00:00Z","OA_type":"gold","corr_author":"1","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"first_name":"Jean-Francois","last_name":"Raskin","full_name":"Raskin, Jean-Francois"},{"full_name":"Sankur, Ocan","last_name":"Sankur","first_name":"Ocan"}],"day":"30","year":"2025","file":[{"access_level":"open_access","date_created":"2026-02-18T07:50:56Z","relation":"main_file","checksum":"4477a7fd4fbf0ba6c8e9b15683b5a6b8","file_size":1075724,"content_type":"application/pdf","date_updated":"2026-02-18T07:50:56Z","creator":"dernst","file_id":"21313","file_name":"2025_LIPIcs_Chatterjee.pdf","success":1}],"publication_status":"published","status":"public","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2026-02-18T07:53:26Z","arxiv":1,"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"article_processing_charge":"No","external_id":{"arxiv":["2504.15960"]},"conference":{"name":"ICALP: Automata, Languages and Programming","location":"Aarhus, Denmark","start_date":"2025-07-08","end_date":"2025-07-11"},"file_date_updated":"2026-02-18T07:50:56Z","ec_funded":1,"alternative_title":["LIPIcs"],"abstract":[{"text":"We consider multiple-environment Markov decision processes (MEMDP), which consist of a finite set of MDPs over the same state space, representing different scenarios of transition structure and probability. The value of a strategy is the probability to satisfy the objective, here a parity objective, in the worst-case scenario, and the value of an MEMDP is the supremum of the values achievable by a strategy.\r\nWe show that deciding whether the value is 1 is a PSPACE-complete problem, and even in P when the number of environments is fixed, along with new insights to the almost-sure winning problem, which is to decide if there exists a strategy with value 1. Pure strategies are sufficient for theses problems, whereas randomization is necessary in general when the value is smaller than 1. We present an algorithm to approximate the value, running in double exponential space. Our results are in contrast to the related model of partially-observable MDPs where all these problems are known to be undecidable.","lang":"eng"}],"publication":"52nd International Colloquium on Automata, Languages, and Programming","title":"The value problem for multiple-environment MDPs with parity objective","article_number":"150","language":[{"iso":"eng"}],"quality_controlled":"1","OA_place":"publisher","department":[{"_id":"KrCh"}],"oa_version":"Published Version","oa":1,"publication_identifier":{"isbn":["9783959773720"]},"_id":"21268","date_created":"2026-02-17T07:49:17Z","doi":"10.4230/LIPIcs.ICALP.2025.150","acknowledgement":"Krishnendu Chatterjee: ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund\r\n(FWF) 10.55776/COE12. Jean-François Raskin: PDR Weave project FORM-LEARN-POMDP funded by FNRS and DFG, and the support of the Fondation ULB. Ocan Sankur: ANR BisoUS (ANR-22-CE48-0012) and ANR EpiRL (ANR-22-CE23-0029).","citation":{"short":"K. Chatterjee, L. Doyen, J.-F. Raskin, O. Sankur, in:, 52nd International Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025.","ieee":"K. Chatterjee, L. Doyen, J.-F. Raskin, and O. Sankur, “The value problem for multiple-environment MDPs with parity objective,” in <i>52nd International Colloquium on Automata, Languages, and Programming</i>, Aarhus, Denmark, 2025.","mla":"Chatterjee, Krishnendu, et al. “The Value Problem for Multiple-Environment MDPs with Parity Objective.” <i>52nd International Colloquium on Automata, Languages, and Programming</i>, 150, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2025.150\">10.4230/LIPIcs.ICALP.2025.150</a>.","ama":"Chatterjee K, Doyen L, Raskin J-F, Sankur O. The value problem for multiple-environment MDPs with parity objective. In: <i>52nd International Colloquium on Automata, Languages, and Programming</i>. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2025.150\">10.4230/LIPIcs.ICALP.2025.150</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Jean-Francois Raskin, and Ocan Sankur. “The Value Problem for Multiple-Environment MDPs with Parity Objective.” In <i>52nd International Colloquium on Automata, Languages, and Programming</i>. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2025.150\">https://doi.org/10.4230/LIPIcs.ICALP.2025.150</a>.","ista":"Chatterjee K, Doyen L, Raskin J-F, Sankur O. 2025. The value problem for multiple-environment MDPs with parity objective. 52nd International Colloquium on Automata, Languages, and Programming. ICALP: Automata, Languages and Programming, LIPIcs, , 150.","apa":"Chatterjee, K., Doyen, L., Raskin, J.-F., &#38; Sankur, O. (2025). The value problem for multiple-environment MDPs with parity objective. In <i>52nd International Colloquium on Automata, Languages, and Programming</i>. Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2025.150\">https://doi.org/10.4230/LIPIcs.ICALP.2025.150</a>"},"scopus_import":"1","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07"},{"status":"public","publication_status":"published","date_updated":"2026-02-19T09:39:15Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2025","day":"09","file":[{"success":1,"file_name":"2025_FSTTCS_Asadi.pdf","file_id":"21316","creator":"dernst","file_size":1054007,"content_type":"application/pdf","date_updated":"2026-02-18T09:13:25Z","checksum":"a66343e3ccc4a9cc5bc699c03d5764ff","relation":"main_file","date_created":"2026-02-18T09:13:25Z","access_level":"open_access"}],"OA_type":"gold","corr_author":"1","date_published":"2025-12-09T00:00:00Z","ddc":["000"],"author":[{"id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","full_name":"Asadi, Ali","last_name":"Asadi","first_name":"Ali"},{"full_name":"Brice, Leonard","first_name":"Leonard","last_name":"Brice"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","full_name":"Thejaswini, K. S.","last_name":"Thejaswini","first_name":"K. S."}],"intvolume":"       360","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"has_accepted_license":"1","acknowledgement":"This work is a part of project VAMOS that has received funding from the European\r\nResearch Council (ERC), grant agreement No 101020093.\r\n","date_created":"2026-02-17T08:27:14Z","doi":"10.4230/lipics.fsttcs.2025.9","_id":"21281","publication_identifier":{"isbn":["9783959774062"]},"month":"12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","citation":{"apa":"Asadi, A., Brice, L., Chatterjee, K., &#38; Thejaswini, K. S. (2025). ε-stationary Nash equilibria in multi-player stochastic graph games. In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 360, p. 9:1-9:17). Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/lipics.fsttcs.2025.9\">https://doi.org/10.4230/lipics.fsttcs.2025.9</a>","ista":"Asadi A, Brice L, Chatterjee K, Thejaswini KS. 2025. ε-stationary Nash equilibria in multi-player stochastic graph games. 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 360, 9:1-9:17.","chicago":"Asadi, Ali, Leonard Brice, Krishnendu Chatterjee, and K. S. Thejaswini. “ε-Stationary Nash Equilibria in Multi-Player Stochastic Graph Games.” In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, 360:9:1-9:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/lipics.fsttcs.2025.9\">https://doi.org/10.4230/lipics.fsttcs.2025.9</a>.","ama":"Asadi A, Brice L, Chatterjee K, Thejaswini KS. ε-stationary Nash equilibria in multi-player stochastic graph games. In: <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 360. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025:9:1-9:17. doi:<a href=\"https://doi.org/10.4230/lipics.fsttcs.2025.9\">10.4230/lipics.fsttcs.2025.9</a>","ieee":"A. Asadi, L. Brice, K. Chatterjee, and K. S. Thejaswini, “ε-stationary Nash equilibria in multi-player stochastic graph games,” in <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Pilani, India, 2025, vol. 360, p. 9:1-9:17.","mla":"Asadi, Ali, et al. “ε-Stationary Nash Equilibria in Multi-Player Stochastic Graph Games.” <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 360, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 9:1-9:17, doi:<a href=\"https://doi.org/10.4230/lipics.fsttcs.2025.9\">10.4230/lipics.fsttcs.2025.9</a>.","short":"A. Asadi, L. Brice, K. Chatterjee, K.S. Thejaswini, in:, 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 9:1-9:17."},"OA_place":"publisher","quality_controlled":"1","language":[{"iso":"eng"}],"oa_version":"Published Version","oa":1,"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"publication":"45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science","abstract":[{"lang":"eng","text":"A strategy profile in a multi-player game is a Nash equilibrium if no player can unilaterally deviate to achieve a strictly better payoff. A profile is an ε-Nash equilibrium if no player can gain more than ε by unilaterally deviating from their strategy. In this work, we use ε-Nash equilibria to approximate the computation of Nash equilibria. Specifically, we focus on turn-based, multiplayer stochastic games played on graphs, where players are restricted to stationary strategies - strategies that use randomness but not memory.\r\nThe problem of deciding the constrained existence of stationary Nash equilibria - where each player’s payoff must lie within a given interval - is known to be ∃ℝ-complete in such a setting (Hansen and Sølvsten, 2020). We extend this line of work to stationary ε-Nash equilibria and present an algorithm that solves the following promise problem: given a game with a Nash equilibrium satisfying the constraints, compute an ε-Nash equilibrium that ε-satisfies those same constraints - satisfies the constraints up to an ε additive error. Our algorithm runs in FNP^NP time.\r\nTo achieve this, we first show that if a constrained Nash equilibrium exists, then one exists where the non-zero probabilities are at least an inverse of a double-exponential in the input. We further prove that such a strategy can be encoded using floating-point representations, as in the work of Frederiksen and Miltersen (2013), which finally gives us our FNP^NP algorithm. \r\nWe further show that the decision version of the promise problem is NP-hard. Finally, we show a partial tightness result by proving a lower bound for such techniques: if a constrained Nash equilibrium exists, then there must be one where the probabilities in the strategies are double-exponentially small."}],"ec_funded":1,"alternative_title":["LIPIcs"],"volume":360,"file_date_updated":"2026-02-18T09:13:25Z","title":"ε-stationary Nash equilibria in multi-player stochastic graph games","arxiv":1,"article_processing_charge":"Yes","external_id":{"arxiv":["2508.15356"]},"page":"9:1-9:17","conference":{"name":"FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science","location":"Pilani, India","start_date":"2025-12-17","end_date":"2025-12-19"},"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}]},{"department":[{"_id":"KrCh"}],"oa_version":"Published Version","oa":1,"quality_controlled":"1","language":[{"iso":"eng"}],"OA_place":"publisher","citation":{"ama":"Chatterjee K, Křišťan JM, Schmid S, Svoboda J, Yeo MX. Boosting payment channel network liquidity with topology optimization and transaction selection. In: <i>39th International Symposium on Distributed Computing</i>. Vol 356. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.DISC.2025.23\">10.4230/LIPIcs.DISC.2025.23</a>","chicago":"Chatterjee, Krishnendu, Jan Matyáš Křišťan, Stefan Schmid, Jakub Svoboda, and Michelle X Yeo. “Boosting Payment Channel Network Liquidity with Topology Optimization and Transaction Selection.” In <i>39th International Symposium on Distributed Computing</i>, Vol. 356. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.DISC.2025.23\">https://doi.org/10.4230/LIPIcs.DISC.2025.23</a>.","short":"K. Chatterjee, J.M. Křišťan, S. Schmid, J. Svoboda, M.X. Yeo, in:, 39th International Symposium on Distributed Computing, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025.","mla":"Chatterjee, Krishnendu, et al. “Boosting Payment Channel Network Liquidity with Topology Optimization and Transaction Selection.” <i>39th International Symposium on Distributed Computing</i>, vol. 356, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.DISC.2025.23\">10.4230/LIPIcs.DISC.2025.23</a>.","ieee":"K. Chatterjee, J. M. Křišťan, S. Schmid, J. Svoboda, and M. X. Yeo, “Boosting payment channel network liquidity with topology optimization and transaction selection,” in <i>39th International Symposium on Distributed Computing</i>, Berlin, Germany, 2025, vol. 356.","apa":"Chatterjee, K., Křišťan, J. M., Schmid, S., Svoboda, J., &#38; Yeo, M. X. (2025). Boosting payment channel network liquidity with topology optimization and transaction selection. In <i>39th International Symposium on Distributed Computing</i> (Vol. 356). Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.DISC.2025.23\">https://doi.org/10.4230/LIPIcs.DISC.2025.23</a>","ista":"Chatterjee K, Křišťan JM, Schmid S, Svoboda J, Yeo MX. 2025. Boosting payment channel network liquidity with topology optimization and transaction selection. 39th International Symposium on Distributed Computing. DISC: Symposium on Distributed Computing, LIPIcs, vol. 356, 23."},"scopus_import":"1","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"10","publication_identifier":{"isbn":["9783959774024"],"issn":["1868-8969"]},"_id":"21412","date_created":"2026-03-08T23:01:46Z","doi":"10.4230/LIPIcs.DISC.2025.23","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2025/1484.pdf"}],"acknowledgement":"Chatterjee, Krishnendu: European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.\r\nKřišťan, Jan Matyáš: Czech Science Foundation Grant no. 24-12046S.\r\nSchmid, Stefan: German Research Foundation (DFG) project ReNO (SPP 2378) from 2023-2027.\r\nSvoboda, Jakub: European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.\r\nYeo, Michelle: MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms).","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"conference":{"start_date":"2025-10-27","end_date":"2025-10-31","location":"Berlin, Germany","name":"DISC: Symposium on Distributed Computing"},"external_id":{"arxiv":["2508.14524"]},"article_processing_charge":"No","arxiv":1,"article_number":"23","title":"Boosting payment channel network liquidity with topology optimization and transaction selection","file_date_updated":"2026-03-09T11:51:59Z","volume":356,"ec_funded":1,"alternative_title":["LIPIcs"],"publication":"39th International Symposium on Distributed Computing","abstract":[{"text":"Payment channel networks (PCNs) are a promising technology that alleviates blockchain scalability by shifting the transaction load from the blockchain to the PCN. Nevertheless, the network topology has to be carefully designed to maximise the transaction throughput in PCNs. Additionally, users in PCNs also have to make optimal decisions on which transactions to forward and which to reject to prolong the lifetime of their channels. In this work, we consider an input sequence of transactions over p parties. Each transaction consists of a transaction size, source, and target, and can be either accepted or rejected (entailing a cost). The goal is to design a PCN topology among the p cooperating parties, along with the channel capacities, and then output a decision for each transaction in the sequence to minimise the cost of creating and augmenting channels, as well as the cost of rejecting transactions. Our main contribution is an 𝒪(p) approximation algorithm for the problem with p parties. We further show that with some assumptions on the distribution of transactions, we can reduce the approximation ratio to 𝒪(√p). We complement our theoretical analysis with an empirical study of our assumptions and approach in the context of the Lightning Network.","lang":"eng"}],"file":[{"creator":"dernst","file_size":1130069,"date_updated":"2026-03-09T11:51:59Z","content_type":"application/pdf","checksum":"8e3d1594365df60163d9df22158a37b1","relation":"main_file","date_created":"2026-03-09T11:51:59Z","access_level":"open_access","success":1,"file_name":"2025_DISC_Chatterjee.pdf","file_id":"21418"}],"day":"22","year":"2025","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2026-03-09T11:52:58Z","publication_status":"published","status":"public","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"intvolume":"       356","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Křišťan","first_name":"Jan Matyáš","full_name":"Křišťan, Jan Matyáš"},{"first_name":"Stefan","last_name":"Schmid","full_name":"Schmid, Stefan"},{"last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub"},{"full_name":"Yeo, Michelle X","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","orcid":"0009-0001-3676-4809","first_name":"Michelle X","last_name":"Yeo"}],"ddc":["000"],"date_published":"2025-10-22T00:00:00Z","OA_type":"gold"},{"PlanS_conform":"1","day":"01","year":"2025","file":[{"file_id":"21417","file_name":"2026_TheoretiCS_Brazdil.pdf","success":1,"access_level":"open_access","date_created":"2026-03-09T11:39:59Z","checksum":"2ccf563ae577ee08d82baf752292ca7b","relation":"main_file","content_type":"application/pdf","date_updated":"2026-03-09T11:39:59Z","file_size":861607,"creator":"dernst"}],"publication_status":"published","status":"public","article_type":"original","publisher":"TheoretiCS Foundation","date_updated":"2026-03-09T11:43:38Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"intvolume":"         4","has_accepted_license":"1","ddc":["000"],"date_published":"2025-04-01T00:00:00Z","OA_type":"gold","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Forejt","first_name":"Vojtěch","full_name":"Forejt, Vojtěch"},{"first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Marta","last_name":"Kwiatkowska","full_name":"Kwiatkowska, Marta"},{"full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","first_name":"Tobias","last_name":"Meggendorfer"},{"full_name":"Parker, David","first_name":"David","last_name":"Parker"},{"last_name":"Ujma","first_name":"Mateusz","full_name":"Ujma, Mateusz"}],"quality_controlled":"1","language":[{"iso":"eng"}],"OA_place":"publisher","DOAJ_listed":"1","department":[{"_id":"KrCh"}],"oa_version":"Published Version","oa":1,"publication_identifier":{"eissn":["2751-4838"]},"_id":"21413","date_created":"2026-03-08T23:01:46Z","doi":"10.46298/theoretics.25.10","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.","citation":{"ieee":"T. Brázdil <i>et al.</i>, “Learning algorithms for verification of Markov decision processes,” <i>TheoretiCS</i>, vol. 4. TheoretiCS Foundation, 2025.","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>.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, T. Meggendorfer, D. Parker, M. Ujma, TheoretiCS 4 (2025).","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>.","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>","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.","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>"},"scopus_import":"1","type":"journal_article","month":"04","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"}],"article_processing_charge":"Yes","external_id":{"arxiv":["2403.09184"]},"file_date_updated":"2026-03-09T11:39:59Z","ec_funded":1,"volume":4,"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"}],"publication":"TheoretiCS","title":"Learning algorithms for verification of Markov decision processes","article_number":"10"},{"publication_status":"published","status":"public","date_updated":"2025-02-27T12:35:48Z","publisher":"IEEE","article_type":"original","year":"2025","day":"01","OA_type":"closed access","date_published":"2025-01-01T00:00:00Z","author":[{"first_name":"Yichao","last_name":"Zhang","full_name":"Zhang, Yichao"},{"first_name":"Jiasheng","last_name":"Wang","full_name":"Wang, Jiasheng"},{"first_name":"Guanghui","last_name":"Wen","full_name":"Wen, Guanghui"},{"full_name":"Guan, Jihong","last_name":"Guan","first_name":"Jihong"},{"last_name":"Zhou","first_name":"Shuigeng","full_name":"Zhou, Shuigeng"},{"last_name":"Chen","first_name":"Guanrong","full_name":"Chen, Guanrong"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Perc, Matjaz","last_name":"Perc","first_name":"Matjaz"}],"intvolume":"        12","isi":1,"_id":"18529","publication_identifier":{"eissn":["2327-4697"]},"date_created":"2024-11-10T23:02:00Z","doi":"10.1109/TNSE.2024.3481434","type":"journal_article","month":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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>","ista":"Zhang Y, Wang J, Wen G, Guan J, Zhou S, Chen G, Chatterjee K, Perc M. 2025. Limitation of time promotes cooperation in structured collaboration systems. IEEE Transactions on Network Science and Engineering. 12(1), 4–12.","chicago":"Zhang, Yichao, Jiasheng Wang, Guanghui Wen, Jihong Guan, Shuigeng Zhou, Guanrong Chen, Krishnendu Chatterjee, and Matjaz Perc. “Limitation of Time Promotes Cooperation in Structured Collaboration Systems.” <i>IEEE Transactions on Network Science and Engineering</i>. IEEE, 2025. <a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">https://doi.org/10.1109/TNSE.2024.3481434</a>.","ama":"Zhang Y, Wang J, Wen G, et al. Limitation of time promotes cooperation in structured collaboration systems. <i>IEEE Transactions on Network Science and Engineering</i>. 2025;12(1):4-12. doi:<a href=\"https://doi.org/10.1109/TNSE.2024.3481434\">10.1109/TNSE.2024.3481434</a>","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>.","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.","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."},"scopus_import":"1","quality_controlled":"1","language":[{"iso":"eng"}],"issue":"1","oa_version":"None","department":[{"_id":"KrCh"}],"volume":12,"publication":"IEEE Transactions on Network Science and Engineering","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"}],"title":"Limitation of time promotes cooperation in structured collaboration systems","external_id":{"isi":["001385382200040"]},"page":"4-12","article_processing_charge":"No"},{"author":[{"full_name":"Hübner, Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","orcid":"0009-0001-5009-4987","first_name":"Valentin","last_name":"Hübner"},{"first_name":"Christian","last_name":"Hilbe","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Staab, Manuel","first_name":"Manuel","last_name":"Staab"},{"id":"4E21749C-F248-11E8-B48F-1D18A9856A87","full_name":"Kleshnina, Maria","orcid":"0000-0002-5518-8317","last_name":"Kleshnina","first_name":"Maria"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"}],"corr_author":"1","OA_type":"hybrid","ddc":["000"],"date_published":"2025-11-01T00:00:00Z","has_accepted_license":"1","intvolume":"        15","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"isi":1,"date_updated":"2026-04-07T12:30:56Z","article_type":"original","publisher":"Springer Nature","status":"public","publication_status":"published","file":[{"date_updated":"2025-12-30T08:01:35Z","content_type":"application/pdf","file_size":1126178,"creator":"dernst","access_level":"open_access","date_created":"2025-12-30T08:01:35Z","relation":"main_file","checksum":"de0a412cbb7d98bf5e6a551c26acbefa","success":1,"file_id":"20888","file_name":"2025_DynGamesAppl_Huebner.pdf"}],"year":"2025","day":"01","PlanS_conform":"1","title":"Time-dependent strategies in repeated asymmetric public goods games","abstract":[{"lang":"eng","text":"The public goods game is among the most studied metaphors of cooperation in groups. In this game, individuals can use their endowments to make contributions towards a good that benefits everyone. Each individual, however, is tempted to free-ride on the contributions of others. Herein, we study repeated public goods games among asymmetric players. Previous work has explored to which extent asymmetry allows for full cooperation, such that players contribute their full endowment each round. However, by design that work focusses on equilibria where individuals make the same contribution each round. Instead, here we consider players whose contributions along the equilibrium path can change from one round to the next. We do so for three different models – one without any budget constraints, one with endowment constraints, and one in which individuals can save their current endowment to be used in subsequent rounds. In each case, we explore two key quantities: the welfare and the resource efficiency that can be achieved in equilibrium. Welfare corresponds to the sum of all players’ payoffs. Resource efficiency relates this welfare to the total contributions made by the players. Compared to constant contribution sequences, we find that time-dependent contributions can improve resource efficiency across all three models. Moreover, they can improve the players’ welfare in the model with savings."}],"publication":"Dynamic Games and Applications","ec_funded":1,"volume":15,"file_date_updated":"2025-12-30T08:01:35Z","article_processing_charge":"Yes (via OA deal)","page":"1617-1645","external_id":{"isi":["001415587800001"]},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"11","type":"journal_article","scopus_import":"1","citation":{"apa":"Hübner, V., Hilbe, C., Staab, M., Kleshnina, M., &#38; Chatterjee, K. (2025). Time-dependent strategies in repeated asymmetric public goods games. <i>Dynamic Games and Applications</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s13235-025-00627-5\">https://doi.org/10.1007/s13235-025-00627-5</a>","ista":"Hübner V, Hilbe C, Staab M, Kleshnina M, Chatterjee K. 2025. Time-dependent strategies in repeated asymmetric public goods games. Dynamic Games and Applications. 15, 1617–1645.","ama":"Hübner V, Hilbe C, Staab M, Kleshnina M, Chatterjee K. Time-dependent strategies in repeated asymmetric public goods games. <i>Dynamic Games and Applications</i>. 2025;15:1617-1645. doi:<a href=\"https://doi.org/10.1007/s13235-025-00627-5\">10.1007/s13235-025-00627-5</a>","chicago":"Hübner, Valentin, Christian Hilbe, Manuel Staab, Maria Kleshnina, and Krishnendu Chatterjee. “Time-Dependent Strategies in Repeated Asymmetric Public Goods Games.” <i>Dynamic Games and Applications</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s13235-025-00627-5\">https://doi.org/10.1007/s13235-025-00627-5</a>.","short":"V. Hübner, C. Hilbe, M. Staab, M. Kleshnina, K. Chatterjee, Dynamic Games and Applications 15 (2025) 1617–1645.","ieee":"V. Hübner, C. Hilbe, M. Staab, M. Kleshnina, and K. Chatterjee, “Time-dependent strategies in repeated asymmetric public goods games,” <i>Dynamic Games and Applications</i>, vol. 15. Springer Nature, pp. 1617–1645, 2025.","mla":"Hübner, Valentin, et al. “Time-Dependent Strategies in Repeated Asymmetric Public Goods Games.” <i>Dynamic Games and Applications</i>, vol. 15, Springer Nature, 2025, pp. 1617–45, doi:<a href=\"https://doi.org/10.1007/s13235-025-00627-5\">10.1007/s13235-025-00627-5</a>."},"acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.), the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement #754411 and the French Agence Nationale de la Recherche (under the Investissement d’Avenir programme, ANR-17-EURE-0010), and ARC SRIEAS Grant SR200100005 Securing Antarctica’s Environmental Future (to M.K.). Open access funding provided by Institute of Science and Technology (IST Austria).","date_created":"2025-02-23T23:01:57Z","doi":"10.1007/s13235-025-00627-5","related_material":{"record":[{"id":"19903","status":"public","relation":"dissertation_contains"}]},"_id":"19074","publication_identifier":{"issn":["2153-0785"],"eissn":["2153-0793"]},"oa_version":"Published Version","oa":1,"department":[{"_id":"KrCh"}],"OA_place":"publisher","language":[{"iso":"eng"}],"quality_controlled":"1"},{"intvolume":"       122","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"isi":1,"has_accepted_license":"1","OA_type":"hybrid","corr_author":"1","ddc":["000"],"date_published":"2025-03-25T00:00:00Z","author":[{"last_name":"Muroya Lei","first_name":"Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"}],"year":"2025","day":"25","file":[{"file_id":"19524","file_name":"2025_PNAS_Muroya.pdf","success":1,"access_level":"open_access","relation":"main_file","checksum":"83501b8a65ee5fdd3f5604fc28eddc22","date_created":"2025-04-07T11:42:22Z","file_size":6805668,"content_type":"application/pdf","date_updated":"2025-04-07T11:42:22Z","creator":"dernst"}],"publication_status":"published","pmid":1,"status":"public","date_updated":"2026-04-28T13:41:14Z","article_type":"original","publisher":"National Academy of Sciences","external_id":{"isi":["001459435600001"],"pmid":["40106357"]},"article_processing_charge":"Yes (in subscription journal)","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"volume":122,"ec_funded":1,"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."}],"publication":"Proceedings of the National Academy of Sciences","file_date_updated":"2025-04-07T11:42:22Z","article_number":"e2419273122","title":"Hardware-optimal quantum algorithms","OA_place":"publisher","quality_controlled":"1","language":[{"iso":"eng"}],"issue":"12","oa_version":"Published Version","oa":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"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.","_id":"19499","publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"related_material":{"link":[{"relation":"software","url":"https://github.com/smml1996/algorithm_synthesis"},{"url":"https://ista.ac.at/en/news/hardware-optimal-quantum-algorithms/","relation":"press_release","description":"News on ISTA website"}]},"doi":"10.1073/pnas.2419273122","date_created":"2025-04-06T22:01:32Z","type":"journal_article","month":"03","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","citation":{"ista":"Muroya Lei S, Chatterjee K, Henzinger TA. 2025. Hardware-optimal quantum algorithms. Proceedings of the National Academy of Sciences. 122(12), e2419273122.","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>","short":"S. Muroya Lei, K. Chatterjee, T.A. Henzinger, Proceedings of the National Academy of Sciences 122 (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>.","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.","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>","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>."},"scopus_import":"1"},{"arxiv":1,"page":"11158-11166","article_processing_charge":"No","external_id":{"arxiv":["2412.16226"]},"conference":{"end_date":"2025-03-04","start_date":"2025-02-25","location":"Philadelphia, PA, United States","name":"AAAI: Conference on Artificial Intelligence"},"project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"volume":39,"ec_funded":1,"abstract":[{"lang":"eng","text":"The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredient in our approach are Positivstellensätze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state of the art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks."}],"publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","title":"Quantified linear and polynomial arithmetic satisfiability via template-based skolemization","OA_place":"repository","quality_controlled":"1","language":[{"iso":"eng"}],"issue":"11","oa_version":"Preprint","oa":1,"department":[{"_id":"KrCh"}],"acknowledgement":"This work was partially funded by ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12.","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.16226"}],"_id":"19667","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"doi":"10.1609/aaai.v39i11.33213","date_created":"2025-05-11T22:02:39Z","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"04","citation":{"ista":"Chatterjee K, Goharshady E, Karrabi M, Motwani HJ, Seeliger M, Zikelic D. 2025. Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 11158–11166.","apa":"Chatterjee, K., Goharshady, E., Karrabi, M., Motwani, H. J., Seeliger, M., &#38; Zikelic, D. (2025). Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 11158–11166). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">https://doi.org/10.1609/aaai.v39i11.33213</a>","ieee":"K. Chatterjee, E. Goharshady, M. Karrabi, H. J. Motwani, M. Seeliger, and D. Zikelic, “Quantified linear and polynomial arithmetic satisfiability via template-based skolemization,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 11, pp. 11158–11166.","mla":"Chatterjee, Krishnendu, et al. “Quantified Linear and Polynomial Arithmetic Satisfiability via Template-Based Skolemization.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 11, Association for the Advancement of Artificial Intelligence, 2025, pp. 11158–66, doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">10.1609/aaai.v39i11.33213</a>.","short":"K. Chatterjee, E. Goharshady, M. Karrabi, H.J. Motwani, M. Seeliger, D. Zikelic, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 11158–11166.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Harshit J. Motwani, Maximilian Seeliger, and Dorde Zikelic. “Quantified Linear and Polynomial Arithmetic Satisfiability via Template-Based Skolemization.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:11158–66. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">https://doi.org/10.1609/aaai.v39i11.33213</a>.","ama":"Chatterjee K, Goharshady E, Karrabi M, Motwani HJ, Seeliger M, Zikelic D. Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:11158-11166. doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">10.1609/aaai.v39i11.33213</a>"},"scopus_import":"1","intvolume":"        39","OA_type":"green","corr_author":"1","date_published":"2025-04-11T00:00:00Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587","last_name":"Kafshdar Goharshadi","first_name":"Ehsan"},{"id":"67638922-f394-11eb-9cf6-f20423e08757","full_name":"Karrabi, Mehrdad","orcid":"0009-0007-5253-9170","last_name":"Karrabi","first_name":"Mehrdad"},{"first_name":"Harshit J.","last_name":"Motwani","full_name":"Motwani, Harshit J."},{"first_name":"Maximilian","last_name":"Seeliger","full_name":"Seeliger, Maximilian"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde"}],"year":"2025","day":"11","publication_status":"published","status":"public","date_updated":"2026-02-16T12:24:47Z","publisher":"Association for the Advancement of Artificial Intelligence"},{"date_published":"2025-04-11T00:00:00Z","OA_type":"green","corr_author":"1","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Luo","first_name":"Ruichen","id":"b391db08-1ffe-11ee-8b67-d18ddcfb5a14","full_name":"Luo, Ruichen"},{"first_name":"Raimundo J","last_name":"Saona Urmeneta","full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","orcid":"0000-0001-5103-038X"},{"first_name":"Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"}],"intvolume":"        39","publication_status":"published","status":"public","publisher":"Association for the Advancement of Artificial Intelligence","date_updated":"2025-05-12T09:42:09Z","day":"11","year":"2025","volume":39,"ec_funded":1,"abstract":[{"lang":"eng","text":"We consider a class of optimization problems defined by a system of linear equations with min and max operators. This class of optimization problems has been studied under restrictive conditions, such as, (C1) the halting or stability condition; (C2) the non-negative coefficients condition; (C3) the sum upto 1 condition; and (C4) the only min or only max operator condition. Several seminal results in the literature focus on special cases. For example, turn-based stochastic games correspond to conditions C2 and C3; and Markov decision process to conditions C2, C3, and C4. However, the systematic computational complexity study of all the cases has not been explored, which we address in this work. Some highlights of our results are: with conditions C2 and C4, and with conditions C3 and C4, the problem is NP-complete, whereas with condition C1 only, the problem is in UP intersects coUP. Finally, we establish the computational complexity of the decision problem of checking the respective conditions."}],"publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","title":"Linear equations with min and max operators: Computational complexity","arxiv":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"external_id":{"arxiv":["2412.12228"]},"article_processing_charge":"No","conference":{"name":"AAAI: Conference on Artificial Intelligence","location":"Philadelphia, PA, United States","start_date":"2025-02-25","end_date":"2025-03-04"},"page":"11150-11157","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"_id":"19669","doi":"10.1609/aaai.v39i11.33212","date_created":"2025-05-11T22:02:40Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.12228"}],"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and the Austrian Science Fund (FWF) 10.55776/COE12 grant.","citation":{"ista":"Chatterjee K, Luo R, Saona Urmeneta RJ, Svoboda J. 2025. Linear equations with min and max operators: Computational complexity. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 11150–11157.","apa":"Chatterjee, K., Luo, R., Saona Urmeneta, R. J., &#38; Svoboda, J. (2025). Linear equations with min and max operators: Computational complexity. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 11150–11157). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i11.33212\">https://doi.org/10.1609/aaai.v39i11.33212</a>","short":"K. Chatterjee, R. Luo, R.J. Saona Urmeneta, J. Svoboda, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 11150–11157.","mla":"Chatterjee, Krishnendu, et al. “Linear Equations with Min and Max Operators: Computational Complexity.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 11, Association for the Advancement of Artificial Intelligence, 2025, pp. 11150–57, doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33212\">10.1609/aaai.v39i11.33212</a>.","ieee":"K. Chatterjee, R. Luo, R. J. Saona Urmeneta, and J. Svoboda, “Linear equations with min and max operators: Computational complexity,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 11, pp. 11150–11157.","ama":"Chatterjee K, Luo R, Saona Urmeneta RJ, Svoboda J. Linear equations with min and max operators: Computational complexity. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:11150-11157. doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33212\">10.1609/aaai.v39i11.33212</a>","chicago":"Chatterjee, Krishnendu, Ruichen Luo, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Linear Equations with Min and Max Operators: Computational Complexity.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:11150–57. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i11.33212\">https://doi.org/10.1609/aaai.v39i11.33212</a>."},"scopus_import":"1","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"04","quality_controlled":"1","language":[{"iso":"eng"}],"issue":"11","OA_place":"repository","department":[{"_id":"KrCh"}],"oa_version":"Preprint","oa":1},{"has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"intvolume":"     15697","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Jafariraviz, Mahdi","first_name":"Mahdi","last_name":"Jafariraviz"},{"first_name":"Raimundo J","last_name":"Saona Urmeneta","full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","orcid":"0000-0001-5103-038X"},{"last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub"}],"ddc":["000"],"date_published":"2025-05-01T00:00:00Z","corr_author":"1","OA_type":"hybrid","file":[{"date_updated":"2025-06-02T07:31:12Z","content_type":"application/pdf","file_size":557481,"creator":"dernst","access_level":"open_access","checksum":"45da6efbcbed20aada16c48c8e55e2d6","relation":"main_file","date_created":"2025-06-02T07:31:12Z","success":1,"file_id":"19767","file_name":"2025_TACAS_Chatterjee.pdf"}],"day":"01","year":"2025","publisher":"Springer Nature","date_updated":"2025-06-02T07:35:06Z","publication_status":"published","status":"public","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"page":"217-236","external_id":{"arxiv":["2505.06769"]},"conference":{"location":"Hamilton, ON, Canada","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2025-05-08","start_date":"2025-05-03"},"article_processing_charge":"No","arxiv":1,"title":"Value iteration with guessing for Markov chains and Markov decision processes","file_date_updated":"2025-06-02T07:31:12Z","volume":15697,"ec_funded":1,"alternative_title":["LNCS"],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","abstract":[{"text":"Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.","lang":"eng"}],"department":[{"_id":"KrCh"}],"oa":1,"oa_version":"Published Version","quality_controlled":"1","language":[{"iso":"eng"}],"OA_place":"publisher","citation":{"chicago":"Chatterjee, Krishnendu, Mahdi Jafariraviz, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Value Iteration with Guessing for Markov Chains and Markov Decision Processes.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:217–36. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">https://doi.org/10.1007/978-3-031-90653-4_11</a>.","ama":"Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. Value iteration with guessing for Markov chains and Markov decision processes. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:217-236. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">10.1007/978-3-031-90653-4_11</a>","ieee":"K. Chatterjee, M. Jafariraviz, R. J. Saona Urmeneta, and J. Svoboda, “Value iteration with guessing for Markov chains and Markov decision processes,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 217–236.","mla":"Chatterjee, Krishnendu, et al. “Value Iteration with Guessing for Markov Chains and Markov Decision Processes.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 217–36, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">10.1007/978-3-031-90653-4_11</a>.","short":"K. Chatterjee, M. Jafariraviz, R.J. Saona Urmeneta, J. Svoboda, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 217–236.","apa":"Chatterjee, K., Jafariraviz, M., Saona Urmeneta, R. J., &#38; Svoboda, J. (2025). Value iteration with guessing for Markov chains and Markov decision processes. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 217–236). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">https://doi.org/10.1007/978-3-031-90653-4_11</a>","ista":"Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. 2025. Value iteration with guessing for Markov chains and Markov decision processes. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 217–236."},"scopus_import":"1","type":"conference","month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"19740","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031906527"]},"doi":"10.1007/978-3-031-90653-4_11","date_created":"2025-05-25T22:17:06Z","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and Austrian Science Fund (FWF) 10.55776/COE12 grant."},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"intvolume":"     15697","has_accepted_license":"1","ddc":["000"],"date_published":"2025-05-01T00:00:00Z","corr_author":"1","OA_type":"hybrid","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Tim","last_name":"Quatmann","full_name":"Quatmann, Tim"},{"last_name":"Schäffeler","first_name":"Maximilian","full_name":"Schäffeler, Maximilian"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian"},{"last_name":"Winkler","first_name":"Tobias","full_name":"Winkler, Tobias"},{"id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3","full_name":"Zilken, Daniel","last_name":"Zilken","first_name":"Daniel"}],"day":"01","year":"2025","file":[{"success":1,"file_id":"19772","file_name":"2025_TACAS_ChatterjeeKrish.pdf","file_size":732136,"content_type":"application/pdf","date_updated":"2025-06-02T10:49:52Z","creator":"dernst","access_level":"open_access","checksum":"64b7f46ef05649b87b827248045c7645","date_created":"2025-06-02T10:49:52Z","relation":"main_file"}],"publication_status":"published","status":"public","publisher":"Springer Nature","date_updated":"2025-06-02T10:55:34Z","arxiv":1,"project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413"}],"external_id":{"arxiv":["2501.11467"]},"page":"130-151","article_processing_charge":"No","conference":{"location":"Hamilton, ON, Canada","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2025-05-03","end_date":"2025-05-08"},"file_date_updated":"2025-06-02T10:49:52Z","ec_funded":1,"alternative_title":["LNCS"],"volume":15697,"abstract":[{"text":"The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates—lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.","lang":"eng"}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","title":"Fixed point certificates for reachability and expected rewards in MDPs","language":[{"iso":"eng"}],"quality_controlled":"1","OA_place":"publisher","department":[{"_id":"KrCh"}],"oa_version":"Published Version","oa":1,"_id":"19743","publication_identifier":{"isbn":["9783031906527"],"issn":["0302-9743"],"eissn":["1611-3349"]},"related_material":{"record":[{"status":"public","relation":"research_data","id":"19771"}]},"date_created":"2025-05-25T22:17:09Z","doi":"10.1007/978-3-031-90653-4_7","acknowledgement":"This project has received funding from the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12, a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, the DFG RTG 378803395 (ConVeY), the EU’s Horizon 2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement Nos. 101034413 (IST-BRIDGE) and 101008233 (MISSION), and the DFG RTG 2236 (UnRAVeL). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632.","citation":{"chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:130–51. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>.","ama":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. Fixed point certificates for reachability and expected rewards in MDPs. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:130-151. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>","mla":"Chatterjee, Krishnendu, et al. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 130–51, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>.","ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Fixed point certificates for reachability and expected rewards in MDPs,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 130–151.","short":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 130–151.","apa":"Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., &#38; Zilken, D. (2025). Fixed point certificates for reachability and expected rewards in MDPs. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 130–151). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>","ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Fixed point certificates for reachability and expected rewards in MDPs. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 130–151."},"scopus_import":"1","type":"conference","month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"abstract":[{"lang":"eng","text":"We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature."}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","ec_funded":1,"alternative_title":["LNCS"],"volume":15697,"file_date_updated":"2025-06-02T11:13:49Z","title":"Refuting equivalence in probabilistic programs with conditioning","arxiv":1,"article_processing_charge":"No","external_id":{"arxiv":["2501.06579"]},"page":"279-300","conference":{"end_date":"2025-05-08","start_date":"2025-05-03","location":"Hamilton, ON, Canada","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"acknowledgement":"This work was partially supported by ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12. Petr Novotný is supported by the Czech Science Foundation grant no. GA23-06963S.","doi":"10.1007/978-3-031-90653-4_14","date_created":"2025-05-25T22:17:10Z","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031906527"]},"_id":"19744","month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","scopus_import":"1","citation":{"ista":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2025. Refuting equivalence in probabilistic programs with conditioning. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 279–300.","apa":"Chatterjee, K., Goharshady, E., Novotný, P., &#38; Zikelic, D. (2025). Refuting equivalence in probabilistic programs with conditioning. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 279–300). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">https://doi.org/10.1007/978-3-031-90653-4_14</a>","mla":"Chatterjee, Krishnendu, et al. “Refuting Equivalence in Probabilistic Programs with Conditioning.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 279–300, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Refuting equivalence in probabilistic programs with conditioning,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 279–300.","short":"K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 279–300.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Refuting Equivalence in Probabilistic Programs with Conditioning.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:279–300. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">https://doi.org/10.1007/978-3-031-90653-4_14</a>.","ama":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. Refuting equivalence in probabilistic programs with conditioning. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:279-300. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>"},"OA_place":"publisher","quality_controlled":"1","language":[{"iso":"eng"}],"oa":1,"oa_version":"Published Version","department":[{"_id":"KrCh"}],"OA_type":"hybrid","corr_author":"1","ddc":["000"],"date_published":"2025-05-01T00:00:00Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587"},{"full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotný"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic"}],"intvolume":"     15697","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"has_accepted_license":"1","status":"public","publication_status":"published","date_updated":"2025-06-02T11:16:13Z","publisher":"Springer Nature","year":"2025","day":"01","file":[{"creator":"dernst","date_updated":"2025-06-02T11:13:49Z","content_type":"application/pdf","file_size":532181,"date_created":"2025-06-02T11:13:49Z","checksum":"7dcd85e7e753bfa994c10b3cf9ebc185","relation":"main_file","access_level":"open_access","success":1,"file_name":"2025_TACAS_Chatterjee_Goharshadi.pdf","file_id":"19773"}]},{"main_file_link":[{"url":"https://doi.org/10.5281/ZENODO.14626585","open_access":"1"}],"_id":"19771","related_material":{"record":[{"id":"19743","relation":"used_in_publication","status":"public"}]},"status":"public","date_created":"2025-06-02T10:13:24Z","doi":"10.5281/ZENODO.14626585","type":"research_data_reference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","date_updated":"2025-06-02T10:55:35Z","citation":{"ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Artifact: Fixed point certificates for reachability and expected rewards in MDPs, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>.","apa":"Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., &#38; Zilken, D. (2025). Artifact: Fixed point certificates for reachability and expected rewards in MDPs. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.14626585\">https://doi.org/10.5281/ZENODO.14626585</a>","short":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken, (2025).","ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Artifact: Fixed point certificates for reachability and expected rewards in MDPs.” Zenodo, 2025.","mla":"Chatterjee, Krishnendu, et al. <i>Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs</i>. Zenodo, 2025, doi:<a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>.","ama":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. Artifact: Fixed point certificates for reachability and expected rewards in MDPs. 2025. doi:<a href=\"https://doi.org/10.5281/ZENODO.14626585\">10.5281/ZENODO.14626585</a>","chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” Zenodo, 2025. <a href=\"https://doi.org/10.5281/ZENODO.14626585\">https://doi.org/10.5281/ZENODO.14626585</a>."},"publisher":"Zenodo","OA_place":"repository","year":"2025","day":"09","oa":1,"oa_version":"Published Version","department":[{"_id":"KrCh"}],"OA_type":"green","abstract":[{"lang":"eng","text":"This artifact allows to review and reproduce the Isabelle proofs and practical experiments from the paper *Fixed Point Certificates for Reachability and Expected Rewards in MDPs*.\r\nThe contents are two-fold:\r\nFirst, the artifact contains a formally verified certificate checker for the certificates presented in the paper.\r\nThe formal Isabelle/HOL proofs of the background theory can be inspected, checked by Isabelle and the code extraction can be retraced.\r\n\r\nSecond, the artifact contains a modified version of the model checking tool `Storm` with support for certificate generation. Together with the provided scripts and benchmark files, this allows to reproduce the experiments from the paper.\r\nAn appropriate subset of the experiments is given to allow a review in a timely manner. In addition, original logfiles from our experiments are provided, allowing a detailed inspection.\r\n\r\nThe package includes convenient installation scripts for [the TACAS 2023 VM](https://doi.org/10.5281/zenodo.7113223) (based on Ubuntu 22.04).\r\nA native installation on Linux or macOS systems (including the newer ARM-based machines) is also possible."}],"ddc":["000"],"date_published":"2025-01-09T00:00:00Z","title":"Artifact: Fixed point certificates for reachability and expected rewards in MDPs","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Quatmann, Tim","first_name":"Tim","last_name":"Quatmann"},{"full_name":"Schäffeler, Maximilian","first_name":"Maximilian","last_name":"Schäffeler"},{"full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","last_name":"Weininger"},{"first_name":"Tobias","last_name":"Winkler","full_name":"Winkler, Tobias"},{"id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3","full_name":"Zilken, Daniel","last_name":"Zilken","first_name":"Daniel"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"article_processing_charge":"No"},{"year":"2025","day":"01","file":[{"file_name":"2025_PNASNexus_Huebner.pdf","file_id":"19867","success":1,"date_created":"2025-06-23T08:09:50Z","checksum":"efd6648db3fc3ea0cdd7155d667e5f11","relation":"main_file","access_level":"open_access","creator":"dernst","file_size":2551195,"content_type":"application/pdf","date_updated":"2025-06-23T08:09:50Z"}],"status":"public","publication_status":"published","pmid":1,"date_updated":"2026-04-07T12:30:56Z","publisher":"Oxford University Press","article_type":"original","intvolume":"         4","tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","short":"CC BY-NC (4.0)","image":"/images/cc_by_nc.png","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode"},"has_accepted_license":"1","corr_author":"1","OA_type":"gold","date_published":"2025-05-01T00:00:00Z","ddc":["000"],"author":[{"last_name":"Hübner","first_name":"Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","full_name":"Hübner, Valentin","orcid":"0009-0001-5009-4987"},{"first_name":"Laura","last_name":"Schmid","full_name":"Schmid, Laura","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6978-7329"},{"last_name":"Hilbe","first_name":"Christian","orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian"},{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"}],"OA_place":"publisher","issue":"5","quality_controlled":"1","language":[{"iso":"eng"}],"oa_version":"Published Version","oa":1,"department":[{"_id":"KrCh"}],"DOAJ_listed":"1","acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.).","date_created":"2025-06-15T22:01:30Z","doi":"10.1093/pnasnexus/pgaf154","related_material":{"record":[{"id":"19903","status":"public","relation":"dissertation_contains"}]},"_id":"19843","publication_identifier":{"eissn":["2752-6542"]},"month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","scopus_import":"1","citation":{"apa":"Hübner, V., Schmid, L., Hilbe, C., &#38; Chatterjee, K. (2025). Stable strategies of direct and indirect reciprocity across all social dilemmas. <i>PNAS Nexus</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/pnasnexus/pgaf154\">https://doi.org/10.1093/pnasnexus/pgaf154</a>","ista":"Hübner V, Schmid L, Hilbe C, Chatterjee K. 2025. Stable strategies of direct and indirect reciprocity across all social dilemmas. PNAS Nexus. 4(5), pgaf154.","chicago":"Hübner, Valentin, Laura Schmid, Christian Hilbe, and Krishnendu Chatterjee. “Stable Strategies of Direct and Indirect Reciprocity across All Social Dilemmas.” <i>PNAS Nexus</i>. Oxford University Press, 2025. <a href=\"https://doi.org/10.1093/pnasnexus/pgaf154\">https://doi.org/10.1093/pnasnexus/pgaf154</a>.","ama":"Hübner V, Schmid L, Hilbe C, Chatterjee K. Stable strategies of direct and indirect reciprocity across all social dilemmas. <i>PNAS Nexus</i>. 2025;4(5). doi:<a href=\"https://doi.org/10.1093/pnasnexus/pgaf154\">10.1093/pnasnexus/pgaf154</a>","mla":"Hübner, Valentin, et al. “Stable Strategies of Direct and Indirect Reciprocity across All Social Dilemmas.” <i>PNAS Nexus</i>, vol. 4, no. 5, pgaf154, Oxford University Press, 2025, doi:<a href=\"https://doi.org/10.1093/pnasnexus/pgaf154\">10.1093/pnasnexus/pgaf154</a>.","ieee":"V. Hübner, L. Schmid, C. Hilbe, and K. Chatterjee, “Stable strategies of direct and indirect reciprocity across all social dilemmas,” <i>PNAS Nexus</i>, vol. 4, no. 5. Oxford University Press, 2025.","short":"V. Hübner, L. Schmid, C. Hilbe, K. Chatterjee, PNAS Nexus 4 (2025)."},"external_id":{"pmid":["40417077"]},"article_processing_charge":"Yes","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"publication":"PNAS Nexus","abstract":[{"lang":"eng","text":"Social dilemmas are collective-action problems where individual interests are at odds with group interests. Such dilemmas occur frequently at all scales of human interactions. When dealing with collective-action problems, people often act reciprocally. They adjust their behavior to match the previous behavior of the recipient. The literature distinguishes two kinds of reciprocity. According to direct reciprocity, individuals react to their immediate experiences with the recipient. They are more likely to cooperate if the recipient previously cooperated with them. According to indirect reciprocity, individuals react to the recipient’s general behavior, irrespectively of whether or not they benefited directly. In practice, the two kinds of reciprocity are often intertwined; people typically base their decisions on both direct experiences and indirect observations. Yet only recently have researchers begun to explore how the two kinds of reciprocity interact. So far, this research only addresses a single type of social dilemma, the donation game, where the effects of individual behaviors are independent. Instead, here we allow for all pairwise social dilemmas. By applying novel techniques to generalize the theory of zero-determinant strategies, we establish an important proof of principle: In all social dilemmas, socially optimal outcomes can be sustained as an equilibrium, using either direct or indirect reciprocity, or arbitrary mixtures thereof. These results neither require games to be repeated infinitely often, nor that individual opinions are synchronized. In this way, we considerably generalize the scope of models of reciprocity, and we build further bridges between the literatures on direct and indirect reciprocity."}],"ec_funded":1,"volume":4,"file_date_updated":"2025-06-23T08:09:50Z","article_number":"pgaf154","title":"Stable strategies of direct and indirect reciprocity across all social dilemmas"}]
