[{"publication_status":"published","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"type":"conference","title":"Boosting payment channel network liquidity with topology optimization and transaction selection","license":"https://creativecommons.org/licenses/by/4.0/","alternative_title":["LIPIcs"],"date_created":"2026-03-08T23:01:46Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Berlin, Germany","name":"DISC: Symposium on Distributed Computing","start_date":"2025-10-27","end_date":"2025-10-31"},"publication_identifier":{"isbn":["9783959774024"],"issn":["1868-8969"]},"year":"2025","article_number":"23","doi":"10.4230/LIPIcs.DISC.2025.23","acknowledgement":"Chatterjee, Krishnendu: European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.\r\nKřišťan, Jan Matyáš: Czech Science Foundation Grant no. 24-12046S.\r\nSchmid, Stefan: German Research Foundation (DFG) project ReNO (SPP 2378) from 2023-2027.\r\nSvoboda, Jakub: European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.\r\nYeo, Michelle: MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms).","external_id":{"arxiv":["2508.14524"]},"date_published":"2025-10-22T00:00:00Z","file":[{"file_size":1130069,"success":1,"date_created":"2026-03-09T11:51:59Z","content_type":"application/pdf","date_updated":"2026-03-09T11:51:59Z","creator":"dernst","access_level":"open_access","relation":"main_file","file_name":"2025_DISC_Chatterjee.pdf","file_id":"21418","checksum":"8e3d1594365df60163d9df22158a37b1"}],"publication":"39th International Symposium on Distributed Computing","abstract":[{"lang":"eng","text":"Payment channel networks (PCNs) are a promising technology that alleviates blockchain scalability by shifting the transaction load from the blockchain to the PCN. Nevertheless, the network topology has to be carefully designed to maximise the transaction throughput in PCNs. Additionally, users in PCNs also have to make optimal decisions on which transactions to forward and which to reject to prolong the lifetime of their channels. In this work, we consider an input sequence of transactions over p parties. Each transaction consists of a transaction size, source, and target, and can be either accepted or rejected (entailing a cost). The goal is to design a PCN topology among the p cooperating parties, along with the channel capacities, and then output a decision for each transaction in the sequence to minimise the cost of creating and augmenting channels, as well as the cost of rejecting transactions. Our main contribution is an 𝒪(p) approximation algorithm for the problem with p parties. We further show that with some assumptions on the distribution of transactions, we can reduce the approximation ratio to 𝒪(√p). We complement our theoretical analysis with an empirical study of our assumptions and approach in the context of the Lightning Network."}],"main_file_link":[{"url":"https://eprint.iacr.org/2025/1484.pdf","open_access":"1"}],"oa_version":"Published Version","day":"22","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Jan Matyáš","last_name":"Křišťan","full_name":"Křišťan, Jan Matyáš"},{"first_name":"Stefan","last_name":"Schmid","full_name":"Schmid, Stefan"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267"},{"full_name":"Yeo, Michelle X","last_name":"Yeo","first_name":"Michelle X","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","orcid":"0009-0001-3676-4809"}],"_id":"21412","status":"public","ddc":["000"],"department":[{"_id":"KrCh"}],"file_date_updated":"2026-03-09T11:51:59Z","arxiv":1,"scopus_import":"1","oa":1,"date_updated":"2026-03-09T11:52:58Z","OA_place":"publisher","month":"10","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","intvolume":"       356","has_accepted_license":"1","citation":{"ista":"Chatterjee K, Křišťan JM, Schmid S, Svoboda J, Yeo MX. 2025. Boosting payment channel network liquidity with topology optimization and transaction selection. 39th International Symposium on Distributed Computing. DISC: Symposium on Distributed Computing, LIPIcs, vol. 356, 23.","short":"K. Chatterjee, J.M. Křišťan, S. Schmid, J. Svoboda, M.X. Yeo, in:, 39th International Symposium on Distributed Computing, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025.","mla":"Chatterjee, Krishnendu, et al. “Boosting Payment Channel Network Liquidity with Topology Optimization and Transaction Selection.” <i>39th International Symposium on Distributed Computing</i>, vol. 356, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.DISC.2025.23\">10.4230/LIPIcs.DISC.2025.23</a>.","apa":"Chatterjee, K., Křišťan, J. M., Schmid, S., Svoboda, J., &#38; Yeo, M. X. (2025). Boosting payment channel network liquidity with topology optimization and transaction selection. In <i>39th International Symposium on Distributed Computing</i> (Vol. 356). Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.DISC.2025.23\">https://doi.org/10.4230/LIPIcs.DISC.2025.23</a>","ieee":"K. Chatterjee, J. M. Křišťan, S. Schmid, J. Svoboda, and M. X. Yeo, “Boosting payment channel network liquidity with topology optimization and transaction selection,” in <i>39th International Symposium on Distributed Computing</i>, Berlin, Germany, 2025, vol. 356.","ama":"Chatterjee K, Křišťan JM, Schmid S, Svoboda J, Yeo MX. Boosting payment channel network liquidity with topology optimization and transaction selection. In: <i>39th International Symposium on Distributed Computing</i>. Vol 356. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.DISC.2025.23\">10.4230/LIPIcs.DISC.2025.23</a>","chicago":"Chatterjee, Krishnendu, Jan Matyáš Křišťan, Stefan Schmid, Jakub Svoboda, and Michelle X Yeo. “Boosting Payment Channel Network Liquidity with Topology Optimization and Transaction Selection.” In <i>39th International Symposium on Distributed Computing</i>, Vol. 356. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.DISC.2025.23\">https://doi.org/10.4230/LIPIcs.DISC.2025.23</a>."},"OA_type":"gold","quality_controlled":"1","volume":356,"article_processing_charge":"No","ec_funded":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"}},{"citation":{"short":"T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, T. Meggendorfer, D. Parker, M. Ujma, TheoretiCS 4 (2025).","ista":"Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Meggendorfer T, Parker D, Ujma M. 2025. Learning algorithms for verification of Markov decision processes. TheoretiCS. 4, 10.","mla":"Brázdil, Tomáš, et al. “Learning Algorithms for Verification of Markov Decision Processes.” <i>TheoretiCS</i>, vol. 4, 10, TheoretiCS Foundation, 2025, doi:<a href=\"https://doi.org/10.46298/theoretics.25.10\">10.46298/theoretics.25.10</a>.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2025). Learning algorithms for verification of Markov decision processes. <i>TheoretiCS</i>. TheoretiCS Foundation. <a href=\"https://doi.org/10.46298/theoretics.25.10\">https://doi.org/10.46298/theoretics.25.10</a>","ieee":"T. Brázdil <i>et al.</i>, “Learning algorithms for verification of Markov decision processes,” <i>TheoretiCS</i>, vol. 4. TheoretiCS Foundation, 2025.","ama":"Brázdil T, Chatterjee K, Chmelik M, et al. Learning algorithms for verification of Markov decision processes. <i>TheoretiCS</i>. 2025;4. doi:<a href=\"https://doi.org/10.46298/theoretics.25.10\">10.46298/theoretics.25.10</a>","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, and Mateusz Ujma. “Learning Algorithms for Verification of Markov Decision Processes.” <i>TheoretiCS</i>. TheoretiCS Foundation, 2025. <a href=\"https://doi.org/10.46298/theoretics.25.10\">https://doi.org/10.46298/theoretics.25.10</a>."},"has_accepted_license":"1","OA_type":"gold","quality_controlled":"1","volume":4,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"ec_funded":1,"article_processing_charge":"Yes","month":"04","OA_place":"publisher","publisher":"TheoretiCS Foundation","intvolume":"         4","oa":1,"date_updated":"2026-03-09T11:43:38Z","_id":"21413","status":"public","department":[{"_id":"KrCh"}],"file_date_updated":"2026-03-09T11:39:59Z","ddc":["000"],"arxiv":1,"scopus_import":"1","oa_version":"Published Version","day":"01","PlanS_conform":"1","author":[{"full_name":"Brázdil, Tomáš","last_name":"Brázdil","first_name":"Tomáš"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"first_name":"Vojtěch","last_name":"Forejt","full_name":"Forejt, Vojtěch"},{"orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kwiatkowska","full_name":"Kwiatkowska, Marta","first_name":"Marta"},{"orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias"},{"last_name":"Parker","full_name":"Parker, David","first_name":"David"},{"full_name":"Ujma, Mateusz","last_name":"Ujma","first_name":"Mateusz"}],"file":[{"relation":"main_file","access_level":"open_access","file_id":"21417","file_name":"2026_TheoretiCS_Brazdil.pdf","checksum":"2ccf563ae577ee08d82baf752292ca7b","file_size":861607,"date_created":"2026-03-09T11:39:59Z","content_type":"application/pdf","success":1,"date_updated":"2026-03-09T11:39:59Z","creator":"dernst"}],"external_id":{"arxiv":["2403.09184"]},"date_published":"2025-04-01T00:00:00Z","publication":"TheoretiCS","abstract":[{"text":"We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs).\r\nThe primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors.\r\nThe presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios.\r\nThe first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.","lang":"eng"}],"date_created":"2026-03-08T23:01:46Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","article_number":"10","publication_identifier":{"eissn":["2751-4838"]},"doi":"10.46298/theoretics.25.10","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement AdG-267989 (QUAREM)*, AdG-246967 (VERIWARE)*, StG-279307 (Graph Games)*\r\n, CoG-863818 (ForM-SMArt), and AdG-834115 (FUN2MODEL), by the EU FP7 project HIERATIC*, by the German Research Foundation (DFG) project 427755713 (GOPro), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE)* , S11407-N23 (RiSE)*\r\n, and P23499-N23* , by the Czech Science Foundation grant No P202/12/P612* and GA23-06963S, by the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant\r\nAgency of Masaryk University, by EPSRC project EP/K038575/1*, and by the Microsoft faculty fellows award*. A preliminary version of this article appeared at ATVA 2014 [33]. The * indicates funding that supported that version.","DOAJ_listed":"1","article_type":"original","publication_status":"published","language":[{"iso":"eng"}],"type":"journal_article","title":"Learning algorithms for verification of Markov decision processes","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}]},{"date_updated":"2026-04-07T12:31:21Z","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"20234"}]},"scopus_import":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"status":"public","_id":"17037","page":"482-505","article_processing_charge":"No","ec_funded":1,"quality_controlled":"1","volume":50,"citation":{"ama":"Attia L, Oliu-Barton M, Saona Urmeneta RJ. Marginal values of a stochastic game. <i>Mathematics of Operations Research</i>. 2025;50(1):482-505. doi:<a href=\"https://doi.org/10.1287/moor.2023.0297\">10.1287/moor.2023.0297</a>","chicago":"Attia, Luc, Miquel Oliu-Barton, and Raimundo J Saona Urmeneta. “Marginal Values of a Stochastic Game.” <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences, 2025. <a href=\"https://doi.org/10.1287/moor.2023.0297\">https://doi.org/10.1287/moor.2023.0297</a>.","ieee":"L. Attia, M. Oliu-Barton, and R. J. Saona Urmeneta, “Marginal values of a stochastic game,” <i>Mathematics of Operations Research</i>, vol. 50, no. 1. Institute for Operations Research and the Management Sciences, pp. 482–505, 2025.","apa":"Attia, L., Oliu-Barton, M., &#38; Saona Urmeneta, R. J. (2025). Marginal values of a stochastic game. <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences. <a href=\"https://doi.org/10.1287/moor.2023.0297\">https://doi.org/10.1287/moor.2023.0297</a>","mla":"Attia, Luc, et al. “Marginal Values of a Stochastic Game.” <i>Mathematics of Operations Research</i>, vol. 50, no. 1, Institute for Operations Research and the Management Sciences, 2025, pp. 482–505, doi:<a href=\"https://doi.org/10.1287/moor.2023.0297\">10.1287/moor.2023.0297</a>.","ista":"Attia L, Oliu-Barton M, Saona Urmeneta RJ. 2025. Marginal values of a stochastic game. Mathematics of Operations Research. 50(1), 482–505.","short":"L. Attia, M. Oliu-Barton, R.J. Saona Urmeneta, Mathematics of Operations Research 50 (2025) 482–505."},"intvolume":"        50","publisher":"Institute for Operations Research and the Management Sciences","month":"02","acknowledgement":"This work was supported by Fondation CFM pour la Recherche; the European Research Council [Grant ERC-CoG-863818 (ForM-SMArt)]; and Agence Nationale de la Recherche [Grant ANR-21-CE40-0020].","doi":"10.1287/moor.2023.0297","year":"2025","publication_identifier":{"issn":["0364-765X"],"eissn":["1526-5471"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2024-05-22T11:41:14Z","type":"journal_article","title":"Marginal values of a stochastic game","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"language":[{"iso":"eng"}],"isi":1,"publication_status":"published","article_type":"original","author":[{"full_name":"Attia, Luc","last_name":"Attia","first_name":"Luc"},{"last_name":"Oliu-Barton","full_name":"Oliu-Barton, Miquel","first_name":"Miquel"},{"id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","first_name":"Raimundo J","last_name":"Saona Urmeneta","full_name":"Saona Urmeneta, Raimundo J","orcid":"0000-0001-5103-038X"}],"day":"01","oa_version":"None","issue":"1","abstract":[{"text":"Zero-sum stochastic games are parameterized by payoffs, transitions, and possibly a discount rate. In this article, we study how the main solution concepts, the discounted and undiscounted values, vary when these parameters are perturbed. We focus on the marginal values, introduced by Mills in 1956 in the context of matrix games—that is, the directional derivatives of the value along any fixed perturbation. We provide a formula for the marginal values of a discounted stochastic game. Further, under mild assumptions on the perturbation, we provide a formula for their limit as the discount rate vanishes and for the marginal values of an undiscounted stochastic game. We also show, via an example, that the two latter differ in general.","lang":"eng"}],"publication":"Mathematics of Operations Research","external_id":{"isi":["001184648000001"]},"date_published":"2025-02-01T00:00:00Z"},{"date_updated":"2025-09-08T09:51:34Z","oa":1,"ddc":["000"],"file_date_updated":"2024-10-01T09:56:54Z","department":[{"_id":"KrCh"}],"arxiv":1,"scopus_import":"1","corr_author":"1","_id":"18155","status":"public","article_processing_charge":"Yes (in subscription journal)","ec_funded":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"page":"600-619","has_accepted_license":"1","citation":{"apa":"Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., &#38; Zikelic, D. (2024). Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 14933, pp. 600–619). Milan, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">https://doi.org/10.1007/978-3-031-71162-6_31</a>","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 14933, Springer Nature, 2024, pp. 600–19, doi:<a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">10.1007/978-3-031-71162-6_31</a>.","short":"K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, D. Zikelic, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp. 600–619.","ista":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods, LNCS, vol. 14933, 600–619.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad Karrabi, and Dorde Zikelic. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 14933:600–619. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">https://doi.org/10.1007/978-3-031-71162-6_31</a>.","ama":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 14933. Springer Nature; 2024:600-619. doi:<a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">10.1007/978-3-031-71162-6_31</a>","ieee":"K. Chatterjee, A. K. Goharshady, E. Goharshady, M. Karrabi, and D. Zikelic, “Sound and complete witnesses for template-based verification of LTL properties on polynomial programs,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Milan, Italy, 2024, vol. 14933, pp. 600–619."},"volume":14933,"quality_controlled":"1","publisher":"Springer Nature","intvolume":"     14933","month":"09","publication_identifier":{"isbn":["9783031711619"],"issn":["0302-9743"],"eissn":["1611-3349"]},"year":"2024","doi":"10.1007/978-3-031-71162-6_31","acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Hong Kong Research Grants Council ECS Project Number 26208122.","date_created":"2024-09-29T22:01:37Z","alternative_title":["LNCS"],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"end_date":"2024-09-13","location":"Milan, Italy","start_date":"2024-09-09","name":"FM: Formal Methods"},"language":[{"iso":"eng"}],"isi":1,"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"type":"conference","title":"Sound and complete witnesses for template-based verification of LTL properties on polynomial programs","publication_status":"published","day":"11","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584"},{"first_name":"Ehsan","full_name":"Goharshady, Ehsan","last_name":"Goharshady"},{"last_name":"Karrabi","full_name":"Karrabi, Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757","first_name":"Mehrdad"},{"orcid":"0000-0002-4681-1699","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","last_name":"Zikelic"}],"oa_version":"Published Version","abstract":[{"text":"We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools.","lang":"eng"}],"file":[{"date_updated":"2024-10-01T09:56:54Z","creator":"dernst","file_size":650495,"success":1,"content_type":"application/pdf","date_created":"2024-10-01T09:56:54Z","checksum":"223845be9e754681ee218866827c95e7","access_level":"open_access","relation":"main_file","file_name":"2024_LNCS_Chatterjee.pdf","file_id":"18165"}],"external_id":{"arxiv":["2403.05386"],"isi":["001336893300031"]},"date_published":"2024-09-11T00:00:00Z","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)"},{"conference":{"end_date":"2024-08-09","location":"Jeju, Korea","name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2024-08-03"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2024-09-29T22:01:38Z","doi":"10.24963/ijcai.2024/1","acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt), the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant, Google Research Award 2023 and the SBI Foundation Hub for Data and Analytics.","publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"year":"2024","publication_status":"published","title":"Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties","type":"conference","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"}],"oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2405.04015"}],"author":[{"last_name":"Akshay","full_name":"Akshay, S","first_name":"S"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"orcid":"0000-0002-4681-1699","last_name":"Zikelic","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde"}],"day":"01","publication":"Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence","date_published":"2024-09-01T00:00:00Z","external_id":{"arxiv":["2405.04015"]},"abstract":[{"lang":"eng","text":"Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defned with respect to paths over MDP states. An increasingly\r\npopular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defned in terms of probability distributions over states. Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verifcation techniques. In this work, we consider the problems of certifed policy (i.e. controller) verifcation and synthesis in MDPs under distributional reach-avoidance specifcations. By certifed we mean that, along with a policy, we also aim to synthesize a (checkable) certifcate ensuring that the MDP indeed satisfes the property. Thus, given the target set of distributions and an unsafe set of distributions over MDP states, our goal is to either synthesize a certifcate for a given policy or synthesize a policy along with a certifcate, proving that the target distribution can be reached while avoiding unsafe distributions. To solve this problem, we introduce the novel notion of distributional reach-avoid certifcates and present automated procedures for (1) synthesizing a certifcate for a given policy, and (2) synthesizing a policy together with the certifcate, both providing formal guarantees on certifcate correctness. Our experimental evaluation demonstrates the ability of our method to solve several non-trivial examples, including a multi-agent robot-swarm model, to synthesize certifed policies and to certify existing policies. "}],"oa":1,"date_updated":"2025-04-14T07:52:46Z","status":"public","_id":"18159","corr_author":"1","arxiv":1,"scopus_import":"1","department":[{"_id":"KrCh"}],"quality_controlled":"1","citation":{"apa":"Akshay, S., Chatterjee, K., Meggendorfer, T., &#38; Zikelic, D. (2024). Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. In <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i> (pp. 3–12). Jeju, Korea: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2024/1\">https://doi.org/10.24963/ijcai.2024/1</a>","mla":"Akshay, S., et al. “Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.” <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2024, pp. 3–12, doi:<a href=\"https://doi.org/10.24963/ijcai.2024/1\">10.24963/ijcai.2024/1</a>.","ista":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2024. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 3–12.","short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 3–12.","ama":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. In: <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2024:3-12. doi:<a href=\"https://doi.org/10.24963/ijcai.2024/1\">10.24963/ijcai.2024/1</a>","chicago":"Akshay, S, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. “Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.” In <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, 3–12. International Joint Conferences on Artificial Intelligence, 2024. <a href=\"https://doi.org/10.24963/ijcai.2024/1\">https://doi.org/10.24963/ijcai.2024/1</a>.","ieee":"S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties,” in <i>Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence</i>, Jeju, Korea, 2024, pp. 3–12."},"page":"3-12","ec_funded":1,"article_processing_charge":"No","month":"09","publisher":"International Joint Conferences on Artificial Intelligence"},{"publication":"33rd International Joint Conference on Artificial Intelligence","external_id":{"arxiv":["2312.13912"]},"date_published":"2024-09-01T00:00:00Z","abstract":[{"text":"Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs in which all uncertainty sets are polytopes and study the problem of solving long-run average reward polytopic RMDPs. We present a novel perspective on this problem and show that it can be reduced to solving long-run average reward turn-based stochastic games with finite state and action spaces. This reduction allows us to derive several important consequences that were hitherto not known to hold for polytopic RMDPs. First, we derive new computational complexity bounds for solving long-run average reward polytopic RMDPs, showing for the first time that the threshold decision problem for them is in NP∩CONP and that they admit a randomized algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is much more efficient in solving long-run average reward polytopic RMDPs compared to state-of-the-art methods based on value iteration. ","lang":"eng"}],"oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2312.13912"}],"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8595-0587","last_name":"Kafshdar Goharshadi","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan"},{"full_name":"Karrabi, Mehrdad","last_name":"Karrabi","first_name":"Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","last_name":"Novotný"},{"last_name":"Zikelic","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699"}],"day":"01","publication_status":"published","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"title":"Solving long-run average reward robust MDPs via stochastic games","type":"conference","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2024-08-09","start_date":"2024-08-03","name":"IJCAI: International Joint Conference on Artificial Intelligence","location":"Jeju, South Korea"},"date_created":"2024-09-29T22:01:39Z","acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Czech Science Foundation\r\ngrant no. GA23-06963S.","doi":"10.24963/ijcai.2024/741","publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"year":"2024","OA_place":"repository","month":"09","publisher":"International Joint Conferences on Artificial Intelligence","OA_type":"green","quality_controlled":"1","citation":{"apa":"Chatterjee, K., Goharshady, E., Karrabi, M., Novotný, P., &#38; Zikelic, D. (2024). Solving long-run average reward robust MDPs via stochastic games. In <i>33rd International Joint Conference on Artificial Intelligence</i> (pp. 6707–6715). Jeju, South Korea: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2024/741\">https://doi.org/10.24963/ijcai.2024/741</a>","mla":"Chatterjee, Krishnendu, et al. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” <i>33rd International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–15, doi:<a href=\"https://doi.org/10.24963/ijcai.2024/741\">10.24963/ijcai.2024/741</a>.","short":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, D. Zikelic, in:, 33rd International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–6715.","ista":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving long-run average reward robust MDPs via stochastic games. 33rd International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 6707–6715.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Petr Novotný, and Dorde Zikelic. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” In <i>33rd International Joint Conference on Artificial Intelligence</i>, 6707–15. International Joint Conferences on Artificial Intelligence, 2024. <a href=\"https://doi.org/10.24963/ijcai.2024/741\">https://doi.org/10.24963/ijcai.2024/741</a>.","ama":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. Solving long-run average reward robust MDPs via stochastic games. In: <i>33rd International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2024:6707-6715. doi:<a href=\"https://doi.org/10.24963/ijcai.2024/741\">10.24963/ijcai.2024/741</a>","ieee":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, and D. Zikelic, “Solving long-run average reward robust MDPs via stochastic games,” in <i>33rd International Joint Conference on Artificial Intelligence</i>, Jeju, South Korea, 2024, pp. 6707–6715."},"page":"6707-6715","ec_funded":1,"article_processing_charge":"No","status":"public","corr_author":"1","_id":"18160","arxiv":1,"scopus_import":"1","department":[{"_id":"KrCh"}],"oa":1,"date_updated":"2025-04-14T07:52:46Z"},{"external_id":{"isi":["001328875900001"]},"date_published":"2024-10-01T00:00:00Z","publication":"Mathematics of Operations Research","abstract":[{"lang":"eng","text":"Matrix games are the most basic model in game theory, and yet robustness with respect to small perturbations of the matrix entries is not fully understood. In this paper, we introduce value positivity and uniform value positivity, two properties that refine the notion of optimality in the context of polynomially perturbed matrix games. The first concept captures how the value depends on the perturbation parameter, and the second consists of the existence of a fixed strategy that guarantees the value of the unperturbed matrix game for every sufficiently small positive parameter. We provide polynomial-time algorithms to check whether a polynomially perturbed matrix game satisfies these properties. We further provide the functional form for a parameterized optimal strategy and the value function. Finally, we translate our results to linear programming and stochastic games, where value positivity is related to the existence of robust solutions."}],"issue":"4","oa_version":"None","day":"01","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Miquel","full_name":"Oliu-Barton, Miquel","last_name":"Oliu-Barton"},{"id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","first_name":"Raimundo J","last_name":"Saona Urmeneta","full_name":"Saona Urmeneta, Raimundo J","orcid":"0000-0001-5103-038X"}],"article_type":"original","publication_status":"published","language":[{"iso":"eng"}],"isi":1,"project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"title":"Value-positivity for matrix games","type":"journal_article","date_created":"2024-10-09T07:02:20Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2024","publication_identifier":{"issn":["0364-765X"],"eissn":["1526-5471"]},"doi":"10.1287/moor.2022.0332","acknowledgement":"This research was supported by Fondation CFM pour la Recherche, the H2020 European Research Council [Grant ERC-CoG-863818 (ForM-SMArt)], the Austrian Science Fund [Grant 10.55776/COE12], ANID Chile [Grant ACT210005], and Agence Nationale de la Recherche [Grant ANR-21-CE40-0020].","month":"10","publisher":"Institute for Operations Research and the Management Sciences","intvolume":"        50","citation":{"ieee":"K. Chatterjee, M. Oliu-Barton, and R. J. Saona Urmeneta, “Value-positivity for matrix games,” <i>Mathematics of Operations Research</i>, vol. 50, no. 4. Institute for Operations Research and the Management Sciences, pp. 2433–3282, 2024.","chicago":"Chatterjee, Krishnendu, Miquel Oliu-Barton, and Raimundo J Saona Urmeneta. “Value-Positivity for Matrix Games.” <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences, 2024. <a href=\"https://doi.org/10.1287/moor.2022.0332\">https://doi.org/10.1287/moor.2022.0332</a>.","ama":"Chatterjee K, Oliu-Barton M, Saona Urmeneta RJ. Value-positivity for matrix games. <i>Mathematics of Operations Research</i>. 2024;50(4):2433-3282. doi:<a href=\"https://doi.org/10.1287/moor.2022.0332\">10.1287/moor.2022.0332</a>","ista":"Chatterjee K, Oliu-Barton M, Saona Urmeneta RJ. 2024. Value-positivity for matrix games. Mathematics of Operations Research. 50(4), 2433–3282.","short":"K. Chatterjee, M. Oliu-Barton, R.J. Saona Urmeneta, Mathematics of Operations Research 50 (2024) 2433–3282.","apa":"Chatterjee, K., Oliu-Barton, M., &#38; Saona Urmeneta, R. J. (2024). Value-positivity for matrix games. <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences. <a href=\"https://doi.org/10.1287/moor.2022.0332\">https://doi.org/10.1287/moor.2022.0332</a>","mla":"Chatterjee, Krishnendu, et al. “Value-Positivity for Matrix Games.” <i>Mathematics of Operations Research</i>, vol. 50, no. 4, Institute for Operations Research and the Management Sciences, 2024, pp. 2433–3282, doi:<a href=\"https://doi.org/10.1287/moor.2022.0332\">10.1287/moor.2022.0332</a>."},"OA_type":"closed access","quality_controlled":"1","volume":50,"article_processing_charge":"No","ec_funded":1,"page":"2433-3282","corr_author":"1","_id":"18266","status":"public","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"scopus_import":"1","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"20234"}]},"date_updated":"2026-04-07T12:31:21Z"},{"_id":"18600","status":"public","department":[{"_id":"KrCh"}],"arxiv":1,"scopus_import":"1","oa":1,"date_updated":"2025-09-08T14:45:11Z","month":"11","OA_place":"repository","publisher":"Springer Nature","intvolume":"     14550","citation":{"ieee":"R. Andriushchenko <i>et al.</i>, “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report,” in <i>TOOLympics Challenge 2023</i>, 2024, vol. 14550, pp. 90–146.","ama":"Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In: <i>TOOLympics Challenge 2023</i>. Vol 14550. Springer Nature; 2024:90-146. doi:<a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">10.1007/978-3-031-67695-6_4</a>","chicago":"Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” In <i>TOOLympics Challenge 2023</i>, 14550:90–146. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">https://doi.org/10.1007/978-3-031-67695-6_4</a>.","short":"R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A. Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer, J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters, L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer Nature, 2024, pp. 90–146.","ista":"Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550, 90–146.","apa":"Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E. M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In <i>TOOLympics Challenge 2023</i> (Vol. 14550, pp. 90–146). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">https://doi.org/10.1007/978-3-031-67695-6_4</a>","mla":"Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” <i>TOOLympics Challenge 2023</i>, vol. 14550, Springer Nature, 2024, pp. 90–146, doi:<a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">10.1007/978-3-031-67695-6_4</a>."},"OA_type":"green","volume":14550,"quality_controlled":"1","article_processing_charge":"No","page":"90-146","publication_status":"published","language":[{"iso":"eng"}],"isi":1,"type":"conference","title":"Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report","alternative_title":["LNCS"],"date_created":"2024-12-01T23:01:53Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2024","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031676949"]},"doi":"10.1007/978-3-031-67695-6_4","acknowledgement":"The authors are ordered alphabetically. This work was supported by DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075 (CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA), by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006 (SMARTITUDE), and by NWO VENI grant 639.021.754.","external_id":{"isi":["001434957500004"],"arxiv":["2405.13583"]},"date_published":"2024-11-01T00:00:00Z","publication":"TOOLympics Challenge 2023","abstract":[{"text":"The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today’s active areas and tomorrow’s challenges in tool-focused research for quantitative verification.","lang":"eng"}],"main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.2405.13583"}],"oa_version":"Preprint","day":"01","author":[{"last_name":"Andriushchenko","full_name":"Andriushchenko, Roman","first_name":"Roman"},{"first_name":"Alexander","last_name":"Bork","full_name":"Bork, Alexander"},{"full_name":"Budde, Carlos E.","last_name":"Budde","first_name":"Carlos E."},{"first_name":"Milan","full_name":"Češka, Milan","last_name":"Češka"},{"first_name":"Kush","last_name":"Grover","full_name":"Grover, Kush"},{"first_name":"Ernst Moritz","last_name":"Hahn","full_name":"Hahn, Ernst Moritz"},{"first_name":"Arnd","last_name":"Hartmanns","full_name":"Hartmanns, Arnd"},{"first_name":"Bryant","full_name":"Israelsen, Bryant","last_name":"Israelsen"},{"full_name":"Jansen, Nils","last_name":"Jansen","first_name":"Nils"},{"full_name":"Jeppson, Joshua","last_name":"Jeppson","first_name":"Joshua"},{"first_name":"Sebastian","full_name":"Junges, Sebastian","last_name":"Junges"},{"first_name":"Maximilian A.","last_name":"Köhl","full_name":"Köhl, Maximilian A."},{"last_name":"Könighofer","full_name":"Könighofer, Bettina","first_name":"Bettina"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan"},{"full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"first_name":"David","full_name":"Parker, David","last_name":"Parker"},{"first_name":"Stefan","last_name":"Pranger","full_name":"Pranger, Stefan"},{"full_name":"Quatmann, Tim","last_name":"Quatmann","first_name":"Tim"},{"first_name":"Enno","full_name":"Ruijters, Enno","last_name":"Ruijters"},{"last_name":"Taylor","full_name":"Taylor, Landon","first_name":"Landon"},{"first_name":"Matthias","full_name":"Volk, Matthias","last_name":"Volk"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881"},{"first_name":"Zhen","full_name":"Zhang, Zhen","last_name":"Zhang"}]},{"type":"journal_article","title":"Stochastic processes with expected stopping time","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"isi":1,"language":[{"iso":"eng"}],"publication_status":"published","DOAJ_listed":"1","article_type":"original","doi":"10.46298/lmcs-20(4:11)2024","acknowledgement":"The authors are grateful to the anonymous reviewers of LICS 2021 and of a previous version of this paper for insightful comments that helped improving the presentation. The research presented in this paper was partially supported by the grant ERC CoG 863818 (ForM-SMArt).","publication_identifier":{"eissn":["1860-5974"]},"year":"2024","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2024-12-08T23:01:56Z","alternative_title":["LMCS"],"abstract":[{"lang":"eng","text":"Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs."}],"publication":"Logical Methods in Computer Science","date_published":"2024-11-12T00:00:00Z","file":[{"date_updated":"2024-12-09T08:38:48Z","creator":"dernst","file_size":416814,"date_created":"2024-12-09T08:38:48Z","content_type":"application/pdf","success":1,"checksum":"b3315c74ce18ce0a30ed33d8c9972992","access_level":"open_access","relation":"main_file","file_id":"18633","file_name":"2024_LMCS_Chatterjee.pdf"}],"external_id":{"isi":["001367316400002"],"arxiv":["2104.07278"]},"author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"}],"day":"12","oa_version":"Published Version","issue":"4","scopus_import":"1","arxiv":1,"department":[{"_id":"KrCh"}],"file_date_updated":"2024-12-09T08:38:48Z","ddc":["000"],"status":"public","corr_author":"1","_id":"18630","date_updated":"2025-09-08T14:54:14Z","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"10004"}]},"oa":1,"intvolume":"        20","publisher":"EPI Sciences","month":"11","OA_place":"publisher","page":"11:1-11:34","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"article_processing_charge":"Yes","ec_funded":1,"OA_type":"gold","quality_controlled":"1","volume":20,"citation":{"ista":"Chatterjee K, Doyen L. 2024. Stochastic processes with expected stopping time. Logical Methods in Computer Science. 20(4), 11:1-11:34.","short":"K. Chatterjee, L. Doyen, Logical Methods in Computer Science 20 (2024) 11:1-11:34.","apa":"Chatterjee, K., &#38; Doyen, L. (2024). Stochastic processes with expected stopping time. <i>Logical Methods in Computer Science</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/lmcs-20(4:11)2024\">https://doi.org/10.46298/lmcs-20(4:11)2024</a>","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4, EPI Sciences, 2024, p. 11:1-11:34, doi:<a href=\"https://doi.org/10.46298/lmcs-20(4:11)2024\">10.46298/lmcs-20(4:11)2024</a>.","ieee":"K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4. EPI Sciences, p. 11:1-11:34, 2024.","ama":"Chatterjee K, Doyen L. Stochastic processes with expected stopping time. <i>Logical Methods in Computer Science</i>. 2024;20(4):11:1-11:34. doi:<a href=\"https://doi.org/10.46298/lmcs-20(4:11)2024\">10.46298/lmcs-20(4:11)2024</a>","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” <i>Logical Methods in Computer Science</i>. EPI Sciences, 2024. <a href=\"https://doi.org/10.46298/lmcs-20(4:11)2024\">https://doi.org/10.46298/lmcs-20(4:11)2024</a>."},"has_accepted_license":"1"},{"OA_place":"publisher","month":"12","publisher":"National Academy of Sciences","intvolume":"       121","has_accepted_license":"1","citation":{"mla":"Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation for Spatial Games.” <i>Proceedings of the National Academy of Sciences of the United States of America</i>, vol. 121, no. 50, e2405605121, National Academy of Sciences, 2024, doi:<a href=\"https://doi.org/10.1073/pnas.2405605121\">10.1073/pnas.2405605121</a>.","apa":"Svoboda, J., &#38; Chatterjee, K. (2024). Density amplifiers of cooperation for spatial games. <i>Proceedings of the National Academy of Sciences of the United States of America</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.2405605121\">https://doi.org/10.1073/pnas.2405605121</a>","short":"J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences of the United States of America 121 (2024).","ista":"Svoboda J, Chatterjee K. 2024. Density amplifiers of cooperation for spatial games. Proceedings of the National Academy of Sciences of the United States of America. 121(50), e2405605121.","ama":"Svoboda J, Chatterjee K. Density amplifiers of cooperation for spatial games. <i>Proceedings of the National Academy of Sciences of the United States of America</i>. 2024;121(50). doi:<a href=\"https://doi.org/10.1073/pnas.2405605121\">10.1073/pnas.2405605121</a>","chicago":"Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation for Spatial Games.” <i>Proceedings of the National Academy of Sciences of the United States of America</i>. National Academy of Sciences, 2024. <a href=\"https://doi.org/10.1073/pnas.2405605121\">https://doi.org/10.1073/pnas.2405605121</a>.","ieee":"J. Svoboda and K. Chatterjee, “Density amplifiers of cooperation for spatial games,” <i>Proceedings of the National Academy of Sciences of the United States of America</i>, vol. 121, no. 50. National Academy of Sciences, 2024."},"volume":121,"OA_type":"hybrid","quality_controlled":"1","article_processing_charge":"Yes","ec_funded":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)"},"_id":"18703","corr_author":"1","status":"public","ddc":["000"],"file_date_updated":"2025-01-02T12:14:15Z","department":[{"_id":"KrCh"}],"scopus_import":"1","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"20138"}]},"oa":1,"date_updated":"2026-04-07T11:49:11Z","external_id":{"isi":["001379596100014"],"pmid":["39642209"]},"file":[{"access_level":"open_access","relation":"main_file","file_id":"18721","file_name":"2024_PNAS_Svoboda.pdf","checksum":"0115e9090b478e0644308c6dab58605b","file_size":2491151,"date_created":"2025-01-02T12:14:15Z","content_type":"application/pdf","success":1,"date_updated":"2025-01-02T12:14:15Z","creator":"dernst"}],"date_published":"2024-12-10T00:00:00Z","publication":"Proceedings of the National Academy of Sciences of the United States of America","abstract":[{"text":"Spatial games provide a simple and elegant mathematical model to study the evolution of cooperation in networks. In spatial games, individuals reside in vertices, adopt simple strategies, and interact with neighbors to receive a payoff. Depending on their own and neighbors’ payoffs, individuals can change their strategy. The payoff is determined by the Prisoners’ Dilemma, a classical matrix game, where players cooperate or defect. While cooperation is the desired behavior, defection provides a higher payoff for a selfish individual. There are many theoretical and empirical studies related to the role of the network in the evolution of cooperation. However, the fundamental question of whether there exist networks that for low initial cooperation rate ensure a high chance of fixation, i.e., cooperation spreads across the whole population, has remained elusive for spatial games with strong selection. In this work, we answer this fundamental question in the affirmative by presenting network structures that ensure high fixation probability for cooperators in the strong selection regime. Besides, our structures have many desirable properties: (a) they ensure the spread of cooperation even for a low initial density of cooperation and high temptation of defection, (b) they have constant degrees, and (c) the number of steps, until cooperation spreads, is at most quadratic in the size of the network.","lang":"eng"}],"issue":"50","pmid":1,"oa_version":"Published Version","day":"10","APC_amount":"3143,76 EUR","author":[{"last_name":"Svoboda","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","orcid":"0000-0002-1419-3267"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"}],"article_type":"original","publication_status":"published","isi":1,"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"}],"type":"journal_article","title":"Density amplifiers of cooperation for spatial games","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","date_created":"2024-12-22T23:01:47Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_number":"e2405605121","year":"2024","publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"doi":"10.1073/pnas.2405605121","acknowledgement":"J.S. and K.C. were supported by the European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12."},{"ec_funded":1,"article_processing_charge":"No","OA_type":"green","quality_controlled":"1","citation":{"ieee":"E. Ceylan, K. Chatterjee, S. Schmid, and J. Svoboda, “Congestion-free rerouting of network flows: Hardness and an FPT algorithm,” in <i>NOMS 2024-2024 IEEE Network Operations and Management Symposium</i>, Seoul, Republic of Korea, 2024.","ama":"Ceylan E, Chatterjee K, Schmid S, Svoboda J. Congestion-free rerouting of network flows: Hardness and an FPT algorithm. In: <i>NOMS 2024-2024 IEEE Network Operations and Management Symposium</i>. IEEE; 2024. doi:<a href=\"https://doi.org/10.1109/noms59830.2024.10575579\">10.1109/noms59830.2024.10575579</a>","chicago":"Ceylan, Esra, Krishnendu Chatterjee, Stefan Schmid, and Jakub Svoboda. “Congestion-Free Rerouting of Network Flows: Hardness and an FPT Algorithm.” In <i>NOMS 2024-2024 IEEE Network Operations and Management Symposium</i>. IEEE, 2024. <a href=\"https://doi.org/10.1109/noms59830.2024.10575579\">https://doi.org/10.1109/noms59830.2024.10575579</a>.","ista":"Ceylan E, Chatterjee K, Schmid S, Svoboda J. 2024. Congestion-free rerouting of network flows: Hardness and an FPT algorithm. NOMS 2024-2024 IEEE Network Operations and Management Symposium. NOMS: Network Operations and Management Symposiu .","short":"E. Ceylan, K. Chatterjee, S. Schmid, J. Svoboda, in:, NOMS 2024-2024 IEEE Network Operations and Management Symposium, IEEE, 2024.","mla":"Ceylan, Esra, et al. “Congestion-Free Rerouting of Network Flows: Hardness and an FPT Algorithm.” <i>NOMS 2024-2024 IEEE Network Operations and Management Symposium</i>, IEEE, 2024, doi:<a href=\"https://doi.org/10.1109/noms59830.2024.10575579\">10.1109/noms59830.2024.10575579</a>.","apa":"Ceylan, E., Chatterjee, K., Schmid, S., &#38; Svoboda, J. (2024). Congestion-free rerouting of network flows: Hardness and an FPT algorithm. In <i>NOMS 2024-2024 IEEE Network Operations and Management Symposium</i>. Seoul, Republic of Korea: IEEE. <a href=\"https://doi.org/10.1109/noms59830.2024.10575579\">https://doi.org/10.1109/noms59830.2024.10575579</a>"},"publisher":"IEEE","OA_place":"other","month":"05","date_updated":"2025-11-05T07:34:27Z","oa":1,"scopus_import":"1","department":[{"_id":"KrCh"}],"status":"public","_id":"18925","corr_author":"1","author":[{"id":"cb1ca1d8-dcc0-11ef-baa5-9f1b3ef75933","first_name":"Esra","last_name":"Ceylan","full_name":"Ceylan, Esra"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Stefan","full_name":"Schmid, Stefan","last_name":"Schmid"},{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","full_name":"Svoboda, Jakub"}],"day":"01","oa_version":"Submitted Version","main_file_link":[{"open_access":"1","url":"https://schmiste.github.io/noms24.pdf"}],"abstract":[{"lang":"eng","text":"Given the increasingly stringent requirements on the performance and efficiency of communication networks, over the last years, great efforts have been made to render networks more flexible and programmable. In particular, modern networks support a flexible rerouting of flows, e.g., depending on the dynamically changing traffic or network conditions. However, the underlying algorithmic problems are still not well-understood today.In this paper, we revisit the k-Network Flow Update problem that asks for a schedule to reroute k unsplittable flows from their current paths to the given new paths, in a congestion-free manner in a capacitated network. We show that the problem is already NP-hard for three acyclic flows on simple directed graphs. Our main contribution is an efficient algorithm for sparse networks; specifically the algorithm is fixed parameter tractable in the number of flows and the treewidth of a graph that is the union of all flows. Our results also settle the open complexity question in the literature."}],"publication":"NOMS 2024-2024 IEEE Network Operations and Management Symposium","date_published":"2024-05-01T00:00:00Z","external_id":{"isi":["001270140300143"]},"doi":"10.1109/noms59830.2024.10575579","acknowledgement":"Research was supported by the Austrian Science Fund (FWF), project I 5025-N (DELTA), 2020-2024. Esra Ceylan’s research was supported by FFG, FEMtech Praktika für Studentinnen. Jakub Svoboda and Krishnendu Chatterjee were supported by the European Research Council (ERC) CoG 863818 (ForM-SMArt).","year":"2024","publication_identifier":{"eissn":["2374-9709"],"isbn":["9798350327946"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2024-05-10","location":"Seoul, Republic of Korea","name":"NOMS: Network Operations and Management Symposiu ","start_date":"2024-05-06"},"date_created":"2025-01-27T15:06:45Z","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"},{"name":"Graphical Games","grant_number":"894907","_id":"bd622a5c-d553-11ed-ba76-bae280ba8aff"}],"title":"Congestion-free rerouting of network flows: Hardness and an FPT algorithm","type":"conference","isi":1,"language":[{"iso":"eng"}],"publication_status":"published"},{"quality_controlled":"1","OA_type":"green","volume":235,"citation":{"apa":"Svoboda, J., Bansal, S., &#38; Chatterjee, K. (2024). Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. In <i>41st International Conference on Machine Learning</i> (Vol. 235, pp. 47331–47344). Vienna, Austria: ML Research Press.","mla":"Svoboda, Jakub, et al. “Reinforcement Learning from Reachability Specifications: PAC Guarantees with Expected Conditional Distance.” <i>41st International Conference on Machine Learning</i>, vol. 235, ML Research Press, 2024, pp. 47331–44.","ista":"Svoboda J, Bansal S, Chatterjee K. 2024. Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. 41st International Conference on Machine Learning. ICML: International Conference on Machine Learning, PMLR, vol. 235, 47331–47344.","short":"J. Svoboda, S. Bansal, K. Chatterjee, in:, 41st International Conference on Machine Learning, ML Research Press, 2024, pp. 47331–47344.","chicago":"Svoboda, Jakub, Suguman Bansal, and Krishnendu Chatterjee. “Reinforcement Learning from Reachability Specifications: PAC Guarantees with Expected Conditional Distance.” In <i>41st International Conference on Machine Learning</i>, 235:47331–44. ML Research Press, 2024.","ama":"Svoboda J, Bansal S, Chatterjee K. Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. In: <i>41st International Conference on Machine Learning</i>. Vol 235. ML Research Press; 2024:47331-47344.","ieee":"J. Svoboda, S. Bansal, and K. Chatterjee, “Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance,” in <i>41st International Conference on Machine Learning</i>, Vienna, Austria, 2024, vol. 235, pp. 47331–47344."},"page":"47331-47344","article_processing_charge":"No","month":"07","OA_place":"publisher","intvolume":"       235","publisher":"ML Research Press","oa":1,"date_updated":"2025-01-30T07:46:16Z","status":"public","_id":"18974","corr_author":"1","scopus_import":"1","department":[{"_id":"KrCh"}],"oa_version":"Preprint","main_file_link":[{"url":"https://openreview.net/forum?id=mXUDDL4r1Q","open_access":"1"}],"author":[{"full_name":"Svoboda, Jakub","last_name":"Svoboda","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267"},{"full_name":"Bansal, Suguman","last_name":"Bansal","first_name":"Suguman"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"}],"day":"29","publication":"41st International Conference on Machine Learning","date_published":"2024-07-29T00:00:00Z","abstract":[{"lang":"eng","text":"Reinforcement Learning (RL) from temporal logical specifications is a fundamental problem in sequential decision making. One of the basic and core such specification is the reachability specification that requires a target set to be eventually visited. Despite strong empirical results for RL from such specifications, the theoretical guarantees are bleak, including the impossibility of Probably Approximately Correct (PAC) guarantee for reachability specifications. Given the impossibility result, in this work we consider the problem of RL from reachability specifications along with the information of expected conditional distance (ECD). We present (a) lower bound results which establish the necessity of ECD information for PAC guarantees and (b) an algorithm that establishes PAC-guarantees given the ECD information. To the best of our knowledge, this is the first RL from reachability specifications that does not make any assumptions on the underlying environment to learn policies."}],"conference":{"start_date":"2024-07-21","name":"ICML: International Conference on Machine Learning","location":"Vienna, Austria","end_date":"2024-07-27"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2025-01-30T07:45:22Z","alternative_title":["PMLR"],"year":"2024","publication_status":"published","type":"conference","title":"Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance","language":[{"iso":"eng"}]},{"oa_version":"Published Version","day":"21","author":[{"first_name":"Stefan","full_name":"Schmid, Stefan","last_name":"Schmid"},{"last_name":"Svoboda","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","orcid":"0000-0002-1419-3267"},{"orcid":"0009-0001-3676-4809","full_name":"Yeo, Michelle X","last_name":"Yeo","first_name":"Michelle X","id":"2D82B818-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2024-03-21T00:00:00Z","external_id":{"isi":["001168211400001"]},"file":[{"checksum":"efd5b7e738bf845312ba53889a3e13e4","access_level":"open_access","relation":"main_file","file_name":"2024_TheorComputerScience_Schmid.pdf","file_id":"17263","date_updated":"2024-07-16T12:02:25Z","creator":"dernst","file_size":603570,"success":1,"date_created":"2024-07-16T12:02:25Z","content_type":"application/pdf"}],"publication":"Theoretical Computer Science","abstract":[{"lang":"eng","text":"We consider a natural problem dealing with weighted packet selection across a rechargeable link, which e.g., finds applications in cryptocurrency networks. The capacity of a link (u, v) is determined by how many nodes u and v allocate for this link. Specifically, the input is a finite ordered sequence of packets that arrive in both directions along a link. Given (u, v) and a packet of weight x going from u to v, node u can either accept or reject the packet. If u accepts the packet, the capacity on link (u, v) decreases by x. Correspondingly, v's capacity on \r\n increases by x. If a node rejects the packet, this will entail a cost affinely linear in the weight of the packet. A link is “rechargeable” in the sense that the total capacity of the link has to remain constant, but the allocation of capacity at the ends of the link can depend arbitrarily on the nodes' decisions. The goal is to minimise the sum of the capacity injected into the link and the cost of rejecting packets. We show that the problem is NP-hard, but can be approximated efficiently with a ratio of (1+E) . (1+3)  for some arbitrary E>0."}],"date_created":"2024-01-16T13:40:41Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_number":"114353","publication_identifier":{"issn":["0304-3975"]},"year":"2024","acknowledgement":"We thank Mahsa Bastankhah and Mohammad Ali Maddah-Ali for fruitful discussions about different variants of the problem. This work is supported by the European Research Council (ERC) Consolidator Project 864228 (AdjustNet), 2020-2025, the ERC CoG 863818 (ForM-SMArt), and the German Research Foundation (DFG) grant 470029389 (FlexNets), 2021-2024.","doi":"10.1016/j.tcs.2023.114353","keyword":["General Computer Science","Theoretical Computer Science"],"article_type":"original","publication_status":"published","language":[{"iso":"eng"}],"isi":1,"title":"Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation","type":"journal_article","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"citation":{"ista":"Schmid S, Svoboda J, Yeo MX. 2024. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. Theoretical Computer Science. 989, 114353.","short":"S. Schmid, J. Svoboda, M.X. Yeo, Theoretical Computer Science 989 (2024).","apa":"Schmid, S., Svoboda, J., &#38; Yeo, M. X. (2024). Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2023.114353\">https://doi.org/10.1016/j.tcs.2023.114353</a>","mla":"Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” <i>Theoretical Computer Science</i>, vol. 989, 114353, Elsevier, 2024, doi:<a href=\"https://doi.org/10.1016/j.tcs.2023.114353\">10.1016/j.tcs.2023.114353</a>.","ieee":"S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation,” <i>Theoretical Computer Science</i>, vol. 989. Elsevier, 2024.","chicago":"Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” <i>Theoretical Computer Science</i>. Elsevier, 2024. <a href=\"https://doi.org/10.1016/j.tcs.2023.114353\">https://doi.org/10.1016/j.tcs.2023.114353</a>.","ama":"Schmid S, Svoboda J, Yeo MX. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. <i>Theoretical Computer Science</i>. 2024;989. doi:<a href=\"https://doi.org/10.1016/j.tcs.2023.114353\">10.1016/j.tcs.2023.114353</a>"},"has_accepted_license":"1","volume":989,"quality_controlled":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"ec_funded":1,"article_processing_charge":"Yes (via OA deal)","month":"03","publisher":"Elsevier","intvolume":"       989","oa":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"19985"}]},"date_updated":"2025-12-02T14:02:37Z","corr_author":"1","_id":"14820","status":"public","department":[{"_id":"KrCh"},{"_id":"KrPi"}],"file_date_updated":"2024-07-16T12:02:25Z","ddc":["000"],"scopus_import":"1"},{"oa_version":"Published Version","day":"18","author":[{"first_name":"Juho","full_name":"Hirvonen, Juho","last_name":"Hirvonen"},{"last_name":"Schmid","full_name":"Schmid, Laura","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","first_name":"Laura","orcid":"0000-0002-6978-7329"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Stefan","full_name":"Schmid, Stefan","last_name":"Schmid"}],"date_published":"2024-01-18T00:00:00Z","file":[{"file_name":"2024_LIPICs_Hirvonen.pdf","file_id":"15028","access_level":"open_access","relation":"main_file","checksum":"4fc7eea6e4ba140b904781fc7df868ec","success":1,"content_type":"application/pdf","date_created":"2024-02-26T09:04:58Z","file_size":867363,"creator":"dernst","date_updated":"2024-02-26T09:04:58Z"}],"external_id":{"isi":["001585185800011"],"arxiv":["2102.13457"]},"publication":"27th International Conference on Principles of Distributed Systems","abstract":[{"lang":"eng","text":"Graphical games are a useful framework for modeling the interactions of (selfish) agents who are connected via an underlying topology and whose behaviors influence each other. They have wide applications ranging from computer science to economics and biology. Yet, even though an agent’s payoff only depends on the actions of their direct neighbors in graphical games, computing the Nash equilibria and making statements about the convergence time of \"natural\" local dynamics in particular can be highly challenging. In this work, we present a novel approach for classifying complexity of Nash equilibria in graphical games by establishing a connection to local graph algorithms, a subfield of distributed computing. In particular, we make the observation that the equilibria of graphical games are equivalent to locally verifiable labelings (LVL) in graphs; vertex labelings which are verifiable with constant-round local algorithms. This connection allows us to derive novel lower bounds on the convergence time to equilibrium of best-response dynamics in graphical games. Since we establish that distributed convergence can sometimes be provably slow, we also introduce and give bounds on an intuitive notion of \"time-constrained\" inefficiency of best responses. We exemplify how our results can be used in the implementation of mechanisms that ensure convergence of best responses to a Nash equilibrium. Our results thus also give insight into the convergence of strategy-proof algorithms for graphical games, which is still not well understood."}],"date_created":"2024-02-18T23:01:01Z","alternative_title":["LIPIcs"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Tokyo, Japan","name":"OPODIS: Conference on Principles of Distributed Systems","start_date":"2023-12-06","end_date":"2023-12-08"},"year":"2024","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773089"]},"article_number":"11","acknowledgement":"This work was partially funded by the Academy of Finland, grant 314888, the European Research Council CoG 863818 (ForM-SMArt), and the Austrian Science Fund (FWF) project I 4800-N (ADVISE). LS was supported by the Stochastic Analysis and Application Research Center (SAARC) under National Research Foundation of Korea grant NRF-2019R1A5A1028324.","doi":"10.4230/LIPIcs.OPODIS.2023.11","publication_status":"published","language":[{"iso":"eng"}],"isi":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"title":"On the convergence time in graphical games: A locality-sensitive approach","type":"conference","has_accepted_license":"1","citation":{"short":"J. Hirvonen, L. Schmid, K. Chatterjee, S. Schmid, in:, 27th International Conference on Principles of Distributed Systems, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","ista":"Hirvonen J, Schmid L, Chatterjee K, Schmid S. 2024. On the convergence time in graphical games: A locality-sensitive approach. 27th International Conference on Principles of Distributed Systems. OPODIS: Conference on Principles of Distributed Systems, LIPIcs, vol. 286, 11.","mla":"Hirvonen, Juho, et al. “On the Convergence Time in Graphical Games: A Locality-Sensitive Approach.” <i>27th International Conference on Principles of Distributed Systems</i>, vol. 286, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11\">10.4230/LIPIcs.OPODIS.2023.11</a>.","apa":"Hirvonen, J., Schmid, L., Chatterjee, K., &#38; Schmid, S. (2024). On the convergence time in graphical games: A locality-sensitive approach. In <i>27th International Conference on Principles of Distributed Systems</i> (Vol. 286). Tokyo, Japan: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11\">https://doi.org/10.4230/LIPIcs.OPODIS.2023.11</a>","ieee":"J. Hirvonen, L. Schmid, K. Chatterjee, and S. Schmid, “On the convergence time in graphical games: A locality-sensitive approach,” in <i>27th International Conference on Principles of Distributed Systems</i>, Tokyo, Japan, 2024, vol. 286.","ama":"Hirvonen J, Schmid L, Chatterjee K, Schmid S. On the convergence time in graphical games: A locality-sensitive approach. In: <i>27th International Conference on Principles of Distributed Systems</i>. Vol 286. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11\">10.4230/LIPIcs.OPODIS.2023.11</a>","chicago":"Hirvonen, Juho, Laura Schmid, Krishnendu Chatterjee, and Stefan Schmid. “On the Convergence Time in Graphical Games: A Locality-Sensitive Approach.” In <i>27th International Conference on Principles of Distributed Systems</i>, Vol. 286. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.OPODIS.2023.11\">https://doi.org/10.4230/LIPIcs.OPODIS.2023.11</a>."},"volume":286,"quality_controlled":"1","article_processing_charge":"No","ec_funded":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"month":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","intvolume":"       286","oa":1,"date_updated":"2025-12-02T13:38:16Z","corr_author":"1","_id":"15006","status":"public","ddc":["000"],"file_date_updated":"2024-02-26T09:04:58Z","department":[{"_id":"KrCh"}],"arxiv":1,"scopus_import":"1"},{"day":"05","APC_amount":"3041,76 EUR","author":[{"first_name":"Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","full_name":"Hübner, Valentin","last_name":"Hübner","orcid":"0009-0001-5009-4987"},{"first_name":"Manuel","full_name":"Staab, Manuel","last_name":"Staab"},{"orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Hilbe","full_name":"Hilbe, Christian"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Kleshnina","full_name":"Kleshnina, Maria","first_name":"Maria"}],"issue":"10","oa_version":"Published Version","pmid":1,"abstract":[{"lang":"eng","text":"Direct reciprocity is a powerful mechanism for cooperation in social dilemmas. The very logic of reciprocity, however, seems to require that individuals are symmetric, and that everyone has the same means to influence each others’ payoffs. Yet in many applications, individuals are asymmetric. Herein, we study the effect of asymmetry in linear public good games. Individuals may differ in their endowments (their ability to contribute to a public good) and in their productivities (how effective their contributions are). Given the individuals’ productivities, we ask which allocation of endowments is optimal for cooperation. To this end, we consider two notions of optimality. The first notion focuses on the resilience of cooperation. The respective endowment distribution ensures that full cooperation is feasible even under the most adverse conditions. The second notion focuses on efficiency. The corresponding endowment distribution maximizes group welfare. Using analytical methods, we fully characterize these two endowment distributions. This analysis reveals that both optimality notions favor some endowment inequality: More productive players ought to get higher endowments. Yet the two notions disagree on how unequal endowments are supposed to be. A focus on resilience results in less inequality. With additional simulations, we show that the optimal endowment allocation needs to account for both the resilience and the efficiency of cooperation."}],"date_published":"2024-03-05T00:00:00Z","external_id":{"pmid":["38408249"],"isi":["001207786500004"]},"file":[{"creator":"dernst","date_updated":"2024-03-12T13:12:22Z","success":1,"date_created":"2024-03-12T13:12:22Z","content_type":"application/pdf","file_size":2203220,"checksum":"068520e3efd4d008bb9177e8aedb7d22","file_name":"2024_PNAS_Huebner.pdf","file_id":"15109","relation":"main_file","access_level":"open_access"}],"publication":"Proceedings of the National Academy of Sciences of the United States of America","year":"2024","article_number":"e2315558121","publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"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.), the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie Grant Agreement #754411 and the French Agence Nationale de la Recherche (under the Investissement d’Avenir Programme, ANR-17-EURE-0010) (to M.K.).","doi":"10.1073/pnas.2315558121","date_created":"2024-03-05T09:18:49Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"isi":1,"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"}],"type":"journal_article","title":"Efficiency and resilience of cooperation in asymmetric social dilemmas","article_type":"original","publication_status":"published","ec_funded":1,"article_processing_charge":"Yes (in subscription journal)","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)"},"has_accepted_license":"1","citation":{"short":"V. Hübner, M. Staab, C. Hilbe, K. Chatterjee, M. Kleshnina, Proceedings of the National Academy of Sciences of the United States of America 121 (2024).","ista":"Hübner V, Staab M, Hilbe C, Chatterjee K, Kleshnina M. 2024. Efficiency and resilience of cooperation in asymmetric social dilemmas. Proceedings of the National Academy of Sciences of the United States of America. 121(10), e2315558121.","mla":"Hübner, Valentin, et al. “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.” <i>Proceedings of the National Academy of Sciences of the United States of America</i>, vol. 121, no. 10, e2315558121, National Academy of Sciences, 2024, doi:<a href=\"https://doi.org/10.1073/pnas.2315558121\">10.1073/pnas.2315558121</a>.","apa":"Hübner, V., Staab, M., Hilbe, C., Chatterjee, K., &#38; Kleshnina, M. (2024). Efficiency and resilience of cooperation in asymmetric social dilemmas. <i>Proceedings of the National Academy of Sciences of the United States of America</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.2315558121\">https://doi.org/10.1073/pnas.2315558121</a>","ieee":"V. Hübner, M. Staab, C. Hilbe, K. Chatterjee, and M. Kleshnina, “Efficiency and resilience of cooperation in asymmetric social dilemmas,” <i>Proceedings of the National Academy of Sciences of the United States of America</i>, vol. 121, no. 10. National Academy of Sciences, 2024.","chicago":"Hübner, Valentin, Manuel Staab, Christian Hilbe, Krishnendu Chatterjee, and Maria Kleshnina. “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.” <i>Proceedings of the National Academy of Sciences of the United States of America</i>. National Academy of Sciences, 2024. <a href=\"https://doi.org/10.1073/pnas.2315558121\">https://doi.org/10.1073/pnas.2315558121</a>.","ama":"Hübner V, Staab M, Hilbe C, Chatterjee K, Kleshnina M. Efficiency and resilience of cooperation in asymmetric social dilemmas. <i>Proceedings of the National Academy of Sciences of the United States of America</i>. 2024;121(10). doi:<a href=\"https://doi.org/10.1073/pnas.2315558121\">10.1073/pnas.2315558121</a>"},"volume":121,"OA_type":"hybrid","quality_controlled":"1","publisher":"National Academy of Sciences","intvolume":"       121","OA_place":"publisher","month":"03","date_updated":"2026-04-07T12:30:56Z","oa":1,"related_material":{"link":[{"description":"News on ISTA Website","url":"https://ista.ac.at/en/news/what-math-tells-us-about-social-dilemmas/","relation":"press_release"}],"record":[{"status":"public","relation":"research_data","id":"15108"},{"relation":"dissertation_contains","status":"public","id":"19903"}]},"ddc":["000"],"file_date_updated":"2024-03-12T13:12:22Z","department":[{"_id":"KrCh"}],"scopus_import":"1","_id":"15083","corr_author":"1","status":"public"},{"year":"2024","doi":"10.5281/ZENODO.10639167","date_updated":"2025-09-04T12:14:54Z","related_material":{"record":[{"id":"15083","status":"public","relation":"used_in_publication"}]},"date_created":"2024-03-12T13:02:58Z","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"ddc":["000"],"type":"research_data_reference","title":"Computer code for \"Efficiency and resilience of cooperation in asymmetric social dilemmas\"","_id":"15108","corr_author":"1","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"article_processing_charge":"No","day":"09","author":[{"last_name":"Hübner","full_name":"Hübner, Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","first_name":"Valentin","orcid":"0009-0001-5009-4987"},{"first_name":"Maria","full_name":"Kleshnina, Maria","last_name":"Kleshnina"}],"citation":{"ista":"Hübner V, Kleshnina M. 2024. Computer code for ‘Efficiency and resilience of cooperation in asymmetric social dilemmas’, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.10639167\">10.5281/ZENODO.10639167</a>.","short":"V. Hübner, M. Kleshnina, (2024).","mla":"Hübner, Valentin, and Maria Kleshnina. <i>Computer Code for “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.”</i> Zenodo, 2024, doi:<a href=\"https://doi.org/10.5281/ZENODO.10639167\">10.5281/ZENODO.10639167</a>.","apa":"Hübner, V., &#38; Kleshnina, M. (2024). Computer code for “Efficiency and resilience of cooperation in asymmetric social dilemmas.” Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.10639167\">https://doi.org/10.5281/ZENODO.10639167</a>","ieee":"V. Hübner and M. Kleshnina, “Computer code for ‘Efficiency and resilience of cooperation in asymmetric social dilemmas.’” Zenodo, 2024.","ama":"Hübner V, Kleshnina M. Computer code for “Efficiency and resilience of cooperation in asymmetric social dilemmas.” 2024. doi:<a href=\"https://doi.org/10.5281/ZENODO.10639167\">10.5281/ZENODO.10639167</a>","chicago":"Hübner, Valentin, and Maria Kleshnina. “Computer Code for ‘Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.’” Zenodo, 2024. <a href=\"https://doi.org/10.5281/ZENODO.10639167\">https://doi.org/10.5281/ZENODO.10639167</a>."},"has_accepted_license":"1","main_file_link":[{"url":"https://10.5281/zenodo.10639167","open_access":"1"}],"oa_version":"Published Version","publisher":"Zenodo","abstract":[{"text":"in the research article \"Efficiency and resilience of cooperation in asymmetric social dilemmas\" (by Valentin Hübner, Manuel Staab, Christian Hilbe, Krishnendu Chatterjee, and Maria Kleshnina).\r\n\r\nWe used different implementations for the case of two and three players, both described below.","lang":"eng"}],"date_published":"2024-02-09T00:00:00Z","month":"02"},{"has_accepted_license":"1","citation":{"chicago":"Svoboda, Jakub, Soham Shrikant Joshi, Josef Tkadlec, and Krishnendu Chatterjee. “Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth Updating.” <i>PLoS Computational Biology</i>. Public Library of Science, 2024. <a href=\"https://doi.org/10.1371/journal.pcbi.1012008\">https://doi.org/10.1371/journal.pcbi.1012008</a>.","ama":"Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. <i>PLoS Computational Biology</i>. 2024;20(3). doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1012008\">10.1371/journal.pcbi.1012008</a>","ieee":"J. Svoboda, S. S. Joshi, J. Tkadlec, and K. Chatterjee, “Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating,” <i>PLoS Computational Biology</i>, vol. 20, no. 3. Public Library of Science, 2024.","apa":"Svoboda, J., Joshi, S. S., Tkadlec, J., &#38; Chatterjee, K. (2024). Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. <i>PLoS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.1012008\">https://doi.org/10.1371/journal.pcbi.1012008</a>","mla":"Svoboda, Jakub, et al. “Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth Updating.” <i>PLoS Computational Biology</i>, vol. 20, no. 3, e1012008, Public Library of Science, 2024, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1012008\">10.1371/journal.pcbi.1012008</a>.","ista":"Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. 2024. Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. PLoS Computational Biology. 20(3), e1012008.","short":"J. Svoboda, S.S. Joshi, J. Tkadlec, K. Chatterjee, PLoS Computational Biology 20 (2024)."},"quality_controlled":"1","OA_type":"gold","volume":20,"ec_funded":1,"article_processing_charge":"Yes","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"OA_place":"publisher","month":"03","publisher":"Public Library of Science","intvolume":"        20","related_material":{"record":[{"id":"20138","relation":"dissertation_contains","status":"public"}]},"oa":1,"date_updated":"2026-04-07T11:49:11Z","corr_author":"1","_id":"15297","status":"public","ddc":["000"],"department":[{"_id":"KrCh"}],"file_date_updated":"2024-08-20T10:52:28Z","arxiv":1,"scopus_import":"1","issue":"3","oa_version":"Published Version","APC_amount":"3149,96 EUR","day":"29","author":[{"full_name":"Svoboda, Jakub","last_name":"Svoboda","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267"},{"id":"f97aac0e-f57c-11ee-93d0-a5a82d8df168","first_name":"Soham Shrikant","last_name":"Joshi","full_name":"Joshi, Soham Shrikant"},{"orcid":"0000-0002-1097-9684","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","last_name":"Tkadlec"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"}],"external_id":{"arxiv":["2401.14914"],"isi":["001194482400002"]},"date_published":"2024-03-29T00:00:00Z","file":[{"relation":"main_file","access_level":"open_access","file_name":"2024_PloSComBio_Svoboda.pdf","file_id":"17450","checksum":"a511cf369d9172beb123fe73f291b5cc","file_size":1425292,"success":1,"content_type":"application/pdf","date_created":"2024-08-20T10:52:28Z","date_updated":"2024-08-20T10:52:28Z","creator":"dernst"}],"publication":"PLoS Computational Biology","abstract":[{"text":"Populations evolve by accumulating advantageous mutations. Every population has some spatial structure that can be modeled by an underlying network. The network then influences the probability that new advantageous mutations fixate. Amplifiers of selection are networks that increase the fixation probability of advantageous mutants, as compared to the unstructured fully-connected network. Whether or not a network is an amplifier depends on the choice of the random process that governs the evolutionary dynamics. Two popular choices are Moran process with Birth-death updating and Moran process with death-Birth updating. Interestingly, while some networks are amplifiers under Birth-death updating and other networks are amplifiers under death-Birth updating, so far no spatial structures have been found that function as an amplifier under both types of updating simultaneously. In this work, we identify networks that act as amplifiers of selection under both versions of the Moran process. The amplifiers are robust, modular, and increase fixation probability for any mutant fitness advantage in a range r ∈ (1, 1.2). To complement this positive result, we also prove that for certain quantities closely related to fixation probability, it is impossible to improve them simultaneously for both versions of the Moran process. Together, our results highlight how the two versions of the Moran process differ and what they have in common.","lang":"eng"}],"date_created":"2024-04-07T22:00:55Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2024","publication_identifier":{"issn":["1553-734X"],"eissn":["1553-7358"]},"article_number":"e1012008","doi":"10.1371/journal.pcbi.1012008","acknowledgement":"We thank Gavin Rees for helpful discussions. J.S., S.J., and K.C were supported by\r\nEuropean Research Council (ERC) CoG 863818 (ForM-SMArt). J.T was supported by Center for Foundations of Modern Computer Science (Charles University project UNCE/SCI/004) and by the project PRIMUS/24/SCI/012 from Charles University. ","article_type":"original","DOAJ_listed":"1","publication_status":"published","isi":1,"language":[{"iso":"eng"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"type":"journal_article","title":"Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating"},{"day":"01","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-6143-1926","id":"4524F760-F248-11E8-B48F-1D18A9856A87","first_name":"Joost P","last_name":"Katoen","full_name":"Katoen, Joost P"},{"first_name":"Stefanie","full_name":"Mohr, Stefanie","last_name":"Mohr"},{"last_name":"Weininger","full_name":"Weininger, Maximilian","first_name":"Maximilian"},{"first_name":"Tobias","last_name":"Winkler","full_name":"Winkler, Tobias"}],"oa_version":"Published Version","abstract":[{"lang":"eng","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."}],"date_published":"2024-10-01T00:00:00Z","file":[{"relation":"main_file","access_level":"open_access","file_name":"2024_FromMethodsSys_Chatterjee.pdf","file_id":"18781","checksum":"111e76b76163640a2c89237642af586f","file_size":2614190,"success":1,"content_type":"application/pdf","date_created":"2025-01-09T07:31:31Z","date_updated":"2025-01-09T07:31:31Z","creator":"dernst"}],"external_id":{"isi":["000946174300001"]},"publication":"Formal Methods in System Design","publication_identifier":{"eissn":["1572-8102"]},"year":"2024","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.","doi":"10.1007/s10703-023-00411-4","date_created":"2023-03-19T23:00:59Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","isi":1,"language":[{"iso":"eng"}],"type":"journal_article","title":"Stochastic games with lexicographic objectives","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"article_type":"original","publication_status":"published","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"article_processing_charge":"Yes (via OA deal)","ec_funded":1,"page":"40-80","citation":{"short":"K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods in System Design 63 (2024) 40–80.","ista":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2024. Stochastic games with lexicographic objectives. Formal Methods in System Design. 63, 40–80.","apa":"Chatterjee, K., Katoen, J. P., Mohr, S., Weininger, M., &#38; Winkler, T. (2024). 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>","mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Objectives.” <i>Formal Methods in System Design</i>, vol. 63, Springer Nature, 2024, pp. 40–80, doi:<a href=\"https://doi.org/10.1007/s10703-023-00411-4\">10.1007/s10703-023-00411-4</a>.","ieee":"K. Chatterjee, J. P. Katoen, S. Mohr, M. Weininger, and T. Winkler, “Stochastic games with lexicographic objectives,” <i>Formal Methods in System Design</i>, vol. 63. Springer Nature, pp. 40–80, 2024.","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, 2024. <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>. 2024;63:40-80. doi:<a href=\"https://doi.org/10.1007/s10703-023-00411-4\">10.1007/s10703-023-00411-4</a>"},"has_accepted_license":"1","volume":63,"OA_type":"hybrid","quality_controlled":"1","publisher":"Springer Nature","intvolume":"        63","month":"10","OA_place":"publisher","date_updated":"2026-04-16T09:31:13Z","related_material":{"record":[{"id":"8272","status":"public","relation":"earlier_version"}]},"oa":1,"file_date_updated":"2025-01-09T07:31:31Z","department":[{"_id":"KrCh"}],"ddc":["000"],"scopus_import":"1","_id":"12738","status":"public"},{"day":"08","author":[{"last_name":"Asadi","full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","first_name":"Ali"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267"},{"first_name":"Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","full_name":"Saona Urmeneta, Raimundo J","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2405.02479"}],"oa_version":"Preprint","abstract":[{"text":"Turn-based discounted-sum games are two-player zero-sum games played on finite directed graphs. The vertices of the graph are partitioned between player 1 and player 2. Plays are infinite walks on the graph where the next vertex is decided by a player that owns the current vertex. Each edge is assigned an integer weight and the payoff of a play is the discounted-sum of the weights of the play. The goal of player 1 is to maximize the discounted-sum payoff against the adversarial player 2. These games lie in NP ∩ coNP and are among the rare combinatorial problems that belong to this complexity class and the existence of a polynomial-time algorithm is a major open question. Since breaking the general exponential barrier has been a challenging problem, faster parameterized algorithms have been considered. If the discount factor is expressed in unary, then discounted-sum games can be solved in polynomial time. However, if the discount factor is arbitrary (or expressed in binary), but the weights are in unary, none of the existing approaches yield a sub-exponential bound. Our main result is a new analysis technique for a classical algorithm (namely, the strategy iteration algorithm) that present a new runtime bound which is [EQUATION] for game graphs with n vertices and absolute weights of at most W. In particular, our result yields a deterministic sub-exponential bound for games with weights that are constant or represented in unary.","lang":"eng"}],"external_id":{"arxiv":["2405.02479"],"isi":["001275042100006"]},"date_published":"2024-07-08T00:00:00Z","publication":"39th Annual ACM/IEEE Symposium on Logic in Computer Science","article_number":"6","publication_identifier":{"eissn":["1043-6871"],"isbn":["9798400706608"]},"year":"2024","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant.\r\n","doi":"10.1145/3661814.3662080","date_created":"2024-06-03T07:43:15Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"name":"LICS: Logic in Computer Science","start_date":"2024-07-08","location":"Tallinn, Estonia","end_date":"2024-07-11"},"language":[{"iso":"eng"}],"isi":1,"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"title":"Deterministic sub-exponential algorithm for discounted-sum games with unary weights","type":"conference","publication_status":"published","article_processing_charge":"No","ec_funded":1,"citation":{"apa":"Asadi, A., Chatterjee, K., Svoboda, J., &#38; Saona Urmeneta, R. J. (2024). Deterministic sub-exponential algorithm for discounted-sum games with unary weights. In <i>39th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Tallinn, Estonia: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3661814.3662080\">https://doi.org/10.1145/3661814.3662080</a>","mla":"Asadi, Ali, et al. “Deterministic Sub-Exponential Algorithm for Discounted-Sum Games with Unary Weights.” <i>39th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 6, Association for Computing Machinery, 2024, doi:<a href=\"https://doi.org/10.1145/3661814.3662080\">10.1145/3661814.3662080</a>.","short":"A. Asadi, K. Chatterjee, J. Svoboda, R.J. Saona Urmeneta, in:, 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Association for Computing Machinery, 2024.","ista":"Asadi A, Chatterjee K, Svoboda J, Saona Urmeneta RJ. 2024. Deterministic sub-exponential algorithm for discounted-sum games with unary weights. 39th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Jakub Svoboda, and Raimundo J Saona Urmeneta. “Deterministic Sub-Exponential Algorithm for Discounted-Sum Games with Unary Weights.” In <i>39th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3661814.3662080\">https://doi.org/10.1145/3661814.3662080</a>.","ama":"Asadi A, Chatterjee K, Svoboda J, Saona Urmeneta RJ. Deterministic sub-exponential algorithm for discounted-sum games with unary weights. In: <i>39th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Association for Computing Machinery; 2024. doi:<a href=\"https://doi.org/10.1145/3661814.3662080\">10.1145/3661814.3662080</a>","ieee":"A. Asadi, K. Chatterjee, J. Svoboda, and R. J. Saona Urmeneta, “Deterministic sub-exponential algorithm for discounted-sum games with unary weights,” in <i>39th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Tallinn, Estonia, 2024."},"quality_controlled":"1","publisher":"Association for Computing Machinery","month":"07","date_updated":"2025-09-08T07:44:29Z","oa":1,"department":[{"_id":"KrCh"}],"scopus_import":"1","arxiv":1,"corr_author":"1","_id":"17098","status":"public"},{"day":"05","author":[{"id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","first_name":"Ali","last_name":"Asadi","full_name":"Asadi, Ali"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","full_name":"Saona Urmeneta, Raimundo J","last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267"}],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"We study two-player zero-sum concurrent stochastic games with finite state and action space played for an infinite number of steps. In every step, the two players simultaneously and independently choose an action. Given the current state and the chosen actions, the next state is obtained according to a stochastic transition function. An objective is a measurable function on plays (or infinite trajectories) of the game, and the value for an objective is the maximal expectation that the player can guarantee against the adversarial player. We consider: (a) stateful-discounted objectives, which are similar to the classical discounted-sum objectives, but states are associated with different discount factors rather than a single discount factor; and (b) parity objectives, which are a canonical representation for ω-regular objectives. For stateful-discounted objectives, given an ordering of the discount factors, the limit value is the limit of the value of the stateful-discounted objectives, as the discount factors approach zero according to the given order.\r\nThe computational problem we consider is the approximation of the value within an arbitrary\r\nadditive error. The above problem is known to be in EXPSPACE for the limit value of statefuldiscounted objectives and in PSPACE for parity objectives. The best-known algorithms for both the above problems are at least exponential time, with an exponential dependence on the number of states and actions. Our main results for the value approximation problem for the limit value of stateful-discounted objectives and parity objectives are as follows: (a) we establish TFNP[NP] complexity; and (b) we present algorithms that improve the dependency on the number of actions in the exponent from linear to logarithmic. In particular, if the number of states is constant, our algorithms run in polynomial time."}],"date_published":"2024-12-05T00:00:00Z","file":[{"file_name":"2024_LIPIcs_Asadi.pdf","file_id":"18777","relation":"main_file","access_level":"open_access","checksum":"5b544ab4692b93300b404435c036ddd4","success":1,"date_created":"2025-01-08T09:49:31Z","content_type":"application/pdf","file_size":847960,"creator":"dernst","date_updated":"2025-01-08T09:49:31Z"}],"external_id":{"arxiv":["2405.02486"],"isi":["001537516500005"]},"publication":"44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","article_number":"5","year":"2024","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773553"]},"doi":"10.4230/LIPIcs.FSTTCS.2024.5","acknowledgement":"This research was partially supported by ERC CoG 863818 (ForM-SMArt), Austrian\r\nScience Fund (FWF) 10.55776/COE12, and French Agence Nationale de la Recherche (ANR)\r\nANR-21-CE40-0020 (CONVERGENCE project)","alternative_title":["LIPIcs"],"date_created":"2024-06-03T07:44:27Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Gujarat, India","start_date":"2024-12-16","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","end_date":"2024-12-18"},"language":[{"iso":"eng"}],"isi":1,"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"type":"conference","title":"Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms","publication_status":"published","ec_funded":1,"article_processing_charge":"No","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"has_accepted_license":"1","citation":{"ista":"Asadi A, Chatterjee K, Saona Urmeneta RJ, Svoboda J. 2024. Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms. 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 323, 5.","short":"A. Asadi, K. Chatterjee, R.J. Saona Urmeneta, J. Svoboda, in:, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","apa":"Asadi, A., Chatterjee, K., Saona Urmeneta, R. J., &#38; Svoboda, J. (2024). Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms. In <i>44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 323). Gujarat, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5\">https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5</a>","mla":"Asadi, Ali, et al. “Concurrent Stochastic Games with Stateful-Discounted and Parity Objectives: Complexity and Algorithms.” <i>44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 323, 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5\">10.4230/LIPIcs.FSTTCS.2024.5</a>.","ieee":"A. Asadi, K. Chatterjee, R. J. Saona Urmeneta, and J. Svoboda, “Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms,” in <i>44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Gujarat, India, 2024, vol. 323.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Concurrent Stochastic Games with Stateful-Discounted and Parity Objectives: Complexity and Algorithms.” In <i>44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Vol. 323. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5\">https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5</a>.","ama":"Asadi A, Chatterjee K, Saona Urmeneta RJ, Svoboda J. Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms. In: <i>44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 323. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5\">10.4230/LIPIcs.FSTTCS.2024.5</a>"},"volume":323,"quality_controlled":"1","OA_type":"gold","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","intvolume":"       323","OA_place":"publisher","month":"12","date_updated":"2025-12-02T13:40:52Z","oa":1,"ddc":["000"],"file_date_updated":"2025-01-08T09:49:31Z","department":[{"_id":"KrCh"}],"scopus_import":"1","arxiv":1,"_id":"17099","corr_author":"1","status":"public"}]