[{"scopus_import":"1","quality_controlled":"1","date_published":"2023-07-01T00:00:00Z","author":[{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","first_name":"Tobias"},{"last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian"}],"article_processing_charge":"No","doi":"10.1109/LICS56636.2023.10175771","date_updated":"2023-12-13T12:06:10Z","conference":{"end_date":"2023-06-29","name":"LICS: Symposium on Logic in Computer Science","start_date":"2023-06-26","location":"Boston, MA, United States"},"month":"07","isi":1,"language":[{"iso":"eng"}],"day":"01","intvolume":"      2023","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2304.09930","open_access":"1"}],"publication_status":"published","abstract":[{"lang":"eng","text":"A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution."}],"arxiv":1,"date_created":"2023-08-06T22:01:10Z","oa_version":"Preprint","publication":"38th Annual ACM/IEEE Symposium on Logic in Computer Science","department":[{"_id":"KrCh"}],"title":"Stopping criteria for value iteration on stochastic games with quantitative objectives","publisher":"Institute of Electrical and Electronics Engineers","citation":{"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.","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>","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>","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.","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.","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>."},"publication_identifier":{"issn":["1043-6871"],"isbn":["9798350335873"]},"status":"public","oa":1,"acknowledgement":"This research was funded in part by DFG projects 383882557 “SUV” and 427755713 “GOPro”.","external_id":{"isi":["001036707700042"],"arxiv":["2304.09930"]},"_id":"13967","year":"2023","volume":2023,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference"},{"date_published":"2023-06-26T00:00:00Z","author":[{"last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Rus, Daniela","first_name":"Daniela","last_name":"Rus"}],"article_processing_charge":"No","doi":"10.1609/aaai.v37i12.26747","date_updated":"2025-07-14T09:09:56Z","scopus_import":"1","quality_controlled":"1","conference":{"location":"Washington, DC, United States","start_date":"2023-02-07","name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14"},"day":"26","month":"06","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020"}],"intvolume":"        37","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2211.16187"}],"publication_status":"published","arxiv":1,"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":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","title":"Quantization-aware interval bound propagation for training certifiably robust quantized neural networks","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Association for the Advancement of Artificial Intelligence","ec_funded":1,"date_created":"2023-08-27T22:01:17Z","oa_version":"Preprint","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.","status":"public","oa":1,"issue":"12","external_id":{"arxiv":["2211.16187"]},"citation":{"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>","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.","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>.","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.","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>.","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.","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>"},"publication_identifier":{"isbn":["9781577358800"]},"volume":37,"page":"14964-14973","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","_id":"14242","year":"2023"},{"status":"public","oa":1,"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.","issue":"5","external_id":{"arxiv":["2211.13626"]},"citation":{"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>","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.","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.","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.","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>.","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>"},"publication_identifier":{"isbn":["9781577358800"]},"volume":37,"page":"5464-5471","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","_id":"14243","year":"2023","arxiv":1,"abstract":[{"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.","lang":"eng"}],"publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","title":"Bidding graph games with partially-observable budgets","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_created":"2023-08-27T22:01:18Z","ec_funded":1,"oa_version":"Published Version","day":"27","month":"06","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"intvolume":"        37","main_file_link":[{"url":"https://doi.org/10.1609/aaai.v37i5.25679","open_access":"1"}],"publication_status":"published","author":[{"orcid":"0000-0001-5588-8287","last_name":"Avni","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy"},{"full_name":"Jecker, Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","first_name":"Ismael R","last_name":"Jecker"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699"}],"date_published":"2023-06-27T00:00:00Z","article_processing_charge":"No","date_updated":"2025-07-14T09:09:56Z","doi":"10.1609/aaai.v37i5.25679","scopus_import":"1","quality_controlled":"1","conference":{"location":"Washington, DC, United States","start_date":"2023-02-07","name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14"}},{"intvolume":"     13964","publication_status":"published","file":[{"access_level":"open_access","creator":"dernst","relation":"main_file","date_created":"2023-09-06T08:25:50Z","success":1,"content_type":"application/pdf","date_updated":"2023-09-06T08:25:50Z","file_id":"14276","checksum":"ed66278b61bb869e1baba3d9b9081271","file_name":"2023_LNCS_CAV_Kretinsky.pdf","file_size":428354}],"day":"17","ddc":["000"],"language":[{"iso":"eng"}],"month":"07","file_date_updated":"2023-09-06T08:25:50Z","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"conference":{"start_date":"2023-07-17","location":"Paris, France","end_date":"2023-07-22","name":"CAV: Computer Aided Verification"},"author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan"},{"full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165"},{"full_name":"Prokop, Maximilian","last_name":"Prokop","first_name":"Maximilian"},{"first_name":"Sabine","last_name":"Rieder","full_name":"Rieder, Sabine"}],"date_published":"2023-07-17T00:00:00Z","date_updated":"2023-09-06T08:27:33Z","doi":"10.1007/978-3-031-37706-8_20","alternative_title":["LNCS"],"article_processing_charge":"Yes (in subscription journal)","scopus_import":"1","quality_controlled":"1","page":"390-414","volume":13964,"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"14259","has_accepted_license":"1","year":"2023","status":"public","oa":1,"acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).","citation":{"short":"J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.","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.","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>.","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>","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>","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.","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>."},"publication_identifier":{"isbn":["9783031377051"],"issn":["0302-9743"],"eissn":["1611-3349"]},"department":[{"_id":"KrCh"}],"title":"Guessing winning policies in LTL synthesis by semantic learning","publication":"35th International Conference on Computer Aided Verification ","publisher":"Springer Nature","oa_version":"Published Version","date_created":"2023-09-03T22:01:16Z","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"}]},{"oa":1,"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant.","status":"public","publication_identifier":{"isbn":["9781611977554"]},"citation":{"chicago":"Chatterjee, Krishnendu, Tobias Meggendorfer, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Faster Algorithm for Turn-Based Stochastic Games with Bounded Treewidth.” In <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i>, 4590–4605. Society for Industrial and Applied Mathematics, 2023. <a href=\"https://doi.org/10.1137/1.9781611977554.ch173\">https://doi.org/10.1137/1.9781611977554.ch173</a>.","ieee":"K. Chatterjee, T. Meggendorfer, R. J. Saona Urmeneta, and J. Svoboda, “Faster algorithm for turn-based stochastic games with bounded treewidth,” in <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i>, Florence, Italy, 2023, pp. 4590–4605.","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>","ama":"Chatterjee K, Meggendorfer T, Saona Urmeneta RJ, Svoboda J. Faster algorithm for turn-based stochastic games with bounded treewidth. In: <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i>. Society for Industrial and Applied Mathematics; 2023:4590-4605. doi:<a href=\"https://doi.org/10.1137/1.9781611977554.ch173\">10.1137/1.9781611977554.ch173</a>","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithm for Turn-Based Stochastic Games with Bounded Treewidth.” <i>Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms</i>, Society for Industrial and Applied Mathematics, 2023, pp. 4590–605, doi:<a href=\"https://doi.org/10.1137/1.9781611977554.ch173\">10.1137/1.9781611977554.ch173</a>.","short":"K. Chatterjee, T. Meggendorfer, R.J. Saona Urmeneta, J. Svoboda, in:, Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial and Applied Mathematics, 2023, pp. 4590–4605.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","page":"4590-4605","year":"2023","_id":"12676","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"}],"publisher":"Society for Industrial and Applied Mathematics","publication":"Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms","title":"Faster algorithm for turn-based stochastic games with bounded treewidth","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"ec_funded":1,"date_created":"2023-02-24T12:20:47Z","oa_version":"Published Version","day":"01","month":"02","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"language":[{"iso":"eng"}],"publication_status":"published","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1137/1.9781611977554.ch173"}],"article_processing_charge":"No","doi":"10.1137/1.9781611977554.ch173","date_updated":"2025-07-14T09:09:50Z","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165"},{"first_name":"Raimundo J","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"orcid":"0000-0002-1419-3267","last_name":"Svoboda","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub"}],"date_published":"2023-02-01T00:00:00Z","quality_controlled":"1","conference":{"end_date":"2023-01-25","name":"SODA: Symposium on Discrete Algorithms","start_date":"2023-01-22","location":"Florence, Italy"}},{"author":[{"full_name":"Mckerral, Jody C.","first_name":"Jody C.","last_name":"Mckerral"},{"id":"4E21749C-F248-11E8-B48F-1D18A9856A87","full_name":"Kleshnina, Maria","last_name":"Kleshnina","first_name":"Maria"},{"full_name":"Ejov, Vladimir","last_name":"Ejov","first_name":"Vladimir"},{"full_name":"Bartle, Louise","last_name":"Bartle","first_name":"Louise"},{"first_name":"James G.","last_name":"Mitchell","full_name":"Mitchell, James G."},{"last_name":"Filar","first_name":"Jerzy A.","full_name":"Filar, Jerzy A."}],"date_published":"2023-02-27T00:00:00Z","article_processing_charge":"No","date_updated":"2023-10-17T12:53:30Z","doi":"10.1371/journal.pone.0279838","scopus_import":"1","quality_controlled":"1","file_date_updated":"2023-03-07T10:26:45Z","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"pmid":1,"ddc":["000"],"day":"27","isi":1,"month":"02","language":[{"iso":"eng"}],"intvolume":"        18","file":[{"access_level":"open_access","creator":"cchlebak","relation":"main_file","date_created":"2023-03-07T10:26:45Z","success":1,"content_type":"application/pdf","file_id":"12712","date_updated":"2023-03-07T10:26:45Z","checksum":"798ed5739a4117b03173e5d56e0534c9","file_name":"2023_PLOSOne_Mckerral.pdf","file_size":1257003}],"publication_status":"published","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."}],"publication":"PLoS One","title":"Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations","department":[{"_id":"KrCh"}],"publisher":"Public Library of Science","date_created":"2023-03-05T23:01:05Z","oa_version":"Published Version","oa":1,"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.","status":"public","issue":"2","article_type":"original","external_id":{"pmid":["36848357"],"isi":["000996122900022"]},"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.","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>","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.","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>.","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."},"publication_identifier":{"eissn":["1932-6203"]},"volume":18,"page":"e0279838","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","_id":"12706","year":"2023","has_accepted_license":"1"},{"publisher":"Springer Nature","publication":"Formal Methods in System Design","title":"Stochastic games with lexicographic objectives","department":[{"_id":"KrCh"}],"ec_funded":1,"date_created":"2023-03-19T23:00:59Z","oa_version":"Published Version","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"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","year":"2023","_id":"12738","article_type":"original","external_id":{"isi":["000946174300001"]},"oa":1,"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.","status":"public","publication_identifier":{"eissn":["1572-8102"]},"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>.","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.","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>","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>","short":"K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods in System Design (2023).","ista":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2023. Stochastic games with lexicographic objectives. Formal Methods in System Design.","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>."},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"article_processing_charge":"No","date_updated":"2025-07-14T09:10:14Z","doi":"10.1007/s10703-023-00411-4","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"8272"}]},"date_published":"2023-03-08T00:00:00Z","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Katoen","first_name":"Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P"},{"full_name":"Mohr, Stefanie","first_name":"Stefanie","last_name":"Mohr"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian"},{"last_name":"Winkler","first_name":"Tobias","full_name":"Winkler, Tobias"}],"quality_controlled":"1","scopus_import":"1","publication_status":"epub_ahead","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/s10703-023-00411-4"}],"ddc":["000"],"day":"08","month":"03","isi":1,"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}]},{"publication_status":"published","file":[{"file_size":827784,"file_name":"2023_ProceedingsRoyalSocietyA_Svoboda.pdf","checksum":"13953d349fbefcb5d21ccc6b303297eb","file_id":"12796","date_updated":"2023-04-03T06:25:29Z","content_type":"application/pdf","success":1,"date_created":"2023-04-03T06:25:29Z","relation":"main_file","access_level":"open_access","creator":"dernst"}],"intvolume":"       479","language":[{"iso":"eng"}],"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"month":"03","isi":1,"day":"29","ddc":["000"],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"article_number":"20220685","file_date_updated":"2023-04-03T06:25:29Z","quality_controlled":"1","scopus_import":"1","related_material":{"link":[{"relation":"research_data","url":"https://doi.org/10.6084/m9.figshare.21261771.v1"}]},"doi":"10.1098/rspa.2022.0685","date_updated":"2025-07-14T09:09:51Z","article_processing_charge":"No","date_published":"2023-03-29T00:00:00Z","author":[{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","first_name":"Josef"},{"full_name":"Kaveh, Kamran","last_name":"Kaveh","first_name":"Kamran"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"}],"year":"2023","has_accepted_license":"1","_id":"12787","type":"journal_article","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","volume":479,"publication_identifier":{"issn":["1364-5021"],"eissn":["1471-2946"]},"citation":{"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.","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>.","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>","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>","short":"J. Svoboda, J. Tkadlec, K. Kaveh, K. Chatterjee, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 479 (2023).","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.","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>."},"external_id":{"isi":["000957125500002"]},"article_type":"original","issue":"2271","oa":1,"status":"public","acknowledgement":"J.S. and K.C. acknowledge support from the ERC CoG 863818 (ForM-SMArt)","oa_version":"Published Version","ec_funded":1,"date_created":"2023-04-02T22:01:09Z","publisher":"The Royal Society","department":[{"_id":"KrCh"}],"title":"Coexistence times in the Moran process with environmental heterogeneity","publication":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","abstract":[{"lang":"eng","text":"Populations evolve in spatially heterogeneous environments. While a certain trait might bring a fitness advantage in some patch of the environment, a different trait might be advantageous in another patch. Here, we study the Moran birth–death process with two types of individuals in a population stretched across two patches of size N, each patch favouring one of the two types. We show that the long-term fate of such populations crucially depends on the migration rate μ\r\n between the patches. To classify the possible fates, we use the distinction between polynomial (short) and exponential (long) timescales. We show that when μ is high then one of the two types fixates on the whole population after a number of steps that is only polynomial in N. By contrast, when μ is low then each type holds majority in the patch where it is favoured for a number of steps that is at least exponential in N. Moreover, we precisely identify the threshold migration rate μ⋆ that separates those two scenarios, thereby exactly delineating the situations that support long-term coexistence of the two types. We also discuss the case of various cycle graphs and we present computer simulations that perfectly match our analytical results."}]},{"quality_controlled":"1","scopus_import":"1","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"7950"}]},"doi":"10.46298/DMTCS.8383","date_updated":"2024-01-04T12:42:09Z","article_processing_charge":"No","date_published":"2023-01-18T00:00:00Z","author":[{"full_name":"Biniaz, Ahmad","last_name":"Biniaz","first_name":"Ahmad"},{"last_name":"Jain","first_name":"Kshitij","full_name":"Jain, Kshitij"},{"full_name":"Lubiw, Anna","first_name":"Anna","last_name":"Lubiw"},{"id":"45CFE238-F248-11E8-B48F-1D18A9856A87","full_name":"Masárová, Zuzana","last_name":"Masárová","orcid":"0000-0002-6660-1322","first_name":"Zuzana"},{"full_name":"Miltzow, Tillmann","first_name":"Tillmann","last_name":"Miltzow"},{"full_name":"Mondal, Debajyoti","first_name":"Debajyoti","last_name":"Mondal"},{"full_name":"Naredla, Anurag Murty","last_name":"Naredla","first_name":"Anurag Murty"},{"last_name":"Tkadlec","orcid":"0000-0002-1097-9684","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef"},{"first_name":"Alexi","last_name":"Turcotte","full_name":"Turcotte, Alexi"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"article_number":"9","file_date_updated":"2023-04-17T08:10:28Z","language":[{"iso":"eng"}],"month":"01","day":"18","ddc":["000"],"publication_status":"published","file":[{"date_updated":"2023-04-17T08:10:28Z","file_id":"12844","file_name":"2022_DMTCS_Biniaz.pdf","checksum":"439102ea4f6e2aeefd7107dfb9ccf532","file_size":2072197,"access_level":"open_access","creator":"dernst","relation":"main_file","success":1,"date_created":"2023-04-17T08:10:28Z","content_type":"application/pdf"}],"intvolume":"        24","abstract":[{"lang":"eng","text":"The input to the token swapping problem is a graph with vertices v1, v2, . . . , vn, and n tokens with labels 1,2, . . . , n, one on each vertex. The goal is to get token i to vertex vi for all i= 1, . . . , n using a minimum number of swaps, where a swap exchanges the tokens on the endpoints of an edge.Token swapping on a tree, also known as “sorting with a transposition tree,” is not known to be in P nor NP-complete. We present some partial results: 1. An optimum swap sequence may need to perform a swap on a leaf vertex that has the correct token (a “happy leaf”), disproving a conjecture of Vaughan. 2. Any algorithm that fixes happy leaves—as all known approximation algorithms for the problem do—has approximation factor at least 4/3. Furthermore, the two best-known 2-approximation algorithms have approximation factor exactly 2. 3. A generalized problem—weighted coloured token swapping—is NP-complete on trees, but solvable in polynomial time on paths and stars. In this version, tokens and vertices have colours, and colours have weights. The goal is to get every token to a vertex of the same colour, and the cost of a swap is the sum of the weights of the two tokens involved."}],"arxiv":1,"oa_version":"Published Version","date_created":"2023-04-16T22:01:08Z","publisher":"EPI Sciences","title":"Token swapping on trees","department":[{"_id":"KrCh"},{"_id":"HeEd"},{"_id":"UlWa"}],"publication":"Discrete Mathematics and Theoretical Computer Science","publication_identifier":{"issn":["1462-7264"],"eissn":["1365-8050"]},"citation":{"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.","chicago":"Biniaz, Ahmad, Kshitij Jain, Anna Lubiw, Zuzana Masárová, Tillmann Miltzow, Debajyoti Mondal, Anurag Murty Naredla, Josef Tkadlec, and Alexi Turcotte. “Token Swapping on Trees.” <i>Discrete Mathematics and Theoretical Computer Science</i>. EPI Sciences, 2023. <a href=\"https://doi.org/10.46298/DMTCS.8383\">https://doi.org/10.46298/DMTCS.8383</a>.","apa":"Biniaz, A., Jain, K., Lubiw, A., Masárová, Z., Miltzow, T., Mondal, D., … Turcotte, A. (2023). Token swapping on trees. <i>Discrete Mathematics and Theoretical Computer Science</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/DMTCS.8383\">https://doi.org/10.46298/DMTCS.8383</a>","ama":"Biniaz A, Jain K, Lubiw A, et al. Token swapping on trees. <i>Discrete Mathematics and Theoretical Computer Science</i>. 2023;24(2). doi:<a href=\"https://doi.org/10.46298/DMTCS.8383\">10.46298/DMTCS.8383</a>","ista":"Biniaz A, Jain K, Lubiw A, Masárová Z, Miltzow T, Mondal D, Naredla AM, Tkadlec J, Turcotte A. 2023. Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. 24(2), 9.","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>."},"external_id":{"arxiv":["1903.06981"]},"article_type":"original","issue":"2","oa":1,"status":"public","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","has_accepted_license":"1","year":"2023","_id":"12833","type":"journal_article","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","volume":24},{"pmid":1,"day":"12","ddc":["000"],"language":[{"iso":"eng"}],"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"}],"month":"04","isi":1,"intvolume":"        14","publication_status":"published","file":[{"date_updated":"2023-04-25T09:13:53Z","file_id":"12868","file_size":1786475,"checksum":"a4b3b7b36fbef068cabf4fb99501fef6","file_name":"2023_NatureComm_Schmid.pdf","relation":"main_file","access_level":"open_access","creator":"dernst","content_type":"application/pdf","date_created":"2023-04-25T09:13:53Z","success":1}],"author":[{"id":"38B437DE-F248-11E8-B48F-1D18A9856A87","full_name":"Schmid, Laura","last_name":"Schmid","orcid":"0000-0002-6978-7329","first_name":"Laura"},{"full_name":"Ekbatani, Farbod","last_name":"Ekbatani","first_name":"Farbod"},{"first_name":"Christian","last_name":"Hilbe","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"}],"date_published":"2023-04-12T00:00:00Z","date_updated":"2025-07-14T09:09:52Z","doi":"10.1038/s41467-023-37817-x","article_processing_charge":"No","scopus_import":"1","quality_controlled":"1","file_date_updated":"2023-04-25T09:13:53Z","article_number":"2086","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","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.","oa":1,"external_id":{"isi":["001003644100020"],"pmid":["37045828"]},"article_type":"original","citation":{"short":"L. Schmid, F. Ekbatani, C. Hilbe, K. Chatterjee, Nature Communications 14 (2023).","mla":"Schmid, Laura, et al. “Quantitative Assessment Can Stabilize Indirect Reciprocity under Imperfect Information.” <i>Nature Communications</i>, vol. 14, 2086, Springer Nature, 2023, doi:<a href=\"https://doi.org/10.1038/s41467-023-37817-x\">10.1038/s41467-023-37817-x</a>.","ista":"Schmid L, Ekbatani F, Hilbe C, Chatterjee K. 2023. Quantitative assessment can stabilize indirect reciprocity under imperfect information. Nature Communications. 14, 2086.","ama":"Schmid L, Ekbatani F, Hilbe C, Chatterjee K. Quantitative assessment can stabilize indirect reciprocity under imperfect information. <i>Nature Communications</i>. 2023;14. doi:<a href=\"https://doi.org/10.1038/s41467-023-37817-x\">10.1038/s41467-023-37817-x</a>","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>","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."},"publication_identifier":{"eissn":["2041-1723"]},"volume":14,"type":"journal_article","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"12861","year":"2023","has_accepted_license":"1","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."}],"department":[{"_id":"KrCh"}],"title":"Quantitative assessment can stabilize indirect reciprocity under imperfect information","publication":"Nature Communications","publisher":"Springer Nature","oa_version":"Published Version","ec_funded":1,"date_created":"2023-04-23T22:01:03Z"},{"publication_identifier":{"eissn":["2045-2322"]},"citation":{"ista":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2022. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 12(1), 1526.","short":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Scientific Reports 12 (2022).","mla":"Svoboda, Jakub, et al. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” <i>Scientific Reports</i>, vol. 12, no. 1, 1526, Springer Nature, 2022, doi:<a href=\"https://doi.org/10.1038/s41598-022-05333-5\">10.1038/s41598-022-05333-5</a>.","ama":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Infection dynamics of COVID-19 virus under lockdown and reopening. <i>Scientific Reports</i>. 2022;12(1). doi:<a href=\"https://doi.org/10.1038/s41598-022-05333-5\">10.1038/s41598-022-05333-5</a>","apa":"Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening. <i>Scientific Reports</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41598-022-05333-5\">https://doi.org/10.1038/s41598-022-05333-5</a>","ieee":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Infection dynamics of COVID-19 virus under lockdown and reopening,” <i>Scientific Reports</i>, vol. 12, no. 1. Springer Nature, 2022.","chicago":"Svoboda, Jakub, Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” <i>Scientific Reports</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1038/s41598-022-05333-5\">https://doi.org/10.1038/s41598-022-05333-5</a>."},"issue":"1","external_id":{"isi":["000749198000039"],"arxiv":["2012.15155"]},"article_type":"original","oa":1,"status":"public","acknowledgement":"K.C. acknowledges support from ERC Consolidator Grant No. (863818: ForM-SMart). A.P. acknowledges support from FWF Grant No. J-4220. M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.","has_accepted_license":"1","year":"2022","_id":"10731","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","type":"journal_article","volume":12,"abstract":[{"lang":"eng","text":"Motivated by COVID-19, we develop and analyze a simple stochastic model for the spread of disease in human population. We track how the number of infected and critically ill people develops over time in order to estimate the demand that is imposed on the hospital system. To keep this demand under control, we consider a class of simple policies for slowing down and reopening society and we compare their efficiency in mitigating the spread of the virus from several different points of view. We find that in order to avoid overwhelming of the hospital system, a policy must impose a harsh lockdown or it must react swiftly (or both). While reacting swiftly is universally beneficial, being harsh pays off only when the country is patient about reopening and when the neighboring countries coordinate their mitigation efforts. Our work highlights the importance of acting decisively when closing down and the importance of patience and coordination between neighboring countries when reopening."}],"arxiv":1,"ec_funded":1,"date_created":"2022-02-06T23:01:30Z","oa_version":"Published Version","publisher":"Springer Nature","publication":"Scientific Reports","title":"Infection dynamics of COVID-19 virus under lockdown and reopening","department":[{"_id":"KrCh"}],"isi":1,"month":"01","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"ddc":["570"],"day":"27","file":[{"content_type":"application/pdf","date_created":"2022-02-07T14:57:59Z","success":1,"relation":"main_file","access_level":"open_access","creator":"alisjak","file_size":2971922,"checksum":"247afd30c173390940f099ead35a28ed","file_name":"2022_ScientificReports_Svoboda.pdf","file_id":"10744","date_updated":"2022-02-07T14:57:59Z"}],"publication_status":"published","intvolume":"        12","quality_controlled":"1","scopus_import":"1","article_processing_charge":"No","doi":"10.1038/s41598-022-05333-5","date_updated":"2025-07-14T09:10:12Z","author":[{"first_name":"Jakub","orcid":"0000-0002-1419-3267","last_name":"Svoboda","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"},{"full_name":"Tkadlec, Josef","last_name":"Tkadlec","first_name":"Josef"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"date_published":"2022-01-27T00:00:00Z","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"article_number":"1526","file_date_updated":"2022-02-07T14:57:59Z"},{"quality_controlled":"1","scopus_import":"1","doi":"10.1016/j.jcss.2022.04.003","date_updated":"2025-07-14T09:09:54Z","related_material":{"record":[{"id":"7402","status":"public","relation":"earlier_version"}]},"article_processing_charge":"No","date_published":"2022-11-01T00:00:00Z","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"}],"language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"month":"11","isi":1,"day":"01","publication_status":"published","intvolume":"       129","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.1802.03642"}],"abstract":[{"text":"Fixed-horizon planning considers a weighted graph and asks to construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping-time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary as the worst-case scenario. A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon or fixed stopping-time distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping-time distribution with expected stopping-time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping-time distribution can be achieved in polynomial time.","lang":"eng"}],"arxiv":1,"oa_version":"Preprint","date_created":"2022-05-22T22:01:40Z","ec_funded":1,"publisher":"Elsevier","title":"Graph planning with expected finite horizon","department":[{"_id":"KrCh"}],"publication":"Journal of Computer and System Sciences","publication_identifier":{"issn":["0022-0000"],"eissn":["1090-2724"]},"citation":{"ama":"Chatterjee K, Doyen L. Graph planning with expected finite horizon. <i>Journal of Computer and System Sciences</i>. 2022;129:1-21. doi:<a href=\"https://doi.org/10.1016/j.jcss.2022.04.003\">10.1016/j.jcss.2022.04.003</a>","ista":"Chatterjee K, Doyen L. 2022. Graph planning with expected finite horizon. Journal of Computer and System Sciences. 129, 1–21.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Graph Planning with Expected Finite Horizon.” <i>Journal of Computer and System Sciences</i>, vol. 129, Elsevier, 2022, pp. 1–21, doi:<a href=\"https://doi.org/10.1016/j.jcss.2022.04.003\">10.1016/j.jcss.2022.04.003</a>.","short":"K. Chatterjee, L. Doyen, Journal of Computer and System Sciences 129 (2022) 1–21.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Graph Planning with Expected Finite Horizon.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2022. <a href=\"https://doi.org/10.1016/j.jcss.2022.04.003\">https://doi.org/10.1016/j.jcss.2022.04.003</a>.","ieee":"K. Chatterjee and L. Doyen, “Graph planning with expected finite horizon,” <i>Journal of Computer and System Sciences</i>, vol. 129. Elsevier, pp. 1–21, 2022.","apa":"Chatterjee, K., &#38; Doyen, L. (2022). Graph planning with expected finite horizon. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2022.04.003\">https://doi.org/10.1016/j.jcss.2022.04.003</a>"},"article_type":"original","external_id":{"arxiv":["1802.03642"],"isi":["000805002800001"]},"acknowledgement":"This work was partially supported by Austrian Science Fund (FWF) NFN Grant No RiSE/SHiNE S11407 and by the grant ERC CoG 863818 (ForM-SMArt).","oa":1,"status":"public","year":"2022","_id":"11402","type":"journal_article","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","page":"1-21","volume":129},{"oa_version":"Published Version","date_created":"2022-06-21T09:26:15Z","ec_funded":1,"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"title":"Differential cost analysis with simultaneous potentials and anti-potentials","publication":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","publisher":"Association for Computing Machinery","abstract":[{"lang":"eng","text":"We present a novel approach to differential cost analysis that, given a program revision, attempts to statically bound the difference in resource usage, or cost, between the two program versions. Differential cost analysis is particularly interesting because of the many compelling applications for it, such as detecting resource-use regressions at code-review time or proving the absence of certain side-channel vulnerabilities. One prior approach to differential cost analysis is to apply relational reasoning that conceptually constructs a product program on which one can over-approximate the difference in costs between the two program versions. However, a significant challenge in any relational approach is effectively aligning the program versions to get precise results. In this paper, our key insight is that we can avoid the need for and the limitations of program alignment if, instead, we bound the difference of two cost-bound summaries rather than directly bounding the concrete cost difference. In particular, our method computes a threshold value for the maximal difference in cost between two program versions simultaneously using two kinds of cost-bound summaries---a potential function that evaluates to an upper bound for the cost incurred in the first program and an anti-potential function that evaluates to a lower bound for the cost incurred in the second. Our method has a number of desirable properties: it can be fully automated, it allows optimizing the threshold value on relative cost, it is suitable for programs that are not syntactically similar, and it supports non-determinism. We have evaluated an implementation of our approach on a number of program pairs collected from the literature, and we find that our method computes tight threshold values on relative cost in most examples."}],"arxiv":1,"_id":"11459","has_accepted_license":"1","year":"2022","page":"442-457","type":"conference","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ista":"Zikelic D, Chang B-YE, Bolignano P, Raimondi F. 2022. Differential cost analysis with simultaneous potentials and anti-potentials. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 442–457.","short":"D. Zikelic, B.-Y.E. Chang, P. Bolignano, F. Raimondi, in:, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 442–457.","mla":"Zikelic, Dorde, et al. “Differential Cost Analysis with Simultaneous Potentials and Anti-Potentials.” <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2022, pp. 442–57, doi:<a href=\"https://doi.org/10.1145/3519939.3523435\">10.1145/3519939.3523435</a>.","ama":"Zikelic D, Chang B-YE, Bolignano P, Raimondi F. Differential cost analysis with simultaneous potentials and anti-potentials. In: <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2022:442-457. doi:<a href=\"https://doi.org/10.1145/3519939.3523435\">10.1145/3519939.3523435</a>","apa":"Zikelic, D., Chang, B.-Y. E., Bolignano, P., &#38; Raimondi, F. (2022). Differential cost analysis with simultaneous potentials and anti-potentials. In <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 442–457). San Diego, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3519939.3523435\">https://doi.org/10.1145/3519939.3523435</a>","chicago":"Zikelic, Dorde, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi. “Differential Cost Analysis with Simultaneous Potentials and Anti-Potentials.” In <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 442–57. Association for Computing Machinery, 2022. <a href=\"https://doi.org/10.1145/3519939.3523435\">https://doi.org/10.1145/3519939.3523435</a>.","ieee":"D. Zikelic, B.-Y. E. Chang, P. Bolignano, and F. Raimondi, “Differential cost analysis with simultaneous potentials and anti-potentials,” in <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, San Diego, CA, United States, 2022, pp. 442–457."},"publication_identifier":{"isbn":["9781450392655"]},"acknowledgement":"We thank Shaun Willows, Thomas Lugnet, and the Living Room Application Vending team for suggesting threshold\r\nbounds as a developer-friendly way to interact with a differential cost analyzer, and we thank Jim Christy, Daniel\r\nSchoepe, and the Prime Video Automated Reasoning team for their support and helpful suggestions throughout the\r\nproject. We also thank Michael Emmi for feedback on an earlier version of this paper. And finally, we thank the anonymous reviewers for their useful feedback and Aws Albarghouthi for shepherding the final version of the paper. Ðorđe Žikelić was also partially supported by ERC CoG 863818 (FoRM-SMArt).","oa":1,"status":"public","external_id":{"arxiv":["2204.00870"],"isi":["000850435600030"]},"tmp":{"short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"conference":{"location":"San Diego, CA, United States","start_date":"2022-06-13","name":"PLDI: Programming Language Design and Implementation","end_date":"2022-06-17"},"file_date_updated":"2022-06-27T07:38:21Z","scopus_import":"1","quality_controlled":"1","author":[{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde"},{"first_name":"Bor-Yuh Evan","last_name":"Chang","full_name":"Chang, Bor-Yuh Evan"},{"first_name":"Pauline","last_name":"Bolignano","full_name":"Bolignano, Pauline"},{"full_name":"Raimondi, Franco","last_name":"Raimondi","first_name":"Franco"}],"date_published":"2022-06-09T00:00:00Z","date_updated":"2025-07-14T09:09:54Z","doi":"10.1145/3519939.3523435","article_processing_charge":"No","publication_status":"published","file":[{"checksum":"7eb915a2ca5b5ce4729321f33b2e16e1","file_name":"2022_PLDI_Zikelic.pdf","file_size":318697,"file_id":"11466","date_updated":"2022-06-27T07:38:21Z","date_created":"2022-06-27T07:38:21Z","success":1,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","relation":"main_file"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"language":[{"iso":"eng"}],"month":"06","isi":1,"day":"09","ddc":["000"]},{"type":"preprint","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publication_status":"submitted","year":"2022","main_file_link":[{"url":"https://arxiv.org/abs/2210.05308","open_access":"1"}],"_id":"14600","external_id":{"arxiv":["2210.05308"]},"day":"29","oa":1,"status":"public","language":[{"iso":"eng"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","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","call_identifier":"H2020"},{"call_identifier":"H2020","name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"month":"11","citation":{"apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (n.d.). Learning control policies for stochastic systems with reach-avoid guarantees. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">https://doi.org/10.48550/ARXIV.2210.05308</a>","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” <i>arXiv</i>. .","chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">https://doi.org/10.48550/ARXIV.2210.05308</a>.","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, ArXiv (n.d.).","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. arXiv, <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>.","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>ArXiv</i>, doi:<a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>.","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Learning control policies for stochastic systems with reach-avoid guarantees","publication":"arXiv","tmp":{"image":"/images/cc_by_sa.png","short":"CC BY-SA (4.0)","name":"Creative Commons Attribution-ShareAlike 4.0 International Public License (CC BY-SA 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-sa/4.0/legalcode"},"oa_version":"Preprint","ec_funded":1,"date_created":"2023-11-24T13:10:09Z","related_material":{"record":[{"id":"14539","status":"public","relation":"dissertation_contains"},{"status":"public","relation":"later_version","id":"14830"}]},"doi":"10.48550/ARXIV.2210.05308","date_updated":"2025-07-14T09:10:02Z","article_processing_charge":"No","arxiv":1,"date_published":"2022-11-29T00:00:00Z","author":[{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"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"}]},{"type":"preprint","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publication_status":"submitted","year":"2022","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2205.11991"}],"_id":"14601","external_id":{"arxiv":["2205.11991"]},"day":"24","oa":1,"status":"public","project":[{"call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"665385","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"language":[{"iso":"eng"}],"month":"05","citation":{"ama":"Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>","short":"D. Zikelic, M. Lechner, K. Chatterjee, T.A. Henzinger, ArXiv (n.d.).","ista":"Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. arXiv, <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>.","mla":"Zikelic, Dorde, et al. “Learning Stabilizing Policies in Stochastic Control Systems.” <i>ArXiv</i>, doi:<a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>.","ieee":"D. Zikelic, M. Lechner, K. Chatterjee, and T. A. Henzinger, “Learning stabilizing policies in stochastic control systems,” <i>arXiv</i>. .","chicago":"Zikelic, Dorde, Mathias Lechner, Krishnendu Chatterjee, and Thomas A Henzinger. “Learning Stabilizing Policies in Stochastic Control Systems.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">https://doi.org/10.48550/arXiv.2205.11991</a>.","apa":"Zikelic, D., Lechner, M., Chatterjee, K., &#38; Henzinger, T. A. (n.d.). Learning stabilizing policies in stochastic control systems. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">https://doi.org/10.48550/arXiv.2205.11991</a>"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Learning stabilizing policies in stochastic control systems","publication":"arXiv","oa_version":"Preprint","ec_funded":1,"date_created":"2023-11-24T13:22:30Z","doi":"10.48550/arXiv.2205.11991","date_updated":"2025-07-14T09:10:00Z","related_material":{"record":[{"id":"14539","relation":"dissertation_contains","status":"public"}]},"article_processing_charge":"No","arxiv":1,"author":[{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde"},{"first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2022-05-24T00:00:00Z","abstract":[{"text":"In this work, we address the problem of learning provably stable neural\r\nnetwork policies for stochastic control systems. While recent work has\r\ndemonstrated the feasibility of certifying given policies using martingale\r\ntheory, the problem of how to learn such policies is little explored. Here, we\r\nstudy the effectiveness of jointly learning a policy together with a martingale\r\ncertificate that proves its stability using a single learning algorithm. We\r\nobserve that the joint optimization problem becomes easily stuck in local\r\nminima when starting from a randomly initialized policy. Our results suggest\r\nthat some form of pre-training of the policy is required for the joint\r\noptimization to repair and verify the policy successfully.","lang":"eng"}]},{"page":"100-119","volume":47,"type":"journal_article","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"9311","year":"2022","acknowledgement":"Partially supported by Austrian Science Fund (FWF) NFN Grant No RiSE/SHiNE S11407, by CONICYT Chile through grant PII 20150140, and by ECOS-CONICYT through grant C15E03.\r\n","status":"public","oa":1,"external_id":{"isi":["000731918100001"],"arxiv":["1904.13360"]},"article_type":"original","issue":"1","citation":{"apa":"Chatterjee, K., Saona Urmeneta, R. J., &#38; Ziliotto, B. (2022). Finite-memory strategies in POMDPs with long-run average objectives. <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences. <a href=\"https://doi.org/10.1287/moor.2020.1116\">https://doi.org/10.1287/moor.2020.1116</a>","ieee":"K. Chatterjee, R. J. Saona Urmeneta, and B. Ziliotto, “Finite-memory strategies in POMDPs with long-run average objectives,” <i>Mathematics of Operations Research</i>, vol. 47, no. 1. Institute for Operations Research and the Management Sciences, pp. 100–119, 2022.","chicago":"Chatterjee, Krishnendu, Raimundo J Saona Urmeneta, and Bruno Ziliotto. “Finite-Memory Strategies in POMDPs with Long-Run Average Objectives.” <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences, 2022. <a href=\"https://doi.org/10.1287/moor.2020.1116\">https://doi.org/10.1287/moor.2020.1116</a>.","mla":"Chatterjee, Krishnendu, et al. “Finite-Memory Strategies in POMDPs with Long-Run Average Objectives.” <i>Mathematics of Operations Research</i>, vol. 47, no. 1, Institute for Operations Research and the Management Sciences, 2022, pp. 100–19, doi:<a href=\"https://doi.org/10.1287/moor.2020.1116\">10.1287/moor.2020.1116</a>.","short":"K. Chatterjee, R.J. Saona Urmeneta, B. Ziliotto, Mathematics of Operations Research 47 (2022) 100–119.","ista":"Chatterjee K, Saona Urmeneta RJ, Ziliotto B. 2022. Finite-memory strategies in POMDPs with long-run average objectives. Mathematics of Operations Research. 47(1), 100–119.","ama":"Chatterjee K, Saona Urmeneta RJ, Ziliotto B. Finite-memory strategies in POMDPs with long-run average objectives. <i>Mathematics of Operations Research</i>. 2022;47(1):100-119. doi:<a href=\"https://doi.org/10.1287/moor.2020.1116\">10.1287/moor.2020.1116</a>"},"publication_identifier":{"eissn":["1526-5471"],"issn":["0364-765X"]},"title":"Finite-memory strategies in POMDPs with long-run average objectives","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"publication":"Mathematics of Operations Research","publisher":"Institute for Operations Research and the Management Sciences","oa_version":"Preprint","date_created":"2021-04-08T09:33:31Z","arxiv":1,"abstract":[{"text":"Partially observable Markov decision processes (POMDPs) are standard models for dynamic systems with probabilistic and nondeterministic behaviour in uncertain environments. We prove that in POMDPs with long-run average objective, the decision maker has approximately optimal strategies with finite memory. This implies notably that approximating the long-run value is recursively enumerable, as well as a weak continuity property of the value with respect to the transition function. ","lang":"eng"}],"intvolume":"        47","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1904.13360"}],"publication_status":"published","day":"01","language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"}],"isi":1,"month":"02","date_published":"2022-02-01T00:00:00Z","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","first_name":"Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","full_name":"Saona Urmeneta, Raimundo J"},{"first_name":"Bruno","last_name":"Ziliotto","full_name":"Ziliotto, Bruno"}],"date_updated":"2023-09-05T13:16:11Z","doi":"10.1287/moor.2020.1116","article_processing_charge":"No","scopus_import":"1","keyword":["Management Science and Operations Research","General Mathematics","Computer Science Applications"],"quality_controlled":"1"},{"file":[{"access_level":"open_access","creator":"cchlebak","relation":"main_file","success":1,"date_created":"2022-01-07T07:50:31Z","content_type":"application/pdf","file_id":"10603","date_updated":"2022-01-07T07:50:31Z","file_name":"2021_ActaInfor_Křetínský.pdf","checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","file_size":1066082}],"publication_status":"published","intvolume":"        59","ddc":["000"],"day":"01","isi":1,"month":"10","language":[{"iso":"eng"}],"project":[{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"file_date_updated":"2022-01-07T07:50:31Z","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"article_processing_charge":"Yes (via OA deal)","doi":"10.1007/s00236-021-00412-y","date_updated":"2023-08-02T13:49:28Z","date_published":"2022-10-01T00:00:00Z","author":[{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"},{"full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165"},{"full_name":"Waldmann, Clara","last_name":"Waldmann","first_name":"Clara"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"}],"quality_controlled":"1","keyword":["computer networks and communications","information systems","software"],"scopus_import":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","type":"journal_article","volume":59,"page":"585-618","has_accepted_license":"1","year":"2022","_id":"10602","external_id":{"isi":["000735765500001"]},"article_type":"original","oa":1,"acknowledgement":"This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art.","status":"public","publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"citation":{"ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” <i>Acta Informatica</i>, vol. 59. Springer Nature, pp. 585–618, 2022.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2022). Index appearance record with preorders. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. <i>Acta Informatica</i>. 2022;59:585-618. doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618.","mla":"Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>, vol. 59, Springer Nature, 2022, pp. 585–618, doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618."},"publisher":"Springer Nature","publication":"Acta Informatica","title":"Index appearance record with preorders","department":[{"_id":"KrCh"}],"date_created":"2022-01-06T12:37:27Z","oa_version":"Published Version","abstract":[{"text":"Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches.","lang":"eng"}]},{"_id":"11938","has_accepted_license":"1","year":"2022","volume":26,"page":"225-240","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","citation":{"chicago":"Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada, Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible Matchings.” <i>Journal of Graph Algorithms and Applications</i>. Brown University, 2022. <a href=\"https://doi.org/10.7155/jgaa.00591\">https://doi.org/10.7155/jgaa.00591</a>.","ieee":"O. Aichholzer <i>et al.</i>, “On compatible matchings,” <i>Journal of Graph Algorithms and Applications</i>, vol. 26, no. 2. Brown University, pp. 225–240, 2022.","apa":"Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D., Pilz, A., … Vogtenhuber, B. (2022). On compatible matchings. <i>Journal of Graph Algorithms and Applications</i>. Brown University. <a href=\"https://doi.org/10.7155/jgaa.00591\">https://doi.org/10.7155/jgaa.00591</a>","ama":"Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings. <i>Journal of Graph Algorithms and Applications</i>. 2022;26(2):225-240. doi:<a href=\"https://doi.org/10.7155/jgaa.00591\">10.7155/jgaa.00591</a>","ista":"Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec J, Vogtenhuber B. 2022. On compatible matchings. Journal of Graph Algorithms and Applications. 26(2), 225–240.","mla":"Aichholzer, Oswin, et al. “On Compatible Matchings.” <i>Journal of Graph Algorithms and Applications</i>, vol. 26, no. 2, Brown University, 2022, pp. 225–40, doi:<a href=\"https://doi.org/10.7155/jgaa.00591\">10.7155/jgaa.00591</a>.","short":"O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz, J. Tkadlec, B. Vogtenhuber, Journal of Graph Algorithms and Applications 26 (2022) 225–240."},"publication_identifier":{"issn":["1526-1719"]},"acknowledgement":"A.A. funded by the Marie Sklodowska-Curie grant agreement No 754411. Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23 (RiSE).","status":"public","oa":1,"issue":"2","article_type":"original","external_id":{"arxiv":["2101.03928"]},"date_created":"2022-08-21T22:01:56Z","ec_funded":1,"oa_version":"Published Version","publication":"Journal of Graph Algorithms and Applications","title":"On compatible matchings","department":[{"_id":"UlWa"},{"_id":"HeEd"},{"_id":"KrCh"}],"publisher":"Brown University","abstract":[{"text":"A matching is compatible to two or more labeled point sets of size n with labels {1, . . . , n} if its straight-line drawing on each of these point sets is crossing-free. We study the maximum number of edges in a matching compatible to two or more labeled point sets in general position in the plane. We show that for any two labeled sets of n points in convex position there exists a compatible matching with ⌊√2n + 1 − 1⌋ edges. More generally, for any ℓ labeled point sets we construct compatible matchings of size Ω(n1/ℓ). As a corresponding upper bound, we use probabilistic arguments to show that for any ℓ given sets of n points there exists a labeling of each set such that the largest compatible matching has O(n2/(ℓ+1)) edges. Finally, we show that Θ(log n) copies of any set of n points are necessary and sufficient for the existence of labelings of these point sets such that any compatible matching consists only of a single edge.","lang":"eng"}],"arxiv":1,"intvolume":"        26","file":[{"date_created":"2022-08-22T06:42:42Z","success":1,"content_type":"application/pdf","access_level":"open_access","creator":"dernst","relation":"main_file","checksum":"dc6e255e3558faff924fd9e370886c11","file_name":"2022_JourGraphAlgorithmsApplic_Aichholzer.pdf","file_size":694538,"file_id":"11940","date_updated":"2022-08-22T06:42:42Z"}],"publication_status":"published","month":"06","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"Z00342","name":"The Wittgenstein Prize","_id":"268116B8-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"ddc":["000"],"day":"01","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"file_date_updated":"2022-08-22T06:42:42Z","scopus_import":"1","quality_controlled":"1","date_published":"2022-06-01T00:00:00Z","author":[{"first_name":"Oswin","last_name":"Aichholzer","full_name":"Aichholzer, Oswin"},{"orcid":"0000-0003-2401-8670","last_name":"Arroyo Guevara","first_name":"Alan M","id":"3207FDC6-F248-11E8-B48F-1D18A9856A87","full_name":"Arroyo Guevara, Alan M"},{"last_name":"Masárová","orcid":"0000-0002-6660-1322","first_name":"Zuzana","id":"45CFE238-F248-11E8-B48F-1D18A9856A87","full_name":"Masárová, Zuzana"},{"full_name":"Parada, Irene","first_name":"Irene","last_name":"Parada"},{"full_name":"Perz, Daniel","first_name":"Daniel","last_name":"Perz"},{"first_name":"Alexander","last_name":"Pilz","full_name":"Pilz, Alexander"},{"last_name":"Tkadlec","orcid":"0000-0002-1097-9684","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef"},{"full_name":"Vogtenhuber, Birgit","first_name":"Birgit","last_name":"Vogtenhuber"}],"article_processing_charge":"No","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"9296"}]},"doi":"10.7155/jgaa.00591","date_updated":"2023-02-23T13:54:21Z"},{"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031131844"]},"citation":{"chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. “Sound and Complete Certificates for Auantitative Termination Analysis of Probabilistic Programs.” In <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, 13371:55–78. Springer, 2022. <a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">https://doi.org/10.1007/978-3-031-13185-1_4</a>.","ieee":"K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Sound and complete certificates for auantitative termination analysis of probabilistic programs,” in <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, Haifa, Israel, 2022, vol. 13371, pp. 55–78.","apa":"Chatterjee, K., Goharshady, A. K., Meggendorfer, T., &#38; Zikelic, D. (2022). Sound and complete certificates for auantitative termination analysis of probabilistic programs. In <i>Proceedings of the 34th International Conference on Computer Aided Verification</i> (Vol. 13371, pp. 55–78). Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">https://doi.org/10.1007/978-3-031-13185-1_4</a>","ama":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Sound and complete certificates for auantitative termination analysis of probabilistic programs. In: <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>. Vol 13371. Springer; 2022:55-78. doi:<a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">10.1007/978-3-031-13185-1_4</a>","ista":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2022. Sound and complete certificates for auantitative termination analysis of probabilistic programs. Proceedings of the 34th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13371, 55–78.","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Certificates for Auantitative Termination Analysis of Probabilistic Programs.” <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, vol. 13371, Springer, 2022, pp. 55–78, doi:<a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">10.1007/978-3-031-13185-1_4</a>.","short":"K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, in:, Proceedings of the 34th International Conference on Computer Aided Verification, Springer, 2022, pp. 55–78."},"external_id":{"isi":["000870304500004"]},"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055, the HKUST Startup Grant R9272 and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","status":"public","oa":1,"has_accepted_license":"1","year":"2022","_id":"12000","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","type":"conference","volume":13371,"page":"55-78","abstract":[{"text":"We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p∈[0,1], we aim for certificates proving that the program terminates with probability at least 1−p. The basic idea of our approach is to find a terminating stochastic invariant, i.e. a subset SI of program states such that (i) the probability of the program ever leaving SI is no more than p, and (ii) almost-surely, the program either leaves SI or terminates.\r\n\r\nWhile stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for qualitative termination analysis, we obtain the first automated, sound, and relatively complete algorithm for quantitative termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant.\r\n\r\nOur prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods.","lang":"eng"}],"date_created":"2022-08-28T22:02:02Z","ec_funded":1,"oa_version":"Published Version","publisher":"Springer","publication":"Proceedings of the 34th International Conference on Computer Aided Verification","title":"Sound and complete certificates for auantitative termination analysis of probabilistic programs","department":[{"_id":"KrCh"}],"isi":1,"month":"08","language":[{"iso":"eng"}],"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program"}],"ddc":["000"],"day":"07","file":[{"relation":"main_file","creator":"alisjak","access_level":"open_access","content_type":"application/pdf","date_created":"2022-08-29T09:17:01Z","success":1,"date_updated":"2022-08-29T09:17:01Z","file_id":"12003","file_size":505094,"checksum":"24e0f810ec52735a90ade95198bc641d","file_name":"2022_LNCS_Chatterjee.pdf"}],"publication_status":"published","intvolume":"     13371","quality_controlled":"1","scopus_import":"1","article_processing_charge":"Yes (in subscription journal)","doi":"10.1007/978-3-031-13185-1_4","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"14539"}]},"alternative_title":["LNCS"],"date_updated":"2025-07-14T09:09:58Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar"},{"last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic"}],"date_published":"2022-08-07T00:00:00Z","conference":{"name":"CAV: Computer Aided Verification","end_date":"2022-08-10","location":"Haifa, Israel","start_date":"2022-08-07"},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"file_date_updated":"2022-08-29T09:17:01Z"},{"article_number":"11:1-11:14","file_date_updated":"2023-01-20T10:19:19Z","conference":{"end_date":"2022-12-20","name":"FSTTC: Foundations of Software Technology and Theoretical Computer Science","start_date":"2022-12-18","location":"Madras, India"},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"article_processing_charge":"No","doi":"10.4230/LIPIcs.FSTTCS.2022.11","date_updated":"2025-07-14T09:09:55Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"first_name":"Ismael R","last_name":"Jecker","full_name":"Jecker, Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425"},{"first_name":"Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"}],"date_published":"2022-12-14T00:00:00Z","quality_controlled":"1","scopus_import":"1","file":[{"content_type":"application/pdf","date_created":"2023-01-20T10:19:19Z","success":1,"relation":"main_file","access_level":"open_access","creator":"dernst","file_size":657396,"checksum":"a21e3ba2421e2c4a06aa2cb6d530ede1","file_name":"2022_LIPICs_Chatterjee.pdf","date_updated":"2023-01-20T10:19:19Z","file_id":"12323"}],"publication_status":"published","intvolume":"       250","ddc":["000"],"day":"14","month":"12","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication":"42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","department":[{"_id":"KrCh"}],"title":"Complexity of spatial games","date_created":"2023-01-01T23:00:50Z","ec_funded":1,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Spatial games form a widely-studied class of games from biology and physics modeling the evolution of social behavior. Formally, such a game is defined by a square (d by d) payoff matrix M and an undirected graph G. Each vertex of G represents an individual, that initially follows some strategy i ∈ {1,2,…,d}. In each round of the game, every individual plays the matrix game with each of its neighbors: An individual following strategy i meeting a neighbor following strategy j receives a payoff equal to the entry (i,j) of M. Then, each individual updates its strategy to its neighbors' strategy with the highest sum of payoffs, and the next round starts. The basic computational problems consist of reachability between configurations and the average frequency of a strategy. For general spatial games and graphs, these problems are in PSPACE. In this paper, we examine restricted setting: the game is a prisoner’s dilemma; and G is a subgraph of grid. We prove that basic computational problems for spatial games with prisoner’s dilemma on a subgraph of a grid are PSPACE-hard."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","volume":250,"year":"2022","has_accepted_license":"1","_id":"12101","acknowledgement":"Krishnendu Chatterjee: The research was partially supported by the ERC CoG 863818\r\n(ForM-SMArt).\r\nIsmaël Jecker: The research was partially supported by the ERC grant 950398 (INFSYS).\r\nJakub Svoboda: The research was partially supported by the ERC CoG 863818 (ForM-SMArt)","status":"public","oa":1,"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959772617"]},"citation":{"mla":"Chatterjee, Krishnendu, et al. “Complexity of Spatial Games.” <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 250, 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">10.4230/LIPIcs.FSTTCS.2022.11</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.","ista":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2022. Complexity of spatial games. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTC: Foundations of Software Technology and Theoretical Computer Science vol. 250, 11:1-11:14.","ama":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Complexity of spatial games. In: <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">10.4230/LIPIcs.FSTTCS.2022.11</a>","apa":"Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., &#38; Svoboda, J. (2022). Complexity of spatial games. In <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 250). Madras, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11</a>","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Complexity of Spatial Games.” In <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Vol. 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11</a>.","ieee":"K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Complexity of spatial games,” in <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Madras, India, 2022, vol. 250."}}]