[{"status":"public","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"date_published":"2026-03-14T00:00:00Z","acknowledgement":"This work was supported by ERC CoG 863818 (ForMSMArt) and Austrian Science Fund (FWF) 10.55776/COE12. We also thank Hossein Zakerinia for his helpful feedback.","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."}],"_id":"21717","type":"conference","date_created":"2026-04-12T22:01:50Z","citation":{"ieee":"A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, and A. Shafiee, “Qualitative analysis of ω-regular objectives on robust MDPs,” in <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36137–36145.","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.","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>","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>.","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."},"scopus_import":"1","issue":"43","title":"Qualitative analysis of ω-regular objectives on robust MDPs","day":"14","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"oa":1,"fulldoi":"https://doi.org/10.1609/aaai.v40i43.40931","arxiv":1,"article_processing_charge":"No","doi":"10.1609/aaai.v40i43.40931","OA_type":"green","intvolume":"        40","publication_status":"published","month":"03","conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2026-01-20","end_date":"2026-01-27","location":"Singapore, Singapore"},"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"ec_funded":1,"language":[{"iso":"eng"}],"author":[{"last_name":"Asadi","first_name":"Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","full_name":"Asadi, Ali"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587","last_name":"Kafshdar Goharshadi","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"full_name":"Karrabi, Mehrdad","last_name":"Karrabi","first_name":"Mehrdad","orcid":"0009-0007-5253-9170","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"first_name":"Ali","last_name":"Shafiee","id":"2783031a-7378-11f0-b2d0-f17f1db2ebad","full_name":"Shafiee, Ali"}],"year":"2026","volume":40,"external_id":{"arxiv":["2505.04539"]},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.04539"}],"page":"36137-36145","OA_place":"repository","quality_controlled":"1","date_updated":"2026-09-16T07:27:43Z","oa_version":"Preprint","publisher":"Association for the Advancement of Artificial Intelligence","publication":"Proceedings of the 40th AAAI Conference on Artificial Intelligence"},{"OA_type":"green","month":"03","intvolume":"        40","publication_status":"published","conference":{"location":"Singapore, Singapore","start_date":"2026-01-20","name":"AAAI: Conference on Artificial Intelligence","end_date":"2026-01-27"},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)"}],"ec_funded":1,"language":[{"iso":"eng"}],"author":[{"full_name":"Asadi, Ali","first_name":"Ali","last_name":"Asadi","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Lurie","first_name":"David","id":"579a6c20-34cf-11f1-acbd-8c2f19cdb4da","full_name":"Lurie, David"},{"id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","last_name":"Saona Urmeneta","first_name":"Raimundo J","orcid":"0000-0001-5103-038X","full_name":"Saona Urmeneta, Raimundo J"}],"oa":1,"publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"corr_author":"1","fulldoi":"https://doi.org/10.1609/aaai.v40i43.40932","arxiv":1,"article_processing_charge":"No","doi":"10.1609/aaai.v40i43.40932","OA_place":"repository","date_updated":"2026-09-16T07:28:33Z","quality_controlled":"1","oa_version":"Preprint","publisher":"Association for the Advancement of Artificial Intelligence","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","year":"2026","page":"36146-36154","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2511.13134","open_access":"1"}],"volume":40,"external_id":{"arxiv":["2511.13134"]},"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.","abstract":[{"text":"Partially observable Markov decision processes (POMDPs) are a central model for uncertainty in sequential decision making. The most basic objective is the reachability objective, where a target set must be eventually visited, and the more general parity objectives can model all omega-regular specifications. For such objectives, the computational analysis problems are the following: (a) qualitative analysis that asks whether the objective can be satisfied with probability 1 (almost-sure winning) or probability arbitrarily close to 1 (limit-sure winning); and (b) quantitative analysis that asks for the approximation of the optimal probability of satisfying the objective. For general POMDPs, almost-sure analysis for reachability objectives is EXPTIME-complete, but limit-sure and quantitative analyses for reachability objectives are undecidable; almost-sure, limit-sure, and quantitative analyses for parity objectives are all undecidable. A special class of POMDPs, called revealing POMDPs, has been studied recently in several works, and for this subclass the almost-sure analysis for parity objectives was shown to be EXPTIME-complete. In this work, we show that for revealing POMDPs the limit-sure analysis for parity objectives is EXPTIME-complete, and even the quantitative analysis for parity objectives can be achieved in EXPTIME.","lang":"eng"}],"_id":"21722","status":"public","department":[{"_id":"KrCh"}],"date_published":"2026-03-14T00:00:00Z","scopus_import":"1","issue":"43","title":"Revealing POMDPs: Qualitative and quantitative analysis for parity objectives","day":"14","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","date_created":"2026-04-12T22:01:52Z","citation":{"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>.","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.","apa":"Asadi, A., Chatterjee, K., Lurie, D., &#38; Saona Urmeneta, R. J. (2026). Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 40, pp. 36146–36154). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">https://doi.org/10.1609/aaai.v40i43.40932</a>","ama":"Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 40. Association for the Advancement of Artificial Intelligence; 2026:36146-36154. doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40932\">10.1609/aaai.v40i43.40932</a>","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>.","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."}},{"article_number":"218","status":"public","keyword":["Static Program Analysis","Differential Privacy","Probabilistic Programming","Martingales"],"date_published":"2026-06-08T00:00:00Z","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.","has_accepted_license":"1","file_date_updated":"2026-06-24T06:19:56Z","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."}],"_id":"22102","researchdata_availability":"yes","type":"journal_article","das_tickbox":"1","citation":{"mla":"Chatterjee, Krishnendu, et al. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, no. PLDI, 218, ACM, 2026, doi:<a href=\"https://doi.org/10.1145/3808296\">10.1145/3808296</a>.","short":"K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming Languages 10 (2026).","ieee":"K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential privacy refutation via supermartingales,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, no. PLDI. ACM, 2026.","apa":"Chatterjee, K., Goharshady, E., &#38; Zikelic, D. (2026). SuperDP: Differential privacy refutation via supermartingales. <i>Proceedings of the ACM on Programming Languages</i>. ACM. <a href=\"https://doi.org/10.1145/3808296\">https://doi.org/10.1145/3808296</a>","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>. ACM, 2026. <a href=\"https://doi.org/10.1145/3808296\">https://doi.org/10.1145/3808296</a>.","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>","ista":"Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 10(PLDI), 218."},"date_created":"2026-06-21T22:02:59Z","issue":"PLDI","scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"SuperDP: Differential privacy refutation via supermartingales","day":"08","fulldoi":"https://doi.org/10.1145/3808296","corr_author":"1","article_processing_charge":"Yes","arxiv":1,"PlanS_conform":"1","oa":1,"publication_identifier":{"eissn":["2475-1421"]},"doi":"10.1145/3808296","OA_type":"gold","ddc":["000"],"publication_status":"published","article_type":"original","intvolume":"        10","month":"06","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587","last_name":"Kafshdar Goharshadi","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"ec_funded":1,"language":[{"iso":"eng"}],"year":"2026","file":[{"date_created":"2026-06-24T06:19:56Z","file_name":"2026_ProcACMProgrammingLanguages_Chatterjee.pdf","access_level":"open_access","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_id":"22135","checksum":"994bf21d6269dabccf1e1091e02962c5","success":1,"file_size":858595,"date_updated":"2026-06-24T06:19:56Z"}],"external_id":{"arxiv":["2603.26215"]},"volume":10,"supplementarymaterial":"no","quality_controlled":"1","date_updated":"2026-09-16T07:36:14Z","OA_place":"publisher","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.","oa_version":"Published Version","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"},"publisher":"ACM","publication":"Proceedings of the ACM on Programming Languages","related_material":{"record":[{"id":"22134","relation":"research_data","status":"public"}]}},{"scopus_import":"1","title":"The effect of the fitness gradient on fixation probability","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","das_tickbox":"1","type":"journal_article","date_created":"2026-06-21T22:02:59Z","citation":{"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>.","short":"J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, K. Chatterjee, Nature Communications 17 (2026).","ieee":"J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, and K. Chatterjee, “The effect of the fitness gradient on fixation probability,” <i>Nature Communications</i>, vol. 17. Springer Nature, 2026.","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>","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>","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."},"has_accepted_license":"1","DOAJ_listed":"1","file_date_updated":"2026-06-24T06:50:24Z","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.","researchdata_availability":"no","_id":"22101","abstract":[{"lang":"eng","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."}],"status":"public","article_number":"5325","department":[{"_id":"KrCh"}],"date_published":"2026-12-01T00:00:00Z","OA_place":"publisher","date_updated":"2026-09-16T07:36:49Z","quality_controlled":"1","dataavailabilitystatement":"Correspondence and requests for materials should be addressed to Krishnendu Chatterjee.","oa_version":"Published Version","supplementarymaterial":"yes","publication":"Nature Communications","publisher":"Springer Nature","tmp":{"short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"year":"2026","volume":17,"file":[{"date_created":"2026-06-24T06:50:24Z","file_name":"2026_NatureComm_Svoboda.pdf","relation":"main_file","content_type":"application/pdf","creator":"dernst","access_level":"open_access","success":1,"checksum":"b660048bb271f24d6763803e247d5c32","file_id":"22136","file_size":1068919,"date_updated":"2026-06-24T06:50:24Z"}],"external_id":{"pmid":["41997932"]},"OA_type":"gold","intvolume":"        17","article_type":"original","ddc":["000"],"publication_status":"published","month":"12","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"}],"ec_funded":1,"language":[{"iso":"eng"}],"author":[{"full_name":"Svoboda, Jakub","first_name":"Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"},{"full_name":"Nemati, Hossein","last_name":"Nemati","first_name":"Hossein"},{"full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Kamran","last_name":"Kaveh","full_name":"Kaveh, Kamran"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"pmid":1,"publication_identifier":{"eissn":["2041-1723"]},"oa":1,"corr_author":"1","fulldoi":"https://doi.org/10.1038/s41467-026-71777-2","article_processing_charge":"Yes","doi":"10.1038/s41467-026-71777-2"},{"keyword":["Bidding Games","Stochastic Games"],"status":"public","article_number":"13:1-13:20","department":[{"_id":"GradSch"},{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2026-08-24T00:00:00Z","has_accepted_license":"1","file_date_updated":"2026-09-17T09:43:28Z","acknowledgement":"The research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), ERC-2020-AdG 101020093\r\n(VAMOS), and the RYC2024-049116-I grant funded by MICIU/AEI/10.13039/501100011033 and\r\nESF+.\r\n","_id":"22920","abstract":[{"lang":"eng","text":"Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the right to move the token is determined by the current vertex. In traditional bidding games - referred to as pure bidding games - the right to move the token is determined at each step through bidding; here we consider Richman bidding, where the winning player of a bid pays the losing player. The winner is decided based on a temporal or quantitative specification evaluated over the resulting infinite play.\r\nIn this work, we combine turn-based games and pure bidding games into generalized bidding games, with player-1 vertices, player-2 vertices, and bidding vertices. This natural and simple generalization of bidding games has far-reaching consequences. First, we show that, as a model, generalized bidding games are more expressive than pure bidding games, and we provide several applications. Second, and most importantly, we show that generalized Richman bidding games are structurally equivalent to simple stochastic games, a well-studied model: they are linearly interreducible to each other. As was previously known, the special case of pure Richman bidding games corresponds to random-turn games. In other words, generalized bidding games extend pure bidding games in the same way that simple stochastic games extend random-turn games. We use this connection to solve generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff and discounted-sum) specifications. From a computational perspective, we establish that generalized bidding games with parity and mean-payoff specifications retain the best known upper bounds for turn-based games and pure bidding games, namely NP∩coNP.\r\nFinally, we study a repair problem that asks whether bidding vertices can be assigned \"owners\" so as to bring the threshold budget required to win the game below a given target. This problem has direct applications in compositional policy synthesis for multi-objective settings, and we show it to be NP-complete."}],"researchdata_availability":"no","das_tickbox":"0","type":"conference","date_created":"2026-09-13T22:01:53Z","citation":{"ieee":"A. Asadi, T. A. Henzinger, E. Goharshady, P. Kebis, and K. Mallik, “Generalized bidding games: Where bidding and stochastic games meet,” in <i>37th International Conference on Concurrency Theory</i>, Liverpool, United Kingdom, 2026, vol. 391.","short":"A. Asadi, T.A. Henzinger, E. Goharshady, P. Kebis, K. Mallik, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","apa":"Asadi, A., Henzinger, T. A., Goharshady, E., Kebis, P., &#38; Mallik, K. (2026). Generalized bidding games: Where bidding and stochastic games meet. In <i>37th International Conference on Concurrency Theory</i> (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.13</a>","mla":"Asadi, Ali, et al. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.” <i>37th International Conference on Concurrency Theory</i>, vol. 391, 13:1-13:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">10.4230/LIPIcs.CONCUR.2026.13</a>.","ista":"Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. 2026. Generalized bidding games: Where bidding and stochastic games meet. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 13:1-13:20.","ama":"Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. Generalized bidding games: Where bidding and stochastic games meet. In: <i>37th International Conference on Concurrency Theory</i>. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">10.4230/LIPIcs.CONCUR.2026.13</a>","chicago":"Asadi, Ali, Thomas A Henzinger, Ehsan Goharshady, Pavol Kebis, and Kaushik Mallik. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.” In <i>37th International Conference on Concurrency Theory</i>, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.13</a>."},"scopus_import":"1","day":"24","title":"Generalized bidding games: Where bidding and stochastic games meet","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LIPIcs"],"publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959774475"]},"oa":1,"article_processing_charge":"Yes","arxiv":1,"corr_author":"1","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13","doi":"10.4230/LIPIcs.CONCUR.2026.13","ddc":["000"],"intvolume":"       391","month":"08","publication_status":"published","OA_type":"gold","conference":{"location":"Liverpool, United Kingdom","name":"CONCUR: Conference on Concurrency Theory","start_date":"2026-09-01","end_date":"2026-09-04"},"language":[{"iso":"eng"}],"ec_funded":1,"project":[{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"author":[{"id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","last_name":"Asadi","first_name":"Ali","full_name":"Asadi, Ali"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","last_name":"Kafshdar Goharshadi","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan"},{"full_name":"Kebis, Pavol","last_name":"Kebis","first_name":"Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik"}],"year":"2026","file":[{"success":1,"checksum":"de9af748d78fa42c173f68a71cbbd8d9","file_id":"22946","file_size":1175682,"date_updated":"2026-09-17T09:43:28Z","date_created":"2026-09-17T09:43:28Z","file_name":"2026_LIPIcsCONCUR_Asadi.pdf","creator":"dernst","relation":"main_file","content_type":"application/pdf","access_level":"open_access"}],"external_id":{"arxiv":["2606.29420"]},"volume":391,"oa_version":"Published Version","quality_controlled":"1","date_updated":"2026-09-17T09:44:41Z","OA_place":"publisher","supplementarymaterial":"yes","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication":"37th International Conference on Concurrency Theory","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"}},{"file_date_updated":"2026-09-17T09:50:00Z","has_accepted_license":"1","acknowledgement":"The research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), and ERC-2020-AdG 101020093\r\n(VAMOS) grants.","researchdata_availability":"no","_id":"22919","abstract":[{"text":"Reachability is the most fundamental logical objective, yet it is notoriously difficult to learn in reinforcement learning settings: even for Markov decision processes, PAC learning of reachability is impossible without additional assumptions. This difficulty also holds in turn-based stochastic games (TBSGs), where two adversarial players interact on a finite state space. In this work, we consider turn-based stochastic games with reachability objectives. For such settings, adversarial learning, in which players are adversarial even in the learning phase, is impossible. Therefore, the goal is to consider learning, in which both players learn the unknown model together. In this spirit, previous literature on PAC learning in TBSGs considers (a) public information shared by both players; and (b) centralized learning, which means that players share the same learning algorithm. In this work, our contribution is two-fold. First, we relax these strong assumptions and ensure learning: (i) with private information not shared with the other player; and (ii) decentralized learning where the players do not share the same learning algorithm. To the best of our knowledge, this work is the first positive result for decentralized and private information learning of TBSGs with reachability objectives. Second, we introduce a game-theoretic generalization of the Expected Conditional Distance (ECD) parameter, which measures the expected length of reaching the target set. We establish a polynomial-sample complexity bound with respect to the number of states, actions, ECD parameter, and inverses of error tolerance and failure probability.","lang":"eng"}],"status":"public","keyword":["formal methods","games and logic","logical aspects of AI","model checking"],"article_number":"12:1-12:23","department":[{"_id":"GradSch"},{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2026-08-24T00:00:00Z","scopus_import":"1","title":"PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance","day":"24","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","das_tickbox":"0","type":"conference","citation":{"chicago":"Asadi, Ali, Krishnendu Chatterjee, and Pavol Kebis. “PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance.” In <i>37th International Conference on Concurrency Theory</i>, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.12</a>.","ama":"Asadi A, Chatterjee K, Kebis P. PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. In: <i>37th International Conference on Concurrency Theory</i>. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12\">10.4230/LIPIcs.CONCUR.2026.12</a>","ista":"Asadi A, Chatterjee K, Kebis P. 2026. PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 12:1-12:23.","ieee":"A. Asadi, K. Chatterjee, and P. Kebis, “PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance,” in <i>37th International Conference on Concurrency Theory</i>, Liverpool, United Kingdom, 2026, vol. 391.","short":"A. Asadi, K. Chatterjee, P. Kebis, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","apa":"Asadi, A., Chatterjee, K., &#38; Kebis, P. (2026). PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance. In <i>37th International Conference on Concurrency Theory</i> (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.12</a>","mla":"Asadi, Ali, et al. “PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance.” <i>37th International Conference on Concurrency Theory</i>, vol. 391, 12:1-12:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12\">10.4230/LIPIcs.CONCUR.2026.12</a>."},"date_created":"2026-09-13T22:01:53Z","OA_type":"gold","ddc":["000"],"publication_status":"published","intvolume":"       391","month":"08","conference":{"location":"Liverpool, United Kingdom","name":"CONCUR: Conference on Concurrency Theory","start_date":"2026-09-01","end_date":"2026-09-04"},"project":[{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"ec_funded":1,"language":[{"iso":"eng"}],"author":[{"id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Kebis, Pavol","first_name":"Pavol","last_name":"Kebis","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a"}],"oa":1,"alternative_title":["LIPIcs"],"publication_identifier":{"isbn":["9783959774475"],"eissn":["1868-8969"]},"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.12","corr_author":"1","article_processing_charge":"Yes","arxiv":1,"doi":"10.4230/LIPIcs.CONCUR.2026.12","OA_place":"publisher","date_updated":"2026-09-17T09:51:25Z","quality_controlled":"1","oa_version":"Published Version","supplementarymaterial":"yes","publication":"37th International Conference on Concurrency Theory","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","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"},"year":"2026","external_id":{"arxiv":["2607.14877"]},"file":[{"date_created":"2026-09-17T09:50:00Z","file_name":"2026_LIPIcsCONCUR_Asadi2.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","creator":"dernst","checksum":"2e6c55b65d9d7ce436a6f59e81d7ba17","file_id":"22947","success":1,"file_size":959234,"date_updated":"2026-09-17T09:50:00Z"}],"volume":391},{"scopus_import":"1","title":"A look back at strategy logic","day":"24","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","das_tickbox":"0","type":"conference","date_created":"2026-09-13T22:01:54Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “A Look Back at Strategy Logic.” <i>37th International Conference on Concurrency Theory</i>, vol. 391, 6:1-6:7, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6\">10.4230/LIPIcs.CONCUR.2026.6</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Piterman, N. (2026). A look back at strategy logic. In <i>37th International Conference on Concurrency Theory</i> (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.6</a>","short":"K. Chatterjee, T.A. Henzinger, N. Piterman, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","ieee":"K. Chatterjee, T. A. Henzinger, and N. Piterman, “A look back at strategy logic,” in <i>37th International Conference on Concurrency Theory</i>, Liverpool, United Kingdom, 2026, vol. 391.","ista":"Chatterjee K, Henzinger TA, Piterman N. 2026. A look back at strategy logic. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 6:1-6:7.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Nir Piterman. “A Look Back at Strategy Logic.” In <i>37th International Conference on Concurrency Theory</i>, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.6</a>.","ama":"Chatterjee K, Henzinger TA, Piterman N. A look back at strategy logic. In: <i>37th International Conference on Concurrency Theory</i>. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6\">10.4230/LIPIcs.CONCUR.2026.6</a>"},"has_accepted_license":"1","file_date_updated":"2026-09-22T05:53:16Z","acknowledgement":" Krishnendu Chatterjee: Supported in part by the Austrian Science Fund (FWF) COE\r\ngrant 10.55776/COE12 and the ERC CoG 863818 (ForM-SMArt).\r\nThomas A. Henzinger: Supported in part by the ERC AdG 101020093 (VAMOS) and the FWF\r\nSFB grant F8502 (SPyCoDe).\r\nNir Piterman: Supported in part by the Swedish research council (VR) project no. 2025-05419 and\r\nthe Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and\r\nAlice Wallenberg Foundation.\r\nAcknowledgements We thank the jury that our paper introducing Strategy Logic at the Conference\r\non Concurrency Theory (CONCUR) 2007 [10] was chosen for a CONCUR Test-of-Time Award at\r\nCONCUR 2026.","_id":"22922","abstract":[{"text":"In this note, we recall the history and our motivation behind the development of Strategy Logic and we discuss some of the work that ensued from its introduction.","lang":"eng"}],"researchdata_availability":"no","status":"public","keyword":["Strategy Logic","Games","Automata"],"article_number":"6:1-6:7","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2026-08-24T00:00:00Z","quality_controlled":"1","OA_place":"publisher","date_updated":"2026-09-22T05:54:30Z","oa_version":"Published Version","supplementarymaterial":"no","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication":"37th International Conference on Concurrency Theory","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"},"year":"2026","file":[{"file_size":517651,"checksum":"f3995df175701f56a702bdb012e4f710","file_id":"22977","success":1,"date_updated":"2026-09-22T05:53:16Z","date_created":"2026-09-22T05:53:16Z","access_level":"open_access","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_name":"2026_LIPIcsCONCUR_Chatterjee.pdf"}],"volume":391,"OA_type":"gold","intvolume":"       391","ddc":["000"],"month":"08","publication_status":"published","conference":{"end_date":"2026-09-04","start_date":"2026-09-01","name":"CONCUR: Conference on Concurrency Theory","location":"Liverpool, United Kingdom"},"project":[{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"ec_funded":1,"language":[{"iso":"eng"}],"author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Piterman, Nir","last_name":"Piterman","first_name":"Nir"}],"alternative_title":["LIPIcs"],"oa":1,"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959774475"]},"corr_author":"1","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.6","article_processing_charge":"Yes","doi":"10.4230/LIPIcs.CONCUR.2026.6"},{"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Fixed point certificates for reachability and expected rewards in MDPs","day":"01","type":"conference","date_created":"2025-05-25T22:17:09Z","citation":{"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>.","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>","ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Fixed point certificates for reachability and expected rewards in MDPs,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 130–151.","ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Fixed point certificates for reachability and expected rewards in MDPs. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 130–151.","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>","chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:130–51. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>."},"acknowledgement":"This project has received funding from the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12, a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, the DFG RTG 378803395 (ConVeY), the EU’s Horizon 2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement Nos. 101034413 (IST-BRIDGE) and 101008233 (MISSION), and the DFG RTG 2236 (UnRAVeL). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632.","has_accepted_license":"1","file_date_updated":"2025-06-02T10:49:52Z","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"}],"_id":"19743","status":"public","date_published":"2025-05-01T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","OA_place":"publisher","date_updated":"2026-09-16T06:57:17Z","oa_version":"Published Version","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"},"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","related_material":{"record":[{"id":"19771","relation":"research_data","status":"public"}]},"publisher":"Springer Nature","year":"2025","volume":15697,"file":[{"date_created":"2025-06-02T10:49:52Z","relation":"main_file","creator":"dernst","content_type":"application/pdf","access_level":"open_access","file_name":"2025_TACAS_ChatterjeeKrish.pdf","file_size":732136,"success":1,"checksum":"64b7f46ef05649b87b827248045c7645","file_id":"19772","date_updated":"2025-06-02T10:49:52Z"}],"page":"130-151","external_id":{"arxiv":["2501.11467"]},"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"},"OA_type":"hybrid","ddc":["000"],"month":"05","intvolume":"     15697","publication_status":"published","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Quatmann, Tim","first_name":"Tim","last_name":"Quatmann"},{"first_name":"Maximilian","last_name":"Schäffeler","full_name":"Schäffeler, Maximilian"},{"last_name":"Weininger","first_name":"Maximilian","orcid":"0000-0002-0163-2152","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian"},{"last_name":"Winkler","first_name":"Tobias","full_name":"Winkler, Tobias"},{"id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3","last_name":"Zilken","first_name":"Daniel","full_name":"Zilken, Daniel"}],"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"}],"ec_funded":1,"language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1007/978-3-031-90653-4_7","corr_author":"1","arxiv":1,"article_processing_charge":"No","alternative_title":["LNCS"],"oa":1,"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031906527"]},"doi":"10.1007/978-3-031-90653-4_7"},{"status":"public","date_published":"2025-05-01T00:00:00Z","department":[{"_id":"KrCh"}],"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and Austrian Science Fund (FWF) 10.55776/COE12 grant.","has_accepted_license":"1","file_date_updated":"2025-06-02T07:31:12Z","_id":"19740","abstract":[{"lang":"eng","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."}],"type":"conference","citation":{"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.","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.","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.","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>"},"date_created":"2025-05-25T22:17:06Z","scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","title":"Value iteration with guessing for Markov chains and Markov decision processes","article_processing_charge":"No","arxiv":1,"fulldoi":"https://doi.org/10.1007/978-3-031-90653-4_11","corr_author":"1","alternative_title":["LNCS"],"oa":1,"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031906527"],"eissn":["1611-3349"]},"doi":"10.1007/978-3-031-90653-4_11","conference":{"location":"Hamilton, ON, Canada","end_date":"2025-05-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2025-05-03"},"publication_status":"published","month":"05","ddc":["000"],"intvolume":"     15697","OA_type":"hybrid","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Mahdi","last_name":"Jafariraviz","full_name":"Jafariraviz, Mahdi"},{"full_name":"Saona Urmeneta, Raimundo J","first_name":"Raimundo J","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub"}],"language":[{"iso":"eng"}],"ec_funded":1,"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"}],"year":"2025","external_id":{"arxiv":["2505.06769"]},"volume":15697,"page":"217-236","file":[{"date_updated":"2025-06-02T07:31:12Z","checksum":"45da6efbcbed20aada16c48c8e55e2d6","file_id":"19767","success":1,"file_size":557481,"file_name":"2025_TACAS_Chatterjee.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","creator":"dernst","date_created":"2025-06-02T07:31:12Z"}],"oa_version":"Published Version","date_updated":"2026-09-16T06:56:56Z","OA_place":"publisher","quality_controlled":"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"},"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","publisher":"Springer Nature"},{"publisher":"Springer Nature","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","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"},"oa_version":"Published Version","date_updated":"2026-09-16T06:57:43Z","quality_controlled":"1","OA_place":"publisher","volume":15697,"file":[{"file_id":"19773","checksum":"7dcd85e7e753bfa994c10b3cf9ebc185","success":1,"file_size":532181,"date_updated":"2025-06-02T11:13:49Z","date_created":"2025-06-02T11:13:49Z","file_name":"2025_TACAS_Chatterjee_Goharshadi.pdf","access_level":"open_access","relation":"main_file","creator":"dernst","content_type":"application/pdf"}],"page":"279-300","external_id":{"arxiv":["2501.06579"]},"year":"2025","language":[{"iso":"eng"}],"ec_funded":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi","first_name":"Ehsan","orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný","first_name":"Petr"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde"}],"ddc":["000"],"intvolume":"     15697","publication_status":"published","month":"05","OA_type":"hybrid","conference":{"location":"Hamilton, ON, Canada","end_date":"2025-05-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2025-05-03"},"doi":"10.1007/978-3-031-90653-4_14","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031906527"]},"oa":1,"alternative_title":["LNCS"],"arxiv":1,"article_processing_charge":"No","corr_author":"1","fulldoi":"https://doi.org/10.1007/978-3-031-90653-4_14","day":"01","title":"Refuting equivalence in probabilistic programs with conditioning","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","citation":{"mla":"Chatterjee, Krishnendu, et al. “Refuting Equivalence in Probabilistic Programs with Conditioning.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 279–300, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Refuting equivalence in probabilistic programs with conditioning,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 279–300.","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.","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>","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.","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>"},"date_created":"2025-05-25T22:17:10Z","type":"conference","_id":"19744","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."}],"has_accepted_license":"1","file_date_updated":"2025-06-02T11:13:49Z","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.","department":[{"_id":"KrCh"}],"date_published":"2025-05-01T00:00:00Z","status":"public"},{"external_id":{"arxiv":["2412.16226"]},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.16226"}],"volume":39,"page":"11158-11166","year":"2025","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","publisher":"Association for the Advancement of Artificial Intelligence","OA_place":"repository","quality_controlled":"1","date_updated":"2026-09-16T06:55:21Z","oa_version":"Preprint","doi":"10.1609/aaai.v39i11.33213","corr_author":"1","fulldoi":"https://doi.org/10.1609/aaai.v39i11.33213","article_processing_charge":"No","arxiv":1,"oa":1,"publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587","first_name":"Ehsan","last_name":"Kafshdar Goharshadi","full_name":"Kafshdar Goharshadi, Ehsan"},{"full_name":"Karrabi, Mehrdad","last_name":"Karrabi","first_name":"Mehrdad","orcid":"0009-0007-5253-9170","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"last_name":"Motwani","first_name":"Harshit J.","full_name":"Motwani, Harshit J."},{"first_name":"Maximilian","last_name":"Seeliger","full_name":"Seeliger, Maximilian"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic"}],"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"language":[{"iso":"eng"}],"ec_funded":1,"conference":{"start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence","end_date":"2025-03-04","location":"Philadelphia, PA, United States"},"OA_type":"green","month":"04","publication_status":"published","intvolume":"        39","date_created":"2025-05-11T22:02:39Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “Quantified Linear and Polynomial Arithmetic Satisfiability via Template-Based Skolemization.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 11, Association for the Advancement of Artificial Intelligence, 2025, pp. 11158–66, doi:<a href=\"https://doi.org/10.1609/aaai.v39i11.33213\">10.1609/aaai.v39i11.33213</a>.","ieee":"K. Chatterjee, E. Goharshady, M. Karrabi, H. J. Motwani, M. Seeliger, and D. Zikelic, “Quantified linear and polynomial arithmetic satisfiability via template-based skolemization,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 11, pp. 11158–11166.","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.","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>","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>","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."},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Quantified linear and polynomial arithmetic satisfiability via template-based skolemization","day":"11","issue":"11","scopus_import":"1","date_published":"2025-04-11T00:00:00Z","department":[{"_id":"KrCh"}],"status":"public","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."}],"_id":"19667","acknowledgement":"This work was partially funded by ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12."},{"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)"}],"ec_funded":1,"language":[{"iso":"eng"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Luo, Ruichen","last_name":"Luo","first_name":"Ruichen","id":"b391db08-1ffe-11ee-8b67-d18ddcfb5a14"},{"orcid":"0000-0001-5103-038X","first_name":"Raimundo J","last_name":"Saona Urmeneta","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","full_name":"Saona Urmeneta, Raimundo J"},{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267"}],"OA_type":"green","month":"04","intvolume":"        39","publication_status":"published","conference":{"end_date":"2025-03-04","start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence","location":"Philadelphia, PA, United States"},"doi":"10.1609/aaai.v39i11.33212","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"oa":1,"fulldoi":"https://doi.org/10.1609/aaai.v39i11.33212","corr_author":"1","article_processing_charge":"No","arxiv":1,"publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","publisher":"Association for the Advancement of Artificial Intelligence","quality_controlled":"1","OA_place":"repository","date_updated":"2026-09-16T06:55:47Z","oa_version":"Preprint","external_id":{"arxiv":["2412.12228"]},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.12228"}],"page":"11150-11157","volume":39,"year":"2025","_id":"19669","abstract":[{"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.","lang":"eng"}],"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and the Austrian Science Fund (FWF) 10.55776/COE12 grant.","department":[{"_id":"KrCh"}],"date_published":"2025-04-11T00:00:00Z","status":"public","title":"Linear equations with min and max operators: Computational complexity","day":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","issue":"11","date_created":"2025-05-11T22:02:40Z","citation":{"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.","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>.","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>.","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>","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."},"type":"conference"},{"status":"public","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"date_published":"2025-06-25T00:00:00Z","file_date_updated":"2025-07-09T13:37:00Z","has_accepted_license":"1","acknowledgement":"The research for this thesis was supported by the European Research Council\r\n(grant agreements No. 863818 and No. 850529), the European Union’s Horizon 2020 research and innovation programme (Marie Skłodowska-Curie grant agreement No. 754411),\r\nthe Austrian Science Fund (grant DOI 10.55776/COE12), the French Agence Nationale\r\nde la Recherche under the Programme d’investissements d’avenir (project reference 17-\r\nEURE-0010) and the Australian Government through the Australian Research Council\r\n(grant No. SR200100005, “Securing Antarctica’s Environmental Future”).","_id":"19903","abstract":[{"text":"Cooperation, that is, one person paying a cost for another's benefit, is a fundamental principle without which no form of society could exist. The extent to which humans cooperate with each other is also an essential feature that differentiates them from other animals. Cooperation occurs even in the absence of altruistic motivations, when it is selfishly incentivised by the expectation of a future reward. For example, many economic interactions are well described that way. This kind of cooperation requires that people exhibit reciprocal behaviour that acts as a mechanism that rewards cooperation.\r\nWith game-theoretic models, it is possible to formally study potential such mechanisms and under what conditions they can exist. This thesis contributes to this effort by analysing recently introduced models of cooperation that advance on previous work by taking into account the potential for pre-existing inequality among cooperating individuals as well as the different forms that reciprocity can take.\r\nIndividuals may differ both intrinsically, in their abilities, as well as extrinsically, in the amount of resources they have available. Allowing for such differences in a model of cooperation helps to understand how inequality affects the potential for, and outcomes of, cooperation among unequals. In this thesis, it is shown that in the presence of intrinsic inequality, a similar unequal distribution of resources can increase the potential for cooperation. This effect is stronger the smaller the group is in which cooperation takes place. It is also shown that under particular assumptions, if the unequal members of a group vary the size of their contributions to a cooperative effort over time, they can thereby increase their efficiency and improve the collective outcome.\r\nCooperative behaviour in a two-person interaction can be rewarded either by direct reciprocation whenever the same two people interact again, or indirectly by a third party who observed the interaction. In the latter case of indirect reciprocity, individuals are proximally rewarded by a good reputation, which ultimately translates to being rewarded with cooperative behaviour by others. This mechanism can enable selfishly motivated cooperation even in circumstances where individuals are unlikely to meet again, akin to how money facilitates trade. While these two forms of reciprocity have mostly been studied in isolation, this thesis analyses both direct and indirect reciprocity in a general model in order to compare their relative effectiveness under different circumstances. The contribution of this thesis is an extension of previous work regarding a specific kind of interaction, whose parameters allow for convenient mathematical analysis, to the most general set of possible interactions.","lang":"eng"}],"supervisor":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"type":"dissertation","date_created":"2025-06-25T13:50:10Z","citation":{"chicago":"Hübner, Valentin. “Reciprocity and Inequality in Social Dilemmas.” Institute of Science and Technology Austria, 2025. <a href=\"https://doi.org/10.15479/AT-ISTA-19903\">https://doi.org/10.15479/AT-ISTA-19903</a>.","ama":"Hübner V. Reciprocity and inequality in social dilemmas. 2025. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-19903\">10.15479/AT-ISTA-19903</a>","ista":"Hübner V. 2025. Reciprocity and inequality in social dilemmas. Institute of Science and Technology Austria.","mla":"Hübner, Valentin. <i>Reciprocity and Inequality in Social Dilemmas</i>. Institute of Science and Technology Austria, 2025, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-19903\">10.15479/AT-ISTA-19903</a>.","apa":"Hübner, V. (2025). <i>Reciprocity and inequality in social dilemmas</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-19903\">https://doi.org/10.15479/AT-ISTA-19903</a>","ieee":"V. Hübner, “Reciprocity and inequality in social dilemmas,” Institute of Science and Technology Austria, 2025.","short":"V. Hübner, Reciprocity and Inequality in Social Dilemmas, Institute of Science and Technology Austria, 2025."},"title":"Reciprocity and inequality in social dilemmas","day":"25","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"publication_identifier":{"issn":["2663-337X"]},"alternative_title":["ISTA Thesis"],"fulldoi":"https://doi.org/10.15479/AT-ISTA-19903","degree_awarded":"PhD","corr_author":"1","article_processing_charge":"No","doi":"10.15479/AT-ISTA-19903","publication_status":"published","ddc":["519"],"month":"06","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"language":[{"iso":"eng"}],"ec_funded":1,"author":[{"id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","last_name":"Hübner","first_name":"Valentin","orcid":"0009-0001-5009-4987","full_name":"Hübner, Valentin"}],"year":"2025","doi_confirm":"1","page":"157","file":[{"date_updated":"2025-06-25T13:38:07Z","file_size":6192760,"checksum":"794c02f8c82ca59ba6dda3bd7eed871a","file_id":"19905","relation":"source_file","content_type":"application/x-xz","creator":"vhuebner","access_level":"closed","file_name":"Thesis Valentin Hübner source.tar.xz","date_created":"2025-06-25T13:38:07Z"},{"creator":"vhuebner","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"Thesis Valentin Hübner.pdf","date_created":"2025-07-09T13:37:00Z","date_updated":"2025-07-09T13:37:00Z","file_size":4837864,"checksum":"ac56063d81c81e40322b6ff5a8c4912e","file_id":"19976"}],"OA_place":"publisher","date_updated":"2026-09-16T06:58:24Z","oa_version":"Published Version","publisher":"Institute of Science and Technology Austria","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"19843"},{"status":"public","relation":"part_of_dissertation","id":"15083"},{"status":"public","id":"19074","relation":"part_of_dissertation"}]},"tmp":{"short":"CC BY-NC (4.0)","image":"/images/cc_by_nc.png","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode"}},{"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"date_published":"2025-08-05T00:00:00Z","status":"public","abstract":[{"lang":"eng","text":"The evolution shapes the world around us.\r\nNot only in biology, where the fittest individuals spread their genes but also in physics and social dynamics, the evolutionary forces determine the development of a state of matter or public opinions.\r\nMany models describe these dynamics.\r\nThis thesis examines the role of the structure in the models of selection.\r\nThe population structure is represented as a graph or a network, and each vertex is occupied by one individual.\r\nEvery individual has a type and fitness that represents the reproductive potential and depends on the type, occupied vertex, and the arrangement of the neighbors.\r\nThe evolution is modeled in discrete steps; in one step, one individual is replaced by a neighbor selected randomly with the influence of fitness.\r\n\r\n\r\n\r\nThe role of the networks is widely examined in the literature.\r\nThe structures that promote the spread of the desired type compared to the structureless case are called amplifiers.\r\nThe existence of amplifiers in various settings is an intensively studied topic, and in some settings, the amplifiers have been identified.\r\nMoreover, there are other important questions about the number of steps until one type spreads over the whole network (fixation time), the computational complexity, and the questions about the robustness of these processes.\r\n\r\n\r\nThis thesis explores the role of structure in evolution from many perspectives.\r\nFirst, it introduces different models and various choices that can be made in the models of evolution.\r\nIt highlights the role of the structure in the real world and how this is reflected in these models.\r\nThen, it describes the previous results and open problems.\r\nSecond, the thesis describes an amplifier for two variants of the Moran process: one with a constant birth rate and the other with a constant death rate.\r\nThis is an important contribution to the robustness of the amplification.\r\nThird, the thesis determines the complexity of spatial games.\r\nThese are processes where the fitness comes from a game, and the strength of selection is high.\r\nIt shows that determining the fate of cooperation in these games is a PSPACE-complete problem.\r\nFourth, the thesis describes the amplifier of cooperation for spatial games.\r\nThis is the first amplifier in this setting.\r\nFifth, the thesis examines the coexistence in the Moran process with environmental heterogeneity.\r\nIn this setting, the fitness depends not only on the type of the individual but also on the occupied vertex.\r\nThe chapter determines the relationship between the interactions of vertices of different types and the coexistence time.\r\nSixth, the thesis examines the social balance on networks and proposes a stochastic dynamic partially aware of the state of the graph, which reaches a balanced position quickly.\r\nFinally, the thesis presents conclusions and outlines the directions for future work.\r\n\r\n\r\n"}],"_id":"20138","has_accepted_license":"1","file_date_updated":"2025-08-21T11:48:39Z","acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForMSMArt) and Austrian Science Fund 10.55776/COE12.\r\n","license":"https://creativecommons.org/licenses/by-nc-sa/4.0/","citation":{"ista":"Svoboda J. 2025. Structural properties of games on graphs. Institute of Science and Technology Austria.","chicago":"Svoboda, Jakub. “Structural Properties of Games on Graphs.” Institute of Science and Technology Austria, 2025. <a href=\"https://doi.org/10.15479/AT-ISTA-20138\">https://doi.org/10.15479/AT-ISTA-20138</a>.","ama":"Svoboda J. Structural properties of games on graphs. 2025. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-20138\">10.15479/AT-ISTA-20138</a>","short":"J. Svoboda, Structural Properties of Games on Graphs, Institute of Science and Technology Austria, 2025.","ieee":"J. Svoboda, “Structural properties of games on graphs,” Institute of Science and Technology Austria, 2025.","apa":"Svoboda, J. (2025). <i>Structural properties of games on graphs</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-20138\">https://doi.org/10.15479/AT-ISTA-20138</a>","mla":"Svoboda, Jakub. <i>Structural Properties of Games on Graphs</i>. Institute of Science and Technology Austria, 2025, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-20138\">10.15479/AT-ISTA-20138</a>."},"date_created":"2025-08-05T14:33:59Z","das_tickbox":"1","supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"type":"dissertation","title":"Structural properties of games on graphs","day":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.15479/AT-ISTA-20138","oa":1,"alternative_title":["ISTA Thesis"],"publication_identifier":{"issn":["2663-337X"]},"fulldoi":"https://doi.org/10.15479/AT-ISTA-20138","degree_awarded":"PhD","corr_author":"1","article_processing_charge":"No","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"}],"ec_funded":1,"language":[{"iso":"eng"}],"author":[{"full_name":"Svoboda, Jakub","last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"}],"month":"08","publication_status":"published","ddc":["000","519"],"doi_confirm":"1","publisher_comment":"Chapter 4 is copyrighted by CC BY-NC-ND\r\n4.0, which prohibits derivatives. Chapter 6 is copyrighted: Copyright (2025) by the American\r\nPhysical Society. For a copy, redistribution, or modification needs to be permitted by the\r\nAmerican Physical Society.\r\n","file":[{"access_level":"open_access","creator":"jsvoboda","content_type":"application/pdf","relation":"main_file","file_name":"2025_Svoboda_Jakub_Thesis.pdf","date_created":"2025-08-14T09:54:43Z","date_updated":"2025-08-14T09:54:43Z","file_size":5927291,"checksum":"c6c4df9777f4537940de7ab392ad57e2","file_id":"20177","success":1},{"access_level":"closed","content_type":"application/zip","relation":"source_file","creator":"jsvoboda","file_name":"2025_Svoboda_Jakub_Thesis.zip","date_created":"2025-08-14T09:55:20Z","date_updated":"2025-08-21T11:48:39Z","file_size":6731815,"checksum":"485e9f9822821bc03666d245d80aaa08","file_id":"20178"}],"page":"167","year":"2025","publisher":"Institute of Science and Technology Austria","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"12787"},{"relation":"part_of_dissertation","id":"12101","status":"public"},{"id":"12257","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","id":"15297","status":"public"},{"status":"public","id":"18703","relation":"part_of_dissertation"}]},"tmp":{"image":"/images/cc_by_nc_sa.png","short":"CC BY-NC-SA (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0)"},"date_updated":"2026-09-16T06:59:33Z","OA_place":"publisher","oa_version":"Published Version"},{"has_accepted_license":"1","file_date_updated":"2025-09-09T06:27:59Z","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and Austrian Science Fund (FWF) 10.55776/COE12.\r\n","_id":"20299","abstract":[{"lang":"eng","text":"Deterministic Markov Decision Processes (DMDPs) are a mathematical framework for decision-making where the outcomes and future possible actions are deterministically determined by the current action taken. DMDPs can be viewed as a finite directed weighted graph, where in each step, the controller chooses an outgoing edge. An objective is a measurable function on runs (or infinite trajectories) of the DMDP, and the value for an objective is the maximal cumulative reward (or weight) that the controller can guarantee. We consider the classical mean-payoff (aka limit-average) objective, which is a basic and fundamental objective.\r\n\r\nHoward's policy iteration algorithm is a popular method for solving DMDPs with mean-payoff objectives. Although Howard's algorithm performs well in practice, as experimental studies suggested, the best known upper bound is exponential and the current known lower bound is as follows: For the input size I, the algorithm requires (math formular) iterations, where (math formular) hides the poly-logarithmic factors, i.e., the current lower bound on iterations is sub-linear with respect to the input size. Our main result is an improved lower bound for this fundamental algorithm where we show that for the input size I, the algorithm requires (math formular) iterations."}],"status":"public","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"date_published":"2025-01-01T00:00:00Z","scopus_import":"1","day":"01","title":"Lower bound on Howard policy iteration for deterministic Markov Decision Processes","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","citation":{"mla":"Asadi, Ali, et al. “Lower Bound on Howard Policy Iteration for Deterministic Markov Decision Processes.” <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, vol. 286, ML Research Press, 2025, pp. 223–32.","ieee":"A. Asadi, K. Chatterjee, and J. De Raaij, “Lower bound on Howard policy iteration for deterministic Markov Decision Processes,” in <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, Rio de Janeiro, Brazil, 2025, vol. 286, pp. 223–232.","apa":"Asadi, A., Chatterjee, K., &#38; De Raaij, J. (2025). Lower bound on Howard policy iteration for deterministic Markov Decision Processes. In <i>The 41st Conference on Uncertainty in Artificial Intelligence</i> (Vol. 286, pp. 223–232). Rio de Janeiro, Brazil: ML Research Press.","short":"A. Asadi, K. Chatterjee, J. De Raaij, in:, The 41st Conference on Uncertainty in Artificial Intelligence, ML Research Press, 2025, pp. 223–232.","chicago":"Asadi, Ali, Krishnendu Chatterjee, and Jakob De Raaij. “Lower Bound on Howard Policy Iteration for Deterministic Markov Decision Processes.” In <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, 286:223–32. ML Research Press, 2025.","ama":"Asadi A, Chatterjee K, De Raaij J. Lower bound on Howard policy iteration for deterministic Markov Decision Processes. In: <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>. Vol 286. ML Research Press; 2025:223-232.","ista":"Asadi A, Chatterjee K, De Raaij J. 2025. Lower bound on Howard policy iteration for deterministic Markov Decision Processes. The 41st Conference on Uncertainty in Artificial Intelligence. UAI: Conference on Uncertainty in Artificial Intelligence, PMLR, vol. 286, 223–232."},"date_created":"2025-09-07T22:01:34Z","month":"01","ddc":["000"],"intvolume":"       286","publication_status":"published","OA_type":"diamond","conference":{"name":"UAI: Conference on Uncertainty in Artificial Intelligence","start_date":"2025-07-21","end_date":"2025-07-25","location":"Rio de Janeiro, Brazil"},"language":[{"iso":"eng"}],"ec_funded":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"author":[{"full_name":"Asadi, Ali","last_name":"Asadi","first_name":"Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"De Raaij, Jakob","first_name":"Jakob","last_name":"De Raaij"}],"publication_identifier":{"eissn":["2640-3498"]},"oa":1,"alternative_title":["PMLR"],"article_processing_charge":"No","arxiv":1,"corr_author":"1","oa_version":"Published Version","quality_controlled":"1","date_updated":"2026-09-16T07:01:05Z","OA_place":"publisher","publisher":"ML Research Press","publication":"The 41st Conference on Uncertainty in Artificial Intelligence","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"},"year":"2025","file":[{"date_created":"2025-09-09T06:27:59Z","file_name":"2025_UAI_Asadi.pdf","access_level":"open_access","content_type":"application/pdf","creator":"dernst","relation":"main_file","file_id":"20313","checksum":"4180c81bb6ed3b4f5c7a8e48d06520c6","success":1,"file_size":317097,"date_updated":"2025-09-09T06:27:59Z"}],"volume":286,"page":"223-232","external_id":{"arxiv":["2506.12254"]}},{"scopus_import":"1","title":"Limit-sure reachability for small memory policies in POMDPs is NP-complete","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","date_created":"2025-09-07T22:01:34Z","citation":{"apa":"Asadi, A., Chatterjee, K., Saona Urmeneta, R. J., &#38; Shafiee, A. (2025). Limit-sure reachability for small memory policies in POMDPs is NP-complete. In <i>The 41st Conference on Uncertainty in Artificial Intelligence</i> (Vol. 286, pp. 238–247). Rio de Janeiro, Brazil: ML Research Press.","ieee":"A. Asadi, K. Chatterjee, R. J. Saona Urmeneta, and A. Shafiee, “Limit-sure reachability for small memory policies in POMDPs is NP-complete,” in <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, Rio de Janeiro, Brazil, 2025, vol. 286, pp. 238–247.","short":"A. Asadi, K. Chatterjee, R.J. Saona Urmeneta, A. Shafiee, in:, The 41st Conference on Uncertainty in Artificial Intelligence, ML Research Press, 2025, pp. 238–247.","mla":"Asadi, Ali, et al. “Limit-Sure Reachability for Small Memory Policies in POMDPs Is NP-Complete.” <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, vol. 286, ML Research Press, 2025, pp. 238–47.","ista":"Asadi A, Chatterjee K, Saona Urmeneta RJ, Shafiee A. 2025. Limit-sure reachability for small memory policies in POMDPs is NP-complete. The 41st Conference on Uncertainty in Artificial Intelligence. UAI: Conference on Uncertainty in Artificial Intelligence, PMLR, vol. 286, 238–247.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Raimundo J Saona Urmeneta, and Ali Shafiee. “Limit-Sure Reachability for Small Memory Policies in POMDPs Is NP-Complete.” In <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>, 286:238–47. ML Research Press, 2025.","ama":"Asadi A, Chatterjee K, Saona Urmeneta RJ, Shafiee A. Limit-sure reachability for small memory policies in POMDPs is NP-complete. In: <i>The 41st Conference on Uncertainty in Artificial Intelligence</i>. Vol 286. ML Research Press; 2025:238-247."},"has_accepted_license":"1","file_date_updated":"2025-09-09T08:19:41Z","acknowledgement":"This research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12, the support of the French Agence Nationale de la Recherche (ANR) under reference ANR-21-CE40-0020 (CONVERGENCE project), and the ERC CoG 863818 (ForM-SMArt) grant.","abstract":[{"lang":"eng","text":"A standard model that arises in several applications in sequential decision-making is partially observable Markov decision processes (POMDPs) where a decision-making agent interacts with an uncertain environment. A basic objective in POMDPs is the reachability objective, where given a target set of states, the goal is to eventually arrive at one of them.\r\n\r\nThe limit-sure problem asks whether reachability can be ensured with probability arbitrarily close to 1. In general, the limit-sure reachability problem for POMDPs is undecidable. However, in many practical cases, the most relevant question is the existence of policies with a small amount of memory. In this work, we study the limit-sure reachability problem for POMDPs with a fixed amount of memory. We establish that the computational complexity of the problem is NP-complete."}],"_id":"20297","status":"public","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"date_published":"2025-07-01T00:00:00Z","date_updated":"2026-09-16T07:03:02Z","quality_controlled":"1","OA_place":"publisher","oa_version":"Published Version","publisher":"ML Research Press","publication":"The 41st Conference on Uncertainty in Artificial Intelligence","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"},"year":"2025","file":[{"date_created":"2025-09-09T08:19:41Z","access_level":"open_access","creator":"dernst","content_type":"application/pdf","relation":"main_file","file_name":"2025_UAI_AsadiAli.pdf","file_size":307458,"checksum":"1a37ebe7ba73ab6985765bf0d17a0acc","file_id":"20315","success":1,"date_updated":"2025-09-09T08:19:41Z"}],"volume":286,"page":"238-247","external_id":{"arxiv":["2412.00941"]},"OA_type":"diamond","month":"07","intvolume":"       286","publication_status":"published","ddc":["000"],"conference":{"location":"Rio de Janeiro, Brazil","name":"UAI: Conference on Uncertainty in Artificial Intelligence","start_date":"2025-07-21","end_date":"2025-07-25"},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"language":[{"iso":"eng"}],"ec_funded":1,"author":[{"full_name":"Asadi, Ali","last_name":"Asadi","first_name":"Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Saona Urmeneta, Raimundo J","first_name":"Raimundo J","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"full_name":"Shafiee, Ali","last_name":"Shafiee","first_name":"Ali","id":"2783031a-7378-11f0-b2d0-f17f1db2ebad"}],"alternative_title":["PMLR"],"publication_identifier":{"eissn":["2640-3498"]},"oa":1,"corr_author":"1","arxiv":1,"article_processing_charge":"No"},{"type":"conference","citation":{"chicago":"Luo, Ruichen, Sebastian U. Stich, Samuel Horváth, and Martin Takáč. “Revisiting LocalSGD and SCAFFOLD: Improved Rates and Missing Analysis.” In <i>The 28th International Conference on Artificial Intelligence and Statistics</i>, 258:2539–47. ML Research Press, 2025.","ama":"Luo R, Stich SU, Horváth S, Takáč M. Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis. In: <i>The 28th International Conference on Artificial Intelligence and Statistics</i>. Vol 258. ML Research Press; 2025:2539-2547.","ista":"Luo R, Stich SU, Horváth S, Takáč M. 2025. Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis. The 28th International Conference on Artificial Intelligence and Statistics. AISTATS: Conference on Artificial Intelligence and Statistics, PMLR, vol. 258, 2539–2547.","mla":"Luo, Ruichen, et al. “Revisiting LocalSGD and SCAFFOLD: Improved Rates and Missing Analysis.” <i>The 28th International Conference on Artificial Intelligence and Statistics</i>, vol. 258, ML Research Press, 2025, pp. 2539–47.","ieee":"R. Luo, S. U. Stich, S. Horváth, and M. Takáč, “Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis,” in <i>The 28th International Conference on Artificial Intelligence and Statistics</i>, Mai Khao, Thailand, 2025, vol. 258, pp. 2539–2547.","apa":"Luo, R., Stich, S. U., Horváth, S., &#38; Takáč, M. (2025). Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis. In <i>The 28th International Conference on Artificial Intelligence and Statistics</i> (Vol. 258, pp. 2539–2547). Mai Khao, Thailand: ML Research Press.","short":"R. Luo, S.U. Stich, S. Horváth, M. Takáč, in:, The 28th International Conference on Artificial Intelligence and Statistics, ML Research Press, 2025, pp. 2539–2547."},"date_created":"2025-09-07T22:01:35Z","scopus_import":"1","title":"Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","department":[{"_id":"KrCh"}],"date_published":"2025-05-01T00:00:00Z","acknowledgement":"The authors thank for the helpful discussions with Eduard Gorbunov, Kumar Kshitij Patel, Anton\r\nRodomanov, and Ali Zindari during the preparation of this work. This work was partially done during the first author’s stays at CISPA and at MBZUAI. The first author also acknowledges ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12.","_id":"20302","abstract":[{"text":"LocalSGD and SCAFFOLD are widely used methods in distributed stochastic optimization, with numerous applications in machine learning, large-scale data processing, and federated learning. However, rigorously establishing their theoretical advantages over simpler methods, such as minibatch SGD (MbSGD), has proven challenging, as existing analyses often rely on strong assumptions, unrealistic premises, or overly restrictive scenarios.\r\n\r\nIn this work, we revisit the convergence properties of LocalSGD and SCAFFOLD under a variety of existing or weaker conditions, including gradient similarity, Hessian similarity, weak convexity, and Lipschitz continuity of the Hessian. Our analysis shows that (i) LocalSGD achieves faster convergence compared to MbSGD for weakly convex functions without requiring stronger gradient similarity assumptions; (ii) LocalSGD benefits significantly from higher-order similarity and smoothness; and (iii) SCAFFOLD demonstrates faster convergence than MbSGD for a broader class of non-quadratic functions. These theoretical insights provide a clearer understanding of the conditions under which LocalSGD and SCAFFOLD outperform MbSGD.","lang":"eng"}],"year":"2025","external_id":{"arxiv":["2501.04443"]},"volume":258,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2501.04443"}],"page":"2539-2547","OA_place":"repository","date_updated":"2026-09-16T07:01:32Z","quality_controlled":"1","oa_version":"Preprint","publication":"The 28th International Conference on Artificial Intelligence and Statistics","publisher":"ML Research Press","alternative_title":["PMLR"],"oa":1,"publication_identifier":{"eissn":["2640-3498"]},"arxiv":1,"article_processing_charge":"No","OA_type":"green","intvolume":"       258","publication_status":"published","month":"05","conference":{"location":"Mai Khao, Thailand","end_date":"2025-05-05","name":"AISTATS: Conference on Artificial Intelligence and Statistics","start_date":"2025-05-03"},"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"}],"ec_funded":1,"language":[{"iso":"eng"}],"author":[{"id":"b391db08-1ffe-11ee-8b67-d18ddcfb5a14","first_name":"Ruichen","last_name":"Luo","full_name":"Luo, Ruichen"},{"last_name":"Stich","first_name":"Sebastian U.","full_name":"Stich, Sebastian U."},{"full_name":"Horváth, Samuel","first_name":"Samuel","last_name":"Horváth"},{"full_name":"Takáč, Martin","last_name":"Takáč","first_name":"Martin"}]},{"date_created":"2025-11-16T23:01:24Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment Solver.” <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:<a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">10.1007/978-3-032-08707-2_19</a>.","short":"K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, M. Saadat, M. Seeliger, D. Zikelic, in:, 23rd International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2025, pp. 411–424.","apa":"Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., Saadat, M., Seeliger, M., &#38; Zikelic, D. (2025). PolyQEnt: A polynomial quantified entailment solver. In <i>23rd International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 16145, pp. 411–424). Bengaluru, India: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">https://doi.org/10.1007/978-3-032-08707-2_19</a>","ieee":"K. Chatterjee <i>et al.</i>, “PolyQEnt: A polynomial quantified entailment solver,” in <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, Bengaluru, India, 2025, vol. 16145, pp. 411–424.","ama":"Chatterjee K, Goharshady AK, Goharshady E, et al. PolyQEnt: A polynomial quantified entailment solver. In: <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>. Vol 16145. Springer Nature; 2025:411-424. doi:<a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">10.1007/978-3-032-08707-2_19</a>","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and Dorde Zikelic. “PolyQEnt: A Polynomial Quantified Entailment Solver.” In <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, 16145:411–24. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">https://doi.org/10.1007/978-3-032-08707-2_19</a>.","ista":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424."},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"PolyQEnt: A polynomial quantified entailment solver","day":"26","scopus_import":"1","date_published":"2025-10-26T00:00:00Z","department":[{"_id":"KrCh"}],"status":"public","_id":"20648","abstract":[{"text":"Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is a tool for solving polynomial quantified entailments in which variables on both sides of the implication are real valued or unbounded integers. Our tool provides a unified framework for polynomial quantified entailment problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks shows the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints.","lang":"eng"}],"acknowledgement":"This work was supported by the following grants: ERC CoG 863818 (ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, ERC StG 101222524 (SPES), the Ethereum Foundation Research Grant FY24-1793, and the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SISSMU-100).","external_id":{"arxiv":["2408.03796"]},"volume":16145,"page":"411-424","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2408.03796","open_access":"1"}],"year":"2025","publication":"23rd International Symposium on Automated Technology for Verification and Analysis","publisher":"Springer Nature","OA_place":"repository","quality_controlled":"1","date_updated":"2026-09-16T07:03:56Z","oa_version":"Preprint","doi":"10.1007/978-3-032-08707-2_19","corr_author":"1","fulldoi":"https://doi.org/10.1007/978-3-032-08707-2_19","arxiv":1,"article_processing_charge":"No","alternative_title":["LNCS"],"publication_identifier":{"issn":["0302-9743"],"isbn":["9783032087065"],"eissn":["1611-3349"]},"oa":1,"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","last_name":"Goharshady"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan"},{"full_name":"Karrabi, Mehrdad","first_name":"Mehrdad","last_name":"Karrabi","orcid":"0009-0007-5253-9170","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"full_name":"Saadat, Milad","last_name":"Saadat","first_name":"Milad"},{"first_name":"Maximilian","last_name":"Seeliger","full_name":"Seeliger, Maximilian"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"ec_funded":1,"language":[{"iso":"eng"}],"conference":{"location":"Bengaluru, India","name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2025-10-27","end_date":"2025-10-31"},"OA_type":"green","intvolume":"     16145","publication_status":"published","month":"10"},{"year":"2025","page":"458-471","external_id":{"arxiv":["2505.09514"]},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.09514"}],"oa_version":"Preprint","date_updated":"2026-09-16T07:05:13Z","quality_controlled":"1","OA_place":"repository","publisher":"IEEE","publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","article_processing_charge":"No","arxiv":1,"fulldoi":"https://doi.org/10.1109/lics65433.2025.00041","corr_author":"1","oa":1,"publication_identifier":{"eisbn":["9798331579005"]},"doi":"10.1109/lics65433.2025.00041","conference":{"end_date":"2025-06-26","name":"LICS: Logic in Computer Science","start_date":"2025-06-23","location":"Singapore, Singapore"},"month":"10","publication_status":"published","OA_type":"green","author":[{"last_name":"Brihaye","first_name":"Thomas","full_name":"Brihaye, Thomas"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Mohr, Stefanie","last_name":"Mohr","first_name":"Stefanie"},{"first_name":"Maximilian","last_name":"Weininger","orcid":"0000-0002-0163-2152","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian"}],"ec_funded":1,"language":[{"iso":"eng"}],"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)"}],"type":"conference","citation":{"ista":"Brihaye T, Chatterjee K, Mohr S, Weininger M. 2025. Risk-aware Markov decision processes using cumulative prospect theory. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 458–471.","ama":"Brihaye T, Chatterjee K, Mohr S, Weininger M. Risk-aware Markov decision processes using cumulative prospect theory. In: <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2025:458-471. doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00041\">10.1109/lics65433.2025.00041</a>","chicago":"Brihaye, Thomas, Krishnendu Chatterjee, Stefanie Mohr, and Maximilian Weininger. “Risk-Aware Markov Decision Processes Using Cumulative Prospect Theory.” In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 458–71. IEEE, 2025. <a href=\"https://doi.org/10.1109/lics65433.2025.00041\">https://doi.org/10.1109/lics65433.2025.00041</a>.","mla":"Brihaye, Thomas, et al. “Risk-Aware Markov Decision Processes Using Cumulative Prospect Theory.” <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2025, pp. 458–71, doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00041\">10.1109/lics65433.2025.00041</a>.","apa":"Brihaye, T., Chatterjee, K., Mohr, S., &#38; Weininger, M. (2025). Risk-aware Markov decision processes using cumulative prospect theory. In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 458–471). Singapore, Singapore: IEEE. <a href=\"https://doi.org/10.1109/lics65433.2025.00041\">https://doi.org/10.1109/lics65433.2025.00041</a>","short":"T. Brihaye, K. Chatterjee, S. Mohr, M. Weininger, in:, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp. 458–471.","ieee":"T. Brihaye, K. Chatterjee, S. Mohr, and M. Weininger, “Risk-aware Markov decision processes using cumulative prospect theory,” in <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Singapore, Singapore, 2025, pp. 458–471."},"date_created":"2025-11-24T14:43:47Z","scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"09","title":"Risk-aware Markov decision processes using cumulative prospect theory","status":"public","date_published":"2025-10-09T00:00:00Z","department":[{"_id":"KrCh"}],"acknowledgement":"This project has received funding from the Fonds de la Recherche Scientifique - FNRS under grant No. T.0027.21, the Belgian National Lottery; the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12; the DFG project 427755713, GOPro, and the DFG research training group GRK 2428 Continuous Verification of Cyber-Physical Systems\r\n(ConVeY); the EU’s Horizon 2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement No. 101034413 (IST-BRIDGE) and the ERC Starting Grant DEUCE (101077178).","_id":"20690","abstract":[{"lang":"eng","text":"Cumulative prospect theory (CPT) is the first theory for decision-making under uncertainty that combines full theoretical soundness and empirically realistic features [1], [Page 2]. While CPT was originally considered in one-shot settings for risk-aware decision-making, we consider CPT in sequential decision-making. The most fundamental and well-studied models for sequential decision-making are Markov chains (MCs), and their generalization Markov decision processes (MDPs). The complexity theoretic study of MCs and MDPs with CPT is a fundamental problem that has not been addressed in the literature.Our contributions are as follows: First, we present an alternative viewpoint for the CPT-value of MCs and MDPs. This allows us to establish a connection with multi-objective reachability analysis and conclude the strategy complexity result that memoryless randomized strategies are necessary and sufficient for optimality. Second, based on this connection, we provide an algorithm for computing the CPT-value in MDPs with infinite-horizon objectives. We show that the problem is in EXPTIME and fixed-parameter tractable. Moreover, we provide a polynomial-time algorithm for the special case of MCs."}]},{"acknowledgement":"This work was partly funded by the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12, the DFG Grant 389792660 as part of TRR 248 (Foundations of Perspicuous Software Systems), the Cluster of Excellence EXC 2050/1 (CeTI, project ID\r\n390696704, as part of Germany’s Excellence Strategy), and by the BMBF (Federal Ministry of Education and Research) in DAAD project 57616814 (SECAI, School of Embedded and\r\nComposite AI) as part of the program Konrad Zuse Schools of Excellence in Artificial Intelligence.","abstract":[{"text":"This paper studies the expected value of multiplicative rewards, where rewards obtained in each step are multiplied (instead of the usual addition), in Markov chains (MCs) and Markov decision processes (MDPs). One of the key differences to additive rewards is that the expected value may diverge to ∞ not only due to recurrent, but also due to transient states.For MCs, computing the value is shown to be possible in polynomial time given an oracle for the comparison of succinctly represented integers (CSRI), which is only known to be solvable in polynomial time subject to number-theoretic conjectures. Interestingly, distinguishing whether the value is ∞ or 0 is at least as hard as CSRI, while determining if it is one of these two can be done in polynomial time. In MDPs, the optimal value can be computed in polynomial space. Further refined complexity results and results on the complexity of optimal schedulers are presented. The techniques developed for MDPs additionally allow to solve the multiplicative variant of the stochastic shortest path problem. Finally, for MCs and MDPs where an absorbing state is reached almost surely, all considered problems are solvable in polynomial time.","lang":"eng"}],"_id":"20689","status":"public","date_published":"2025-10-09T00:00:00Z","department":[{"_id":"KrCh"}],"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Multiplicative rewards in Markovian models","day":"09","type":"conference","citation":{"mla":"Baier, Christel, et al. “Multiplicative Rewards in Markovian Models.” <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2025, pp. 499–512, doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00044\">10.1109/lics65433.2025.00044</a>.","ieee":"C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Multiplicative rewards in Markovian models,” in <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Singapore, Singapore, 2025, pp. 499–512.","apa":"Baier, C., Chatterjee, K., Meggendorfer, T., &#38; Piribauer, J. (2025). Multiplicative rewards in Markovian models. In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 499–512). Singapore, Singapore: IEEE. <a href=\"https://doi.org/10.1109/lics65433.2025.00044\">https://doi.org/10.1109/lics65433.2025.00044</a>","short":"C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, in:, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp. 499–512.","ama":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Multiplicative rewards in Markovian models. In: <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2025:499-512. doi:<a href=\"https://doi.org/10.1109/lics65433.2025.00044\">10.1109/lics65433.2025.00044</a>","chicago":"Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer. “Multiplicative Rewards in Markovian Models.” In <i>2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 499–512. IEEE, 2025. <a href=\"https://doi.org/10.1109/lics65433.2025.00044\">https://doi.org/10.1109/lics65433.2025.00044</a>.","ista":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2025. Multiplicative rewards in Markovian models. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 499–512."},"date_created":"2025-11-24T14:24:00Z","conference":{"end_date":"2025-06-26","start_date":"2025-06-23","name":"LICS: Logic in Computer Science","location":"Singapore, Singapore"},"OA_type":"green","publication_status":"published","month":"10","author":[{"full_name":"Baier, Christel","first_name":"Christel","last_name":"Baier"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","first_name":"Tobias","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias"},{"first_name":"Jakob","last_name":"Piribauer","full_name":"Piribauer, Jakob"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"ec_funded":1,"language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1109/lics65433.2025.00044","corr_author":"1","arxiv":1,"article_processing_charge":"No","publication_identifier":{"eisbn":["9798331579005"]},"oa":1,"doi":"10.1109/lics65433.2025.00044","quality_controlled":"1","OA_place":"repository","date_updated":"2026-09-16T07:05:41Z","oa_version":"Preprint","publication":"2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science","publisher":"IEEE","year":"2025","page":"499-512","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2504.18277","open_access":"1"}],"external_id":{"arxiv":["2504.18277"]}}]