[{"main_file_link":[{"open_access":"1","url":"https://openreview.net/forum?id=mXUDDL4r1Q"}],"status":"public","date_updated":"2025-01-30T07:46:16Z","volume":235,"month":"07","publication_status":"published","OA_type":"green","_id":"18974","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"47331-47344","oa_version":"Preprint","quality_controlled":"1","publication":"41st International Conference on Machine Learning","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"type":"conference","OA_place":"publisher","scopus_import":"1","corr_author":"1","alternative_title":["PMLR"],"title":"Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance","intvolume":"       235","date_created":"2025-01-30T07:45:22Z","year":"2024","article_processing_charge":"No","publisher":"ML Research Press","citation":{"ista":"Svoboda J, Bansal S, Chatterjee K. 2024. Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. 41st International Conference on Machine Learning. ICML: International Conference on Machine Learning, PMLR, vol. 235, 47331–47344.","ieee":"J. Svoboda, S. Bansal, and K. Chatterjee, “Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance,” in <i>41st International Conference on Machine Learning</i>, Vienna, Austria, 2024, vol. 235, pp. 47331–47344.","chicago":"Svoboda, Jakub, Suguman Bansal, and Krishnendu Chatterjee. “Reinforcement Learning from Reachability Specifications: PAC Guarantees with Expected Conditional Distance.” In <i>41st International Conference on Machine Learning</i>, 235:47331–44. ML Research Press, 2024.","apa":"Svoboda, J., Bansal, S., &#38; Chatterjee, K. (2024). Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. In <i>41st International Conference on Machine Learning</i> (Vol. 235, pp. 47331–47344). Vienna, Austria: ML Research Press.","short":"J. Svoboda, S. Bansal, K. Chatterjee, in:, 41st International Conference on Machine Learning, ML Research Press, 2024, pp. 47331–47344.","ama":"Svoboda J, Bansal S, Chatterjee K. Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. In: <i>41st International Conference on Machine Learning</i>. Vol 235. ML Research Press; 2024:47331-47344.","mla":"Svoboda, Jakub, et al. “Reinforcement Learning from Reachability Specifications: PAC Guarantees with Expected Conditional Distance.” <i>41st International Conference on Machine Learning</i>, vol. 235, ML Research Press, 2024, pp. 47331–44."},"day":"29","conference":{"name":"ICML: International Conference on Machine Learning","end_date":"2024-07-27","location":"Vienna, Austria","start_date":"2024-07-21"},"abstract":[{"text":"Reinforcement Learning (RL) from temporal logical specifications is a fundamental problem in sequential decision making. One of the basic and core such specification is the reachability specification that requires a target set to be eventually visited. Despite strong empirical results for RL from such specifications, the theoretical guarantees are bleak, including the impossibility of Probably Approximately Correct (PAC) guarantee for reachability specifications. Given the impossibility result, in this work we consider the problem of RL from reachability specifications along with the information of expected conditional distance (ECD). We present (a) lower bound results which establish the necessity of ECD information for PAC guarantees and (b) an algorithm that establishes PAC-guarantees given the ECD information. To the best of our knowledge, this is the first RL from reachability specifications that does not make any assumptions on the underlying environment to learn policies.","lang":"eng"}],"oa":1,"author":[{"last_name":"Svoboda","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","first_name":"Jakub"},{"first_name":"Suguman","full_name":"Bansal, Suguman","last_name":"Bansal"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"}],"date_published":"2024-07-29T00:00:00Z"},{"has_accepted_license":"1","title":"Equivalence and similarity refutation for probabilistic programs","publication_identifier":{"eissn":["2475-1421"]},"external_id":{"arxiv":["2404.03430"]},"intvolume":"         8","year":"2024","date_created":"2024-07-21T22:01:01Z","ddc":["000"],"file_date_updated":"2024-07-22T07:17:14Z","article_processing_charge":"Yes (via OA deal)","publisher":"Association for Computing Machinery","file":[{"creator":"dernst","success":1,"file_name":"2024_ACMProgLang_Chatterjee.pdf","content_type":"application/pdf","date_updated":"2024-07-22T07:17:14Z","file_size":355421,"date_created":"2024-07-22T07:17:14Z","file_id":"17290","relation":"main_file","checksum":"8cbf220f284a4a87d093db5320c5afdd","access_level":"open_access"}],"citation":{"short":"K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).","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>","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>.","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.","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.","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>","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>."},"day":"20","abstract":[{"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.","lang":"eng"}],"oa":1,"arxiv":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Kafshdar Goharshadi","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587","first_name":"Ehsan","full_name":"Kafshdar Goharshadi, Ehsan"},{"last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","first_name":"Petr"},{"first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic"}],"date_published":"2024-06-20T00:00:00Z","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","article_type":"original","doi":"10.1145/3656462","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"date_updated":"2025-04-14T07:52:47Z","status":"public","publication_status":"published","volume":8,"month":"06","OA_type":"hybrid","_id":"17283","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","article_number":"232","project":[{"call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"publication":"Proceedings of the ACM on Programming Languages","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"type":"journal_article","OA_place":"publisher","scopus_import":"1","corr_author":"1","ec_funded":1},{"publication":" Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing","project":[{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"language":[{"iso":"eng"}],"type":"conference","department":[{"_id":"KrCh"},{"_id":"KrPi"}],"ec_funded":1,"corr_author":"1","scopus_import":"1","date_updated":"2025-04-14T07:52:47Z","status":"public","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"month":"06","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"17328","oa_version":"Published Version","page":"268-278","quality_controlled":"1","conference":{"end_date":"2024-06-21","name":"PODC: Symposium on Principles of Distributed Computing","location":"Nantes, France","start_date":"2024-06-17"},"abstract":[{"text":"We study selfish mining attacks in longest-chain blockchains like Bitcoin, but where the proof of work is replaced with efficient proof systems - like proofs of stake or proofs of space - and consider the problem of computing an optimal selfish mining attack which maximizes expected relative revenue of the adversary, thus minimizing the chain quality. To this end, we propose a novel selfish mining attack that aims to maximize this objective and formally model the attack as a Markov decision process (MDP). We then present a formal analysis procedure which computes an ϵ-tight lower bound on the optimal expected relative revenue in the MDP and a strategy that achieves this ϵ-tight lower bound, where ϵ > 0 may be any specified precision. Our analysis is fully automated and provides formal guarantees on the correctness. We evaluate our selfish mining attack and observe that it achieves superior expected relative revenue compared to two considered baselines.\r\nIn concurrent work [Sarenche FC'24] does an automated analysis on selfish mining in predictable longest-chain blockchains based on efficient proof systems. Predictable means the randomness for the challenges is fixed for many blocks (as used e.g., in Ouroboros), while we consider unpredictable (Bitcoin-like) chains where the challenge is derived from the previous block.","lang":"eng"}],"day":"17","date_published":"2024-06-17T00:00:00Z","oa":1,"arxiv":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Amirali","full_name":"Ebrahimzadeh, Amirali","last_name":"Ebrahimzadeh"},{"last_name":"Karrabi","id":"67638922-f394-11eb-9cf6-f20423e08757","first_name":"Mehrdad","full_name":"Karrabi, Mehrdad"},{"last_name":"Pietrzak","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9139-1654","first_name":"Krzysztof Z","full_name":"Pietrzak, Krzysztof Z"},{"last_name":"Yeo","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","orcid":"0009-0001-3676-4809","full_name":"Yeo, Michelle X","first_name":"Michelle X"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699"}],"acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) grant and the MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms) grant.\r\n","doi":"10.1145/3662158.3662769","title":"Fully automated selfish mining analysis in efficient proof systems blockchains","has_accepted_license":"1","year":"2024","date_created":"2024-07-28T22:01:10Z","publication_identifier":{"isbn":["9798400706684"]},"external_id":{"arxiv":["2405.04420"]},"ddc":["000"],"file_date_updated":"2024-07-29T07:18:12Z","citation":{"chicago":"Chatterjee, Krishnendu, Amirali Ebrahimzadeh, Mehrdad Karrabi, Krzysztof Z Pietrzak, Michelle X Yeo, and Dorde Zikelic. “Fully Automated Selfish Mining Analysis in Efficient Proof Systems Blockchains.” In <i> Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i>, 268–78. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3662158.3662769\">https://doi.org/10.1145/3662158.3662769</a>.","apa":"Chatterjee, K., Ebrahimzadeh, A., Karrabi, M., Pietrzak, K. Z., Yeo, M. X., &#38; Zikelic, D. (2024). Fully automated selfish mining analysis in efficient proof systems blockchains. In <i> Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i> (pp. 268–278). Nantes, France: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3662158.3662769\">https://doi.org/10.1145/3662158.3662769</a>","ista":"Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D. 2024. Fully automated selfish mining analysis in efficient proof systems blockchains.  Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing. PODC: Symposium on Principles of Distributed Computing, 268–278.","ieee":"K. Chatterjee, A. Ebrahimzadeh, M. Karrabi, K. Z. Pietrzak, M. X. Yeo, and D. Zikelic, “Fully automated selfish mining analysis in efficient proof systems blockchains,” in <i> Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i>, Nantes, France, 2024, pp. 268–278.","mla":"Chatterjee, Krishnendu, et al. “Fully Automated Selfish Mining Analysis in Efficient Proof Systems Blockchains.” <i> Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i>, Association for Computing Machinery, 2024, pp. 268–78, doi:<a href=\"https://doi.org/10.1145/3662158.3662769\">10.1145/3662158.3662769</a>.","ama":"Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D. Fully automated selfish mining analysis in efficient proof systems blockchains. In: <i> Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i>. Association for Computing Machinery; 2024:268-278. doi:<a href=\"https://doi.org/10.1145/3662158.3662769\">10.1145/3662158.3662769</a>","short":"K. Chatterjee, A. Ebrahimzadeh, M. Karrabi, K.Z. Pietrzak, M.X. Yeo, D. Zikelic, in:,  Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing, Association for Computing Machinery, 2024, pp. 268–278."},"article_processing_charge":"Yes (via OA deal)","publisher":"Association for Computing Machinery","file":[{"file_id":"17334","relation":"main_file","access_level":"open_access","checksum":"6122bd97b42751ff81c452a19970f67d","date_updated":"2024-07-29T07:18:12Z","file_size":832034,"file_name":"2024_ACM_Chatterjee.pdf","creator":"dernst","success":1,"content_type":"application/pdf","date_created":"2024-07-29T07:18:12Z"}]},{"publication_status":"published","month":"06","status":"public","date_updated":"2025-04-14T07:52:47Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"quality_controlled":"1","page":"40-49","_id":"17329","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","language":[{"iso":"eng"}],"publication":"Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"}],"ec_funded":1,"scopus_import":"1","corr_author":"1","type":"conference","department":[{"_id":"DaAl"},{"_id":"KrCh"}],"date_created":"2024-07-28T22:01:10Z","year":"2024","publication_identifier":{"isbn":["9798400706684"]},"title":"Game dynamics and equilibrium computation in the population protocol model","has_accepted_license":"1","citation":{"short":"D.-A. Alistarh, K. Chatterjee, M. Karrabi, J.M. Lazarsfeld, in:, Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing, Association for Computing Machinery, 2024, pp. 40–49.","ama":"Alistarh D-A, Chatterjee K, Karrabi M, Lazarsfeld JM. Game dynamics and equilibrium computation in the population protocol model. In: <i>Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i>. Association for Computing Machinery; 2024:40-49. doi:<a href=\"https://doi.org/10.1145/3662158.3662768\">10.1145/3662158.3662768</a>","mla":"Alistarh, Dan-Adrian, et al. “Game Dynamics and Equilibrium Computation in the Population Protocol Model.” <i>Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i>, Association for Computing Machinery, 2024, pp. 40–49, doi:<a href=\"https://doi.org/10.1145/3662158.3662768\">10.1145/3662158.3662768</a>.","ieee":"D.-A. Alistarh, K. Chatterjee, M. Karrabi, and J. M. Lazarsfeld, “Game dynamics and equilibrium computation in the population protocol model,” in <i>Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i>, Nantes, France, 2024, pp. 40–49.","ista":"Alistarh D-A, Chatterjee K, Karrabi M, Lazarsfeld JM. 2024. Game dynamics and equilibrium computation in the population protocol model. Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing. PODC: Symposium on Principles of Distributed Computing, 40–49.","apa":"Alistarh, D.-A., Chatterjee, K., Karrabi, M., &#38; Lazarsfeld, J. M. (2024). Game dynamics and equilibrium computation in the population protocol model. In <i>Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i> (pp. 40–49). Nantes, France: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3662158.3662768\">https://doi.org/10.1145/3662158.3662768</a>","chicago":"Alistarh, Dan-Adrian, Krishnendu Chatterjee, Mehrdad Karrabi, and John M Lazarsfeld. “Game Dynamics and Equilibrium Computation in the Population Protocol Model.” In <i>Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing</i>, 40–49. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3662158.3662768\">https://doi.org/10.1145/3662158.3662768</a>."},"publisher":"Association for Computing Machinery","file":[{"access_level":"open_access","checksum":"65a40437f83373fa79dd999d5287509e","relation":"main_file","file_id":"17335","date_created":"2024-07-29T07:37:31Z","content_type":"application/pdf","file_name":"2024_ACMPODC_Alistarh.pdf","creator":"dernst","success":1,"file_size":750908,"date_updated":"2024-07-29T07:37:31Z"}],"article_processing_charge":"Yes (via OA deal)","ddc":["000"],"file_date_updated":"2024-07-29T07:37:31Z","date_published":"2024-06-17T00:00:00Z","author":[{"id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","last_name":"Alistarh","full_name":"Alistarh, Dan-Adrian","first_name":"Dan-Adrian","orcid":"0000-0003-3650-940X"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Karrabi","id":"67638922-f394-11eb-9cf6-f20423e08757","full_name":"Karrabi, Mehrdad","first_name":"Mehrdad"},{"full_name":"Lazarsfeld, John M","first_name":"John M","last_name":"Lazarsfeld","id":"17ce3656-183e-11ef-84c3-8932383e1b23"}],"oa":1,"abstract":[{"lang":"eng","text":"We initiate the study of game dynamics in the population protocol model: n agents each maintain a current local strategy and interact in pairs uniformly at random. Upon each interaction, the agents play a two-person game and receive a payoff from an underlying utility function, and they can subsequently update their strategies according to a fixed local algorithm. In this setting, we ask how the distribution over agent strategies evolves over a sequence of interactions, and we introduce a new distributional equilibrium concept to quantify the quality of such distributions. As an initial example, we study a class of repeated prisoner's dilemma games, and we consider a family of simple local update algorithms that yield non-trivial dynamics over the distribution of agent strategies. We show that these dynamics are related to a new class of high-dimensional Ehrenfest random walks, and we derive exact characterizations of their stationary distributions, bounds on their mixing times, and prove their convergence to approximate distributional equilibria. Our results highlight trade-offs between the local state space of each agent, and the convergence rate and approximation factor of the underlying dynamics. Our approach opens the door towards the further characterization of equilibrium computation for other classes of games and dynamics in the population setting."}],"conference":{"location":"Nantes, France","start_date":"2024-06-17","end_date":"2024-06-21","name":"PODC: Symposium on Principles of Distributed Computing"},"day":"17","doi":"10.1145/3662158.3662768","acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) grant. We thank James Aspnes and Thomas Sauerwald for several helpful discussions on Ehrenfest random walks."},{"publisher":"Springer Nature","file":[{"date_created":"2024-08-12T08:39:12Z","content_type":"application/pdf","file_name":"2024_CAV_Meggendorfer.pdf","creator":"dernst","success":1,"file_size":368487,"date_updated":"2024-08-12T08:39:12Z","checksum":"c888231d0a47b55786b7b4c0f02216bb","access_level":"open_access","relation":"main_file","file_id":"17419"}],"article_processing_charge":"Yes (in subscription journal)","citation":{"chicago":"Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games.” In <i>36th International Conference on Computer Aided Verification</i>, 14683:359–72. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-65633-0_16\">https://doi.org/10.1007/978-3-031-65633-0_16</a>.","apa":"Meggendorfer, T., &#38; Weininger, M. (2024). Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. In <i>36th International Conference on Computer Aided Verification</i> (Vol. 14683, pp. 359–372). Montreal, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-65633-0_16\">https://doi.org/10.1007/978-3-031-65633-0_16</a>","ista":"Meggendorfer T, Weininger M. 2024. Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. 36th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 14683, 359–372.","ieee":"T. Meggendorfer and M. Weininger, “Playing games with your PET: Extending the Partial Exploration Tool to stochastic games,” in <i>36th International Conference on Computer Aided Verification</i>, Montreal, Canada, 2024, vol. 14683, pp. 359–372.","mla":"Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games.” <i>36th International Conference on Computer Aided Verification</i>, vol. 14683, Springer Nature, 2024, pp. 359–72, doi:<a href=\"https://doi.org/10.1007/978-3-031-65633-0_16\">10.1007/978-3-031-65633-0_16</a>.","ama":"Meggendorfer T, Weininger M. Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. In: <i>36th International Conference on Computer Aided Verification</i>. Vol 14683. Springer Nature; 2024:359-372. doi:<a href=\"https://doi.org/10.1007/978-3-031-65633-0_16\">10.1007/978-3-031-65633-0_16</a>","short":"T. Meggendorfer, M. Weininger, in:, 36th International Conference on Computer Aided Verification, Springer Nature, 2024, pp. 359–372."},"file_date_updated":"2024-08-12T08:39:12Z","ddc":["000"],"external_id":{"isi":["001307897000016"],"arxiv":["2405.03885"]},"publication_identifier":{"issn":["0302-9743"],"eisbn":["9783031656330"],"eissn":["1611-3349"],"isbn":["9783031656323"]},"year":"2024","date_created":"2024-08-09T11:24:54Z","intvolume":"     14683","has_accepted_license":"1","title":"Playing games with your PET: Extending the Partial Exploration Tool to stochastic games","doi":"10.1007/978-3-031-65633-0_16","acknowledgement":"M. Weininger has received funding from the EU’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101034413.","arxiv":1,"author":[{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"},{"last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","first_name":"Maximilian"}],"oa":1,"date_published":"2024-07-01T00:00:00Z","day":"01","conference":{"start_date":"2024-07-24","location":"Montreal, Canada","end_date":"2024-07-27","name":"CAV: Computer Aided Verification"},"abstract":[{"text":"We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic games, based on a recent unified framework for sound value iteration algorithms. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability/safety and mean payoff. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.","lang":"eng"}],"quality_controlled":"1","_id":"17402","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"Published Version","page":"359-372","isi":1,"month":"07","volume":14683,"publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"date_updated":"2025-09-08T08:53:55Z","status":"public","corr_author":"1","scopus_import":"1","ec_funded":1,"alternative_title":["LNCS"],"department":[{"_id":"KrCh"}],"type":"conference","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"publication":"36th International Conference on Computer Aided Verification"},{"corr_author":"1","scopus_import":"1","type":"journal_article","OA_place":"publisher","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"publication":"Information and Computation","quality_controlled":"1","article_number":"105214","related_material":{"record":[{"relation":"earlier_version","id":"14417","status":"public"}]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","_id":"17474","oa_version":"Published Version","OA_type":"hybrid","volume":301,"publication_status":"published","month":"12","isi":1,"status":"public","date_updated":"2025-09-08T09:10:06Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.1016/j.ic.2024.105214","article_type":"original","acknowledgement":"Krishnendu Chatterjee reports financial support was provided by European Research Council.","date_published":"2024-12-01T00:00:00Z","oa":1,"arxiv":1,"author":[{"first_name":"Christel","full_name":"Baier, Christel","last_name":"Baier"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer"},{"last_name":"Piribauer","full_name":"Piribauer, Jakob","first_name":"Jakob"}],"abstract":[{"text":"Entropic risk (ERisk) is an established risk measure in finance, quantifying risk by an exponential re-weighting of rewards. We study ERisk for the first time in the context of turn-based stochastic games with the total reward objective. This gives rise to an objective function that demands the control of systems in a risk-averse manner. We show that the resulting games are determined and, in particular, admit optimal memoryless deterministic strategies. This contrasts risk measures that previously have been considered in the special case of Markov decision processes and that require randomization and/or memory. We provide several results on the decidability and the computational complexity of the threshold problem, i.e. whether the optimal value of ERisk exceeds a given threshold. Furthermore, an approximation algorithm for the optimal value of ERisk is provided.","lang":"eng"}],"day":"01","citation":{"ama":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Entropic risk for turn-based stochastic games. <i>Information and Computation</i>. 2024;301. doi:<a href=\"https://doi.org/10.1016/j.ic.2024.105214\">10.1016/j.ic.2024.105214</a>","mla":"Baier, Christel, et al. “Entropic Risk for Turn-Based Stochastic Games.” <i>Information and Computation</i>, vol. 301, 105214, Elsevier, 2024, doi:<a href=\"https://doi.org/10.1016/j.ic.2024.105214\">10.1016/j.ic.2024.105214</a>.","short":"C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, Information and Computation 301 (2024).","apa":"Baier, C., Chatterjee, K., Meggendorfer, T., &#38; Piribauer, J. (2024). Entropic risk for turn-based stochastic games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2024.105214\">https://doi.org/10.1016/j.ic.2024.105214</a>","chicago":"Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer. “Entropic Risk for Turn-Based Stochastic Games.” <i>Information and Computation</i>. Elsevier, 2024. <a href=\"https://doi.org/10.1016/j.ic.2024.105214\">https://doi.org/10.1016/j.ic.2024.105214</a>.","ieee":"C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Entropic risk for turn-based stochastic games,” <i>Information and Computation</i>, vol. 301. Elsevier, 2024.","ista":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2024. Entropic risk for turn-based stochastic games. Information and Computation. 301, 105214."},"file":[{"file_id":"18817","relation":"main_file","access_level":"open_access","checksum":"f68e0c2f46f9b9c86815406bcf2ee2d4","file_size":724703,"date_updated":"2025-01-09T13:49:03Z","file_name":"2024_InformationComputation_Baier.pdf","success":1,"creator":"dernst","content_type":"application/pdf","date_created":"2025-01-09T13:49:03Z"}],"publisher":"Elsevier","article_processing_charge":"Yes (in subscription journal)","file_date_updated":"2025-01-09T13:49:03Z","ddc":["000"],"intvolume":"       301","year":"2024","date_created":"2024-09-01T22:01:07Z","publication_identifier":{"eissn":["1090-2651"],"issn":["0890-5401"]},"external_id":{"arxiv":["2307.06611"],"isi":["001301143400001"]},"title":"Entropic risk for turn-based stochastic games","has_accepted_license":"1"},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2025-09-08T09:51:34Z","isi":1,"month":"09","volume":14933,"publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","_id":"18155","page":"600-619","oa_version":"Published Version","quality_controlled":"1","project":[{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"type":"conference","corr_author":"1","scopus_import":"1","alternative_title":["LNCS"],"ec_funded":1,"has_accepted_license":"1","title":"Sound and complete witnesses for template-based verification of LTL properties on polynomial programs","external_id":{"arxiv":["2403.05386"],"isi":["001336893300031"]},"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031711619"],"eissn":["1611-3349"]},"date_created":"2024-09-29T22:01:37Z","year":"2024","intvolume":"     14933","ddc":["000"],"file_date_updated":"2024-10-01T09:56:54Z","article_processing_charge":"Yes (in subscription journal)","publisher":"Springer Nature","file":[{"access_level":"open_access","checksum":"223845be9e754681ee218866827c95e7","relation":"main_file","file_id":"18165","date_created":"2024-10-01T09:56:54Z","content_type":"application/pdf","creator":"dernst","success":1,"file_name":"2024_LNCS_Chatterjee.pdf","file_size":650495,"date_updated":"2024-10-01T09:56:54Z"}],"citation":{"short":"K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, D. Zikelic, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp. 600–619.","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 14933, Springer Nature, 2024, pp. 600–19, doi:<a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">10.1007/978-3-031-71162-6_31</a>.","ama":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 14933. Springer Nature; 2024:600-619. doi:<a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">10.1007/978-3-031-71162-6_31</a>","ieee":"K. Chatterjee, A. K. Goharshady, E. Goharshady, M. Karrabi, and D. Zikelic, “Sound and complete witnesses for template-based verification of LTL properties on polynomial programs,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Milan, Italy, 2024, vol. 14933, pp. 600–619.","ista":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods, LNCS, vol. 14933, 600–619.","apa":"Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., &#38; Zikelic, D. (2024). Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 14933, pp. 600–619). Milan, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">https://doi.org/10.1007/978-3-031-71162-6_31</a>","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad Karrabi, and Dorde Zikelic. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 14933:600–619. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">https://doi.org/10.1007/978-3-031-71162-6_31</a>."},"day":"11","conference":{"name":"FM: Formal Methods","end_date":"2024-09-13","start_date":"2024-09-09","location":"Milan, Italy"},"abstract":[{"lang":"eng","text":"We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools."}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar"},{"first_name":"Ehsan","full_name":"Goharshady, Ehsan","last_name":"Goharshady"},{"id":"67638922-f394-11eb-9cf6-f20423e08757","last_name":"Karrabi","first_name":"Mehrdad","full_name":"Karrabi, Mehrdad"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699"}],"arxiv":1,"oa":1,"date_published":"2024-09-11T00:00:00Z","acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Hong Kong Research Grants Council ECS Project Number 26208122.","doi":"10.1007/978-3-031-71162-6_31"},{"_id":"18159","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"3-12","quality_controlled":"1","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2405.04015","open_access":"1"}],"date_updated":"2025-04-14T07:52:46Z","status":"public","month":"09","publication_status":"published","department":[{"_id":"KrCh"}],"type":"conference","corr_author":"1","scopus_import":"1","ec_funded":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"}],"publication":"Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence","language":[{"iso":"eng"}],"publisher":"International Joint Conferences on Artificial Intelligence","article_processing_charge":"No","citation":{"ista":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2024. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 3–12.","ieee":"S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties,” in <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, Jeju, Korea, 2024, pp. 3–12.","chicago":"Akshay, S, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. “Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.” In <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, 3–12. International Joint Conferences on Artificial Intelligence, 2024. <a href=\"https://doi.org/10.24963/ijcai.2024/1\">https://doi.org/10.24963/ijcai.2024/1</a>.","apa":"Akshay, S., Chatterjee, K., Meggendorfer, T., &#38; Zikelic, D. (2024). Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. In <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i> (pp. 3–12). Jeju, Korea: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2024/1\">https://doi.org/10.24963/ijcai.2024/1</a>","short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 3–12.","mla":"Akshay, S., et al. “Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.” <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2024, pp. 3–12, doi:<a href=\"https://doi.org/10.24963/ijcai.2024/1\">10.24963/ijcai.2024/1</a>.","ama":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. In: <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2024:3-12. doi:<a href=\"https://doi.org/10.24963/ijcai.2024/1\">10.24963/ijcai.2024/1</a>"},"title":"Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties","publication_identifier":{"isbn":["9781956792041"],"issn":["1045-0823"]},"external_id":{"arxiv":["2405.04015"]},"year":"2024","date_created":"2024-09-29T22:01:38Z","acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt), the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant, Google Research Award 2023 and the SBI Foundation Hub for Data and Analytics.","doi":"10.24963/ijcai.2024/1","day":"01","abstract":[{"lang":"eng","text":"Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defned with respect to paths over MDP states. An increasingly\r\npopular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defned in terms of probability distributions over states. Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verifcation techniques. In this work, we consider the problems of certifed policy (i.e. controller) verifcation and synthesis in MDPs under distributional reach-avoidance specifcations. By certifed we mean that, along with a policy, we also aim to synthesize a (checkable) certifcate ensuring that the MDP indeed satisfes the property. Thus, given the target set of distributions and an unsafe set of distributions over MDP states, our goal is to either synthesize a certifcate for a given policy or synthesize a policy along with a certifcate, proving that the target distribution can be reached while avoiding unsafe distributions. To solve this problem, we introduce the novel notion of distributional reach-avoid certifcates and present automated procedures for (1) synthesizing a certifcate for a given policy, and (2) synthesizing a policy together with the certifcate, both providing formal guarantees on certifcate correctness. Our experimental evaluation demonstrates the ability of our method to solve several non-trivial examples, including a multi-agent robot-swarm model, to synthesize certifed policies and to certify existing policies. "}],"conference":{"end_date":"2024-08-09","name":"IJCAI: International Joint Conference on Artificial Intelligence","location":"Jeju, Korea","start_date":"2024-08-03"},"oa":1,"arxiv":1,"author":[{"full_name":"Akshay, S","first_name":"S","last_name":"Akshay"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"},{"last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","full_name":"Zikelic, Dorde"}],"date_published":"2024-09-01T00:00:00Z"},{"doi":"10.24963/ijcai.2024/741","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.","arxiv":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Ehsan","full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","last_name":"Kafshdar Goharshadi"},{"full_name":"Karrabi, Mehrdad","first_name":"Mehrdad","last_name":"Karrabi","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"first_name":"Petr","full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný"},{"full_name":"Zikelic, Dorde","first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic"}],"oa":1,"date_published":"2024-09-01T00:00:00Z","day":"01","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"}],"conference":{"location":"Jeju, South Korea","start_date":"2024-08-03","end_date":"2024-08-09","name":"IJCAI: International Joint Conference on Artificial Intelligence"},"article_processing_charge":"No","publisher":"International Joint Conferences on Artificial Intelligence","citation":{"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.","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.","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.","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>","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>."},"external_id":{"arxiv":["2312.13912"]},"publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"year":"2024","date_created":"2024-09-29T22:01:39Z","title":"Solving long-run average reward robust MDPs via stochastic games","scopus_import":"1","corr_author":"1","ec_funded":1,"department":[{"_id":"KrCh"}],"type":"conference","OA_place":"repository","language":[{"iso":"eng"}],"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"}],"publication":"33rd International Joint Conference on Artificial Intelligence","quality_controlled":"1","page":"6707-6715","_id":"18160","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","publication_status":"published","month":"09","OA_type":"green","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2312.13912"}],"status":"public","date_updated":"2025-04-14T07:52:46Z"},{"type":"journal_article","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"ec_funded":1,"scopus_import":"1","corr_author":"1","publication":"Mathematics of Operations Research","project":[{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"language":[{"iso":"eng"}],"_id":"18266","page":"2433-3282","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","quality_controlled":"1","related_material":{"record":[{"relation":"dissertation_contains","id":"20234","status":"public"}]},"status":"public","date_updated":"2026-04-07T12:31:21Z","OA_type":"closed access","month":"10","publication_status":"published","volume":50,"isi":1,"article_type":"original","issue":"4","acknowledgement":"This research was supported by Fondation CFM pour la Recherche, the H2020 European Research Council [Grant ERC-CoG-863818 (ForM-SMArt)], the Austrian Science Fund [Grant 10.55776/COE12], ANID Chile [Grant ACT210005], and Agence Nationale de la Recherche [Grant ANR-21-CE40-0020].","doi":"10.1287/moor.2022.0332","abstract":[{"lang":"eng","text":"Matrix games are the most basic model in game theory, and yet robustness with respect to small perturbations of the matrix entries is not fully understood. In this paper, we introduce value positivity and uniform value positivity, two properties that refine the notion of optimality in the context of polynomially perturbed matrix games. The first concept captures how the value depends on the perturbation parameter, and the second consists of the existence of a fixed strategy that guarantees the value of the unperturbed matrix game for every sufficiently small positive parameter. We provide polynomial-time algorithms to check whether a polynomially perturbed matrix game satisfies these properties. We further provide the functional form for a parameterized optimal strategy and the value function. Finally, we translate our results to linear programming and stochastic games, where value positivity is related to the existence of robust solutions."}],"day":"01","date_published":"2024-10-01T00:00:00Z","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Miquel","full_name":"Oliu-Barton, Miquel","last_name":"Oliu-Barton"},{"last_name":"Saona Urmeneta","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","orcid":"0000-0001-5103-038X","full_name":"Saona Urmeneta, Raimundo J","first_name":"Raimundo J"}],"citation":{"chicago":"Chatterjee, Krishnendu, Miquel Oliu-Barton, and Raimundo J Saona Urmeneta. “Value-Positivity for Matrix Games.” <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences, 2024. <a href=\"https://doi.org/10.1287/moor.2022.0332\">https://doi.org/10.1287/moor.2022.0332</a>.","apa":"Chatterjee, K., Oliu-Barton, M., &#38; Saona Urmeneta, R. J. (2024). Value-positivity for matrix games. <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences. <a href=\"https://doi.org/10.1287/moor.2022.0332\">https://doi.org/10.1287/moor.2022.0332</a>","ista":"Chatterjee K, Oliu-Barton M, Saona Urmeneta RJ. 2024. Value-positivity for matrix games. Mathematics of Operations Research. 50(4), 2433–3282.","ieee":"K. Chatterjee, M. Oliu-Barton, and R. J. Saona Urmeneta, “Value-positivity for matrix games,” <i>Mathematics of Operations Research</i>, vol. 50, no. 4. Institute for Operations Research and the Management Sciences, pp. 2433–3282, 2024.","ama":"Chatterjee K, Oliu-Barton M, Saona Urmeneta RJ. Value-positivity for matrix games. <i>Mathematics of Operations Research</i>. 2024;50(4):2433-3282. doi:<a href=\"https://doi.org/10.1287/moor.2022.0332\">10.1287/moor.2022.0332</a>","mla":"Chatterjee, Krishnendu, et al. “Value-Positivity for Matrix Games.” <i>Mathematics of Operations Research</i>, vol. 50, no. 4, Institute for Operations Research and the Management Sciences, 2024, pp. 2433–3282, doi:<a href=\"https://doi.org/10.1287/moor.2022.0332\">10.1287/moor.2022.0332</a>.","short":"K. Chatterjee, M. Oliu-Barton, R.J. Saona Urmeneta, Mathematics of Operations Research 50 (2024) 2433–3282."},"article_processing_charge":"No","publisher":"Institute for Operations Research and the Management Sciences","title":"Value-positivity for matrix games","intvolume":"        50","date_created":"2024-10-09T07:02:20Z","year":"2024","publication_identifier":{"issn":["0364-765X"],"eissn":["1526-5471"]},"external_id":{"isi":["001328875900001"]}},{"citation":{"ama":"Chatterjee K, Meggendorfer T, Saona Urmeneta RJ, Svoboda J. Faster algorithm for turn-based stochastic games with bounded treewidth. In: <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i>. Society for Industrial and Applied Mathematics; 2023:4590-4605. doi:<a href=\"https://doi.org/10.1137/1.9781611977554.ch173\">10.1137/1.9781611977554.ch173</a>","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithm for Turn-Based Stochastic Games with Bounded Treewidth.” <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i>, Society for Industrial and Applied Mathematics, 2023, pp. 4590–605, doi:<a href=\"https://doi.org/10.1137/1.9781611977554.ch173\">10.1137/1.9781611977554.ch173</a>.","short":"K. Chatterjee, T. Meggendorfer, R.J. Saona Urmeneta, J. Svoboda, in:, Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial and Applied Mathematics, 2023, pp. 4590–4605.","apa":"Chatterjee, K., Meggendorfer, T., Saona Urmeneta, R. J., &#38; Svoboda, J. (2023). Faster algorithm for turn-based stochastic games with bounded treewidth. In <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i> (pp. 4590–4605). Florence, Italy: Society for Industrial and Applied Mathematics. <a href=\"https://doi.org/10.1137/1.9781611977554.ch173\">https://doi.org/10.1137/1.9781611977554.ch173</a>","chicago":"Chatterjee, Krishnendu, Tobias Meggendorfer, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Faster Algorithm for Turn-Based Stochastic Games with Bounded Treewidth.” In <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i>, 4590–4605. Society for Industrial and Applied Mathematics, 2023. <a href=\"https://doi.org/10.1137/1.9781611977554.ch173\">https://doi.org/10.1137/1.9781611977554.ch173</a>.","ieee":"K. Chatterjee, T. Meggendorfer, R. J. Saona Urmeneta, and J. Svoboda, “Faster algorithm for turn-based stochastic games with bounded treewidth,” in <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i>, Florence, Italy, 2023, pp. 4590–4605.","ista":"Chatterjee K, Meggendorfer T, Saona Urmeneta RJ, Svoboda J. 2023. Faster algorithm for turn-based stochastic games with bounded treewidth. Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 4590–4605."},"publisher":"Society for Industrial and Applied Mathematics","article_processing_charge":"No","ddc":["000"],"date_created":"2023-02-24T12:20:47Z","year":"2023","publication_identifier":{"isbn":["9781611977554"]},"title":"Faster algorithm for turn-based stochastic games with bounded treewidth","doi":"10.1137/1.9781611977554.ch173","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant.","date_published":"2023-02-01T00:00:00Z","oa":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer"},{"orcid":"0000-0001-5103-038X","full_name":"Saona Urmeneta, Raimundo J","first_name":"Raimundo J","last_name":"Saona Urmeneta","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"first_name":"Jakub","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda"}],"conference":{"location":"Florence, Italy","start_date":"2023-01-22","end_date":"2023-01-25","name":"SODA: Symposium on Discrete Algorithms"},"abstract":[{"lang":"eng","text":"Turn-based stochastic games (aka simple stochastic games) are two-player zero-sum games played on directed graphs with probabilistic transitions. The goal of player-max is to maximize the probability to reach a target state against the adversarial player-min. These games lie in NP ∩ coNP and are among the rare combinatorial problems that belong to this complexity class for which the existence of polynomial-time algorithm is a major open question. While randomized sub-exponential time algorithm exists, all known deterministic algorithms require exponential time in the worst-case. An important open question has been whether faster algorithms can be obtained parametrized by the treewidth of the game graph. Even deterministic sub-exponential time algorithm for constant treewidth turn-based stochastic games has remain elusive. In this work our main result is a deterministic algorithm to solve turn-based stochastic games that, given a game with n states, treewidth at most t, and the bit-complexity of the probabilistic transition function log D, has running time O ((tn2 log D)t log n). In particular, our algorithm is quasi-polynomial time for games with constant or poly-logarithmic treewidth."}],"day":"01","quality_controlled":"1","oa_version":"Published Version","_id":"12676","page":"4590-4605","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","month":"02","status":"public","date_updated":"2026-06-18T17:28:38Z","main_file_link":[{"url":"https://doi.org/10.1137/1.9781611977554.ch173","open_access":"1"}],"ec_funded":1,"corr_author":"1","type":"conference","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"publication":"Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms","project":[{"grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}]},{"publication_identifier":{"eissn":["1932-6203"]},"external_id":{"isi":["000996122900022"],"pmid":["36848357"]},"intvolume":"        18","year":"2023","date_created":"2023-03-05T23:01:05Z","has_accepted_license":"1","title":"Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations","pmid":1,"article_processing_charge":"No","publisher":"Public Library of Science","file":[{"checksum":"798ed5739a4117b03173e5d56e0534c9","access_level":"open_access","relation":"main_file","file_id":"12712","date_created":"2023-03-07T10:26:45Z","content_type":"application/pdf","success":1,"file_name":"2023_PLOSOne_Mckerral.pdf","creator":"cchlebak","file_size":1257003,"date_updated":"2023-03-07T10:26:45Z"}],"citation":{"mla":"Mckerral, Jody C., et al. “Empirical Parameterisation and Dynamical Analysis of the Allometric Rosenzweig-MacArthur Equations.” <i>PLoS One</i>, vol. 18, no. 2, Public Library of Science, 2023, p. e0279838, doi:<a href=\"https://doi.org/10.1371/journal.pone.0279838\">10.1371/journal.pone.0279838</a>.","ama":"Mckerral JC, Kleshnina M, Ejov V, Bartle L, Mitchell JG, Filar JA. Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations. <i>PLoS One</i>. 2023;18(2):e0279838. doi:<a href=\"https://doi.org/10.1371/journal.pone.0279838\">10.1371/journal.pone.0279838</a>","short":"J.C. Mckerral, M. Kleshnina, V. Ejov, L. Bartle, J.G. Mitchell, J.A. Filar, PLoS One 18 (2023) e0279838.","chicago":"Mckerral, Jody C., Maria Kleshnina, Vladimir Ejov, Louise Bartle, James G. Mitchell, and Jerzy A. Filar. “Empirical Parameterisation and Dynamical Analysis of the Allometric Rosenzweig-MacArthur Equations.” <i>PLoS One</i>. Public Library of Science, 2023. <a href=\"https://doi.org/10.1371/journal.pone.0279838\">https://doi.org/10.1371/journal.pone.0279838</a>.","apa":"Mckerral, J. C., Kleshnina, M., Ejov, V., Bartle, L., Mitchell, J. G., &#38; Filar, J. A. (2023). Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations. <i>PLoS One</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0279838\">https://doi.org/10.1371/journal.pone.0279838</a>","ieee":"J. C. Mckerral, M. Kleshnina, V. Ejov, L. Bartle, J. G. Mitchell, and J. A. Filar, “Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations,” <i>PLoS One</i>, vol. 18, no. 2. Public Library of Science, p. e0279838, 2023.","ista":"Mckerral JC, Kleshnina M, Ejov V, Bartle L, Mitchell JG, Filar JA. 2023. Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations. PLoS One. 18(2), e0279838."},"ddc":["000"],"file_date_updated":"2023-03-07T10:26:45Z","oa":1,"author":[{"full_name":"Mckerral, Jody C.","first_name":"Jody C.","last_name":"Mckerral"},{"first_name":"Maria","full_name":"Kleshnina, Maria","id":"4E21749C-F248-11E8-B48F-1D18A9856A87","last_name":"Kleshnina"},{"last_name":"Ejov","first_name":"Vladimir","full_name":"Ejov, Vladimir"},{"full_name":"Bartle, Louise","first_name":"Louise","last_name":"Bartle"},{"last_name":"Mitchell","full_name":"Mitchell, James G.","first_name":"James G."},{"full_name":"Filar, Jerzy A.","first_name":"Jerzy A.","last_name":"Filar"}],"date_published":"2023-02-27T00:00:00Z","day":"27","abstract":[{"lang":"eng","text":"Allometric settings of population dynamics models are appealing due to their parsimonious nature and broad utility when studying system level effects. Here, we parameterise the size-scaled Rosenzweig-MacArthur differential equations to eliminate prey-mass dependency, facilitating an in depth analytic study of the equations which incorporates scaling parameters’ contributions to coexistence. We define the functional response term to match empirical findings, and examine situations where metabolic theory derivations and observation diverge. The dynamical properties of the Rosenzweig-MacArthur system, encompassing the distribution of size-abundance equilibria, the scaling of period and amplitude of population cycling, and relationships between predator and prey abundances, are consistent with empirical observation. Our parameterisation is an accurate minimal model across 15+ orders of mass magnitude."}],"doi":"10.1371/journal.pone.0279838","issue":"2","acknowledgement":"This research was supported by an Australian Government Research Training Program\r\n(RTP) Scholarship to JCM (https://www.dese.gov.au), and LB is supported by the Centre de\r\nrecherche sur le vieillissement Fellowship Program. The funders had no role in study design, data collection and analysis, decision to publish, or preparation of the manuscript.","article_type":"original","month":"02","volume":18,"publication_status":"published","isi":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2023-10-17T12:53:30Z","quality_controlled":"1","_id":"12706","oa_version":"Published Version","page":"e0279838","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"publication":"PLoS One","scopus_import":"1","department":[{"_id":"KrCh"}],"type":"journal_article"},{"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"20138"}],"link":[{"relation":"research_data","url":"https://doi.org/10.6084/m9.figshare.21261771.v1"}]},"article_number":"20220685","quality_controlled":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"12787","oa_version":"Published Version","isi":1,"month":"03","volume":479,"publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2026-04-07T11:49:11Z","scopus_import":"1","ec_funded":1,"department":[{"_id":"KrCh"}],"type":"journal_article","language":[{"iso":"eng"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"}],"publication":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","file":[{"checksum":"13953d349fbefcb5d21ccc6b303297eb","access_level":"open_access","relation":"main_file","file_id":"12796","date_created":"2023-04-03T06:25:29Z","file_size":827784,"date_updated":"2023-04-03T06:25:29Z","content_type":"application/pdf","file_name":"2023_ProceedingsRoyalSocietyA_Svoboda.pdf","success":1,"creator":"dernst"}],"article_processing_charge":"No","publisher":"The Royal Society","citation":{"short":"J. Svoboda, J. Tkadlec, K. Kaveh, K. Chatterjee, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 479 (2023).","mla":"Svoboda, Jakub, et al. “Coexistence Times in the Moran Process with Environmental Heterogeneity.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 479, no. 2271, 20220685, The Royal Society, 2023, doi:<a href=\"https://doi.org/10.1098/rspa.2022.0685\">10.1098/rspa.2022.0685</a>.","ama":"Svoboda J, Tkadlec J, Kaveh K, Chatterjee K. Coexistence times in the Moran process with environmental heterogeneity. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. 2023;479(2271). doi:<a href=\"https://doi.org/10.1098/rspa.2022.0685\">10.1098/rspa.2022.0685</a>","ista":"Svoboda J, Tkadlec J, Kaveh K, Chatterjee K. 2023. Coexistence times in the Moran process with environmental heterogeneity. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences. 479(2271), 20220685.","ieee":"J. Svoboda, J. Tkadlec, K. Kaveh, and K. Chatterjee, “Coexistence times in the Moran process with environmental heterogeneity,” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 479, no. 2271. The Royal Society, 2023.","apa":"Svoboda, J., Tkadlec, J., Kaveh, K., &#38; Chatterjee, K. (2023). Coexistence times in the Moran process with environmental heterogeneity. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. The Royal Society. <a href=\"https://doi.org/10.1098/rspa.2022.0685\">https://doi.org/10.1098/rspa.2022.0685</a>","chicago":"Svoboda, Jakub, Josef Tkadlec, Kamran Kaveh, and Krishnendu Chatterjee. “Coexistence Times in the Moran Process with Environmental Heterogeneity.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. The Royal Society, 2023. <a href=\"https://doi.org/10.1098/rspa.2022.0685\">https://doi.org/10.1098/rspa.2022.0685</a>."},"file_date_updated":"2023-04-03T06:25:29Z","ddc":["000"],"external_id":{"isi":["000957125500002"]},"publication_identifier":{"issn":["1364-5021"],"eissn":["1471-2946"]},"year":"2023","date_created":"2023-04-02T22:01:09Z","intvolume":"       479","has_accepted_license":"1","title":"Coexistence times in the Moran process with environmental heterogeneity","doi":"10.1098/rspa.2022.0685","acknowledgement":"J.S. and K.C. acknowledge support from the ERC CoG 863818 (ForM-SMArt)","issue":"2271","article_type":"original","author":[{"first_name":"Jakub","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda"},{"orcid":"0000-0002-1097-9684","first_name":"Josef","full_name":"Tkadlec, Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Kamran","full_name":"Kaveh, Kamran","last_name":"Kaveh"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}],"oa":1,"date_published":"2023-03-29T00:00:00Z","day":"29","abstract":[{"lang":"eng","text":"Populations evolve in spatially heterogeneous environments. While a certain trait might bring a fitness advantage in some patch of the environment, a different trait might be advantageous in another patch. Here, we study the Moran birth–death process with two types of individuals in a population stretched across two patches of size N, each patch favouring one of the two types. We show that the long-term fate of such populations crucially depends on the migration rate μ\r\n between the patches. To classify the possible fates, we use the distinction between polynomial (short) and exponential (long) timescales. We show that when μ is high then one of the two types fixates on the whole population after a number of steps that is only polynomial in N. By contrast, when μ is low then each type holds majority in the patch where it is favoured for a number of steps that is at least exponential in N. Moreover, we precisely identify the threshold migration rate μ⋆ that separates those two scenarios, thereby exactly delineating the situations that support long-term coexistence of the two types. We also discuss the case of various cycle graphs and we present computer simulations that perfectly match our analytical results."}]},{"has_accepted_license":"1","title":"Token swapping on trees","external_id":{"arxiv":["1903.06981"]},"publication_identifier":{"issn":["1462-7264"],"eissn":["1365-8050"]},"date_created":"2023-04-16T22:01:08Z","year":"2023","intvolume":"        24","file_date_updated":"2023-04-17T08:10:28Z","ddc":["000"],"article_processing_charge":"No","publisher":"EPI Sciences","file":[{"content_type":"application/pdf","file_name":"2022_DMTCS_Biniaz.pdf","success":1,"creator":"dernst","file_size":2072197,"date_updated":"2023-04-17T08:10:28Z","date_created":"2023-04-17T08:10:28Z","file_id":"12844","access_level":"open_access","checksum":"439102ea4f6e2aeefd7107dfb9ccf532","relation":"main_file"}],"citation":{"short":"A. Biniaz, K. Jain, A. Lubiw, Z. Masárová, T. Miltzow, D. Mondal, A.M. Naredla, J. Tkadlec, A. Turcotte, Discrete Mathematics and Theoretical Computer Science 24 (2023).","mla":"Biniaz, Ahmad, et al. “Token Swapping on Trees.” <i>Discrete Mathematics and Theoretical Computer Science</i>, vol. 24, no. 2, 9, EPI Sciences, 2023, doi:<a href=\"https://doi.org/10.46298/DMTCS.8383\">10.46298/DMTCS.8383</a>.","ama":"Biniaz A, Jain K, Lubiw A, et al. Token swapping on trees. <i>Discrete Mathematics and Theoretical Computer Science</i>. 2023;24(2). doi:<a href=\"https://doi.org/10.46298/DMTCS.8383\">10.46298/DMTCS.8383</a>","ieee":"A. Biniaz <i>et al.</i>, “Token swapping on trees,” <i>Discrete Mathematics and Theoretical Computer Science</i>, vol. 24, no. 2. EPI Sciences, 2023.","ista":"Biniaz A, Jain K, Lubiw A, Masárová Z, Miltzow T, Mondal D, Naredla AM, Tkadlec J, Turcotte A. 2023. Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. 24(2), 9.","chicago":"Biniaz, Ahmad, Kshitij Jain, Anna Lubiw, Zuzana Masárová, Tillmann Miltzow, Debajyoti Mondal, Anurag Murty Naredla, Josef Tkadlec, and Alexi Turcotte. “Token Swapping on Trees.” <i>Discrete Mathematics and Theoretical Computer Science</i>. EPI Sciences, 2023. <a href=\"https://doi.org/10.46298/DMTCS.8383\">https://doi.org/10.46298/DMTCS.8383</a>.","apa":"Biniaz, A., Jain, K., Lubiw, A., Masárová, Z., Miltzow, T., Mondal, D., … Turcotte, A. (2023). Token swapping on trees. <i>Discrete Mathematics and Theoretical Computer Science</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/DMTCS.8383\">https://doi.org/10.46298/DMTCS.8383</a>"},"day":"18","abstract":[{"lang":"eng","text":"The input to the token swapping problem is a graph with vertices v1, v2, . . . , vn, and n tokens with labels 1,2, . . . , n, one on each vertex. The goal is to get token i to vertex vi for all i= 1, . . . , n using a minimum number of swaps, where a swap exchanges the tokens on the endpoints of an edge.Token swapping on a tree, also known as “sorting with a transposition tree,” is not known to be in P nor NP-complete. We present some partial results: 1. An optimum swap sequence may need to perform a swap on a leaf vertex that has the correct token (a “happy leaf”), disproving a conjecture of Vaughan. 2. Any algorithm that fixes happy leaves—as all known approximation algorithms for the problem do—has approximation factor at least 4/3. Furthermore, the two best-known 2-approximation algorithms have approximation factor exactly 2. 3. A generalized problem—weighted coloured token swapping—is NP-complete on trees, but solvable in polynomial time on paths and stars. In this version, tokens and vertices have colours, and colours have weights. The goal is to get every token to a vertex of the same colour, and the cost of a swap is the sum of the weights of the two tokens involved."}],"author":[{"full_name":"Biniaz, Ahmad","first_name":"Ahmad","last_name":"Biniaz"},{"full_name":"Jain, Kshitij","first_name":"Kshitij","last_name":"Jain"},{"full_name":"Lubiw, Anna","first_name":"Anna","last_name":"Lubiw"},{"orcid":"0000-0002-6660-1322","first_name":"Zuzana","full_name":"Masárová, Zuzana","last_name":"Masárová","id":"45CFE238-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Miltzow, Tillmann","first_name":"Tillmann","last_name":"Miltzow"},{"last_name":"Mondal","first_name":"Debajyoti","full_name":"Mondal, Debajyoti"},{"last_name":"Naredla","full_name":"Naredla, Anurag Murty","first_name":"Anurag Murty"},{"last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","first_name":"Josef","full_name":"Tkadlec, Josef"},{"full_name":"Turcotte, Alexi","first_name":"Alexi","last_name":"Turcotte"}],"arxiv":1,"oa":1,"date_published":"2023-01-18T00:00:00Z","acknowledgement":"This work was begun at the University of Waterloo and was partially supported by the Natural Sciences and Engineering Council of Canada (NSERC).\r\n","issue":"2","article_type":"original","doi":"10.46298/DMTCS.8383","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2025-01-20T14:05:09Z","month":"01","publication_status":"published","volume":24,"_id":"12833","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"7950"}]},"article_number":"9","quality_controlled":"1","publication":"Discrete Mathematics and Theoretical Computer Science","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"},{"_id":"HeEd"},{"_id":"UlWa"}],"type":"journal_article","scopus_import":"1"},{"ddc":["000"],"file_date_updated":"2023-04-25T09:13:53Z","publisher":"Springer Nature","file":[{"relation":"main_file","checksum":"a4b3b7b36fbef068cabf4fb99501fef6","access_level":"open_access","file_id":"12868","date_created":"2023-04-25T09:13:53Z","creator":"dernst","success":1,"file_name":"2023_NatureComm_Schmid.pdf","content_type":"application/pdf","file_size":1786475,"date_updated":"2023-04-25T09:13:53Z"}],"article_processing_charge":"No","citation":{"chicago":"Schmid, Laura, Farbod Ekbatani, Christian Hilbe, and Krishnendu Chatterjee. “Quantitative Assessment Can Stabilize Indirect Reciprocity under Imperfect Information.” <i>Nature Communications</i>. Springer Nature, 2023. <a href=\"https://doi.org/10.1038/s41467-023-37817-x\">https://doi.org/10.1038/s41467-023-37817-x</a>.","apa":"Schmid, L., Ekbatani, F., Hilbe, C., &#38; Chatterjee, K. (2023). Quantitative assessment can stabilize indirect reciprocity under imperfect information. <i>Nature Communications</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41467-023-37817-x\">https://doi.org/10.1038/s41467-023-37817-x</a>","ista":"Schmid L, Ekbatani F, Hilbe C, Chatterjee K. 2023. Quantitative assessment can stabilize indirect reciprocity under imperfect information. Nature Communications. 14, 2086.","ieee":"L. Schmid, F. Ekbatani, C. Hilbe, and K. Chatterjee, “Quantitative assessment can stabilize indirect reciprocity under imperfect information,” <i>Nature Communications</i>, vol. 14. Springer Nature, 2023.","mla":"Schmid, Laura, et al. “Quantitative Assessment Can Stabilize Indirect Reciprocity under Imperfect Information.” <i>Nature Communications</i>, vol. 14, 2086, Springer Nature, 2023, doi:<a href=\"https://doi.org/10.1038/s41467-023-37817-x\">10.1038/s41467-023-37817-x</a>.","ama":"Schmid L, Ekbatani F, Hilbe C, Chatterjee K. Quantitative assessment can stabilize indirect reciprocity under imperfect information. <i>Nature Communications</i>. 2023;14. doi:<a href=\"https://doi.org/10.1038/s41467-023-37817-x\">10.1038/s41467-023-37817-x</a>","short":"L. Schmid, F. Ekbatani, C. Hilbe, K. Chatterjee, Nature Communications 14 (2023)."},"has_accepted_license":"1","pmid":1,"title":"Quantitative assessment can stabilize indirect reciprocity under imperfect information","publication_identifier":{"eissn":["2041-1723"]},"external_id":{"isi":["001003644100020"],"pmid":["37045828"]},"intvolume":"        14","date_created":"2023-04-23T22:01:03Z","year":"2023","acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.). L.S. received additional partial support by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), and also thanks the support by the Stochastic Analysis and Application Research Center (SAARC) under National Research Foundation of Korea grant NRF-2019R1A5A1028324. The authors additionally thank Stefan Schmid for providing access to his lab infrastructure at the University of Vienna for the purpose of collecting simulation data.","article_type":"original","doi":"10.1038/s41467-023-37817-x","day":"12","abstract":[{"lang":"eng","text":"The field of indirect reciprocity investigates how social norms can foster cooperation when individuals continuously monitor and assess each other’s social interactions. By adhering to certain social norms, cooperating individuals can improve their reputation and, in turn, receive benefits from others. Eight social norms, known as the “leading eight,\" have been shown to effectively promote the evolution of cooperation as long as information is public and reliable. These norms categorize group members as either ’good’ or ’bad’. In this study, we examine a scenario where individuals instead assign nuanced reputation scores to each other, and only cooperate with those whose reputation exceeds a certain threshold. We find both analytically and through simulations that such quantitative assessments are error-correcting, thus facilitating cooperation in situations where information is private and unreliable. Moreover, our results identify four specific norms that are robust to such conditions, and may be relevant for helping to sustain cooperation in natural populations."}],"oa":1,"author":[{"first_name":"Laura","full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","last_name":"Schmid"},{"first_name":"Farbod","full_name":"Ekbatani, Farbod","last_name":"Ekbatani"},{"last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","first_name":"Christian"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2023-04-12T00:00:00Z","oa_version":"Published Version","_id":"12861","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","quality_controlled":"1","article_number":"2086","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"date_updated":"2025-04-15T06:26:15Z","status":"public","volume":14,"month":"04","publication_status":"published","isi":1,"department":[{"_id":"KrCh"}],"type":"journal_article","scopus_import":"1","ec_funded":1,"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"},{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"}],"publication":"Nature Communications","language":[{"iso":"eng"}]},{"abstract":[{"lang":"eng","text":"A classical problem for Markov chains is determining their stationary (or steady-state) distribution. This problem has an equally classical solution based on eigenvectors and linear equation systems. However, this approach does not scale to large instances, and iterative solutions are desirable. It turns out that a naive approach, as used by current model checkers, may yield completely wrong results. We present a new approach, which utilizes recent advances in partial exploration and mean payoff computation to obtain a correct, converging approximation."}],"conference":{"end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22","location":"Paris, France"},"day":"22","date_published":"2023-04-22T00:00:00Z","author":[{"last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias"}],"arxiv":1,"oa":1,"doi":"10.1007/978-3-031-30823-9_25","title":"Correct approximation of stationary distributions","has_accepted_license":"1","date_created":"2023-06-18T22:00:46Z","year":"2023","intvolume":"     13993","external_id":{"arxiv":["2301.08137"],"isi":["001288688000025"]},"publication_identifier":{"isbn":["9783031308222"],"eissn":["1611-3349"],"issn":["0302-9743"]},"file_date_updated":"2023-06-19T07:18:40Z","ddc":["000"],"citation":{"ama":"Meggendorfer T. Correct approximation of stationary distributions. In: <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13993. Springer Nature; 2023:489-507. doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_25\">10.1007/978-3-031-30823-9_25</a>","mla":"Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.” <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13993, Springer Nature, 2023, pp. 489–507, doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_25\">10.1007/978-3-031-30823-9_25</a>.","short":"T. Meggendorfer, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 489–507.","chicago":"Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.” In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, 13993:489–507. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_25\">https://doi.org/10.1007/978-3-031-30823-9_25</a>.","apa":"Meggendorfer, T. (2023). Correct approximation of stationary distributions. In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13993, pp. 489–507). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_25\">https://doi.org/10.1007/978-3-031-30823-9_25</a>","ista":"Meggendorfer T. 2023. Correct approximation of stationary distributions. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 489–507.","ieee":"T. Meggendorfer, “Correct approximation of stationary distributions,” in <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13993, pp. 489–507."},"article_processing_charge":"No","file":[{"file_id":"13148","checksum":"59f707a3949c03793251b0d04c62542a","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_name":"2023_LNCS_Meggendorfer.pdf","success":1,"creator":"dernst","file_size":521951,"date_updated":"2023-06-19T07:18:40Z","date_created":"2023-06-19T07:18:40Z"}],"publisher":"Springer Nature","publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","language":[{"iso":"eng"}],"type":"conference","department":[{"_id":"KrCh"}],"alternative_title":["LNCS"],"corr_author":"1","scopus_import":"1","status":"public","date_updated":"2025-09-09T12:28:12Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"isi":1,"volume":13993,"publication_status":"published","month":"04","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","_id":"13139","page":"489-507","oa_version":"Published Version","quality_controlled":"1","related_material":{"record":[{"relation":"research_data","status":"public","id":"14990"}]}},{"doi":"10.1007/978-3-031-30823-9_1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","date_published":"2023-04-22T00:00:00Z","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","first_name":"Mathias","full_name":"Lechner, Mathias"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699"}],"oa":1,"abstract":[{"text":"Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.","lang":"eng"}],"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2023-04-27","start_date":"2023-04-22","location":"Paris, France"},"day":"22","citation":{"short":"K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25.","mla":"Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, vol. 13993, Springer Nature, 2023, pp. 3–25, doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">10.1007/978-3-031-30823-9_1</a>.","ama":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: <i>Tools and Algorithms for the Construction and Analysis of Systems </i>. Vol 13993. Springer Nature; 2023:3-25. doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">10.1007/978-3-031-30823-9_1</a>","ista":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.","ieee":"K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier framework for neural network controllers and certificates of stochastic systems,” in <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, Paris, France, 2023, vol. 13993, pp. 3–25.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” In <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, 13993:3–25. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">https://doi.org/10.1007/978-3-031-30823-9_1</a>.","apa":"Chatterjee, K., Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2023). A learner-verifier framework for neural network controllers and certificates of stochastic systems. In <i>Tools and Algorithms for the Construction and Analysis of Systems </i> (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">https://doi.org/10.1007/978-3-031-30823-9_1</a>"},"article_processing_charge":"No","file":[{"checksum":"3d8a8bb24d211bc83360dfc2fd744307","access_level":"open_access","relation":"main_file","file_id":"13150","date_created":"2023-06-19T08:29:30Z","content_type":"application/pdf","creator":"dernst","success":1,"file_name":"2023_LNCS_Chatterjee.pdf","file_size":528455,"date_updated":"2023-06-19T08:29:30Z"}],"publisher":"Springer Nature","ddc":["000"],"file_date_updated":"2023-06-19T08:29:30Z","year":"2023","date_created":"2023-06-18T22:00:47Z","intvolume":"     13993","external_id":{"isi":["001288688000001"]},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308222"]},"title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","has_accepted_license":"1","ec_funded":1,"alternative_title":["LNCS"],"scopus_import":"1","corr_author":"1","type":"conference","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"language":[{"iso":"eng"}],"publication":"Tools and Algorithms for the Construction and Analysis of Systems ","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"},{"name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"665385"}],"quality_controlled":"1","oa_version":"Published Version","_id":"13142","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","page":"3-25","isi":1,"month":"04","volume":13993,"publication_status":"published","date_updated":"2025-09-09T12:29:26Z","status":"public","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"}},{"quality_controlled":"1","article_number":"4153","related_material":{"record":[{"status":"public","id":"13336","relation":"research_data"}]},"_id":"13258","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","volume":14,"publication_status":"published","month":"07","isi":1,"status":"public","date_updated":"2025-04-14T07:43:55Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ec_funded":1,"scopus_import":"1","corr_author":"1","type":"journal_article","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"publication":"Nature Communications","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"},{"_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","call_identifier":"H2020"}],"citation":{"mla":"Kleshnina, Maria, et al. “The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games.” <i>Nature Communications</i>, vol. 14, 4153, Springer Nature, 2023, doi:<a href=\"https://doi.org/10.1038/s41467-023-39625-9\">10.1038/s41467-023-39625-9</a>.","ama":"Kleshnina M, Hilbe C, Simsa S, Chatterjee K, Nowak MA. The effect of environmental information on evolution of cooperation in stochastic games. <i>Nature Communications</i>. 2023;14. doi:<a href=\"https://doi.org/10.1038/s41467-023-39625-9\">10.1038/s41467-023-39625-9</a>","short":"M. Kleshnina, C. Hilbe, S. Simsa, K. Chatterjee, M.A. Nowak, Nature Communications 14 (2023).","apa":"Kleshnina, M., Hilbe, C., Simsa, S., Chatterjee, K., &#38; Nowak, M. A. (2023). The effect of environmental information on evolution of cooperation in stochastic games. <i>Nature Communications</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41467-023-39625-9\">https://doi.org/10.1038/s41467-023-39625-9</a>","chicago":"Kleshnina, Maria, Christian Hilbe, Stepan Simsa, Krishnendu Chatterjee, and Martin A. Nowak. “The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games.” <i>Nature Communications</i>. Springer Nature, 2023. <a href=\"https://doi.org/10.1038/s41467-023-39625-9\">https://doi.org/10.1038/s41467-023-39625-9</a>.","ista":"Kleshnina M, Hilbe C, Simsa S, Chatterjee K, Nowak MA. 2023. The effect of environmental information on evolution of cooperation in stochastic games. Nature Communications. 14, 4153.","ieee":"M. Kleshnina, C. Hilbe, S. Simsa, K. Chatterjee, and M. A. Nowak, “The effect of environmental information on evolution of cooperation in stochastic games,” <i>Nature Communications</i>, vol. 14. Springer Nature, 2023."},"file":[{"relation":"main_file","checksum":"5aceefdfe76686267b93ae4fe81899f1","access_level":"open_access","file_id":"13337","date_created":"2023-07-31T11:32:36Z","date_updated":"2023-07-31T11:32:36Z","file_size":1601682,"creator":"dernst","success":1,"file_name":"2023_NatureComm_Kleshnina.pdf","content_type":"application/pdf"}],"publisher":"Springer Nature","article_processing_charge":"Yes","ddc":["000"],"file_date_updated":"2023-07-31T11:32:36Z","intvolume":"        14","year":"2023","date_created":"2023-07-23T22:01:11Z","publication_identifier":{"eissn":["2041-1723"]},"external_id":{"isi":["001029450400031"],"pmid":["37438341"]},"title":"The effect of environmental information on evolution of cooperation in stochastic games","pmid":1,"has_accepted_license":"1","doi":"10.1038/s41467-023-39625-9","article_type":"original","acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.), the European Research Council Starting Grant 850529: E-DIRECT (to C.H.), the European Union’s Horizon 2020 research and innovation program under the Marie Sklodowska-Curie Grant Agreement #754411 and the French Agence Nationale de la Recherche (under the Investissement d’Avenir programme, ANR-17-EURE-0010) (to M.K.).","date_published":"2023-07-12T00:00:00Z","oa":1,"author":[{"first_name":"Maria","full_name":"Kleshnina, Maria","id":"4E21749C-F248-11E8-B48F-1D18A9856A87","last_name":"Kleshnina"},{"orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","first_name":"Christian","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Simsa, Stepan","first_name":"Stepan","orcid":"0000-0001-6687-1210","id":"409d615c-2f95-11ee-b934-90a352102c1e","last_name":"Simsa"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Nowak","first_name":"Martin A.","full_name":"Nowak, Martin A."}],"abstract":[{"lang":"eng","text":"Many human interactions feature the characteristics of social dilemmas where individual actions have consequences for the group and the environment. The feedback between behavior and environment can be studied with the framework of stochastic games. In stochastic games, the state of the environment can change, depending on the choices made by group members. Past work suggests that such feedback can reinforce cooperative behaviors. In particular, cooperation can evolve in stochastic games even if it is infeasible in each separate repeated game. In stochastic games, participants have an interest in conditioning their strategies on the state of the environment. Yet in many applications, precise information about the state could be scarce. Here, we study how the availability of information (or lack thereof) shapes evolution of cooperation. Already for simple examples of two state games we find surprising effects. In some cases, cooperation is only possible if there is precise information about the state of the environment. In other cases, cooperation is most abundant when there is no information about the state of the environment. We systematically analyze all stochastic games of a given complexity class, to determine when receiving information about the environment is better, neutral, or worse for evolution of cooperation."}],"day":"12"},{"author":[{"last_name":"Kleshnina","id":"4E21749C-F248-11E8-B48F-1D18A9856A87","first_name":"Maria","full_name":"Kleshnina, Maria"}],"oa":1,"date_published":"2023-06-20T00:00:00Z","day":"20","corr_author":"1","doi":"10.5281/ZENODO.8059564","department":[{"_id":"KrCh"}],"type":"research_data_reference","month":"06","year":"2023","date_created":"2023-07-31T11:30:46Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/zenodo.8059564"}],"status":"public","date_updated":"2025-04-15T06:54:58Z","title":"kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games","related_material":{"record":[{"relation":"used_in_publication","id":"13258","status":"public"}]},"publisher":"Zenodo","article_processing_charge":"No","citation":{"mla":"Kleshnina, Maria. <i>Kleshnina/Stochgames_info: The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.8059564\">10.5281/ZENODO.8059564</a>.","ama":"Kleshnina M. kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.8059564\">10.5281/ZENODO.8059564</a>","short":"M. Kleshnina, (2023).","apa":"Kleshnina, M. (2023). kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.8059564\">https://doi.org/10.5281/ZENODO.8059564</a>","chicago":"Kleshnina, Maria. “Kleshnina/Stochgames_info: The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.8059564\">https://doi.org/10.5281/ZENODO.8059564</a>.","ieee":"M. Kleshnina, “kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games.” Zenodo, 2023.","ista":"Kleshnina M. 2023. kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.8059564\">10.5281/ZENODO.8059564</a>."},"ddc":["000"],"oa_version":"Published Version","_id":"13336","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"arxiv":1,"author":[{"orcid":"0000-0002-8122-2881","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881"}],"oa":1,"date_published":"2023-07-01T00:00:00Z","day":"01","conference":{"start_date":"2023-06-26","location":"Boston, MA, United States","end_date":"2023-06-29","name":"LICS: Logic in Computer Science"},"abstract":[{"lang":"eng","text":"A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution."}],"doi":"10.1109/LICS56636.2023.10175771","acknowledgement":"This research was funded in part by DFG projects 383882557 “SUV” and 427755713 “GOPro”.","external_id":{"isi":["001036707700042"],"arxiv":["2304.09930"]},"publication_identifier":{"issn":["1043-6871"],"isbn":["9798350335873"]},"year":"2023","date_created":"2023-08-06T22:01:10Z","intvolume":"      2023","title":"Stopping criteria for value iteration on stochastic games with quantitative objectives","publisher":"Institute of Electrical and Electronics Engineers","article_processing_charge":"No","citation":{"apa":"Kretinsky, J., Meggendorfer, T., &#38; Weininger, M. (2023). Stopping criteria for value iteration on stochastic games with quantitative objectives. In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (Vol. 2023). Boston, MA, United States: Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">https://doi.org/10.1109/LICS56636.2023.10175771</a>","chicago":"Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Vol. 2023. Institute of Electrical and Electronics Engineers, 2023. <a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">https://doi.org/10.1109/LICS56636.2023.10175771</a>.","ista":"Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2023.","ieee":"J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value iteration on stochastic games with quantitative objectives,” in <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Boston, MA, United States, 2023, vol. 2023.","ama":"Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration on stochastic games with quantitative objectives. In: <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Vol 2023. Institute of Electrical and Electronics Engineers; 2023. doi:<a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">10.1109/LICS56636.2023.10175771</a>","mla":"Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, vol. 2023, Institute of Electrical and Electronics Engineers, 2023, doi:<a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">10.1109/LICS56636.2023.10175771</a>.","short":"J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2023."},"language":[{"iso":"eng"}],"publication":"38th Annual ACM/IEEE Symposium on Logic in Computer Science","corr_author":"1","scopus_import":"1","department":[{"_id":"KrCh"}],"type":"conference","isi":1,"month":"07","publication_status":"published","volume":2023,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2304.09930"}],"status":"public","date_updated":"2025-07-10T11:50:43Z","quality_controlled":"1","oa_version":"Preprint","_id":"13967","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"}]