[{"scopus_import":"1","has_accepted_license":"1","intvolume":"       286","oa":1,"date_updated":"2025-07-14T09:10:03Z","article_processing_charge":"No","title":"On the convergence time in graphical games: A locality-sensitive approach","publication":"27th International Conference on Principles of Distributed Systems","language":[{"iso":"eng"}],"conference":{"name":"OPODIS: Conference on Principles of Distributed Systems","start_date":"2023-12-06","location":"Tokyo, Japan","end_date":"2023-12-08"},"month":"01","publication_identifier":{"issn":["18688969"],"isbn":["9783959773089"]},"oa_version":"Published Version","day":"18","file":[{"relation":"main_file","file_size":867363,"content_type":"application/pdf","access_level":"open_access","creator":"dernst","date_created":"2024-02-26T09:04:58Z","date_updated":"2024-02-26T09:04:58Z","success":1,"file_id":"15028","file_name":"2024_LIPICs_Hirvonen.pdf","checksum":"4fc7eea6e4ba140b904781fc7df868ec"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Hirvonen, Juho","first_name":"Juho","last_name":"Hirvonen"},{"full_name":"Schmid, Laura","first_name":"Laura","orcid":"0000-0002-6978-7329","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","last_name":"Schmid"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Schmid","full_name":"Schmid, Stefan","first_name":"Stefan"}],"arxiv":1,"alternative_title":["LIPIcs"],"status":"public","type":"conference","ec_funded":1,"article_number":"11","acknowledgement":"This work was partially funded by the Academy of Finland, grant 314888, the European Research Council CoG 863818 (ForM-SMArt), and the Austrian Science Fund (FWF) project I 4800-N (ADVISE). LS was supported by the Stochastic Analysis and Application Research Center (SAARC) under National Research Foundation of Korea grant NRF-2019R1A5A1028324.","year":"2024","citation":{"ama":"Hirvonen J, Schmid L, Chatterjee K, Schmid S. On the convergence time in graphical games: A locality-sensitive approach. In: <i>27th International Conference on Principles of Distributed Systems</i>. Vol 286. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11\">10.4230/LIPIcs.OPODIS.2023.11</a>","ieee":"J. Hirvonen, L. Schmid, K. Chatterjee, and S. Schmid, “On the convergence time in graphical games: A locality-sensitive approach,” in <i>27th International Conference on Principles of Distributed Systems</i>, Tokyo, Japan, 2024, vol. 286.","short":"J. Hirvonen, L. Schmid, K. Chatterjee, S. Schmid, in:, 27th International Conference on Principles of Distributed Systems, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","mla":"Hirvonen, Juho, et al. “On the Convergence Time in Graphical Games: A Locality-Sensitive Approach.” <i>27th International Conference on Principles of Distributed Systems</i>, vol. 286, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11\">10.4230/LIPIcs.OPODIS.2023.11</a>.","ista":"Hirvonen J, Schmid L, Chatterjee K, Schmid S. 2024. On the convergence time in graphical games: A locality-sensitive approach. 27th International Conference on Principles of Distributed Systems. OPODIS: Conference on Principles of Distributed Systems, LIPIcs, vol. 286, 11.","chicago":"Hirvonen, Juho, Laura Schmid, Krishnendu Chatterjee, and Stefan Schmid. “On the Convergence Time in Graphical Games: A Locality-Sensitive Approach.” In <i>27th International Conference on Principles of Distributed Systems</i>, Vol. 286. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11\">https://doi.org/10.4230/LIPIcs.OPODIS.2023.11</a>.","apa":"Hirvonen, J., Schmid, L., Chatterjee, K., &#38; Schmid, S. (2024). On the convergence time in graphical games: A locality-sensitive approach. In <i>27th International Conference on Principles of Distributed Systems</i> (Vol. 286). Tokyo, Japan: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11\">https://doi.org/10.4230/LIPIcs.OPODIS.2023.11</a>"},"date_created":"2024-02-18T23:01:01Z","doi":"10.4230/LIPIcs.OPODIS.2023.11","file_date_updated":"2024-02-26T09:04:58Z","_id":"15006","ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"arxiv":["2102.13457"]},"abstract":[{"text":"Graphical games are a useful framework for modeling the interactions of (selfish) agents who are connected via an underlying topology and whose behaviors influence each other. They have wide applications ranging from computer science to economics and biology. Yet, even though an agent’s payoff only depends on the actions of their direct neighbors in graphical games, computing the Nash equilibria and making statements about the convergence time of \"natural\" local dynamics in particular can be highly challenging. In this work, we present a novel approach for classifying complexity of Nash equilibria in graphical games by establishing a connection to local graph algorithms, a subfield of distributed computing. In particular, we make the observation that the equilibria of graphical games are equivalent to locally verifiable labelings (LVL) in graphs; vertex labelings which are verifiable with constant-round local algorithms. This connection allows us to derive novel lower bounds on the convergence time to equilibrium of best-response dynamics in graphical games. Since we establish that distributed convergence can sometimes be provably slow, we also introduce and give bounds on an intuitive notion of \"time-constrained\" inefficiency of best responses. We exemplify how our results can be used in the implementation of mechanisms that ensure convergence of best responses to a Nash equilibrium. Our results thus also give insight into the convergence of strategy-proof algorithms for graphical games, which is still not well understood.","lang":"eng"}],"publication_status":"published","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2024-01-18T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":286,"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}]},{"article_processing_charge":"No","oa":1,"date_updated":"2025-07-14T09:09:50Z","title":"Faster algorithm for turn-based stochastic games with bounded treewidth","language":[{"iso":"eng"}],"publication":"Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165"},{"last_name":"Saona Urmeneta","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","orcid":"0000-0001-5103-038X","first_name":"Raimundo J","full_name":"Saona Urmeneta, Raimundo J"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","first_name":"Jakub"}],"publication_identifier":{"isbn":["9781611977554"]},"month":"02","conference":{"location":"Florence, Italy","end_date":"2023-01-25","name":"SODA: Symposium on Discrete Algorithms","start_date":"2023-01-22"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1137/1.9781611977554.ch173"}],"day":"01","type":"conference","status":"public","year":"2023","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant.","date_created":"2023-02-24T12:20:47Z","citation":{"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>","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>","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.","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>.","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>.","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."},"ec_funded":1,"_id":"12676","doi":"10.1137/1.9781611977554.ch173","publication_status":"published","abstract":[{"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.","lang":"eng"}],"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"date_published":"2023-02-01T00:00:00Z","publisher":"Society for Industrial and Applied Mathematics","quality_controlled":"1","page":"4590-4605","department":[{"_id":"GradSch"},{"_id":"KrCh"}]},{"doi":"10.1371/journal.pone.0279838","_id":"12706","article_type":"original","file_date_updated":"2023-03-07T10:26:45Z","date_created":"2023-03-05T23:01:05Z","citation":{"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.","ama":"Mckerral JC, Kleshnina M, Ejov V, Bartle L, Mitchell JG, Filar JA. Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations. <i>PLoS One</i>. 2023;18(2):e0279838. doi:<a href=\"https://doi.org/10.1371/journal.pone.0279838\">10.1371/journal.pone.0279838</a>","short":"J.C. Mckerral, M. Kleshnina, V. Ejov, L. Bartle, J.G. Mitchell, J.A. Filar, PLoS One 18 (2023) e0279838.","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>.","chicago":"Mckerral, Jody C., Maria Kleshnina, Vladimir Ejov, Louise Bartle, James G. Mitchell, and Jerzy A. Filar. “Empirical Parameterisation and Dynamical Analysis of the Allometric Rosenzweig-MacArthur Equations.” <i>PLoS One</i>. Public Library of Science, 2023. <a href=\"https://doi.org/10.1371/journal.pone.0279838\">https://doi.org/10.1371/journal.pone.0279838</a>.","apa":"Mckerral, J. C., Kleshnina, M., Ejov, V., Bartle, L., Mitchell, J. G., &#38; Filar, J. A. (2023). Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations. <i>PLoS One</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0279838\">https://doi.org/10.1371/journal.pone.0279838</a>"},"year":"2023","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.","quality_controlled":"1","volume":18,"page":"e0279838","department":[{"_id":"KrCh"}],"date_published":"2023-02-27T00:00:00Z","publisher":"Public Library of Science","abstract":[{"lang":"eng","text":"Allometric settings of population dynamics models are appealing due to their parsimonious nature and broad utility when studying system level effects. Here, we parameterise the size-scaled Rosenzweig-MacArthur differential equations to eliminate prey-mass dependency, facilitating an in depth analytic study of the equations which incorporates scaling parameters’ contributions to coexistence. We define the functional response term to match empirical findings, and examine situations where metabolic theory derivations and observation diverge. The dynamical properties of the Rosenzweig-MacArthur system, encompassing the distribution of size-abundance equilibria, the scaling of period and amplitude of population cycling, and relationships between predator and prey abundances, are consistent with empirical observation. Our parameterisation is an accurate minimal model across 15+ orders of mass magnitude."}],"external_id":{"isi":["000996122900022"],"pmid":["36848357"]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000"],"publication_status":"published","publication":"PLoS One","language":[{"iso":"eng"}],"has_accepted_license":"1","scopus_import":"1","intvolume":"        18","isi":1,"title":"Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations","issue":"2","article_processing_charge":"No","oa":1,"date_updated":"2023-10-17T12:53:30Z","status":"public","type":"journal_article","pmid":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","access_level":"open_access","file_size":1257003,"content_type":"application/pdf","creator":"cchlebak","date_updated":"2023-03-07T10:26:45Z","date_created":"2023-03-07T10:26:45Z","file_name":"2023_PLOSOne_Mckerral.pdf","checksum":"798ed5739a4117b03173e5d56e0534c9","file_id":"12712","success":1}],"oa_version":"Published Version","day":"27","month":"02","publication_identifier":{"eissn":["1932-6203"]},"author":[{"full_name":"Mckerral, Jody C.","first_name":"Jody C.","last_name":"Mckerral"},{"first_name":"Maria","full_name":"Kleshnina, Maria","last_name":"Kleshnina","id":"4E21749C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ejov","full_name":"Ejov, Vladimir","first_name":"Vladimir"},{"last_name":"Bartle","first_name":"Louise","full_name":"Bartle, Louise"},{"last_name":"Mitchell","full_name":"Mitchell, James G.","first_name":"James G."},{"full_name":"Filar, Jerzy A.","first_name":"Jerzy A.","last_name":"Filar"}]},{"year":"2023","acknowledgement":"Tobias Winkler and Joost-Pieter Katoen are supported by the DFG RTG 2236 UnRAVeL and the innovation programme under the Marie Skłodowska-Curie grant agreement No. 101008233 (Mission). Krishnendu Chatterjee is supported by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) Project ICT15-003. Maximilian Weininger is supported by the DFG projects 383882557 Statistical Unbounded Verification (SUV) and 427755713 Group-By Objectives in Probabilistic Verification (GOPro). Stefanie Mohr is supported by the DFG RTG 2428 CONVEY. Open Access funding enabled and organized by Projekt DEAL.","date_created":"2023-03-19T23:00:59Z","citation":{"chicago":"Chatterjee, Krishnendu, Joost P Katoen, Stefanie Mohr, Maximilian Weininger, and Tobias Winkler. “Stochastic Games with Lexicographic Objectives.” <i>Formal Methods in System Design</i>. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/s10703-023-00411-4\">https://doi.org/10.1007/s10703-023-00411-4</a>.","mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Objectives.” <i>Formal Methods in System Design</i>, Springer Nature, 2023, doi:<a href=\"https://doi.org/10.1007/s10703-023-00411-4\">10.1007/s10703-023-00411-4</a>.","ista":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2023. Stochastic games with lexicographic objectives. Formal Methods in System Design.","ama":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. Stochastic games with lexicographic objectives. <i>Formal Methods in System Design</i>. 2023. doi:<a href=\"https://doi.org/10.1007/s10703-023-00411-4\">10.1007/s10703-023-00411-4</a>","ieee":"K. Chatterjee, J. P. Katoen, S. Mohr, M. Weininger, and T. Winkler, “Stochastic games with lexicographic objectives,” <i>Formal Methods in System Design</i>. Springer Nature, 2023.","short":"K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods in System Design (2023).","apa":"Chatterjee, K., Katoen, J. P., Mohr, S., Weininger, M., &#38; Winkler, T. (2023). Stochastic games with lexicographic objectives. <i>Formal Methods in System Design</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10703-023-00411-4\">https://doi.org/10.1007/s10703-023-00411-4</a>"},"related_material":{"record":[{"id":"8272","relation":"earlier_version","status":"public"}]},"ec_funded":1,"article_type":"original","_id":"12738","doi":"10.1007/s10703-023-00411-4","publication_status":"epub_ahead","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000"],"abstract":[{"text":"We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as controllable and adversarial non-determinism. Lexicographic order allows one to consider multiple objectives with a strict preference order. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. For a mixture of reachability and safety objectives, we show that deterministic lexicographically optimal strategies exist and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in NP∩coNP, matching the current known bound for single objectives; and in general the decision problem is PSPACE-hard and can be solved in NEXPTIME∩coNEXPTIME. We present an algorithm that computes the lexicographically optimal strategies via a reduction to the computation of optimal strategies in a sequence of single-objectives games. For omega-regular objectives, we restrict our analysis to one-player games, also known as Markov decision processes. We show that lexicographically optimal strategies exist and need either randomization or finite memory. We present an algorithm that solves the relevant decision problem in polynomial time. We have implemented our algorithms and report experimental results on various case studies.","lang":"eng"}],"external_id":{"isi":["000946174300001"]},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"date_published":"2023-03-08T00:00:00Z","publisher":"Springer Nature","quality_controlled":"1","department":[{"_id":"KrCh"}],"article_processing_charge":"No","oa":1,"date_updated":"2025-07-14T09:10:14Z","title":"Stochastic games with lexicographic objectives","isi":1,"scopus_import":"1","language":[{"iso":"eng"}],"publication":"Formal Methods in System Design","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Katoen, Joost P","first_name":"Joost P","last_name":"Katoen","id":"4524F760-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Mohr","full_name":"Mohr, Stefanie","first_name":"Stefanie"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"},{"last_name":"Winkler","full_name":"Winkler, Tobias","first_name":"Tobias"}],"publication_identifier":{"eissn":["1572-8102"]},"month":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"08","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/s10703-023-00411-4"}],"oa_version":"Published Version","status":"public","type":"journal_article"},{"status":"public","type":"journal_article","author":[{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","first_name":"Jakub","full_name":"Svoboda, Jakub"},{"orcid":"0000-0002-1097-9684","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","first_name":"Josef"},{"last_name":"Kaveh","first_name":"Kamran","full_name":"Kaveh, Kamran"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}],"month":"03","publication_identifier":{"eissn":["1471-2946"],"issn":["1364-5021"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"creator":"dernst","content_type":"application/pdf","access_level":"open_access","file_size":827784,"relation":"main_file","checksum":"13953d349fbefcb5d21ccc6b303297eb","file_id":"12796","file_name":"2023_ProceedingsRoyalSocietyA_Svoboda.pdf","success":1,"date_updated":"2023-04-03T06:25:29Z","date_created":"2023-04-03T06:25:29Z"}],"oa_version":"Published Version","day":"29","language":[{"iso":"eng"}],"publication":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","article_processing_charge":"No","issue":"2271","oa":1,"date_updated":"2025-07-14T09:09:51Z","title":"Coexistence times in the Moran process with environmental heterogeneity","isi":1,"has_accepted_license":"1","scopus_import":"1","intvolume":"       479","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"date_published":"2023-03-29T00:00:00Z","publisher":"The Royal Society","volume":479,"quality_controlled":"1","department":[{"_id":"KrCh"}],"publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000"],"abstract":[{"text":"Populations evolve in spatially heterogeneous environments. While a certain trait might bring a fitness advantage in some patch of the environment, a different trait might be advantageous in another patch. Here, we study the Moran birth–death process with two types of individuals in a population stretched across two patches of size N, each patch favouring one of the two types. We show that the long-term fate of such populations crucially depends on the migration rate μ\r\n between the patches. To classify the possible fates, we use the distinction between polynomial (short) and exponential (long) timescales. We show that when μ is high then one of the two types fixates on the whole population after a number of steps that is only polynomial in N. By contrast, when μ is low then each type holds majority in the patch where it is favoured for a number of steps that is at least exponential in N. Moreover, we precisely identify the threshold migration rate μ⋆ that separates those two scenarios, thereby exactly delineating the situations that support long-term coexistence of the two types. We also discuss the case of various cycle graphs and we present computer simulations that perfectly match our analytical results.","lang":"eng"}],"external_id":{"isi":["000957125500002"]},"article_type":"original","_id":"12787","file_date_updated":"2023-04-03T06:25:29Z","doi":"10.1098/rspa.2022.0685","year":"2023","acknowledgement":"J.S. and K.C. acknowledge support from the ERC CoG 863818 (ForM-SMArt)","citation":{"apa":"Svoboda, J., Tkadlec, J., Kaveh, K., &#38; Chatterjee, K. (2023). Coexistence times in the Moran process with environmental heterogeneity. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. The Royal Society. <a href=\"https://doi.org/10.1098/rspa.2022.0685\">https://doi.org/10.1098/rspa.2022.0685</a>","mla":"Svoboda, Jakub, et al. “Coexistence Times in the Moran Process with Environmental Heterogeneity.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 479, no. 2271, 20220685, The Royal Society, 2023, doi:<a href=\"https://doi.org/10.1098/rspa.2022.0685\">10.1098/rspa.2022.0685</a>.","ista":"Svoboda J, Tkadlec J, Kaveh K, Chatterjee K. 2023. Coexistence times in the Moran process with environmental heterogeneity. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences. 479(2271), 20220685.","chicago":"Svoboda, Jakub, Josef Tkadlec, Kamran Kaveh, and Krishnendu Chatterjee. “Coexistence Times in the Moran Process with Environmental Heterogeneity.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. The Royal Society, 2023. <a href=\"https://doi.org/10.1098/rspa.2022.0685\">https://doi.org/10.1098/rspa.2022.0685</a>.","short":"J. Svoboda, J. Tkadlec, K. Kaveh, K. Chatterjee, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 479 (2023).","ama":"Svoboda J, Tkadlec J, Kaveh K, Chatterjee K. Coexistence times in the Moran process with environmental heterogeneity. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. 2023;479(2271). doi:<a href=\"https://doi.org/10.1098/rspa.2022.0685\">10.1098/rspa.2022.0685</a>","ieee":"J. Svoboda, J. Tkadlec, K. Kaveh, and K. Chatterjee, “Coexistence times in the Moran process with environmental heterogeneity,” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 479, no. 2271. The Royal Society, 2023."},"date_created":"2023-04-02T22:01:09Z","article_number":"20220685","related_material":{"link":[{"url":"https://doi.org/10.6084/m9.figshare.21261771.v1","relation":"research_data"}]},"ec_funded":1},{"publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000"],"abstract":[{"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.","lang":"eng"}],"external_id":{"arxiv":["1903.06981"]},"date_published":"2023-01-18T00:00:00Z","publisher":"EPI Sciences","quality_controlled":"1","volume":24,"department":[{"_id":"KrCh"},{"_id":"HeEd"},{"_id":"UlWa"}],"year":"2023","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","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>","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.","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>","short":"A. Biniaz, K. Jain, A. Lubiw, Z. Masárová, T. Miltzow, D. Mondal, A.M. Naredla, J. Tkadlec, A. Turcotte, Discrete Mathematics and Theoretical Computer Science 24 (2023).","mla":"Biniaz, Ahmad, et al. “Token Swapping on Trees.” <i>Discrete Mathematics and Theoretical Computer Science</i>, vol. 24, no. 2, 9, EPI Sciences, 2023, doi:<a href=\"https://doi.org/10.46298/DMTCS.8383\">10.46298/DMTCS.8383</a>.","ista":"Biniaz A, Jain K, Lubiw A, Masárová Z, Miltzow T, Mondal D, Naredla AM, Tkadlec J, Turcotte A. 2023. Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. 24(2), 9.","chicago":"Biniaz, Ahmad, Kshitij Jain, Anna Lubiw, Zuzana Masárová, Tillmann Miltzow, Debajyoti Mondal, Anurag Murty Naredla, Josef Tkadlec, and Alexi Turcotte. “Token Swapping on Trees.” <i>Discrete Mathematics and Theoretical Computer Science</i>. EPI Sciences, 2023. <a href=\"https://doi.org/10.46298/DMTCS.8383\">https://doi.org/10.46298/DMTCS.8383</a>."},"date_created":"2023-04-16T22:01:08Z","article_number":"9","related_material":{"record":[{"relation":"earlier_version","id":"7950","status":"public"}]},"article_type":"original","_id":"12833","file_date_updated":"2023-04-17T08:10:28Z","doi":"10.46298/DMTCS.8383","arxiv":1,"author":[{"full_name":"Biniaz, Ahmad","first_name":"Ahmad","last_name":"Biniaz"},{"full_name":"Jain, Kshitij","first_name":"Kshitij","last_name":"Jain"},{"last_name":"Lubiw","full_name":"Lubiw, Anna","first_name":"Anna"},{"first_name":"Zuzana","full_name":"Masárová, Zuzana","orcid":"0000-0002-6660-1322","last_name":"Masárová","id":"45CFE238-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Miltzow","first_name":"Tillmann","full_name":"Miltzow, Tillmann"},{"last_name":"Mondal","first_name":"Debajyoti","full_name":"Mondal, Debajyoti"},{"last_name":"Naredla","full_name":"Naredla, Anurag Murty","first_name":"Anurag Murty"},{"orcid":"0000-0002-1097-9684","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","first_name":"Josef"},{"full_name":"Turcotte, Alexi","first_name":"Alexi","last_name":"Turcotte"}],"publication_identifier":{"eissn":["1365-8050"],"issn":["1462-7264"]},"month":"01","file":[{"file_size":2072197,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","creator":"dernst","date_updated":"2023-04-17T08:10:28Z","date_created":"2023-04-17T08:10:28Z","checksum":"439102ea4f6e2aeefd7107dfb9ccf532","file_id":"12844","file_name":"2022_DMTCS_Biniaz.pdf","success":1}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","day":"18","oa_version":"Published Version","type":"journal_article","status":"public","issue":"2","article_processing_charge":"No","date_updated":"2024-01-04T12:42:09Z","oa":1,"title":"Token swapping on trees","intvolume":"        24","has_accepted_license":"1","scopus_import":"1","language":[{"iso":"eng"}],"publication":"Discrete Mathematics and Theoretical Computer Science"},{"external_id":{"pmid":["37045828"],"isi":["001003644100020"]},"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."}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publication_status":"published","department":[{"_id":"KrCh"}],"volume":14,"quality_controlled":"1","publisher":"Springer Nature","date_published":"2023-04-12T00:00:00Z","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"ec_funded":1,"article_number":"2086","date_created":"2023-04-23T22:01:03Z","citation":{"ista":"Schmid L, Ekbatani F, Hilbe C, Chatterjee K. 2023. Quantitative assessment can stabilize indirect reciprocity under imperfect information. Nature Communications. 14, 2086.","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>.","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>.","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.","ama":"Schmid L, Ekbatani F, Hilbe C, Chatterjee K. Quantitative assessment can stabilize indirect reciprocity under imperfect information. <i>Nature Communications</i>. 2023;14. doi:<a href=\"https://doi.org/10.1038/s41467-023-37817-x\">10.1038/s41467-023-37817-x</a>","short":"L. Schmid, F. Ekbatani, C. Hilbe, K. Chatterjee, Nature Communications 14 (2023).","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>"},"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.","year":"2023","doi":"10.1038/s41467-023-37817-x","file_date_updated":"2023-04-25T09:13:53Z","_id":"12861","article_type":"original","oa_version":"Published Version","day":"12","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"file_id":"12868","checksum":"a4b3b7b36fbef068cabf4fb99501fef6","file_name":"2023_NatureComm_Schmid.pdf","success":1,"date_updated":"2023-04-25T09:13:53Z","date_created":"2023-04-25T09:13:53Z","creator":"dernst","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_size":1786475}],"month":"04","publication_identifier":{"eissn":["2041-1723"]},"author":[{"first_name":"Laura","full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329","last_name":"Schmid","id":"38B437DE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ekbatani","full_name":"Ekbatani, Farbod","first_name":"Farbod"},{"orcid":"0000-0001-5116-955X","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian","first_name":"Christian"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}],"pmid":1,"type":"journal_article","status":"public","intvolume":"        14","scopus_import":"1","has_accepted_license":"1","isi":1,"title":"Quantitative assessment can stabilize indirect reciprocity under imperfect information","oa":1,"date_updated":"2025-07-14T09:09:52Z","article_processing_charge":"No","publication":"Nature Communications","language":[{"iso":"eng"}]},{"alternative_title":["LNCS"],"status":"public","type":"conference","author":[{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer"}],"arxiv":1,"day":"22","oa_version":"Published Version","file":[{"checksum":"59f707a3949c03793251b0d04c62542a","file_id":"13148","file_name":"2023_LNCS_Meggendorfer.pdf","success":1,"date_updated":"2023-06-19T07:18:40Z","date_created":"2023-06-19T07:18:40Z","creator":"dernst","relation":"main_file","file_size":521951,"content_type":"application/pdf","access_level":"open_access"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Paris, France","end_date":"2023-04-27","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22"},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308222"]},"month":"04","language":[{"iso":"eng"}],"publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","title":"Correct approximation of stationary distributions","oa":1,"date_updated":"2024-02-27T07:19:33Z","article_processing_charge":"No","scopus_import":"1","has_accepted_license":"1","intvolume":"     13993","department":[{"_id":"KrCh"}],"page":"489-507","volume":13993,"quality_controlled":"1","publisher":"Springer Nature","date_published":"2023-04-22T00:00:00Z","publication_status":"published","external_id":{"arxiv":["2301.08137"]},"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."}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"file_date_updated":"2023-06-19T07:18:40Z","_id":"13139","doi":"10.1007/978-3-031-30823-9_25","citation":{"short":"T. Meggendorfer, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 489–507.","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>","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.","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>.","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.","chicago":"Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.” In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, 13993:489–507. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_25\">https://doi.org/10.1007/978-3-031-30823-9_25</a>.","apa":"Meggendorfer, T. (2023). Correct approximation of stationary distributions. In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13993, pp. 489–507). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_25\">https://doi.org/10.1007/978-3-031-30823-9_25</a>"},"date_created":"2023-06-18T22:00:46Z","year":"2023","related_material":{"record":[{"status":"public","relation":"research_data","id":"14990"}]}},{"alternative_title":["LNCS"],"status":"public","type":"conference","conference":{"start_date":"2023-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2023-04-27","location":"Paris, France"},"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031308222"],"eissn":["1611-3349"]},"month":"04","day":"22","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2023-06-19T08:29:30Z","date_updated":"2023-06-19T08:29:30Z","success":1,"checksum":"3d8a8bb24d211bc83360dfc2fd744307","file_name":"2023_LNCS_Chatterjee.pdf","file_id":"13150","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_size":528455,"creator":"dernst"}],"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dorde","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","orcid":"0000-0002-4681-1699"}],"publication":"Tools and Algorithms for the Construction and Analysis of Systems ","language":[{"iso":"eng"}],"intvolume":"     13993","has_accepted_license":"1","scopus_import":"1","date_updated":"2025-07-14T09:09:52Z","oa":1,"article_processing_charge":"No","title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","publisher":"Springer Nature","date_published":"2023-04-22T00:00:00Z","page":"3-25","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","volume":13993,"project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"call_identifier":"H2020","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"abstract":[{"lang":"eng","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."}],"publication_status":"published","doi":"10.1007/978-3-031-30823-9_1","file_date_updated":"2023-06-19T08:29:30Z","_id":"13142","ec_funded":1,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","year":"2023","date_created":"2023-06-18T22:00:47Z","citation":{"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>","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.","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>","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>.","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>.","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."}},{"related_material":{"record":[{"id":"14506","relation":"dissertation_contains","status":"public"}]},"ec_funded":1,"year":"2023","acknowledgement":"We thank Mahsa Bastankhah and Mohammad Ali Maddah-Ali for fruitful discussions about different variants of the problem. This work is supported by the European Research Council (ERC) Consolidator Project 864228 (AdjustNet), 2020-2025, the ERC CoG 863818 (ForM-SMArt), and the German Research Foundation (DFG) grant 470029389 (FlexNets), 2021–2024.","date_created":"2023-07-16T22:01:12Z","citation":{"ama":"Schmid S, Svoboda J, Yeo MX. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. In: <i>SIROCCO 2023: Structural Information and Communication Complexity </i>. Vol 13892. Springer Nature; 2023:576-594. doi:<a href=\"https://doi.org/10.1007/978-3-031-32733-9_26\">10.1007/978-3-031-32733-9_26</a>","ieee":"S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation,” in <i>SIROCCO 2023: Structural Information and Communication Complexity </i>, Alcala de Henares, Spain, 2023, vol. 13892, pp. 576–594.","short":"S. Schmid, J. Svoboda, M.X. Yeo, in:, SIROCCO 2023: Structural Information and Communication Complexity , Springer Nature, 2023, pp. 576–594.","mla":"Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” <i>SIROCCO 2023: Structural Information and Communication Complexity </i>, vol. 13892, Springer Nature, 2023, pp. 576–94, doi:<a href=\"https://doi.org/10.1007/978-3-031-32733-9_26\">10.1007/978-3-031-32733-9_26</a>.","chicago":"Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” In <i>SIROCCO 2023: Structural Information and Communication Complexity </i>, 13892:576–94. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-32733-9_26\">https://doi.org/10.1007/978-3-031-32733-9_26</a>.","ista":"Schmid S, Svoboda J, Yeo MX. 2023. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. SIROCCO 2023: Structural Information and Communication Complexity . SIROCCO: Structural Information and Communication Complexity, LNCS, vol. 13892, 576–594.","apa":"Schmid, S., Svoboda, J., &#38; Yeo, M. X. (2023). Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. In <i>SIROCCO 2023: Structural Information and Communication Complexity </i> (Vol. 13892, pp. 576–594). Alcala de Henares, Spain: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-32733-9_26\">https://doi.org/10.1007/978-3-031-32733-9_26</a>"},"doi":"10.1007/978-3-031-32733-9_26","_id":"13238","abstract":[{"text":"We consider a natural problem dealing with weighted packet selection across a rechargeable link, which e.g., finds applications in cryptocurrency networks. The capacity of a link (u, v) is determined by how much nodes u and v allocate for this link. Specifically, the input is a finite ordered sequence of packets that arrive in both directions along a link. Given (u, v) and a packet of weight x going from u to v, node u can either accept or reject the packet. If u accepts the packet, the capacity on link (u, v) decreases by x. Correspondingly, v’s capacity on (u, v) increases by x. If a node rejects the packet, this will entail a cost affinely linear in the weight of the packet. A link is “rechargeable” in the sense that the total capacity of the link has to remain constant, but the allocation of capacity at the ends of the link can depend arbitrarily on the nodes’ decisions. The goal is to minimise the sum of the capacity injected into the link and the cost of rejecting packets. We show that the problem is NP-hard, but can be approximated efficiently with a ratio of (1+ε)⋅(1+3–√) for some arbitrary ε>0.\r\n.","lang":"eng"}],"external_id":{"arxiv":["2204.13459"]},"publication_status":"published","date_published":"2023-05-25T00:00:00Z","publisher":"Springer Nature","quality_controlled":"1","volume":13892,"department":[{"_id":"KrPi"},{"_id":"KrCh"}],"page":"576-594","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"intvolume":"     13892","scopus_import":"1","article_processing_charge":"No","oa":1,"date_updated":"2025-07-14T09:09:53Z","title":"Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation","publication":"SIROCCO 2023: Structural Information and Communication Complexity ","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783031327322"],"eissn":["1611-3349"],"issn":["0302-9743"]},"month":"05","conference":{"location":"Alcala de Henares, Spain","end_date":"2023-06-09","name":"SIROCCO: Structural Information and Communication Complexity","start_date":"2023-06-06"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2204.13459"}],"day":"25","arxiv":1,"author":[{"last_name":"Schmid","first_name":"Stefan","full_name":"Schmid, Stefan"},{"first_name":"Jakub","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267","last_name":"Svoboda","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"},{"first_name":"Michelle X","full_name":"Yeo, Michelle X","last_name":"Yeo","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","orcid":"0009-0001-3676-4809"}],"type":"conference","status":"public","alternative_title":["LNCS"]},{"publication_status":"published","external_id":{"pmid":["37438341"],"isi":["001029450400031"]},"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"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":14,"publisher":"Springer Nature","date_published":"2023-07-12T00:00:00Z","date_created":"2023-07-23T22:01:11Z","citation":{"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>","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.","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>.","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).","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>","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."},"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.).","year":"2023","ec_funded":1,"related_material":{"record":[{"status":"public","id":"13336","relation":"research_data"}]},"article_number":"4153","file_date_updated":"2023-07-31T11:32:36Z","article_type":"original","_id":"13258","doi":"10.1038/s41467-023-39625-9","author":[{"first_name":"Maria","full_name":"Kleshnina, Maria","last_name":"Kleshnina","id":"4E21749C-F248-11E8-B48F-1D18A9856A87"},{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","last_name":"Hilbe","orcid":"0000-0001-5116-955X","first_name":"Christian","full_name":"Hilbe, Christian"},{"last_name":"Simsa","id":"409d615c-2f95-11ee-b934-90a352102c1e","orcid":"0000-0001-6687-1210","first_name":"Stepan","full_name":"Simsa, Stepan"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Martin A.","full_name":"Nowak, Martin A.","last_name":"Nowak"}],"day":"12","oa_version":"Published Version","file":[{"relation":"main_file","file_size":1601682,"access_level":"open_access","content_type":"application/pdf","creator":"dernst","date_created":"2023-07-31T11:32:36Z","date_updated":"2023-07-31T11:32:36Z","success":1,"file_id":"13337","checksum":"5aceefdfe76686267b93ae4fe81899f1","file_name":"2023_NatureComm_Kleshnina.pdf"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07","publication_identifier":{"eissn":["2041-1723"]},"pmid":1,"type":"journal_article","status":"public","title":"The effect of environmental information on evolution of cooperation in stochastic games","date_updated":"2025-07-14T09:09:53Z","oa":1,"article_processing_charge":"Yes","intvolume":"        14","scopus_import":"1","has_accepted_license":"1","isi":1,"language":[{"iso":"eng"}],"publication":"Nature Communications"},{"month":"06","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"20","main_file_link":[{"url":"https://doi.org/10.5281/zenodo.8059564","open_access":"1"}],"oa_version":"Published Version","author":[{"last_name":"Kleshnina","id":"4E21749C-F248-11E8-B48F-1D18A9856A87","first_name":"Maria","full_name":"Kleshnina, Maria"}],"date_published":"2023-06-20T00:00:00Z","type":"research_data_reference","status":"public","publisher":"Zenodo","department":[{"_id":"KrCh"}],"related_material":{"record":[{"status":"public","id":"13258","relation":"used_in_publication"}]},"article_processing_charge":"No","year":"2023","oa":1,"date_updated":"2025-07-14T09:09:53Z","date_created":"2023-07-31T11:30:46Z","citation":{"apa":"Kleshnina, M. (2023). kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.8059564\">https://doi.org/10.5281/ZENODO.8059564</a>","chicago":"Kleshnina, Maria. “Kleshnina/Stochgames_info: The Effect of Environmental Information on Evolution of Cooperation in Stochastic Games.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.8059564\">https://doi.org/10.5281/ZENODO.8059564</a>.","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>.","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>.","short":"M. Kleshnina, (2023).","ieee":"M. Kleshnina, “kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games.” Zenodo, 2023.","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>"},"title":"kleshnina/stochgames_info: The effect of environmental information on evolution of cooperation in stochastic games","doi":"10.5281/ZENODO.8059564","_id":"13336"},{"page":"11926-11935","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"volume":37,"quality_controlled":"1","publisher":"Association for the Advancement of Artificial Intelligence","date_published":"2023-06-26T00:00:00Z","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"external_id":{"arxiv":["2210.05308"]},"abstract":[{"text":"We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks.","lang":"eng"}],"publication_status":"published","doi":"10.1609/aaai.v37i10.26407","_id":"14830","ec_funded":1,"related_material":{"record":[{"status":"public","id":"14600","relation":"earlier_version"}]},"date_created":"2024-01-18T07:44:31Z","citation":{"apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.","chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>.","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>.","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935.","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–11935."},"keyword":["General Medicine"],"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.","year":"2023","status":"public","type":"conference","day":"26","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2023-02-07","name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14","location":"Washington, DC, United States"},"month":"06","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"author":[{"first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic"},{"first_name":"Mathias","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"}],"arxiv":1,"publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","language":[{"iso":"eng"}],"intvolume":"        37","title":"Learning control policies for stochastic systems with reach-avoid guarantees","date_updated":"2025-07-14T09:10:02Z","article_processing_charge":"No","issue":"10"},{"author":[{"orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","full_name":"Meggendorfer, Tobias"}],"day":"18","oa_version":"Published Version","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/zenodo.7548214"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"The software artefact to evaluate the approximation of stationary distributions implementation."}],"ddc":["000"],"month":"01","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"KrCh"}],"publisher":"Zenodo","status":"public","type":"research_data_reference","date_published":"2023-01-18T00:00:00Z","citation":{"apa":"Meggendorfer, T. (2023). Artefact for: Correct Approximation of Stationary Distributions. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.7548214\">https://doi.org/10.5281/ZENODO.7548214</a>","chicago":"Meggendorfer, Tobias. “Artefact for: Correct Approximation of Stationary Distributions.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.7548214\">https://doi.org/10.5281/ZENODO.7548214</a>.","mla":"Meggendorfer, Tobias. <i>Artefact for: Correct Approximation of Stationary Distributions</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.7548214\">10.5281/ZENODO.7548214</a>.","ista":"Meggendorfer T. 2023. Artefact for: Correct Approximation of Stationary Distributions, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.7548214\">10.5281/ZENODO.7548214</a>.","ama":"Meggendorfer T. Artefact for: Correct Approximation of Stationary Distributions. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.7548214\">10.5281/ZENODO.7548214</a>","ieee":"T. Meggendorfer, “Artefact for: Correct Approximation of Stationary Distributions.” Zenodo, 2023.","short":"T. Meggendorfer, (2023)."},"date_created":"2024-02-14T14:27:06Z","title":"Artefact for: Correct Approximation of Stationary Distributions","oa":1,"date_updated":"2024-02-27T07:19:32Z","article_processing_charge":"No","year":"2023","related_material":{"record":[{"relation":"used_in_publication","id":"13139","status":"public"}]},"has_accepted_license":"1","_id":"14990","doi":"10.5281/ZENODO.7548214"},{"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"status":"public","type":"conference","date_published":"2023-12-15T00:00:00Z","arxiv":1,"publication_status":"epub_ahead","author":[{"last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","full_name":"Zikelic, Dorde"},{"first_name":"Mathias","full_name":"Lechner, Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"id":"a235593c-d7fa-11eb-a0c5-b22ca3c66ee6","last_name":"Verma","first_name":"Abhinav","full_name":"Verma, Abhinav"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"abstract":[{"text":"Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","day":"15","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2312.01456","open_access":"1"}],"external_id":{"arxiv":["2312.01456"]},"month":"12","conference":{"start_date":"2023-12-10","name":"NeurIPS: Neural Information Processing Systems","end_date":"2023-12-16","location":"New Orleans, LO, United States"},"_id":"15023","language":[{"iso":"eng"}],"publication":"37th Conference on Neural Information Processing Systems","date_created":"2024-02-25T09:23:24Z","citation":{"chicago":"Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” In <i>37th Conference on Neural Information Processing Systems</i>, 2023.","ista":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems.","mla":"Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” <i>37th Conference on Neural Information Processing Systems</i>, 2023.","ieee":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional policy learning in stochastic control systems with formal guarantees,” in <i>37th Conference on Neural Information Processing Systems</i>, New Orleans, LO, United States, 2023.","ama":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy learning in stochastic control systems with formal guarantees. In: <i>37th Conference on Neural Information Processing Systems</i>. ; 2023.","short":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, 2023.","apa":"Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., &#38; Henzinger, T. A. (2023). Compositional policy learning in stochastic control systems with formal guarantees. In <i>37th Conference on Neural Information Processing Systems</i>. New Orleans, LO, United States."},"title":"Compositional policy learning in stochastic control systems with formal guarantees","article_processing_charge":"No","year":"2023","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt).","oa":1,"date_updated":"2025-07-14T09:10:04Z","ec_funded":1},{"year":"2023","acknowledgement":"This research was funded in part by DFG projects 383882557 “SUV” and 427755713 “GOPro”.","date_created":"2023-08-06T22:01:10Z","citation":{"short":"J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2023.","ama":"Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration on stochastic games with quantitative objectives. In: <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Vol 2023. Institute of Electrical and Electronics Engineers; 2023. doi:<a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">10.1109/LICS56636.2023.10175771</a>","ieee":"J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value iteration on stochastic games with quantitative objectives,” in <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Boston, MA, United States, 2023, vol. 2023.","mla":"Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, vol. 2023, Institute of Electrical and Electronics Engineers, 2023, doi:<a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">10.1109/LICS56636.2023.10175771</a>.","ista":"Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science vol. 2023.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Vol. 2023. Institute of Electrical and Electronics Engineers, 2023. <a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">https://doi.org/10.1109/LICS56636.2023.10175771</a>.","apa":"Kretinsky, J., Meggendorfer, T., &#38; Weininger, M. (2023). Stopping criteria for value iteration on stochastic games with quantitative objectives. In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (Vol. 2023). Boston, MA, United States: Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LICS56636.2023.10175771\">https://doi.org/10.1109/LICS56636.2023.10175771</a>"},"doi":"10.1109/LICS56636.2023.10175771","_id":"13967","abstract":[{"text":"A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution.","lang":"eng"}],"external_id":{"isi":["001036707700042"],"arxiv":["2304.09930"]},"publication_status":"published","date_published":"2023-07-01T00:00:00Z","publisher":"Institute of Electrical and Electronics Engineers","volume":2023,"quality_controlled":"1","department":[{"_id":"KrCh"}],"isi":1,"scopus_import":"1","intvolume":"      2023","article_processing_charge":"No","date_updated":"2023-12-13T12:06:10Z","oa":1,"title":"Stopping criteria for value iteration on stochastic games with quantitative objectives","publication":"38th Annual ACM/IEEE Symposium on Logic in Computer Science","language":[{"iso":"eng"}],"month":"07","publication_identifier":{"isbn":["9798350335873"],"issn":["1043-6871"]},"conference":{"name":"LICS: Symposium on Logic in Computer Science","start_date":"2023-06-26","location":"Boston, MA, United States","end_date":"2023-06-29"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2304.09930","open_access":"1"}],"oa_version":"Preprint","day":"01","arxiv":1,"author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","full_name":"Kretinsky, Jan"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger","full_name":"Weininger, Maximilian","first_name":"Maximilian"}],"type":"conference","status":"public"},{"conference":{"start_date":"2023-02-07","name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14","location":"Washington, DC, United States"},"month":"06","publication_identifier":{"isbn":["9781577358800"]},"oa_version":"Preprint","day":"26","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2211.16187","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Mathias","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","orcid":"0000-0002-4681-1699","first_name":"Dorde","full_name":"Zikelic, Dorde"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Rus","full_name":"Rus, Daniela","first_name":"Daniela"}],"arxiv":1,"status":"public","type":"conference","intvolume":"        37","scopus_import":"1","oa":1,"date_updated":"2025-07-14T09:09:56Z","article_processing_charge":"No","issue":"12","title":"Quantization-aware interval bound propagation for training certifiably robust quantized neural networks","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","language":[{"iso":"eng"}],"external_id":{"arxiv":["2211.16187"]},"abstract":[{"lang":"eng","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."}],"publication_status":"published","publisher":"Association for the Advancement of Artificial Intelligence","date_published":"2023-06-26T00:00:00Z","page":"14964-14973","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"volume":37,"quality_controlled":"1","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","call_identifier":"H2020"}],"ec_funded":1,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. 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.","year":"2023","date_created":"2023-08-27T22:01:17Z","citation":{"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>.","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>.","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.","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.","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.","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>","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>"},"doi":"10.1609/aaai.v37i12.26747","_id":"14242"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"27","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1609/aaai.v37i5.25679"}],"oa_version":"Published Version","publication_identifier":{"isbn":["9781577358800"]},"month":"06","conference":{"start_date":"2023-02-07","name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14","location":"Washington, DC, United States"},"arxiv":1,"author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287","first_name":"Guy","full_name":"Avni, Guy"},{"first_name":"Ismael R","full_name":"Jecker, Ismael R","last_name":"Jecker","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425"},{"full_name":"Zikelic, Dorde","first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","status":"public","intvolume":"        37","scopus_import":"1","title":"Bidding graph games with partially-observable budgets","issue":"5","article_processing_charge":"No","oa":1,"date_updated":"2025-07-14T09:09:56Z","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Two-player zero-sum \"graph games\" are central in logic, verification, and multi-agent systems. The game proceeds by placing a token on a vertex of a graph, and allowing the players to move it to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In \"bidding games\", however, the players have budgets and in each turn, an auction (bidding) determines which player moves the token. So far, bidding games have only been studied as full-information games. In this work we initiate the study of partial-information bidding games: we study bidding games in which a player's initial budget is drawn from a known probability distribution. We show that while for some bidding mechanisms and objectives, it is straightforward to adapt the results from the full-information setting to the partial-information setting, for others, the analysis is significantly more challenging, requires new techniques, and gives rise to interesting results. Specifically, we study games with \"mean-payoff\" objectives in combination with \"poorman\" bidding. We construct optimal strategies for a partially-informed player who plays against a fully-informed adversary. We show that, somewhat surprisingly, the \"value\" under pure strategies does not necessarily exist in such games."}],"external_id":{"arxiv":["2211.13626"]},"publication_status":"published","quality_controlled":"1","volume":37,"page":"5464-5471","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_published":"2023-06-27T00:00:00Z","project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","call_identifier":"H2020","name":"International IST Doctoral Program"}],"ec_funded":1,"citation":{"apa":"Avni, G., Jecker, I. R., &#38; Zikelic, D. (2023). Bidding graph games with partially-observable budgets. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 5464–5471). Washington, DC, United States. <a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">https://doi.org/10.1609/aaai.v37i5.25679</a>","ista":"Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 5464–5471.","chicago":"Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with Partially-Observable Budgets.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:5464–71, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">https://doi.org/10.1609/aaai.v37i5.25679</a>.","mla":"Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 5, 2023, pp. 5464–71, doi:<a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">10.1609/aaai.v37i5.25679</a>.","short":"G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, 2023, pp. 5464–5471.","ama":"Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable budgets. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. ; 2023:5464-5471. doi:<a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">10.1609/aaai.v37i5.25679</a>","ieee":"G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable budgets,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471."},"date_created":"2023-08-27T22:01:18Z","year":"2023","acknowledgement":"This research was supported in part by ISF grant no.1679/21, 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.","doi":"10.1609/aaai.v37i5.25679","_id":"14243"},{"alternative_title":["LNCS"],"status":"public","type":"conference","oa_version":"Published Version","day":"17","file":[{"success":1,"file_id":"14276","file_name":"2023_LNCS_CAV_Kretinsky.pdf","checksum":"ed66278b61bb869e1baba3d9b9081271","date_created":"2023-09-06T08:25:50Z","date_updated":"2023-09-06T08:25:50Z","creator":"dernst","file_size":428354,"content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CAV: Computer Aided Verification","start_date":"2023-07-17","location":"Paris, France","end_date":"2023-07-22"},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031377051"]},"month":"07","author":[{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias"},{"last_name":"Prokop","first_name":"Maximilian","full_name":"Prokop, Maximilian"},{"full_name":"Rieder, Sabine","first_name":"Sabine","last_name":"Rieder"}],"publication":"35th International Conference on Computer Aided Verification ","language":[{"iso":"eng"}],"has_accepted_license":"1","scopus_import":"1","intvolume":"     13964","title":"Guessing winning policies in LTL synthesis by semantic learning","date_updated":"2023-09-06T08:27:33Z","oa":1,"article_processing_charge":"Yes (in subscription journal)","department":[{"_id":"KrCh"}],"page":"390-414","volume":13964,"quality_controlled":"1","publisher":"Springer Nature","date_published":"2023-07-17T00:00:00Z","abstract":[{"text":"We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.","lang":"eng"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publication_status":"published","doi":"10.1007/978-3-031-37706-8_20","file_date_updated":"2023-09-06T08:25:50Z","_id":"14259","date_created":"2023-09-03T22:01:16Z","citation":{"mla":"Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” <i>35th International Conference on Computer Aided Verification </i>, vol. 13964, Springer Nature, 2023, pp. 390–414, doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">10.1007/978-3-031-37706-8_20</a>.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In <i>35th International Conference on Computer Aided Verification </i>, 13964:390–414. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">https://doi.org/10.1007/978-3-031-37706-8_20</a>.","ista":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies in LTL synthesis by semantic learning. 35th International Conference on Computer Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.","ieee":"J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning policies in LTL synthesis by semantic learning,” in <i>35th International Conference on Computer Aided Verification </i>, Paris, France, 2023, vol. 13964, pp. 390–414.","ama":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies in LTL synthesis by semantic learning. In: <i>35th International Conference on Computer Aided Verification </i>. Vol 13964. Springer Nature; 2023:390-414. doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">10.1007/978-3-031-37706-8_20</a>","short":"J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.","apa":"Kretinsky, J., Meggendorfer, T., Prokop, M., &#38; Rieder, S. (2023). Guessing winning policies in LTL synthesis by semantic learning. In <i>35th International Conference on Computer Aided Verification </i> (Vol. 13964, pp. 390–414). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">https://doi.org/10.1007/978-3-031-37706-8_20</a>"},"acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).","year":"2023"},{"doi":"10.1007/978-3-031-37709-9_5","file_date_updated":"2023-09-20T08:46:43Z","_id":"14317","ec_funded":1,"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.","year":"2023","citation":{"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.","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>.","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>.","short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 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>","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."},"date_created":"2023-09-10T22:01:12Z","publisher":"Springer Nature","date_published":"2023-07-17T00:00:00Z","page":"86-112","department":[{"_id":"KrCh"}],"volume":13966,"quality_controlled":"1","project":[{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"abstract":[{"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.","lang":"eng"}],"publication_status":"published","publication":"International Conference on Computer Aided Verification","language":[{"iso":"eng"}],"has_accepted_license":"1","intvolume":"     13966","scopus_import":"1","date_updated":"2025-07-14T09:09:56Z","oa":1,"article_processing_charge":"Yes (in subscription journal)","title":"MDPs as distribution transformers: Affine invariant synthesis for safety objectives","alternative_title":["LNCS"],"type":"conference","status":"public","conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","end_date":"2023-07-22","location":"Paris, France"},"month":"07","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031377082"],"eissn":["1611-3349"]},"oa_version":"Published Version","day":"17","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"dernst","access_level":"open_access","content_type":"application/pdf","file_size":531745,"relation":"main_file","file_id":"14349","checksum":"f143c8eedf609f20f2aad2eeb496d53f","file_name":"2023_LNCS_Akshay.pdf","success":1,"date_updated":"2023-09-20T08:46:43Z","date_created":"2023-09-20T08:46:43Z"}],"author":[{"first_name":"S.","full_name":"Akshay, S.","last_name":"Akshay"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","orcid":"0000-0002-4681-1699","first_name":"Dorde","full_name":"Zikelic, Dorde"}]}]