[{"OA_place":"repository","OA_type":"green","language":[{"iso":"eng"}],"scopus_import":"1","issue":"43","publication":"Proceedings of the 40th AAAI Conference on Artificial Intelligence","ec_funded":1,"publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"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.","page":"36137-36145","citation":{"short":"A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, A. Shafiee, in:, Proceedings of the 40th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–36145.","ieee":"A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, and A. Shafiee, “Qualitative analysis of ω-regular objectives on robust MDPs,” in <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36137–36145.","ista":"Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. 2026. Qualitative analysis of ω-regular objectives on robust MDPs. Proceedings of the 40th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 40, 36137–36145.","ama":"Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. Qualitative analysis of ω-regular objectives on robust MDPs. In: <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>. Vol 40. Association for the Advancement of Artificial Intelligence; 2026:36137-36145. doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">10.1609/aaai.v40i43.40931</a>","mla":"Asadi, Ali, et al. “Qualitative Analysis of ω-Regular Objectives on Robust MDPs.” <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i>, vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–45, doi:<a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">10.1609/aaai.v40i43.40931</a>.","apa":"Asadi, A., Chatterjee, K., Goharshady, E., Karrabi, M., &#38; Shafiee, A. (2026). Qualitative analysis of ω-regular objectives on robust MDPs. In <i>Proceedings of the 40th AAAI Conference on Artificial Intelligence</i> (Vol. 40, pp. 36137–36145). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v40i43.40931\">https://doi.org/10.1609/aaai.v40i43.40931</a>","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>."},"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"}],"date_updated":"2026-09-16T07:27:43Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Asadi, Ali","first_name":"Ali","last_name":"Asadi","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan"},{"orcid":"0009-0007-5253-9170","full_name":"Karrabi, Mehrdad","last_name":"Karrabi","first_name":"Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"id":"2783031a-7378-11f0-b2d0-f17f1db2ebad","first_name":"Ali","last_name":"Shafiee","full_name":"Shafiee, Ali"}],"date_created":"2026-04-12T22:01:50Z","status":"public","title":"Qualitative analysis of ω-regular objectives on robust MDPs","_id":"21717","abstract":[{"text":"Robust Markov Decision Processes (RMDPs) generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for ω-regular objectives. The qualitative analysis problem asks whether the objective can be ensured with probability 1. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. Our contributions are twofold. We first present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives. We then report experimental results demonstrating the effectiveness of our oracle-based approach on classical RMDP examples from the literature scaling up to thousands of states.","lang":"eng"}],"oa_version":"Preprint","type":"conference","doi":"10.1609/aaai.v40i43.40931","volume":40,"oa":1,"day":"14","publisher":"Association for the Advancement of Artificial Intelligence","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"month":"03","external_id":{"arxiv":["2505.04539"]},"article_processing_charge":"No","conference":{"location":"Singapore, Singapore","end_date":"2026-01-27","start_date":"2026-01-20","name":"AAAI: Conference on Artificial Intelligence"},"date_published":"2026-03-14T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2505.04539"}],"arxiv":1,"fulldoi":"https://doi.org/10.1609/aaai.v40i43.40931","intvolume":"        40","publication_status":"published","quality_controlled":"1","year":"2026"},{"language":[{"iso":"eng"}],"OA_type":"gold","OA_place":"publisher","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.","ec_funded":1,"publication_identifier":{"eissn":["2475-1421"]},"issue":"PLDI","scopus_import":"1","publication":"Proceedings of the ACM on Programming Languages","PlanS_conform":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-09-16T07:36:14Z","supplementarymaterial":"no","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12"}],"citation":{"short":"K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming Languages 10 (2026).","ista":"Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 10(PLDI), 218.","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.","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>","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>.","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>."},"related_material":{"record":[{"status":"public","id":"22134","relation":"research_data"}]},"abstract":[{"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.","lang":"eng"}],"article_type":"original","type":"journal_article","oa_version":"Published Version","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","last_name":"Kafshdar Goharshadi"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"date_created":"2026-06-21T22:02:59Z","status":"public","_id":"22102","title":"SuperDP: Differential privacy refutation via supermartingales","file":[{"file_size":858595,"file_name":"2026_ProcACMProgrammingLanguages_Chatterjee.pdf","content_type":"application/pdf","date_updated":"2026-06-24T06:19:56Z","file_id":"22135","relation":"main_file","creator":"dernst","access_level":"open_access","date_created":"2026-06-24T06:19:56Z","checksum":"994bf21d6269dabccf1e1091e02962c5","success":1}],"doi":"10.1145/3808296","researchdata_availability":"yes","volume":10,"article_number":"218","month":"06","department":[{"_id":"KrCh"}],"publisher":"ACM","external_id":{"arxiv":["2603.26215"]},"corr_author":"1","oa":1,"day":"08","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.","arxiv":1,"fulldoi":"https://doi.org/10.1145/3808296","das_tickbox":"1","keyword":["Static Program Analysis","Differential Privacy","Probabilistic Programming","Martingales"],"article_processing_charge":"Yes","file_date_updated":"2026-06-24T06:19:56Z","date_published":"2026-06-08T00:00:00Z","has_accepted_license":"1","intvolume":"        10","quality_controlled":"1","year":"2026","publication_status":"published","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"]},{"main_file_link":[{"url":"https://doi.org/10.5281/ZENODO.18930113","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","fulldoi":"https://doi.org/10.5281/ZENODO.18930113","date_updated":"2026-09-16T07:36:13Z","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>SuperDP: Differential Privacy Refutation via Supermartingales</i>. Zenodo, 2026, doi:<a href=\"https://doi.org/10.5281/ZENODO.18930113\">10.5281/ZENODO.18930113</a>.","ama":"Chatterjee K, Goharshady E, Zikelic D. SuperDP: Differential Privacy Refutation via Supermartingales. 2026. doi:<a href=\"https://doi.org/10.5281/ZENODO.18930113\">10.5281/ZENODO.18930113</a>","ista":"Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential Privacy Refutation via Supermartingales, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.18930113\">10.5281/ZENODO.18930113</a>.","ieee":"K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential Privacy Refutation via Supermartingales.” Zenodo, 2026.","short":"K. Chatterjee, E. Goharshady, D. Zikelic, (2026).","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” Zenodo, 2026. <a href=\"https://doi.org/10.5281/ZENODO.18930113\">https://doi.org/10.5281/ZENODO.18930113</a>.","apa":"Chatterjee, K., Goharshady, E., &#38; Zikelic, D. (2026). SuperDP: Differential Privacy Refutation via Supermartingales. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.18930113\">https://doi.org/10.5281/ZENODO.18930113</a>"},"article_processing_charge":"No","date_published":"2026-03-09T00:00:00Z","related_material":{"record":[{"relation":"used_in_publication","id":"22102","status":"public"}]},"has_accepted_license":"1","abstract":[{"text":"This artifact provides the source code, benchmarks, and scripts necessary to build and reproduce the experimental results for `SuperDP` (Accepted at PLDI 2026). It also includes instructions for running the tool on user-provided inputs.","lang":"eng"}],"year":"2026","oa_version":"Published Version","type":"research_data_reference","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Kafshdar Goharshadi","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"status":"public","date_created":"2026-06-24T06:25:29Z","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"_id":"22134","title":"SuperDP: Differential Privacy Refutation via Supermartingales","doi":"10.5281/ZENODO.18930113","OA_place":"repository","OA_type":"green","month":"03","department":[{"_id":"KrCh"}],"publisher":"Zenodo","oa":1,"corr_author":"1","day":"09"},{"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"intvolume":"       391","year":"2026","quality_controlled":"1","publication_status":"published","keyword":["Bidding Games","Stochastic Games"],"article_processing_charge":"Yes","file_date_updated":"2026-09-17T09:43:28Z","alternative_title":["LIPIcs"],"date_published":"2026-08-24T00:00:00Z","has_accepted_license":"1","conference":{"end_date":"2026-09-04","start_date":"2026-09-01","name":"CONCUR: Conference on Concurrency Theory","location":"Liverpool, United Kingdom"},"arxiv":1,"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13","das_tickbox":"0","corr_author":"1","oa":1,"day":"24","department":[{"_id":"GradSch"},{"_id":"KrCh"},{"_id":"ToHe"}],"month":"08","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","external_id":{"arxiv":["2606.29420"]},"article_number":"13:1-13:20","file":[{"file_id":"22946","file_name":"2026_LIPIcsCONCUR_Asadi.pdf","content_type":"application/pdf","date_updated":"2026-09-17T09:43:28Z","file_size":1175682,"success":1,"checksum":"de9af748d78fa42c173f68a71cbbd8d9","date_created":"2026-09-17T09:43:28Z","access_level":"open_access","relation":"main_file","creator":"dernst"}],"researchdata_availability":"no","doi":"10.4230/LIPIcs.CONCUR.2026.13","volume":391,"status":"public","author":[{"id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","first_name":"Ehsan","last_name":"Kafshdar Goharshadi","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"last_name":"Kebis","first_name":"Pavol","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a","full_name":"Kebis, Pavol"},{"orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"}],"date_created":"2026-09-13T22:01:53Z","_id":"22920","title":"Generalized bidding games: Where bidding and stochastic games meet","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."}],"type":"conference","oa_version":"Published Version","project":[{"name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"},{"name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"}],"citation":{"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.","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.","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.","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>","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>.","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>","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>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-09-17T09:44:41Z","supplementarymaterial":"yes","scopus_import":"1","publication":"37th International Conference on Concurrency Theory","publication_identifier":{"eissn":["1868-8969"],"isbn":["9783959774475"]},"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","ec_funded":1,"OA_type":"gold","OA_place":"publisher","language":[{"iso":"eng"}]},{"OA_place":"publisher","OA_type":"hybrid","language":[{"iso":"eng"}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031906527"],"eissn":["1611-3349"]},"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.","ec_funded":1,"page":"279-300","citation":{"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>.","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>","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>","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.","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."},"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"grant_number":"COE12","name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee"}],"date_updated":"2026-09-16T06:57:43Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Refuting equivalence in probabilistic programs with conditioning","_id":"19744","date_created":"2025-05-25T22:17:10Z","status":"public","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","last_name":"Kafshdar Goharshadi"},{"full_name":"Novotný, Petr","first_name":"Petr","last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic"}],"type":"conference","oa_version":"Published Version","abstract":[{"lang":"eng","text":"We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature."}],"volume":15697,"doi":"10.1007/978-3-031-90653-4_14","file":[{"checksum":"7dcd85e7e753bfa994c10b3cf9ebc185","date_created":"2025-06-02T11:13:49Z","success":1,"relation":"main_file","creator":"dernst","access_level":"open_access","file_id":"19773","file_size":532181,"file_name":"2025_TACAS_Chatterjee_Goharshadi.pdf","content_type":"application/pdf","date_updated":"2025-06-02T11:13:49Z"}],"day":"01","oa":1,"corr_author":"1","external_id":{"arxiv":["2501.06579"]},"publisher":"Springer Nature","month":"05","department":[{"_id":"KrCh"}],"conference":{"start_date":"2025-05-03","end_date":"2025-05-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Hamilton, ON, Canada"},"has_accepted_license":"1","file_date_updated":"2025-06-02T11:13:49Z","date_published":"2025-05-01T00:00:00Z","alternative_title":["LNCS"],"article_processing_charge":"No","fulldoi":"https://doi.org/10.1007/978-3-031-90653-4_14","arxiv":1,"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"publication_status":"published","year":"2025","quality_controlled":"1","intvolume":"     15697"},{"language":[{"iso":"eng"}],"OA_type":"green","OA_place":"repository","ec_funded":1,"acknowledgement":"This work was partially funded by ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12.","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","scopus_import":"1","issue":"11","date_updated":"2026-09-16T06:55:21Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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>.","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>","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>.","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.","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."},"page":"11158-11166","project":[{"grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12"}],"oa_version":"Preprint","type":"conference","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."}],"title":"Quantified linear and polynomial arithmetic satisfiability via template-based skolemization","_id":"19667","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Kafshdar Goharshadi","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587"},{"full_name":"Karrabi, Mehrdad","orcid":"0009-0007-5253-9170","id":"67638922-f394-11eb-9cf6-f20423e08757","last_name":"Karrabi","first_name":"Mehrdad"},{"full_name":"Motwani, Harshit J.","last_name":"Motwani","first_name":"Harshit J."},{"full_name":"Seeliger, Maximilian","last_name":"Seeliger","first_name":"Maximilian"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"date_created":"2025-05-11T22:02:39Z","status":"public","volume":39,"doi":"10.1609/aaai.v39i11.33213","external_id":{"arxiv":["2412.16226"]},"publisher":"Association for the Advancement of Artificial Intelligence","month":"04","department":[{"_id":"KrCh"}],"day":"11","oa":1,"corr_author":"1","fulldoi":"https://doi.org/10.1609/aaai.v39i11.33213","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.16226"}],"arxiv":1,"conference":{"location":"Philadelphia, PA, United States","start_date":"2025-02-25","end_date":"2025-03-04","name":"AAAI: Conference on Artificial Intelligence"},"date_published":"2025-04-11T00:00:00Z","article_processing_charge":"No","publication_status":"published","year":"2025","quality_controlled":"1","intvolume":"        39"},{"date_updated":"2026-09-16T07:03:56Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"411-424","citation":{"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>","mla":"Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment Solver.” <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:<a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">10.1007/978-3-032-08707-2_19</a>.","ieee":"K. Chatterjee <i>et al.</i>, “PolyQEnt: A polynomial quantified entailment solver,” in <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, Bengaluru, India, 2025, vol. 16145, pp. 411–424.","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.","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.","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>.","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>"},"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12"}],"oa_version":"Preprint","type":"conference","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"}],"title":"PolyQEnt: A polynomial quantified entailment solver","_id":"20648","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","last_name":"Kafshdar Goharshadi","first_name":"Ehsan"},{"full_name":"Karrabi, Mehrdad","orcid":"0009-0007-5253-9170","id":"67638922-f394-11eb-9cf6-f20423e08757","last_name":"Karrabi","first_name":"Mehrdad"},{"last_name":"Saadat","first_name":"Milad","full_name":"Saadat, Milad"},{"full_name":"Seeliger, Maximilian","first_name":"Maximilian","last_name":"Seeliger"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic"}],"date_created":"2025-11-16T23:01:24Z","status":"public","language":[{"iso":"eng"}],"OA_place":"repository","OA_type":"green","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783032087065"]},"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).","ec_funded":1,"publication":"23rd International Symposium on Automated Technology for Verification and Analysis","scopus_import":"1","fulldoi":"https://doi.org/10.1007/978-3-032-08707-2_19","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2408.03796","open_access":"1"}],"arxiv":1,"conference":{"end_date":"2025-10-31","start_date":"2025-10-27","name":"ATVA: Automated Technology for Verification and Analysis","location":"Bengaluru, India"},"date_published":"2025-10-26T00:00:00Z","alternative_title":["LNCS"],"article_processing_charge":"No","publication_status":"published","year":"2025","quality_controlled":"1","intvolume":"     16145","volume":16145,"doi":"10.1007/978-3-032-08707-2_19","external_id":{"arxiv":["2408.03796"]},"publisher":"Springer Nature","department":[{"_id":"KrCh"}],"month":"10","day":"26","oa":1,"corr_author":"1"},{"page":"6707-6715","citation":{"ama":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. Solving long-run average reward robust MDPs via stochastic games. In: <i>33rd International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2024:6707-6715. doi:<a href=\"https://doi.org/10.24963/ijcai.2024/741\">10.24963/ijcai.2024/741</a>","mla":"Chatterjee, Krishnendu, et al. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” <i>33rd International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–15, doi:<a href=\"https://doi.org/10.24963/ijcai.2024/741\">10.24963/ijcai.2024/741</a>.","ieee":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, and D. Zikelic, “Solving long-run average reward robust MDPs via stochastic games,” in <i>33rd International Joint Conference on Artificial Intelligence</i>, Jeju, South Korea, 2024, pp. 6707–6715.","short":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, D. Zikelic, in:, 33rd International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–6715.","ista":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving long-run average reward robust MDPs via stochastic games. 33rd International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 6707–6715.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Petr Novotný, and Dorde Zikelic. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” In <i>33rd International Joint Conference on Artificial Intelligence</i>, 6707–15. International Joint Conferences on Artificial Intelligence, 2024. <a href=\"https://doi.org/10.24963/ijcai.2024/741\">https://doi.org/10.24963/ijcai.2024/741</a>.","apa":"Chatterjee, K., Goharshady, E., Karrabi, M., Novotný, P., &#38; Zikelic, D. (2024). Solving long-run average reward robust MDPs via stochastic games. In <i>33rd International Joint Conference on Artificial Intelligence</i> (pp. 6707–6715). Jeju, South Korea: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2024/741\">https://doi.org/10.24963/ijcai.2024/741</a>"},"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"date_updated":"2026-10-16T08:07:05Z","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","status":"public","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"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","orcid":"0009-0007-5253-9170","last_name":"Karrabi","first_name":"Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotný","full_name":"Novotný, Petr"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"date_created":"2024-09-29T22:01:39Z","title":"Solving long-run average reward robust MDPs via stochastic games","_id":"18160","abstract":[{"text":"Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs in which all uncertainty sets are polytopes and study the problem of solving long-run average reward polytopic RMDPs. We present a novel perspective on this problem and show that it can be reduced to solving long-run average reward turn-based stochastic games with finite state and action spaces. This reduction allows us to derive several important consequences that were hitherto not known to hold for polytopic RMDPs. First, we derive new computational complexity bounds for solving long-run average reward polytopic RMDPs, showing for the first time that the threshold decision problem for them is in NP∩CONP and that they admit a randomized algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is much more efficient in solving long-run average reward polytopic RMDPs compared to state-of-the-art methods based on value iteration. ","lang":"eng"}],"type":"conference","oa_version":"Preprint","OA_type":"green","OA_place":"repository","language":[{"iso":"eng"}],"scopus_import":"1","publication":"33rd International Joint Conference on Artificial Intelligence","ec_funded":1,"acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Czech Science Foundation\r\ngrant no. GA23-06963S.","publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"article_processing_charge":"No","conference":{"location":"Jeju, South Korea","name":"IJCAI: International Joint Conference on Artificial Intelligence","end_date":"2024-08-09","start_date":"2024-08-03"},"date_published":"2024-09-01T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2312.13912"}],"arxiv":1,"das_tickbox":"0","fulldoi":"https://doi.org/10.24963/ijcai.2024/741","publication_status":"published","year":"2024","quality_controlled":"1","doi":"10.24963/ijcai.2024/741","researchdata_availability":"no","corr_author":"1","oa":1,"day":"01","publisher":"International Joint Conferences on Artificial Intelligence","month":"09","department":[{"_id":"KrCh"}],"external_id":{"arxiv":["2312.13912"]}},{"_id":"17283","title":"Equivalence and similarity refutation for probabilistic programs","status":"public","date_created":"2024-07-21T22:01:01Z","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","first_name":"Ehsan","last_name":"Kafshdar Goharshadi","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"full_name":"Novotný, Petr","first_name":"Petr","last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"article_type":"original","oa_version":"Published Version","type":"journal_article","abstract":[{"lang":"eng","text":"We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature."}],"project":[{"grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"citation":{"chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Equivalence and Similarity Refutation for Probabilistic Programs.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3656462\">https://doi.org/10.1145/3656462</a>.","apa":"Chatterjee, K., Goharshady, E., Novotný, P., &#38; Zikelic, D. (2024). Equivalence and similarity refutation for probabilistic programs. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3656462\">https://doi.org/10.1145/3656462</a>","mla":"Chatterjee, Krishnendu, et al. “Equivalence and Similarity Refutation for Probabilistic Programs.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, 232, Association for Computing Machinery, 2024, doi:<a href=\"https://doi.org/10.1145/3656462\">10.1145/3656462</a>.","ama":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. Equivalence and similarity refutation for probabilistic programs. <i>Proceedings of the ACM on Programming Languages</i>. 2024;8. doi:<a href=\"https://doi.org/10.1145/3656462\">10.1145/3656462</a>","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Equivalence and similarity refutation for probabilistic programs,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8. Association for Computing Machinery, 2024.","short":"K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).","ista":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2024. Equivalence and similarity refutation for probabilistic programs. Proceedings of the ACM on Programming Languages. 8, 232."},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_updated":"2026-10-16T08:08:51Z","supplementarymaterial":"no","publication":"Proceedings of the ACM on Programming Languages","scopus_import":"1","ec_funded":1,"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant. Petr Novotný\r\nis supported by the Czech Science Foundation grant no. GA23-06963S.\r\n","publication_identifier":{"eissn":["2475-1421"]},"OA_type":"hybrid","OA_place":"publisher","language":[{"iso":"eng"}],"ddc":["000"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"quality_controlled":"1","year":"2024","publication_status":"published","intvolume":"         8","file_date_updated":"2024-07-22T07:17:14Z","date_published":"2024-06-20T00:00:00Z","has_accepted_license":"1","article_processing_charge":"Yes (via OA deal)","fulldoi":"https://doi.org/10.1145/3656462","das_tickbox":"0","arxiv":1,"day":"20","oa":1,"corr_author":"1","external_id":{"arxiv":["2404.03430"]},"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"month":"06","publisher":"Association for Computing Machinery","article_number":"232","volume":8,"file":[{"file_id":"17290","file_size":355421,"file_name":"2024_ACMProgLang_Chatterjee.pdf","date_updated":"2024-07-22T07:17:14Z","content_type":"application/pdf","date_created":"2024-07-22T07:17:14Z","checksum":"8cbf220f284a4a87d093db5320c5afdd","success":1,"creator":"dernst","relation":"main_file","access_level":"open_access"}],"doi":"10.1145/3656462","researchdata_availability":"no"},{"intvolume":"     13047","publication_status":"published","year":"2021","quality_controlled":"1","article_processing_charge":"No","conference":{"location":"Virtual","name":"FM: Formal Methods","start_date":"2021-11-20","end_date":"2021-11-26"},"date_published":"2021-11-10T00:00:00Z","alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2108.02188"}],"arxiv":1,"fulldoi":"https://doi.org/10.1007/978-3-030-90870-6_33","oa":1,"day":"10","publisher":"Springer Nature","month":"11","department":[{"_id":"KrCh"}],"external_id":{"arxiv":["2108.02188"],"isi":["000758218600033"]},"isi":1,"doi":"10.1007/978-3-030-90870-6_33","volume":13047,"date_created":"2021-12-05T23:01:45Z","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","last_name":"Kafshdar Goharshadi","first_name":"Ehsan"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotný","full_name":"Novotný, Petr"},{"last_name":"Zárevúcky","first_name":"Jiří","full_name":"Zárevúcky, Jiří"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"status":"public","title":"On lexicographic proof rules for probabilistic termination","_id":"10414","abstract":[{"lang":"eng","text":"We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in LexRSM not existing even for simple terminating programs. Our contributions are twofold: First, we introduce a generalization of LexRSMs which allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs."}],"oa_version":"Preprint","type":"conference","citation":{"mla":"Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>24th International Symposium on Formal Methods</i>, vol. 13047, Springer Nature, 2021, pp. 619–39, doi:<a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">10.1007/978-3-030-90870-6_33</a>.","ama":"Chatterjee K, Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. In: <i>24th International Symposium on Formal Methods</i>. Vol 13047. Springer Nature; 2021:619-639. doi:<a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">10.1007/978-3-030-90870-6_33</a>","ista":"Chatterjee K, Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2021. On lexicographic proof rules for probabilistic termination. 24th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” in <i>24th International Symposium on Formal Methods</i>, Virtual, 2021, vol. 13047, pp. 619–639.","short":"K. Chatterjee, E. Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, in:, 24th International Symposium on Formal Methods, Springer Nature, 2021, pp. 619–639.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” In <i>24th International Symposium on Formal Methods</i>, 13047:619–39. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">https://doi.org/10.1007/978-3-030-90870-6_33</a>.","apa":"Chatterjee, K., Goharshady, E., Novotný, P., Zárevúcky, J., &#38; Zikelic, D. (2021). On lexicographic proof rules for probabilistic termination. In <i>24th International Symposium on Formal Methods</i> (Vol. 13047, pp. 619–639). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">https://doi.org/10.1007/978-3-030-90870-6_33</a>"},"page":"619-639","project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","call_identifier":"H2020","grant_number":"665385"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"14778"},{"status":"public","id":"14539","relation":"dissertation_contains"}]},"date_updated":"2026-04-07T13:27:55Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","publication":"24th International Symposium on Formal Methods","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the Czech Science Foundation grant No. GJ19-15134Y, and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9-783-0309-0869-0"],"eisbn":["978-3-030-90870-6"]},"ec_funded":1,"language":[{"iso":"eng"}]}]