[{"project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.1007/978-3-031-65633-0_16","citation":{"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>.","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>","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>","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.","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>.","short":"T. Meggendorfer, M. Weininger, in:, 36th International Conference on Computer Aided Verification, Springer Nature, 2024, pp. 359–372."},"scopus_import":"1","department":[{"_id":"KrCh"}],"volume":14683,"_id":"17402","oa_version":"Published Version","quality_controlled":"1","conference":{"name":"CAV: Computer Aided Verification","location":"Montreal, Canada","start_date":"2024-07-24","end_date":"2024-07-27"},"license":"https://creativecommons.org/licenses/by/4.0/","external_id":{"arxiv":["2405.03885"],"isi":["001307897000016"]},"day":"01","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031656323"],"eisbn":["9783031656330"],"issn":["0302-9743"]},"file_date_updated":"2024-08-12T08:39:12Z","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,"title":"Playing games with your PET: Extending the Partial Exploration Tool to stochastic games","date_updated":"2025-09-08T08:53:55Z","author":[{"last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","first_name":"Tobias","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"}],"language":[{"iso":"eng"}],"intvolume":"     14683","has_accepted_license":"1","date_created":"2024-08-09T11:24:54Z","abstract":[{"lang":"eng","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."}],"alternative_title":["LNCS"],"publisher":"Springer Nature","status":"public","month":"07","corr_author":"1","ddc":["000"],"publication":"36th International Conference on Computer Aided Verification","ec_funded":1,"isi":1,"type":"conference","oa":1,"page":"359-372","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2024-07-01T00:00:00Z","publication_status":"published","article_processing_charge":"Yes (in subscription journal)","year":"2024","file":[{"relation":"main_file","date_created":"2024-08-12T08:39:12Z","file_name":"2024_CAV_Meggendorfer.pdf","creator":"dernst","checksum":"c888231d0a47b55786b7b4c0f02216bb","file_size":368487,"content_type":"application/pdf","access_level":"open_access","file_id":"17419","success":1,"date_updated":"2024-08-12T08:39:12Z"}]},{"citation":{"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>","ista":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2024. Entropic risk for turn-based stochastic games. Information and Computation. 301, 105214.","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>","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.","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).","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>."},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.1016/j.ic.2024.105214","department":[{"_id":"KrCh"}],"scopus_import":"1","volume":301,"_id":"17474","quality_controlled":"1","oa_version":"Published Version","OA_place":"publisher","external_id":{"isi":["001301143400001"],"arxiv":["2307.06611"]},"file_date_updated":"2025-01-09T13:49:03Z","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"14417"}]},"article_type":"original","publication_identifier":{"issn":["0890-5401"],"eissn":["1090-2651"]},"acknowledgement":"Krishnendu Chatterjee reports financial support was provided by European Research Council.","day":"01","arxiv":1,"date_updated":"2025-09-08T09:10:06Z","title":"Entropic risk for turn-based stochastic games","author":[{"last_name":"Baier","first_name":"Christel","full_name":"Baier, Christel"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","first_name":"Tobias"},{"full_name":"Piribauer, Jakob","first_name":"Jakob","last_name":"Piribauer"}],"OA_type":"hybrid","language":[{"iso":"eng"}],"intvolume":"       301","date_created":"2024-09-01T22:01:07Z","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"}],"has_accepted_license":"1","publisher":"Elsevier","status":"public","publication":"Information and Computation","month":"12","ddc":["000"],"corr_author":"1","isi":1,"type":"journal_article","oa":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_number":"105214","date_published":"2024-12-01T00:00:00Z","year":"2024","article_processing_charge":"Yes (in subscription journal)","publication_status":"published","file":[{"success":1,"file_id":"18817","date_updated":"2025-01-09T13:49:03Z","relation":"main_file","date_created":"2025-01-09T13:49:03Z","file_name":"2024_InformationComputation_Baier.pdf","checksum":"f68e0c2f46f9b9c86815406bcf2ee2d4","creator":"dernst","file_size":724703,"content_type":"application/pdf","access_level":"open_access"}]},{"day":"11","file_date_updated":"2024-10-01T09:56:54Z","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031711619"],"eissn":["1611-3349"]},"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.","arxiv":1,"conference":{"start_date":"2024-09-09","name":"FM: Formal Methods","location":"Milan, Italy","end_date":"2024-09-13"},"external_id":{"arxiv":["2403.05386"],"isi":["001336893300031"]},"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Goharshady","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Goharshady, Ehsan","first_name":"Ehsan","last_name":"Goharshady"},{"id":"67638922-f394-11eb-9cf6-f20423e08757","full_name":"Karrabi, Mehrdad","last_name":"Karrabi","first_name":"Mehrdad"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde"}],"title":"Sound and complete witnesses for template-based verification of LTL properties on polynomial programs","date_updated":"2025-09-08T09:51:34Z","scopus_import":"1","department":[{"_id":"KrCh"}],"volume":14933,"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"doi":"10.1007/978-3-031-71162-6_31","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"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>","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.","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>","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>.","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.","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.","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>."},"_id":"18155","oa_version":"Published Version","quality_controlled":"1","page":"600-619","ec_funded":1,"isi":1,"type":"conference","oa":1,"publication_status":"published","article_processing_charge":"Yes (in subscription journal)","year":"2024","file":[{"file_id":"18165","success":1,"date_updated":"2024-10-01T09:56:54Z","date_created":"2024-10-01T09:56:54Z","relation":"main_file","creator":"dernst","checksum":"223845be9e754681ee218866827c95e7","file_name":"2024_LNCS_Chatterjee.pdf","file_size":650495,"access_level":"open_access","content_type":"application/pdf"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2024-09-11T00:00:00Z","has_accepted_license":"1","date_created":"2024-09-29T22:01:37Z","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."}],"alternative_title":["LNCS"],"publisher":"Springer Nature","language":[{"iso":"eng"}],"intvolume":"     14933","month":"09","corr_author":"1","ddc":["000"],"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","status":"public"},{"month":"09","corr_author":"1","status":"public","publication":"Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence","date_created":"2024-09-29T22:01:38Z","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. "}],"publisher":"International Joint Conferences on Artificial Intelligence","language":[{"iso":"eng"}],"article_processing_charge":"No","year":"2024","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2024-09-01T00:00:00Z","page":"3-12","ec_funded":1,"type":"conference","oa":1,"_id":"18159","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2405.04015","open_access":"1"}],"quality_controlled":"1","oa_version":"Preprint","scopus_import":"1","department":[{"_id":"KrCh"}],"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"doi":"10.24963/ijcai.2024/1","citation":{"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>.","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.","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>","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>","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.","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>.","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."},"author":[{"full_name":"Akshay, S","first_name":"S","last_name":"Akshay"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","first_name":"Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699"}],"date_updated":"2025-04-14T07:52:46Z","title":"Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties","publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"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.","day":"01","arxiv":1,"conference":{"location":"Jeju, Korea","name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2024-08-03","end_date":"2024-08-09"},"external_id":{"arxiv":["2405.04015"]}},{"page":"6707-6715","type":"conference","ec_funded":1,"oa":1,"year":"2024","article_processing_charge":"No","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2024-09-01T00:00:00Z","abstract":[{"lang":"eng","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. "}],"date_created":"2024-09-29T22:01:39Z","publisher":"International Joint Conferences on Artificial Intelligence","OA_type":"green","language":[{"iso":"eng"}],"status":"public","corr_author":"1","month":"09","publication":"33rd International Joint Conference on Artificial Intelligence","publication_identifier":{"isbn":["9781956792041"],"issn":["1045-0823"]},"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.","day":"01","arxiv":1,"conference":{"end_date":"2024-08-09","location":"Jeju, South Korea","name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2024-08-03"},"OA_place":"repository","external_id":{"arxiv":["2312.13912"]},"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"id":"67638922-f394-11eb-9cf6-f20423e08757","full_name":"Karrabi, Mehrdad","first_name":"Mehrdad","last_name":"Karrabi"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","last_name":"Novotný","first_name":"Petr"},{"orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"date_updated":"2025-04-14T07:52:46Z","title":"Solving long-run average reward robust MDPs via stochastic games","scopus_import":"1","department":[{"_id":"KrCh"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"doi":"10.24963/ijcai.2024/741","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.","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>.","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>","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>","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.","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>."},"_id":"18160","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2312.13912","open_access":"1"}],"oa_version":"Preprint","quality_controlled":"1"},{"file":[{"date_updated":"2024-07-29T07:18:12Z","success":1,"file_id":"17334","file_size":832034,"access_level":"open_access","content_type":"application/pdf","date_created":"2024-07-29T07:18:12Z","relation":"main_file","creator":"dernst","checksum":"6122bd97b42751ff81c452a19970f67d","file_name":"2024_ACM_Chatterjee.pdf"}],"year":"2024","article_processing_charge":"Yes (via OA deal)","publication_status":"published","date_published":"2024-06-17T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"268-278","oa":1,"ec_funded":1,"type":"conference","publication":"Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing","corr_author":"1","status":"public","month":"06","ddc":["000"],"das_tickbox":"1","publisher":"Association for Computing Machinery","abstract":[{"lang":"eng","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."}],"date_created":"2024-07-28T22:01:10Z","has_accepted_license":"1","language":[{"iso":"eng"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Ebrahimzadeh","first_name":"Amirali","full_name":"Ebrahimzadeh, Amirali"},{"full_name":"Karrabi, Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757","last_name":"Karrabi","orcid":"0009-0007-5253-9170","first_name":"Mehrdad"},{"id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","full_name":"Pietrzak, Krzysztof Z","orcid":"0000-0002-9139-1654","last_name":"Pietrzak","first_name":"Krzysztof Z"},{"id":"2D82B818-F248-11E8-B48F-1D18A9856A87","full_name":"Yeo, Michelle X","orcid":"0009-0001-3676-4809","last_name":"Yeo","first_name":"Michelle X"},{"first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2026-07-07T13:30:07Z","title":"Fully automated selfish mining analysis in efficient proof systems blockchains","arxiv":1,"publication_identifier":{"isbn":["9798400706684"]},"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","file_date_updated":"2024-07-29T07:18:12Z","day":"17","external_id":{"arxiv":["2405.04420"]},"conference":{"end_date":"2024-06-21","start_date":"2024-06-17","name":"PODC: Symposium on Principles of Distributed Computing","location":"Nantes, France"},"quality_controlled":"1","oa_version":"Published Version","_id":"17328","scopus_import":"1","department":[{"_id":"KrCh"},{"_id":"KrPi"}],"citation":{"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.","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>.","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.","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>","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>","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>.","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."},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.1145/3662158.3662769","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}]},{"publisher":"Public Library of Science","abstract":[{"lang":"eng","text":"Populations evolve by accumulating advantageous mutations. Every population has some spatial structure that can be modeled by an underlying network. The network then influences the probability that new advantageous mutations fixate. Amplifiers of selection are networks that increase the fixation probability of advantageous mutants, as compared to the unstructured fully-connected network. Whether or not a network is an amplifier depends on the choice of the random process that governs the evolutionary dynamics. Two popular choices are Moran process with Birth-death updating and Moran process with death-Birth updating. Interestingly, while some networks are amplifiers under Birth-death updating and other networks are amplifiers under death-Birth updating, so far no spatial structures have been found that function as an amplifier under both types of updating simultaneously. In this work, we identify networks that act as amplifiers of selection under both versions of the Moran process. The amplifiers are robust, modular, and increase fixation probability for any mutant fitness advantage in a range r ∈ (1, 1.2). To complement this positive result, we also prove that for certain quantities closely related to fixation probability, it is impossible to improve them simultaneously for both versions of the Moran process. Together, our results highlight how the two versions of the Moran process differ and what they have in common."}],"date_created":"2024-04-07T22:00:55Z","has_accepted_license":"1","intvolume":"        20","OA_type":"gold","language":[{"iso":"eng"}],"issue":"3","month":"03","corr_author":"1","publication":"PLoS Computational Biology","ddc":["000"],"status":"public","oa":1,"type":"journal_article","isi":1,"ec_funded":1,"file":[{"creator":"dernst","file_name":"2024_PloSComBio_Svoboda.pdf","checksum":"a511cf369d9172beb123fe73f291b5cc","date_created":"2024-08-20T10:52:28Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_size":1425292,"file_id":"17450","success":1,"date_updated":"2024-08-20T10:52:28Z"}],"article_processing_charge":"Yes","year":"2024","publication_status":"published","date_published":"2024-03-29T00:00:00Z","article_number":"e1012008","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":20,"scopus_import":"1","department":[{"_id":"KrCh"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.1371/journal.pcbi.1012008","citation":{"ama":"Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. <i>PLoS Computational Biology</i>. 2024;20(3). doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1012008\">10.1371/journal.pcbi.1012008</a>","ista":"Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. 2024. Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. PLoS Computational Biology. 20(3), e1012008.","apa":"Svoboda, J., Joshi, S. S., Tkadlec, J., &#38; Chatterjee, K. (2024). Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. <i>PLoS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.1012008\">https://doi.org/10.1371/journal.pcbi.1012008</a>","ieee":"J. Svoboda, S. S. Joshi, J. Tkadlec, and K. Chatterjee, “Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating,” <i>PLoS Computational Biology</i>, vol. 20, no. 3. Public Library of Science, 2024.","mla":"Svoboda, Jakub, et al. “Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth Updating.” <i>PLoS Computational Biology</i>, vol. 20, no. 3, e1012008, Public Library of Science, 2024, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1012008\">10.1371/journal.pcbi.1012008</a>.","short":"J. Svoboda, S.S. Joshi, J. Tkadlec, K. Chatterjee, PLoS Computational Biology 20 (2024).","chicago":"Svoboda, Jakub, Soham Shrikant Joshi, Josef Tkadlec, and Krishnendu Chatterjee. “Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth Updating.” <i>PLoS Computational Biology</i>. Public Library of Science, 2024. <a href=\"https://doi.org/10.1371/journal.pcbi.1012008\">https://doi.org/10.1371/journal.pcbi.1012008</a>."},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"APC_amount":"3149,96 EUR","oa_version":"Published Version","quality_controlled":"1","_id":"15297","DOAJ_listed":"1","arxiv":1,"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"20138"}]},"file_date_updated":"2024-08-20T10:52:28Z","publication_identifier":{"eissn":["1553-7358"],"issn":["1553-734X"]},"acknowledgement":"We thank Gavin Rees for helpful discussions. J.S., S.J., and K.C were supported by\r\nEuropean Research Council (ERC) CoG 863818 (ForM-SMArt). J.T was supported by Center for Foundations of Modern Computer Science (Charles University project UNCE/SCI/004) and by the project PRIMUS/24/SCI/012 from Charles University. ","article_type":"original","day":"29","external_id":{"isi":["001194482400002"],"arxiv":["2401.14914"]},"OA_place":"publisher","author":[{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267","last_name":"Svoboda","first_name":"Jakub"},{"id":"f97aac0e-f57c-11ee-93d0-a5a82d8df168","full_name":"Joshi, Soham Shrikant","first_name":"Soham Shrikant","last_name":"Joshi"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"}],"date_updated":"2026-07-27T12:52:03Z","title":"Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating"},{"ddc":["000"],"month":"12","corr_author":"1","publication":"Proceedings of the National Academy of Sciences of the United States of America","status":"public","issue":"50","language":[{"iso":"eng"}],"OA_type":"hybrid","intvolume":"       121","abstract":[{"lang":"eng","text":"Spatial games provide a simple and elegant mathematical model to study the evolution of cooperation in networks. In spatial games, individuals reside in vertices, adopt simple strategies, and interact with neighbors to receive a payoff. Depending on their own and neighbors’ payoffs, individuals can change their strategy. The payoff is determined by the Prisoners’ Dilemma, a classical matrix game, where players cooperate or defect. While cooperation is the desired behavior, defection provides a higher payoff for a selfish individual. There are many theoretical and empirical studies related to the role of the network in the evolution of cooperation. However, the fundamental question of whether there exist networks that for low initial cooperation rate ensure a high chance of fixation, i.e., cooperation spreads across the whole population, has remained elusive for spatial games with strong selection. In this work, we answer this fundamental question in the affirmative by presenting network structures that ensure high fixation probability for cooperators in the strong selection regime. Besides, our structures have many desirable properties: (a) they ensure the spread of cooperation even for a low initial density of cooperation and high temptation of defection, (b) they have constant degrees, and (c) the number of steps, until cooperation spreads, is at most quadratic in the size of the network."}],"date_created":"2024-12-22T23:01:47Z","has_accepted_license":"1","pmid":1,"publisher":"National Academy of Sciences","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_number":"e2405605121","date_published":"2024-12-10T00:00:00Z","article_processing_charge":"Yes","year":"2024","publication_status":"published","file":[{"file_size":2491151,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2025-01-02T12:14:15Z","checksum":"0115e9090b478e0644308c6dab58605b","file_name":"2024_PNAS_Svoboda.pdf","creator":"dernst","date_updated":"2025-01-02T12:14:15Z","file_id":"18721","success":1}],"type":"journal_article","isi":1,"ec_funded":1,"oa":1,"_id":"18703","oa_version":"Published Version","quality_controlled":"1","APC_amount":"3143,76 EUR","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"citation":{"chicago":"Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation for Spatial Games.” <i>Proceedings of the National Academy of Sciences of the United States of America</i>. National Academy of Sciences, 2024. <a href=\"https://doi.org/10.1073/pnas.2405605121\">https://doi.org/10.1073/pnas.2405605121</a>.","short":"J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences of the United States of America 121 (2024).","mla":"Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation for Spatial Games.” <i>Proceedings of the National Academy of Sciences of the United States of America</i>, vol. 121, no. 50, e2405605121, National Academy of Sciences, 2024, doi:<a href=\"https://doi.org/10.1073/pnas.2405605121\">10.1073/pnas.2405605121</a>.","ieee":"J. Svoboda and K. Chatterjee, “Density amplifiers of cooperation for spatial games,” <i>Proceedings of the National Academy of Sciences of the United States of America</i>, vol. 121, no. 50. National Academy of Sciences, 2024.","ista":"Svoboda J, Chatterjee K. 2024. Density amplifiers of cooperation for spatial games. Proceedings of the National Academy of Sciences of the United States of America. 121(50), e2405605121.","apa":"Svoboda, J., &#38; Chatterjee, K. (2024). Density amplifiers of cooperation for spatial games. <i>Proceedings of the National Academy of Sciences of the United States of America</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.2405605121\">https://doi.org/10.1073/pnas.2405605121</a>","ama":"Svoboda J, Chatterjee K. Density amplifiers of cooperation for spatial games. <i>Proceedings of the National Academy of Sciences of the United States of America</i>. 2024;121(50). doi:<a href=\"https://doi.org/10.1073/pnas.2405605121\">10.1073/pnas.2405605121</a>"},"tmp":{"image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)"},"doi":"10.1073/pnas.2405605121","department":[{"_id":"KrCh"}],"scopus_import":"1","volume":121,"date_updated":"2026-07-27T12:52:03Z","title":"Density amplifiers of cooperation for spatial games","author":[{"last_name":"Svoboda","orcid":"0000-0002-1419-3267","first_name":"Jakub","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"}],"license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","OA_place":"publisher","external_id":{"isi":["001379596100014"],"pmid":["39642209"]},"related_material":{"record":[{"id":"20138","relation":"dissertation_contains","status":"public"}]},"file_date_updated":"2025-01-02T12:14:15Z","publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"acknowledgement":"J.S. and K.C. were supported by the European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.","article_type":"original","day":"10"},{"_id":"18266","quality_controlled":"1","oa_version":"None","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"citation":{"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.","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>.","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>","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.","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>.","short":"K. Chatterjee, M. Oliu-Barton, R.J. Saona Urmeneta, Mathematics of Operations Research 50 (2024) 2433–3282."},"doi":"10.1287/moor.2022.0332","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"scopus_import":"1","volume":50,"title":"Value-positivity for matrix games","date_updated":"2026-07-29T13:14:36Z","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Oliu-Barton, Miquel","first_name":"Miquel","last_name":"Oliu-Barton"},{"full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","first_name":"Raimundo J"}],"external_id":{"isi":["001328875900001"]},"day":"01","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].","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"20234"}]},"publication_identifier":{"eissn":["1526-5471"],"issn":["0364-765X"]},"article_type":"original","month":"10","status":"public","corr_author":"1","publication":"Mathematics of Operations Research","issue":"4","language":[{"iso":"eng"}],"OA_type":"closed access","intvolume":"        50","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."}],"date_created":"2024-10-09T07:02:20Z","publisher":"Institute for Operations Research and the Management Sciences","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2024-10-01T00:00:00Z","publication_status":"published","year":"2024","article_processing_charge":"No","ec_funded":1,"type":"journal_article","isi":1,"page":"2433-3282"},{"date_updated":"2026-08-12T06:39:26Z","title":"Stochastic processes with expected stopping time","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"}],"OA_place":"publisher","external_id":{"isi":["001367316400002"],"arxiv":["2104.07278"]},"related_material":{"record":[{"status":"public","id":"10004","relation":"earlier_version"}]},"article_type":"original","file_date_updated":"2024-12-09T08:38:48Z","acknowledgement":"The authors are grateful to the anonymous reviewers of LICS 2021 and of a previous version of this paper for insightful comments that helped improving the presentation. The research presented in this paper was partially supported by the grant ERC CoG 863818 (ForM-SMArt).","publication_identifier":{"eissn":["1860-5974"]},"day":"12","arxiv":1,"DOAJ_listed":"1","_id":"18630","oa_version":"Published Version","quality_controlled":"1","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.46298/lmcs-20(4:11)2024","citation":{"short":"K. Chatterjee, L. Doyen, Logical Methods in Computer Science 20 (2024) 11:1-11:34.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” <i>Logical Methods in Computer Science</i>. EPI Sciences, 2024. <a href=\"https://doi.org/10.46298/lmcs-20(4:11)2024\">https://doi.org/10.46298/lmcs-20(4:11)2024</a>.","apa":"Chatterjee, K., &#38; Doyen, L. (2024). Stochastic processes with expected stopping time. <i>Logical Methods in Computer Science</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/lmcs-20(4:11)2024\">https://doi.org/10.46298/lmcs-20(4:11)2024</a>","ista":"Chatterjee K, Doyen L. 2024. Stochastic processes with expected stopping time. Logical Methods in Computer Science. 20(4), 11:1-11:34.","ama":"Chatterjee K, Doyen L. Stochastic processes with expected stopping time. <i>Logical Methods in Computer Science</i>. 2024;20(4):11:1-11:34. doi:<a href=\"https://doi.org/10.46298/lmcs-20(4:11)2024\">10.46298/lmcs-20(4:11)2024</a>","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4, EPI Sciences, 2024, p. 11:1-11:34, doi:<a href=\"https://doi.org/10.46298/lmcs-20(4:11)2024\">10.46298/lmcs-20(4:11)2024</a>.","ieee":"K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4. EPI Sciences, p. 11:1-11:34, 2024."},"scopus_import":"1","department":[{"_id":"KrCh"}],"volume":20,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2024-11-12T00:00:00Z","article_processing_charge":"Yes","year":"2024","publication_status":"published","file":[{"file_id":"18633","success":1,"date_updated":"2024-12-09T08:38:48Z","date_created":"2024-12-09T08:38:48Z","relation":"main_file","checksum":"b3315c74ce18ce0a30ed33d8c9972992","creator":"dernst","file_name":"2024_LMCS_Chatterjee.pdf","file_size":416814,"access_level":"open_access","content_type":"application/pdf"}],"ec_funded":1,"isi":1,"type":"journal_article","oa":1,"page":"11:1-11:34","corr_author":"1","publication":"Logical Methods in Computer Science","month":"11","status":"public","ddc":["000"],"issue":"4","OA_type":"gold","language":[{"iso":"eng"}],"intvolume":"        20","alternative_title":["LMCS"],"date_created":"2024-12-08T23:01:56Z","has_accepted_license":"1","abstract":[{"lang":"eng","text":"Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs."}],"publisher":"EPI Sciences"},{"_id":"12676","main_file_link":[{"url":"https://doi.org/10.1137/1.9781611977554.ch173","open_access":"1"}],"oa_version":"Published Version","quality_controlled":"1","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"citation":{"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>.","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.","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>","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.","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>.","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."},"doi":"10.1137/1.9781611977554.ch173","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"date_updated":"2026-06-18T17:28:38Z","title":"Faster algorithm for turn-based stochastic games with bounded treewidth","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165"},{"last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","first_name":"Raimundo J","full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"last_name":"Svoboda","orcid":"0000-0002-1419-3267","first_name":"Jakub","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"}],"conference":{"end_date":"2023-01-25","start_date":"2023-01-22","name":"SODA: Symposium on Discrete Algorithms","location":"Florence, Italy"},"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant.","publication_identifier":{"isbn":["9781611977554"]},"day":"01","publication":"Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms","month":"02","corr_author":"1","status":"public","ddc":["000"],"language":[{"iso":"eng"}],"date_created":"2023-02-24T12:20:47Z","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."}],"publisher":"Society for Industrial and Applied Mathematics","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2023-02-01T00:00:00Z","article_processing_charge":"No","year":"2023","publication_status":"published","type":"conference","ec_funded":1,"oa":1,"page":"4590-4605"},{"issue":"2","ddc":["000"],"publication":"PLoS One","month":"02","status":"public","publisher":"Public Library of Science","pmid":1,"abstract":[{"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.","lang":"eng"}],"date_created":"2023-03-05T23:01:05Z","has_accepted_license":"1","intvolume":"        18","language":[{"iso":"eng"}],"file":[{"success":1,"file_id":"12712","date_updated":"2023-03-07T10:26:45Z","checksum":"798ed5739a4117b03173e5d56e0534c9","file_name":"2023_PLOSOne_Mckerral.pdf","creator":"cchlebak","relation":"main_file","date_created":"2023-03-07T10:26:45Z","content_type":"application/pdf","access_level":"open_access","file_size":1257003}],"publication_status":"published","article_processing_charge":"No","year":"2023","date_published":"2023-02-27T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"e0279838","oa":1,"isi":1,"type":"journal_article","oa_version":"Published Version","quality_controlled":"1","_id":"12706","volume":18,"scopus_import":"1","department":[{"_id":"KrCh"}],"doi":"10.1371/journal.pone.0279838","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"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>","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>","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.","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>.","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.","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>."},"author":[{"last_name":"Mckerral","first_name":"Jody C.","full_name":"Mckerral, Jody C."},{"last_name":"Kleshnina","first_name":"Maria","full_name":"Kleshnina, Maria","id":"4E21749C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ejov, Vladimir","first_name":"Vladimir","last_name":"Ejov"},{"full_name":"Bartle, Louise","last_name":"Bartle","first_name":"Louise"},{"full_name":"Mitchell, James G.","first_name":"James G.","last_name":"Mitchell"},{"first_name":"Jerzy A.","last_name":"Filar","full_name":"Filar, Jerzy A."}],"title":"Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations","date_updated":"2023-10-17T12:53:30Z","day":"27","article_type":"original","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.","publication_identifier":{"eissn":["1932-6203"]},"file_date_updated":"2023-03-07T10:26:45Z","external_id":{"pmid":["36848357"],"isi":["000996122900022"]}},{"publication_status":"published","article_processing_charge":"No","year":"2023","file":[{"date_updated":"2023-04-17T08:10:28Z","success":1,"file_id":"12844","access_level":"open_access","content_type":"application/pdf","file_size":2072197,"checksum":"439102ea4f6e2aeefd7107dfb9ccf532","creator":"dernst","file_name":"2022_DMTCS_Biniaz.pdf","date_created":"2023-04-17T08:10:28Z","relation":"main_file"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_published":"2023-01-18T00:00:00Z","article_number":"9","type":"journal_article","oa":1,"issue":"2","status":"public","month":"01","ddc":["000"],"publication":"Discrete Mathematics and Theoretical Computer Science","has_accepted_license":"1","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."}],"date_created":"2023-04-16T22:01:08Z","publisher":"EPI Sciences","language":[{"iso":"eng"}],"intvolume":"        24","author":[{"full_name":"Biniaz, Ahmad","last_name":"Biniaz","first_name":"Ahmad"},{"last_name":"Jain","first_name":"Kshitij","full_name":"Jain, Kshitij"},{"first_name":"Anna","last_name":"Lubiw","full_name":"Lubiw, Anna"},{"first_name":"Zuzana","last_name":"Masárová","orcid":"0000-0002-6660-1322","full_name":"Masárová, Zuzana","id":"45CFE238-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Miltzow, Tillmann","last_name":"Miltzow","first_name":"Tillmann"},{"full_name":"Mondal, Debajyoti","last_name":"Mondal","first_name":"Debajyoti"},{"full_name":"Naredla, Anurag Murty","first_name":"Anurag Murty","last_name":"Naredla"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684"},{"full_name":"Turcotte, Alexi","last_name":"Turcotte","first_name":"Alexi"}],"title":"Token swapping on trees","date_updated":"2025-01-20T14:05:09Z","day":"18","related_material":{"record":[{"id":"7950","relation":"earlier_version","status":"public"}]},"publication_identifier":{"eissn":["1365-8050"],"issn":["1462-7264"]},"file_date_updated":"2023-04-17T08:10:28Z","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","article_type":"original","arxiv":1,"external_id":{"arxiv":["1903.06981"]},"_id":"12833","oa_version":"Published Version","quality_controlled":"1","scopus_import":"1","department":[{"_id":"KrCh"},{"_id":"HeEd"},{"_id":"UlWa"}],"volume":24,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"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>","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>","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.","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.","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>.","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).","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>."},"doi":"10.46298/DMTCS.8383"},{"author":[{"first_name":"Laura","last_name":"Schmid","orcid":"0000-0002-6978-7329","full_name":"Schmid, Laura","id":"38B437DE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Farbod","last_name":"Ekbatani","full_name":"Ekbatani, Farbod"},{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian","orcid":"0000-0001-5116-955X","last_name":"Hilbe","first_name":"Christian"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"}],"title":"Quantitative assessment can stabilize indirect reciprocity under imperfect information","date_updated":"2025-04-15T06:26:15Z","day":"12","file_date_updated":"2023-04-25T09:13:53Z","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.","publication_identifier":{"eissn":["2041-1723"]},"article_type":"original","external_id":{"isi":["001003644100020"],"pmid":["37045828"]},"oa_version":"Published Version","quality_controlled":"1","_id":"12861","volume":14,"department":[{"_id":"KrCh"}],"scopus_import":"1","doi":"10.1038/s41467-023-37817-x","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"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>.","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.","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.","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>","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>.","short":"L. Schmid, F. Ekbatani, C. Hilbe, K. Chatterjee, Nature Communications 14 (2023)."},"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"file":[{"checksum":"a4b3b7b36fbef068cabf4fb99501fef6","creator":"dernst","file_name":"2023_NatureComm_Schmid.pdf","date_created":"2023-04-25T09:13:53Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_size":1786475,"success":1,"file_id":"12868","date_updated":"2023-04-25T09:13:53Z"}],"publication_status":"published","year":"2023","article_processing_charge":"No","date_published":"2023-04-12T00:00:00Z","article_number":"2086","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa":1,"ec_funded":1,"type":"journal_article","isi":1,"month":"04","ddc":["000"],"publication":"Nature Communications","status":"public","publisher":"Springer Nature","has_accepted_license":"1","pmid":1,"date_created":"2023-04-23T22:01:03Z","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."}],"intvolume":"        14","language":[{"iso":"eng"}]},{"department":[{"_id":"KrCh"}],"scopus_import":"1","volume":13993,"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>","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.","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>","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>.","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.","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>."},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.1007/978-3-031-30823-9_25","_id":"13139","oa_version":"Published Version","quality_controlled":"1","day":"22","file_date_updated":"2023-06-19T07:18:40Z","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308222"],"issn":["0302-9743"]},"related_material":{"record":[{"status":"public","id":"14990","relation":"research_data"}]},"arxiv":1,"conference":{"location":"Paris, France","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22","end_date":"2023-04-27"},"external_id":{"isi":["001288688000025"],"arxiv":["2301.08137"]},"author":[{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","first_name":"Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer"}],"title":"Correct approximation of stationary distributions","date_updated":"2025-09-09T12:28:12Z","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."}],"has_accepted_license":"1","date_created":"2023-06-18T22:00:46Z","alternative_title":["LNCS"],"publisher":"Springer Nature","language":[{"iso":"eng"}],"intvolume":"     13993","status":"public","publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","ddc":["000"],"month":"04","corr_author":"1","page":"489-507","isi":1,"type":"conference","oa":1,"publication_status":"published","article_processing_charge":"No","year":"2023","file":[{"file_size":521951,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2023-06-19T07:18:40Z","checksum":"59f707a3949c03793251b0d04c62542a","file_name":"2023_LNCS_Meggendorfer.pdf","creator":"dernst","date_updated":"2023-06-19T07:18:40Z","success":1,"file_id":"13148"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2023-04-22T00:00:00Z"},{"conference":{"start_date":"2023-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Paris, France","end_date":"2023-04-27"},"external_id":{"isi":["001288688000001"]},"file_date_updated":"2023-06-19T08:29:30Z","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.","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031308222"],"eissn":["1611-3349"]},"day":"22","date_updated":"2025-09-09T12:29:26Z","title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"doi":"10.1007/978-3-031-30823-9_1","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"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>.","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>.","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.","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>","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.","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>"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","volume":13993,"_id":"13142","oa_version":"Published Version","quality_controlled":"1","ec_funded":1,"type":"conference","isi":1,"oa":1,"page":"3-25","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2023-04-22T00:00:00Z","article_processing_charge":"No","year":"2023","publication_status":"published","file":[{"creator":"dernst","file_name":"2023_LNCS_Chatterjee.pdf","checksum":"3d8a8bb24d211bc83360dfc2fd744307","relation":"main_file","date_created":"2023-06-19T08:29:30Z","content_type":"application/pdf","access_level":"open_access","file_size":528455,"success":1,"file_id":"13150","date_updated":"2023-06-19T08:29:30Z"}],"language":[{"iso":"eng"}],"intvolume":"     13993","alternative_title":["LNCS"],"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"}],"has_accepted_license":"1","date_created":"2023-06-18T22:00:47Z","publisher":"Springer Nature","month":"04","ddc":["000"],"corr_author":"1","publication":"Tools and Algorithms for the Construction and Analysis of Systems ","status":"public"},{"oa":1,"isi":1,"type":"journal_article","ec_funded":1,"file":[{"date_updated":"2023-07-31T11:32:36Z","success":1,"file_id":"13337","content_type":"application/pdf","access_level":"open_access","file_size":1601682,"creator":"dernst","checksum":"5aceefdfe76686267b93ae4fe81899f1","file_name":"2023_NatureComm_Kleshnina.pdf","relation":"main_file","date_created":"2023-07-31T11:32:36Z"}],"publication_status":"published","article_processing_charge":"Yes","year":"2023","date_published":"2023-07-12T00:00:00Z","article_number":"4153","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1","date_created":"2023-07-23T22:01:11Z","pmid":1,"intvolume":"        14","language":[{"iso":"eng"}],"status":"public","publication":"Nature Communications","corr_author":"1","month":"07","ddc":["000"],"day":"12","file_date_updated":"2023-07-31T11:32:36Z","related_material":{"record":[{"status":"public","id":"13336","relation":"research_data"}]},"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.).","publication_identifier":{"eissn":["2041-1723"]},"external_id":{"isi":["001029450400031"],"pmid":["37438341"]},"author":[{"full_name":"Kleshnina, Maria","id":"4E21749C-F248-11E8-B48F-1D18A9856A87","last_name":"Kleshnina","first_name":"Maria"},{"first_name":"Christian","last_name":"Hilbe","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Simsa","orcid":"0000-0001-6687-1210","first_name":"Stepan","full_name":"Simsa, Stepan","id":"409d615c-2f95-11ee-b934-90a352102c1e"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Nowak, Martin A.","first_name":"Martin A.","last_name":"Nowak"}],"title":"The effect of environmental information on evolution of cooperation in stochastic games","date_updated":"2025-04-14T07:43:55Z","volume":14,"department":[{"_id":"KrCh"}],"scopus_import":"1","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"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>.","short":"M. Kleshnina, C. Hilbe, S. Simsa, K. Chatterjee, M.A. Nowak, Nature Communications 14 (2023).","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.","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>.","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>","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>","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."},"doi":"10.1038/s41467-023-39625-9","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}],"quality_controlled":"1","oa_version":"Published Version","_id":"13258"},{"date_updated":"2025-04-15T06:54:58Z","date_published":"2023-06-20T00:00:00Z","title":"kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Kleshnina, Maria","id":"4E21749C-F248-11E8-B48F-1D18A9856A87","last_name":"Kleshnina","first_name":"Maria"}],"article_processing_charge":"No","year":"2023","oa":1,"type":"research_data_reference","related_material":{"record":[{"relation":"used_in_publication","id":"13258","status":"public"}]},"day":"20","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/zenodo.8059564"}],"oa_version":"Published Version","status":"public","corr_author":"1","month":"06","ddc":["000"],"_id":"13336","doi":"10.5281/ZENODO.8059564","citation":{"short":"M. Kleshnina, (2023).","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>.","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>.","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>","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>","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>.","ieee":"M. Kleshnina, “kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games.” Zenodo, 2023."},"publisher":"Zenodo","date_created":"2023-07-31T11:30:46Z","department":[{"_id":"KrCh"}]},{"date_published":"2023-06-26T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","year":"2023","article_processing_charge":"No","oa":1,"ec_funded":1,"type":"conference","page":"14964-14973","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","month":"06","status":"public","issue":"12","intvolume":"        37","language":[{"iso":"eng"}],"publisher":"Association for the Advancement of Artificial Intelligence","date_created":"2023-08-27T22:01:17Z","abstract":[{"text":"We study the problem of training and certifying adversarially robust quantized neural networks (QNNs). Quantization is a technique for making neural networks more efficient by running them using low-bit integer arithmetic and is therefore commonly adopted in industry. Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization, and certification of the quantized representation is necessary to guarantee robustness. In this work, we present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs. Inspired by advances in robust learning of non-quantized networks, our training algorithm computes the gradient of an abstract representation of the actual network. Unlike existing approaches, our method can handle the discrete semantics of QNNs. Based on QA-IBP, we also develop a complete verification procedure for verifying the adversarial robustness of QNNs, which is guaranteed to terminate and produce a correct answer. Compared to existing approaches, the key advantage of our verification procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate experimentally that our approach significantly outperforms existing methods and establish the new state-of-the-art for training and certifying the robustness of QNNs.","lang":"eng"}],"title":"Quantization-aware interval bound propagation for training certifiably robust quantized neural networks","date_updated":"2025-03-31T16:01:08Z","author":[{"first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Rus, Daniela","first_name":"Daniela","last_name":"Rus"}],"external_id":{"arxiv":["2211.16187"]},"conference":{"start_date":"2023-02-07","location":"Washington, DC, United States","name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14"},"arxiv":1,"day":"26","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. Research was sponsored by the United\r\nStates Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under Cooperative Agreement Number FA8750-19-2-\r\n1000. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied,\r\nof the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright\r\nnotation herein. The research was also funded in part by the AI2050 program at Schmidt Futures (Grant G-22-63172) and Capgemini SE.","publication_identifier":{"isbn":["9781577358800"]},"oa_version":"Preprint","quality_controlled":"1","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2211.16187","open_access":"1"}],"_id":"14242","doi":"10.1609/aaai.v37i12.26747","citation":{"short":"M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, D. Rus, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–14973.","chicago":"Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, Thomas A Henzinger, and Daniela Rus. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:14964–73. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">https://doi.org/10.1609/aaai.v37i12.26747</a>.","ama":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973. doi:<a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">10.1609/aaai.v37i12.26747</a>","ista":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 14964–14973.","apa":"Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., &#38; Rus, D. (2023). Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 14964–14973). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">https://doi.org/10.1609/aaai.v37i12.26747</a>","ieee":"M. Lechner, D. Zikelic, K. Chatterjee, T. A. Henzinger, and D. Rus, “Quantization-aware interval bound propagation for training certifiably robust quantized neural networks,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973.","mla":"Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 12, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:<a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">10.1609/aaai.v37i12.26747</a>."},"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"volume":37,"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"scopus_import":"1"},{"conference":{"end_date":"2023-07-22","start_date":"2023-07-17","name":"CAV: Computer Aided Verification","location":"Paris, France"},"external_id":{"isi":["001310805600005"]},"day":"17","file_date_updated":"2023-09-20T08:46:43Z","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031377082"]},"acknowledgement":"This work was supported in part by the 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 as well as DST/CEFIPRA/INRIA project EQuaVE and SERB Matrices grant MTR/2018/00074.","title":"MDPs as distribution transformers: Affine invariant synthesis for safety objectives","date_updated":"2025-09-09T12:56:00Z","author":[{"last_name":"Akshay","first_name":"S.","full_name":"Akshay, S."},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","first_name":"Tobias"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic"}],"project":[{"name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"citation":{"mla":"Akshay, S., et al. “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.” <i>International Conference on Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 86–112, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">10.1007/978-3-031-37709-9_5</a>.","ieee":"S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “MDPs as distribution transformers: Affine invariant synthesis for safety objectives,” in <i>International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 86–112.","apa":"Akshay, S., Chatterjee, K., Meggendorfer, T., &#38; Zikelic, D. (2023). MDPs as distribution transformers: Affine invariant synthesis for safety objectives. In <i>International Conference on Computer Aided Verification</i> (Vol. 13966, pp. 86–112). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">https://doi.org/10.1007/978-3-031-37709-9_5</a>","ista":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 86–112.","ama":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. In: <i>International Conference on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:86-112. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">10.1007/978-3-031-37709-9_5</a>","chicago":"Akshay, S., Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.” In <i>International Conference on Computer Aided Verification</i>, 13966:86–112. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">https://doi.org/10.1007/978-3-031-37709-9_5</a>.","short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 86–112."},"doi":"10.1007/978-3-031-37709-9_5","scopus_import":"1","department":[{"_id":"KrCh"}],"volume":13966,"_id":"14317","quality_controlled":"1","oa_version":"Published Version","type":"conference","ec_funded":1,"isi":1,"oa":1,"page":"86-112","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2023-07-17T00:00:00Z","publication_status":"published","article_processing_charge":"Yes (in subscription journal)","year":"2023","file":[{"date_updated":"2023-09-20T08:46:43Z","file_id":"14349","success":1,"file_size":531745,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2023-09-20T08:46:43Z","checksum":"f143c8eedf609f20f2aad2eeb496d53f","file_name":"2023_LNCS_Akshay.pdf","creator":"dernst"}],"language":[{"iso":"eng"}],"intvolume":"     13966","has_accepted_license":"1","abstract":[{"lang":"eng","text":"Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization.\r\nIn light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples."}],"date_created":"2023-09-10T22:01:12Z","alternative_title":["LNCS"],"publisher":"Springer Nature","status":"public","month":"07","ddc":["000"],"publication":"International Conference on Computer Aided Verification"}]