[{"page":"1-21","quality_controlled":"1","main_file_link":[{"url":" https://doi.org/10.48550/arXiv.1802.03642","open_access":"1"}],"publisher":"Elsevier","article_processing_charge":"No","doi":"10.1016/j.jcss.2022.04.003","type":"journal_article","_id":"11402","date_updated":"2025-07-14T09:09:54Z","publication":"Journal of Computer and System Sciences","status":"public","project":[{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"acknowledgement":"This work was partially supported by Austrian Science Fund (FWF) NFN Grant No RiSE/SHiNE S11407 and by the grant ERC CoG 863818 (ForM-SMArt).","date_published":"2022-11-01T00:00:00Z","ec_funded":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"7402"}]},"external_id":{"arxiv":["1802.03642"],"isi":["000805002800001"]},"isi":1,"year":"2022","abstract":[{"lang":"eng","text":"Fixed-horizon planning considers a weighted graph and asks to construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping-time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary as the worst-case scenario. A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon or fixed stopping-time distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping-time distribution with expected stopping-time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping-time distribution can be achieved in polynomial time."}],"intvolume":"       129","publication_identifier":{"eissn":["1090-2724"],"issn":["0022-0000"]},"publication_status":"published","oa_version":"Preprint","title":"Graph planning with expected finite horizon","day":"01","scopus_import":"1","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"}],"date_created":"2022-05-22T22:01:40Z","article_type":"original","volume":129,"language":[{"iso":"eng"}],"oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ieee":"K. Chatterjee and L. Doyen, “Graph planning with expected finite horizon,” <i>Journal of Computer and System Sciences</i>, vol. 129. Elsevier, pp. 1–21, 2022.","short":"K. Chatterjee, L. Doyen, Journal of Computer and System Sciences 129 (2022) 1–21.","ama":"Chatterjee K, Doyen L. Graph planning with expected finite horizon. <i>Journal of Computer and System Sciences</i>. 2022;129:1-21. doi:<a href=\"https://doi.org/10.1016/j.jcss.2022.04.003\">10.1016/j.jcss.2022.04.003</a>","apa":"Chatterjee, K., &#38; Doyen, L. (2022). Graph planning with expected finite horizon. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2022.04.003\">https://doi.org/10.1016/j.jcss.2022.04.003</a>","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Graph Planning with Expected Finite Horizon.” <i>Journal of Computer and System Sciences</i>, vol. 129, Elsevier, 2022, pp. 1–21, doi:<a href=\"https://doi.org/10.1016/j.jcss.2022.04.003\">10.1016/j.jcss.2022.04.003</a>.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Graph Planning with Expected Finite Horizon.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2022. <a href=\"https://doi.org/10.1016/j.jcss.2022.04.003\">https://doi.org/10.1016/j.jcss.2022.04.003</a>.","ista":"Chatterjee K, Doyen L. 2022. Graph planning with expected finite horizon. Journal of Computer and System Sciences. 129, 1–21."},"month":"11","arxiv":1,"department":[{"_id":"KrCh"}]},{"month":"02","arxiv":1,"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"oa":1,"language":[{"iso":"eng"}],"issue":"1","citation":{"ieee":"K. Chatterjee, R. J. Saona Urmeneta, and B. Ziliotto, “Finite-memory strategies in POMDPs with long-run average objectives,” <i>Mathematics of Operations Research</i>, vol. 47, no. 1. Institute for Operations Research and the Management Sciences, pp. 100–119, 2022.","short":"K. Chatterjee, R.J. Saona Urmeneta, B. Ziliotto, Mathematics of Operations Research 47 (2022) 100–119.","ama":"Chatterjee K, Saona Urmeneta RJ, Ziliotto B. Finite-memory strategies in POMDPs with long-run average objectives. <i>Mathematics of Operations Research</i>. 2022;47(1):100-119. doi:<a href=\"https://doi.org/10.1287/moor.2020.1116\">10.1287/moor.2020.1116</a>","apa":"Chatterjee, K., Saona Urmeneta, R. J., &#38; Ziliotto, B. (2022). Finite-memory strategies in POMDPs with long-run average objectives. <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences. <a href=\"https://doi.org/10.1287/moor.2020.1116\">https://doi.org/10.1287/moor.2020.1116</a>","mla":"Chatterjee, Krishnendu, et al. “Finite-Memory Strategies in POMDPs with Long-Run Average Objectives.” <i>Mathematics of Operations Research</i>, vol. 47, no. 1, Institute for Operations Research and the Management Sciences, 2022, pp. 100–19, doi:<a href=\"https://doi.org/10.1287/moor.2020.1116\">10.1287/moor.2020.1116</a>.","ista":"Chatterjee K, Saona Urmeneta RJ, Ziliotto B. 2022. Finite-memory strategies in POMDPs with long-run average objectives. Mathematics of Operations Research. 47(1), 100–119.","chicago":"Chatterjee, Krishnendu, Raimundo J Saona Urmeneta, and Bruno Ziliotto. “Finite-Memory Strategies in POMDPs with Long-Run Average Objectives.” <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences, 2022. <a href=\"https://doi.org/10.1287/moor.2020.1116\">https://doi.org/10.1287/moor.2020.1116</a>."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","last_name":"Saona Urmeneta","first_name":"Raimundo J","orcid":"0000-0001-5103-038X"},{"first_name":"Bruno","last_name":"Ziliotto","full_name":"Ziliotto, Bruno"}],"day":"01","scopus_import":"1","title":"Finite-memory strategies in POMDPs with long-run average objectives","oa_version":"Preprint","volume":47,"article_type":"original","date_created":"2021-04-08T09:33:31Z","intvolume":"        47","abstract":[{"lang":"eng","text":"Partially observable Markov decision processes (POMDPs) are standard models for dynamic systems with probabilistic and nondeterministic behaviour in uncertain environments. We prove that in POMDPs with long-run average objective, the decision maker has approximately optimal strategies with finite memory. This implies notably that approximating the long-run value is recursively enumerable, as well as a weak continuity property of the value with respect to the transition function. "}],"publication_status":"published","publication_identifier":{"eissn":["1526-5471"],"issn":["0364-765X"]},"year":"2022","isi":1,"external_id":{"arxiv":["1904.13360"],"isi":["000731918100001"]},"keyword":["Management Science and Operations Research","General Mathematics","Computer Science Applications"],"project":[{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"status":"public","publication":"Mathematics of Operations Research","date_published":"2022-02-01T00:00:00Z","acknowledgement":"Partially supported by Austrian Science Fund (FWF) NFN Grant No RiSE/SHiNE S11407, by CONICYT Chile through grant PII 20150140, and by ECOS-CONICYT through grant C15E03.\r\n","doi":"10.1287/moor.2020.1116","article_processing_charge":"No","publisher":"Institute for Operations Research and the Management Sciences","date_updated":"2023-09-05T13:16:11Z","_id":"9311","type":"journal_article","page":"100-119","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1904.13360"}],"quality_controlled":"1"},{"doi":"10.7155/jgaa.00591","article_processing_charge":"No","publisher":"Brown University","date_updated":"2023-02-23T13:54:21Z","_id":"11938","type":"journal_article","page":"225-240","ddc":["000"],"quality_controlled":"1","year":"2022","external_id":{"arxiv":["2101.03928"]},"related_material":{"record":[{"id":"9296","relation":"earlier_version","status":"public"}]},"project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020"},{"grant_number":"Z00342","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"268116B8-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"publication":"Journal of Graph Algorithms and Applications","status":"public","ec_funded":1,"acknowledgement":"A.A. funded by the Marie Sklodowska-Curie grant agreement No 754411. Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23 (RiSE).","date_published":"2022-06-01T00:00:00Z","author":[{"first_name":"Oswin","last_name":"Aichholzer","full_name":"Aichholzer, Oswin"},{"first_name":"Alan M","orcid":"0000-0003-2401-8670","last_name":"Arroyo Guevara","id":"3207FDC6-F248-11E8-B48F-1D18A9856A87","full_name":"Arroyo Guevara, Alan M"},{"full_name":"Masárová, Zuzana","id":"45CFE238-F248-11E8-B48F-1D18A9856A87","last_name":"Masárová","first_name":"Zuzana","orcid":"0000-0002-6660-1322"},{"full_name":"Parada, Irene","last_name":"Parada","first_name":"Irene"},{"last_name":"Perz","full_name":"Perz, Daniel","first_name":"Daniel"},{"first_name":"Alexander","full_name":"Pilz, Alexander","last_name":"Pilz"},{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","first_name":"Josef"},{"last_name":"Vogtenhuber","full_name":"Vogtenhuber, Birgit","first_name":"Birgit"}],"scopus_import":"1","day":"01","title":"On compatible matchings","oa_version":"Published Version","volume":26,"article_type":"original","date_created":"2022-08-21T22:01:56Z","has_accepted_license":"1","intvolume":"        26","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"lang":"eng","text":"A matching is compatible to two or more labeled point sets of size n with labels {1, . . . , n} if its straight-line drawing on each of these point sets is crossing-free. We study the maximum number of edges in a matching compatible to two or more labeled point sets in general position in the plane. We show that for any two labeled sets of n points in convex position there exists a compatible matching with ⌊√2n + 1 − 1⌋ edges. More generally, for any ℓ labeled point sets we construct compatible matchings of size Ω(n1/ℓ). As a corresponding upper bound, we use probabilistic arguments to show that for any ℓ given sets of n points there exists a labeling of each set such that the largest compatible matching has O(n2/(ℓ+1)) edges. Finally, we show that Θ(log n) copies of any set of n points are necessary and sufficient for the existence of labelings of these point sets such that any compatible matching consists only of a single edge."}],"publication_identifier":{"issn":["1526-1719"]},"publication_status":"published","file_date_updated":"2022-08-22T06:42:42Z","month":"06","arxiv":1,"department":[{"_id":"UlWa"},{"_id":"HeEd"},{"_id":"KrCh"}],"file":[{"access_level":"open_access","content_type":"application/pdf","success":1,"file_name":"2022_JourGraphAlgorithmsApplic_Aichholzer.pdf","checksum":"dc6e255e3558faff924fd9e370886c11","relation":"main_file","creator":"dernst","date_updated":"2022-08-22T06:42:42Z","date_created":"2022-08-22T06:42:42Z","file_size":694538,"file_id":"11940"}],"oa":1,"language":[{"iso":"eng"}],"issue":"2","citation":{"short":"O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz, J. Tkadlec, B. Vogtenhuber, Journal of Graph Algorithms and Applications 26 (2022) 225–240.","ieee":"O. Aichholzer <i>et al.</i>, “On compatible matchings,” <i>Journal of Graph Algorithms and Applications</i>, vol. 26, no. 2. Brown University, pp. 225–240, 2022.","ama":"Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings. <i>Journal of Graph Algorithms and Applications</i>. 2022;26(2):225-240. doi:<a href=\"https://doi.org/10.7155/jgaa.00591\">10.7155/jgaa.00591</a>","mla":"Aichholzer, Oswin, et al. “On Compatible Matchings.” <i>Journal of Graph Algorithms and Applications</i>, vol. 26, no. 2, Brown University, 2022, pp. 225–40, doi:<a href=\"https://doi.org/10.7155/jgaa.00591\">10.7155/jgaa.00591</a>.","apa":"Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D., Pilz, A., … Vogtenhuber, B. (2022). On compatible matchings. <i>Journal of Graph Algorithms and Applications</i>. Brown University. <a href=\"https://doi.org/10.7155/jgaa.00591\">https://doi.org/10.7155/jgaa.00591</a>","chicago":"Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada, Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible Matchings.” <i>Journal of Graph Algorithms and Applications</i>. Brown University, 2022. <a href=\"https://doi.org/10.7155/jgaa.00591\">https://doi.org/10.7155/jgaa.00591</a>.","ista":"Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec J, Vogtenhuber B. 2022. On compatible matchings. Journal of Graph Algorithms and Applications. 26(2), 225–240."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"abstract":[{"lang":"eng","text":"Structural balance theory is an established framework for studying social relationships of friendship and enmity. These relationships are modeled by a signed network whose energy potential measures the level of imbalance, while stochastic dynamics drives the network toward a state of minimum energy that captures social balance. It is known that this energy landscape has local minima that can trap socially aware dynamics, preventing it from reaching balance. Here we first study the robustness and attractor properties of these local minima. We show that a stochastic process can reach them from an abundance of initial states and that some local minima cannot be escaped by mild perturbations of the network. Motivated by these anomalies, we introduce best-edge dynamics (BED), a new plausible stochastic process. We prove that BED always reaches balance and that it does so fast in various interesting settings."}],"intvolume":"       106","publication_identifier":{"issn":["2470-0045"],"eissn":["2470-0053"]},"publication_status":"published","title":"Social balance on networks: Local minima and best-edge dynamics","oa_version":"Preprint","day":"29","scopus_import":"1","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267"},{"last_name":"Zikelic","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","orcid":"0000-0002-1097-9684"}],"date_created":"2023-01-16T09:57:57Z","article_type":"original","volume":106,"language":[{"iso":"eng"}],"oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"short":"K. Chatterjee, J. Svoboda, D. Zikelic, A. Pavlogiannis, J. Tkadlec, Physical Review E 106 (2022).","ieee":"K. Chatterjee, J. Svoboda, D. Zikelic, A. Pavlogiannis, and J. Tkadlec, “Social balance on networks: Local minima and best-edge dynamics,” <i>Physical Review E</i>, vol. 106, no. 3. American Physical Society, 2022.","ama":"Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. Social balance on networks: Local minima and best-edge dynamics. <i>Physical Review E</i>. 2022;106(3). doi:<a href=\"https://doi.org/10.1103/physreve.106.034321\">10.1103/physreve.106.034321</a>","mla":"Chatterjee, Krishnendu, et al. “Social Balance on Networks: Local Minima and Best-Edge Dynamics.” <i>Physical Review E</i>, vol. 106, no. 3, 034321, American Physical Society, 2022, doi:<a href=\"https://doi.org/10.1103/physreve.106.034321\">10.1103/physreve.106.034321</a>.","apa":"Chatterjee, K., Svoboda, J., Zikelic, D., Pavlogiannis, A., &#38; Tkadlec, J. (2022). Social balance on networks: Local minima and best-edge dynamics. <i>Physical Review E</i>. American Physical Society. <a href=\"https://doi.org/10.1103/physreve.106.034321\">https://doi.org/10.1103/physreve.106.034321</a>","ista":"Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. 2022. Social balance on networks: Local minima and best-edge dynamics. Physical Review E. 106(3), 034321.","chicago":"Chatterjee, Krishnendu, Jakub Svoboda, Dorde Zikelic, Andreas Pavlogiannis, and Josef Tkadlec. “Social Balance on Networks: Local Minima and Best-Edge Dynamics.” <i>Physical Review E</i>. American Physical Society, 2022. <a href=\"https://doi.org/10.1103/physreve.106.034321\">https://doi.org/10.1103/physreve.106.034321</a>."},"issue":"3","arxiv":1,"month":"09","article_number":"034321","department":[{"_id":"KrCh"}],"quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2210.02394"}],"publisher":"American Physical Society","article_processing_charge":"No","doi":"10.1103/physreve.106.034321","type":"journal_article","_id":"12257","date_updated":"2025-07-14T09:09:49Z","publication":"Physical Review E","status":"public","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"665385","name":"International IST Doctoral Program"}],"acknowledgement":"K.C. acknowledges support from ERC Start Grant No. (279307: Graph Games), ERC Consolidator Grant No. (863818: ForM-SMart), and Austrian Science Fund (FWF)\r\nGrants No. P23499-N23 and No. S11407-N23 (RiSE). This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie\r\nSkłodowska-Curie Grant Agreement No. 665385.","date_published":"2022-09-29T00:00:00Z","ec_funded":1,"external_id":{"isi":["000870243100001"],"arxiv":["2210.02394"]},"year":"2022","isi":1},{"title":"Optimal strategies for selecting coordinators","oa_version":"Published Version","author":[{"full_name":"Zeiner, Martin","last_name":"Zeiner","first_name":"Martin"},{"first_name":"Ulrich","last_name":"Schmid","full_name":"Schmid, Ulrich"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"}],"day":"31","scopus_import":"1","article_type":"original","date_created":"2020-11-22T23:01:26Z","volume":289,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"       289","abstract":[{"text":"We study optimal election sequences for repeatedly selecting a (very) small group of leaders among a set of participants (players) with publicly known unique ids. In every time slot, every player has to select exactly one player that it considers to be the current leader, oblivious to the selection of the other players, but with the overarching goal of maximizing a given parameterized global (“social”) payoff function in the limit. We consider a quite generic model, where the local payoff achieved by a given player depends, weighted by some arbitrary but fixed real parameter, on the number of different leaders chosen in a round, the number of players that choose the given player as the leader, and whether the chosen leader has changed w.r.t. the previous round or not. The social payoff can be the maximum, average or minimum local payoff of the players. Possible applications include quite diverse examples such as rotating coordinator-based distributed algorithms and long-haul formation flying of social birds. Depending on the weights and the particular social payoff, optimal sequences can be very different, from simple round-robin where all players chose the same leader alternatingly every time slot to very exotic patterns, where a small group of leaders (at most 2) is elected in every time slot. Moreover, we study the question if and when a single player would not benefit w.r.t. its local payoff when deviating from the given optimal sequence, i.e., when our optimal sequences are Nash equilibria in the restricted strategy space of oblivious strategies. As this is the case for many parameterizations of our model, our results reveal that no punishment is needed to make it rational for the players to optimize the social payoff.","lang":"eng"}],"has_accepted_license":"1","publication_status":"published","publication_identifier":{"issn":["0166218X"]},"file_date_updated":"2021-02-04T11:28:42Z","month":"01","file":[{"file_id":"9089","creator":"dernst","date_updated":"2021-02-04T11:28:42Z","date_created":"2021-02-04T11:28:42Z","file_size":652739,"checksum":"f1039ff5a2d6ca116720efdb84ee9d5e","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_name":"2021_DiscreteApplMath_Zeiner.pdf","success":1}],"department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","issue":"1","citation":{"ama":"Zeiner M, Schmid U, Chatterjee K. Optimal strategies for selecting coordinators. <i>Discrete Applied Mathematics</i>. 2021;289(1):392-415. doi:<a href=\"https://doi.org/10.1016/j.dam.2020.10.022\">10.1016/j.dam.2020.10.022</a>","ieee":"M. Zeiner, U. Schmid, and K. Chatterjee, “Optimal strategies for selecting coordinators,” <i>Discrete Applied Mathematics</i>, vol. 289, no. 1. Elsevier, pp. 392–415, 2021.","short":"M. Zeiner, U. Schmid, K. Chatterjee, Discrete Applied Mathematics 289 (2021) 392–415.","ista":"Zeiner M, Schmid U, Chatterjee K. 2021. Optimal strategies for selecting coordinators. Discrete Applied Mathematics. 289(1), 392–415.","chicago":"Zeiner, Martin, Ulrich Schmid, and Krishnendu Chatterjee. “Optimal Strategies for Selecting Coordinators.” <i>Discrete Applied Mathematics</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.dam.2020.10.022\">https://doi.org/10.1016/j.dam.2020.10.022</a>.","apa":"Zeiner, M., Schmid, U., &#38; Chatterjee, K. (2021). Optimal strategies for selecting coordinators. <i>Discrete Applied Mathematics</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.dam.2020.10.022\">https://doi.org/10.1016/j.dam.2020.10.022</a>","mla":"Zeiner, Martin, et al. “Optimal Strategies for Selecting Coordinators.” <i>Discrete Applied Mathematics</i>, vol. 289, no. 1, Elsevier, 2021, pp. 392–415, doi:<a href=\"https://doi.org/10.1016/j.dam.2020.10.022\">10.1016/j.dam.2020.10.022</a>."},"publisher":"Elsevier","doi":"10.1016/j.dam.2020.10.022","article_processing_charge":"No","type":"journal_article","date_updated":"2023-08-04T11:12:41Z","_id":"8793","ddc":["510"],"page":"392-415","quality_controlled":"1","external_id":{"isi":["000596823800035"]},"isi":1,"year":"2021","project":[{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"publication":"Discrete Applied Mathematics","status":"public","acknowledgement":"We are grateful to Matthias Függer and Thomas Nowak for having raised our interest in the problem studied in this paper.\r\nThis work has been supported the Austrian Science Fund (FWF) projects S11405, S11407 (RiSE), and P28182 (ADynNet).","date_published":"2021-01-31T00:00:00Z"},{"year":"2021","related_material":{"record":[{"relation":"later_version","status":"public","id":"11938"}]},"external_id":{"arxiv":["2101.03928"]},"ec_funded":1,"acknowledgement":"A.A. funded by the Marie Skłodowska-Curie grant agreement No. 754411. Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23 (RiSE).","conference":{"end_date":"2021-03-02","start_date":"2021-02-28","name":"WALCOM: Algorithms and Computation","location":"Yangon, Myanmar"},"date_published":"2021-02-16T00:00:00Z","status":"public","publication":"15th International Conference on Algorithms and Computation","project":[{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z00342","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"268116B8-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-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","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"_id":"9296","date_updated":"2023-02-21T16:33:44Z","type":"conference","alternative_title":["LNCS"],"article_processing_charge":"No","doi":"10.1007/978-3-030-68211-8_18","publisher":"Springer Nature","main_file_link":[{"url":"https://arxiv.org/abs/2101.03928","open_access":"1"}],"quality_controlled":"1","page":"221-233","department":[{"_id":"UlWa"},{"_id":"HeEd"},{"_id":"KrCh"}],"month":"02","arxiv":1,"citation":{"ista":"Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec J, Vogtenhuber B. 2021. On compatible matchings. 15th International Conference on Algorithms and Computation. WALCOM: Algorithms and Computation, LNCS, vol. 12635, 221–233.","chicago":"Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada, Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible Matchings.” In <i>15th International Conference on Algorithms and Computation</i>, 12635:221–33. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-68211-8_18\">https://doi.org/10.1007/978-3-030-68211-8_18</a>.","apa":"Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D., Pilz, A., … Vogtenhuber, B. (2021). On compatible matchings. In <i>15th International Conference on Algorithms and Computation</i> (Vol. 12635, pp. 221–233). Yangon, Myanmar: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-68211-8_18\">https://doi.org/10.1007/978-3-030-68211-8_18</a>","mla":"Aichholzer, Oswin, et al. “On Compatible Matchings.” <i>15th International Conference on Algorithms and Computation</i>, vol. 12635, Springer Nature, 2021, pp. 221–33, doi:<a href=\"https://doi.org/10.1007/978-3-030-68211-8_18\">10.1007/978-3-030-68211-8_18</a>.","ama":"Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings. In: <i>15th International Conference on Algorithms and Computation</i>. Vol 12635. Springer Nature; 2021:221-233. doi:<a href=\"https://doi.org/10.1007/978-3-030-68211-8_18\">10.1007/978-3-030-68211-8_18</a>","ieee":"O. Aichholzer <i>et al.</i>, “On compatible matchings,” in <i>15th International Conference on Algorithms and Computation</i>, Yangon, Myanmar, 2021, vol. 12635, pp. 221–233.","short":"O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz, J. Tkadlec, B. Vogtenhuber, in:, 15th International Conference on Algorithms and Computation, Springer Nature, 2021, pp. 221–233."},"user_id":"D865714E-FA4E-11E9-B85B-F5C5E5697425","oa":1,"language":[{"iso":"eng"}],"volume":12635,"date_created":"2021-03-28T22:01:41Z","scopus_import":"1","day":"16","author":[{"full_name":"Aichholzer, Oswin","last_name":"Aichholzer","first_name":"Oswin"},{"last_name":"Arroyo Guevara","id":"3207FDC6-F248-11E8-B48F-1D18A9856A87","full_name":"Arroyo Guevara, Alan M","first_name":"Alan M","orcid":"0000-0003-2401-8670"},{"first_name":"Zuzana","orcid":"0000-0002-6660-1322","last_name":"Masárová","id":"45CFE238-F248-11E8-B48F-1D18A9856A87","full_name":"Masárová, Zuzana"},{"first_name":"Irene","full_name":"Parada, Irene","last_name":"Parada"},{"first_name":"Daniel","last_name":"Perz","full_name":"Perz, Daniel"},{"first_name":"Alexander","full_name":"Pilz, Alexander","last_name":"Pilz"},{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","orcid":"0000-0002-1097-9684"},{"first_name":"Birgit","last_name":"Vogtenhuber","full_name":"Vogtenhuber, Birgit"}],"oa_version":"Preprint","title":"On compatible matchings","publication_identifier":{"eissn":["16113349"],"issn":["03029743"],"isbn":["9783030682101"]},"publication_status":"published","intvolume":"     12635","abstract":[{"text":" matching is compatible to two or more labeled point sets of size n with labels   {1,…,n}  if its straight-line drawing on each of these point sets is crossing-free. We study the maximum number of edges in a matching compatible to two or more labeled point sets in general position in the plane. We show that for any two labeled convex sets of n points there exists a compatible matching with   ⌊2n−−√⌋  edges. More generally, for any   ℓ  labeled point sets we construct compatible matchings of size   Ω(n1/ℓ) . As a corresponding upper bound, we use probabilistic arguments to show that for any   ℓ  given sets of n points there exists a labeling of each set such that the largest compatible matching has   O(n2/(ℓ+1))  edges. Finally, we show that   Θ(logn)  copies of any set of n points are necessary and sufficient for the existence of a labeling such that any compatible matching consists only of a single edge.","lang":"eng"}]},{"year":"2021","isi":1,"external_id":{"arxiv":["2104.07466"],"isi":["000947350400089"]},"keyword":["Computer science","Computational modeling","Markov processes","Probabilistic logic","Formal verification","Game Theory"],"status":"public","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","project":[{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"ec_funded":1,"acknowledgement":"The authors are grateful to the anonymous referees for their valuable comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For M. H. the research leading to these results has received funding from the European Research Council under the European Unions Seventh Framework Programme (FP/2007–2013) / ERC Grant Agreement no. 340506.","date_published":"2021-07-07T00:00:00Z","conference":{"name":"LICS: Symposium on Logic in Computer Science","start_date":"2021-06-29","end_date":"2021-07-02","location":"Rome, Italy"},"article_processing_charge":"No","doi":"10.1109/LICS52264.2021.9470739","publisher":"Institute of Electrical and Electronics Engineers","_id":"10002","date_updated":"2025-07-14T09:10:07Z","type":"conference","page":"1-13","main_file_link":[{"url":"https://arxiv.org/abs/2104.07466","open_access":"1"}],"quality_controlled":"1","month":"07","arxiv":1,"department":[{"_id":"KrCh"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13, doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>.","apa":"Chatterjee, K., Dvorak, W., Henzinger, M. H., &#38; Svozil, A. (2021). Symbolic time and space tradeoffs for probabilistic verification. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13). Rome, Italy: Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorak, Monika H Henzinger, and Alexander Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 1–13. Institute of Electrical and Electronics Engineers, 2021. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>.","ista":"Chatterjee K, Dvorak W, Henzinger MH, Svozil A. 2021. Symbolic time and space tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science, 1–13.","short":"K. Chatterjee, W. Dvorak, M.H. Henzinger, A. Svozil, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13.","ieee":"K. Chatterjee, W. Dvorak, M. H. Henzinger, and A. Svozil, “Symbolic time and space tradeoffs for probabilistic verification,” in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021, pp. 1–13.","ama":"Chatterjee K, Dvorak W, Henzinger MH, Svozil A. Symbolic time and space tradeoffs for probabilistic verification. In: <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics Engineers; 2021:1-13. doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>"},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","day":"07","scopus_import":"1","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Wolfgang","full_name":"Dvorak, Wolfgang","last_name":"Dvorak"},{"first_name":"Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Svozil, Alexander","last_name":"Svozil","first_name":"Alexander"}],"title":"Symbolic time and space tradeoffs for probabilistic verification","oa_version":"Preprint","date_created":"2021-09-12T22:01:24Z","abstract":[{"lang":"eng","text":"We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with  n  vertices and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of  ω -regular objectives for MDPs. We consider the canonical parity objectives for  ω -regular objectives, and for parity objectives with  d -priorities we present an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 ."}],"publication_identifier":{"isbn":["978-1-6654-4896-3"],"issn":["1043-6871"],"eisbn":["978-1-6654-4895-6"]},"publication_status":"published"},{"month":"06","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"citation":{"ama":"Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. Multiple-environment Markov decision processes: Efficient analysis and applications. In: <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>. Vol 30. Association for the Advancement of Artificial Intelligence; 2020:48-56.","short":"K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, A. Royer, in:, Proceedings of the 30th International Conference on Automated Planning and Scheduling, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56.","ieee":"K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, and A. Royer, “Multiple-environment Markov decision processes: Efficient analysis and applications,” in <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, Nancy, France, 2020, vol. 30, pp. 48–56.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Deep Karkhanis, Petr Novotný, and Amélie Royer. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” In <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, 30:48–56. Association for the Advancement of Artificial Intelligence, 2020.","ista":"Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. 2020. Multiple-environment Markov decision processes: Efficient analysis and applications. Proceedings of the 30th International Conference on Automated Planning and Scheduling. ICAPS: International Conference on Automated Planning and Scheduling vol. 30, 48–56.","mla":"Chatterjee, Krishnendu, et al. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, vol. 30, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56.","apa":"Chatterjee, K., Chmelik, M., Karkhanis, D., Novotný, P., &#38; Royer, A. (2020). Multiple-environment Markov decision processes: Efficient analysis and applications. In <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i> (Vol. 30, pp. 48–56). Nancy, France: Association for the Advancement of Artificial Intelligence."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin"},{"first_name":"Deep","full_name":"Karkhanis, Deep","last_name":"Karkhanis"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","last_name":"Novotný","first_name":"Petr"},{"full_name":"Royer, Amélie","id":"3811D890-F248-11E8-B48F-1D18A9856A87","last_name":"Royer","orcid":"0000-0002-8407-0705","first_name":"Amélie"}],"scopus_import":"1","day":"01","title":"Multiple-environment Markov decision processes: Efficient analysis and applications","oa_version":"None","volume":30,"date_created":"2020-08-02T22:00:58Z","intvolume":"        30","abstract":[{"lang":"eng","text":"Multiple-environment Markov decision processes (MEMDPs) are MDPs equipped with not one, but multiple probabilistic transition functions, which represent the various possible unknown environments. While the previous research on MEMDPs focused on theoretical properties for long-run average payoff, we study them with discounted-sum payoff and focus on their practical advantages and applications. MEMDPs can be viewed as a special case of Partially observable and Mixed observability MDPs: the state of the system is perfectly observable, but not the environment. We show that the specific structure of MEMDPs allows for more efficient algorithmic analysis, in particular for faster belief updates. We demonstrate the applicability of MEMDPs in several domains. In particular, we formalize the sequential decision-making approach to contextual recommendation systems as MEMDPs and substantially improve over the previous MDP approach."}],"publication_identifier":{"issn":["23340835"],"eissn":["23340843"]},"publication_status":"published","year":"2020","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8390"}]},"project":[{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"publication":"Proceedings of the 30th International Conference on Automated Planning and Scheduling","status":"public","acknowledgement":"Krishnendu Chatterjee is supported by the Austrian ScienceFund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE),and COST Action GAMENET. Petr Novotn ́y is supported bythe Czech Science Foundation grant No. GJ19-15134Y.","date_published":"2020-06-01T00:00:00Z","conference":{"location":"Nancy, France","start_date":"2020-10-26","end_date":"2020-10-30","name":"ICAPS: International Conference on Automated Planning and Scheduling"},"article_processing_charge":"No","publisher":"Association for the Advancement of Artificial Intelligence","date_updated":"2023-09-07T13:16:18Z","_id":"8193","type":"conference","page":"48-56","quality_controlled":"1"},{"oa":1,"language":[{"iso":"eng"}],"citation":{"ista":"Wang P, Fu H, Chatterjee K, Deng Y, Xu M. 2020. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. Proceedings of the ACM on Programming Languages. vol. 4, 25.","chicago":"Wang, Peixin, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” In <i>Proceedings of the ACM on Programming Languages</i>, Vol. 4. ACM, 2020. <a href=\"https://doi.org/10.1145/3371093\">https://doi.org/10.1145/3371093</a>.","mla":"Wang, Peixin, et al. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 4, no. POPL, 25, ACM, 2020, doi:<a href=\"https://doi.org/10.1145/3371093\">10.1145/3371093</a>.","apa":"Wang, P., Fu, H., Chatterjee, K., Deng, Y., &#38; Xu, M. (2020). Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In <i>Proceedings of the ACM on Programming Languages</i> (Vol. 4). ACM. <a href=\"https://doi.org/10.1145/3371093\">https://doi.org/10.1145/3371093</a>","ama":"Wang P, Fu H, Chatterjee K, Deng Y, Xu M. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In: <i>Proceedings of the ACM on Programming Languages</i>. Vol 4. ACM; 2020. doi:<a href=\"https://doi.org/10.1145/3371093\">10.1145/3371093</a>","short":"P. Wang, H. Fu, K. Chatterjee, Y. Deng, M. Xu, in:, Proceedings of the ACM on Programming Languages, ACM, 2020.","ieee":"P. Wang, H. Fu, K. Chatterjee, Y. Deng, and M. Xu, “Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time,” in <i>Proceedings of the ACM on Programming Languages</i>, 2020, vol. 4, no. POPL."},"issue":"POPL","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","arxiv":1,"month":"01","department":[{"_id":"KrCh"}],"file":[{"access_level":"open_access","content_type":"application/pdf","success":1,"file_name":"2019_ACM_POPL_Wang.pdf","checksum":"c6193d109ff4ecb17e7a6513d8eb34c0","relation":"main_file","creator":"cziletti","date_updated":"2020-09-01T11:12:58Z","file_size":564151,"date_created":"2020-09-01T11:12:58Z","file_id":"8328"}],"article_number":"25","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"         4","abstract":[{"lang":"eng","text":"The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature."}],"file_date_updated":"2020-09-01T11:12:58Z","publication_identifier":{"eissn":["2475-1421"]},"publication_status":"published","day":"01","scopus_import":"1","author":[{"first_name":"Peixin","last_name":"Wang","full_name":"Wang, Peixin"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Deng, Yuxin","last_name":"Deng","first_name":"Yuxin"},{"last_name":"Xu","full_name":"Xu, Ming","first_name":"Ming"}],"oa_version":"Published Version","title":"Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time","volume":4,"date_created":"2020-08-30T22:01:12Z","status":"public","publication":"Proceedings of the ACM on Programming Languages","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"}],"date_published":"2020-01-01T00:00:00Z","acknowledgement":"We thank anonymous reviewers for helpful comments, especially for pointing to us a scenario of piecewise-linear approximation (Remark5). The research was partially supported by the National Natural Science Foundation of China (NSFC) under Grant No. 61802254, 61672229, 61832015,61772336,11871221 and Austrian Science Fund (FWF) NFN under Grant No. S11407-N23 (RiSE/SHiNE). We thank Prof. Yuxi Fu, director of the BASICS Lab at Shanghai Jiao Tong University, for his support.","year":"2020","related_material":{"link":[{"url":"https://doi.org/10.5281/zenodo.3533633","relation":"software"}]},"external_id":{"arxiv":["1902.04744"]},"ddc":["004"],"quality_controlled":"1","article_processing_charge":"No","doi":"10.1145/3371093","publisher":"ACM","_id":"8324","date_updated":"2024-02-22T15:16:45Z","type":"conference"},{"abstract":[{"lang":"eng","text":"We consider a real-time setting where an environment releases sequences of firm-deadline tasks, and an online scheduler chooses on-the-fly the ones to execute on a single processor so as to maximize cumulated utility. The competitive ratio is a well-known performance measure for the scheduler: it gives the worst-case ratio, among all possible choices for the environment, of the cumulated utility of the online scheduler versus an offline scheduler that knows these choices in advance. Traditionally, competitive analysis is performed by hand, while automated techniques are rare and only handle static environments with independent tasks. We present a quantitative-verification framework for precedence-aware competitive analysis, where task releases may depend on preceding scheduling choices, i.e., the environment can respond to scheduling decisions dynamically . We consider two general classes of precedences: 1) follower precedences force the release of a dependent task upon the completion of a set of precursor tasks, while and 2) pairing precedences modify the characteristics of a dependent task provided the completion of a set of precursor tasks. Precedences make competitive analysis challenging, as the online and offline schedulers operate on diverging sequences. We make a formal presentation of our framework, and use a GPU-based implementation to analyze ten well-known schedulers on precedence-based application examples taken from the existing literature: 1) a handshake protocol (HP); 2) network packet-switching; 3) query scheduling (QS); and 4) a sporadic-interrupt setting. Our experimental results show that precedences and task parameters can vary drastically the best scheduler. Our framework thus supports application designers in choosing the best scheduler among a given set automatically."}],"intvolume":"        39","publication_status":"published","publication_identifier":{"eissn":["19374151"],"issn":["02780070"]},"author":[{"first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Nico","last_name":"Schaumberger","full_name":"Schaumberger, Nico"},{"first_name":"Ulrich","last_name":"Schmid","full_name":"Schmid, Ulrich"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":"1","day":"01","title":"Precedence-aware automated competitive analysis of real-time scheduling","oa_version":"None","volume":39,"article_type":"original","date_created":"2020-11-22T23:01:24Z","language":[{"iso":"eng"}],"issue":"11","citation":{"short":"A. Pavlogiannis, N. Schaumberger, U. Schmid, K. Chatterjee, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 3981–3992.","ieee":"A. Pavlogiannis, N. Schaumberger, U. Schmid, and K. Chatterjee, “Precedence-aware automated competitive analysis of real-time scheduling,” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>, vol. 39, no. 11. IEEE, pp. 3981–3992, 2020.","ama":"Pavlogiannis A, Schaumberger N, Schmid U, Chatterjee K. Precedence-aware automated competitive analysis of real-time scheduling. <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. 2020;39(11):3981-3992. doi:<a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">10.1109/TCAD.2020.3012803</a>","mla":"Pavlogiannis, Andreas, et al. “Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling.” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>, vol. 39, no. 11, IEEE, 2020, pp. 3981–92, doi:<a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">10.1109/TCAD.2020.3012803</a>.","apa":"Pavlogiannis, A., Schaumberger, N., Schmid, U., &#38; Chatterjee, K. (2020). Precedence-aware automated competitive analysis of real-time scheduling. <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. IEEE. <a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">https://doi.org/10.1109/TCAD.2020.3012803</a>","ista":"Pavlogiannis A, Schaumberger N, Schmid U, Chatterjee K. 2020. Precedence-aware automated competitive analysis of real-time scheduling. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 39(11), 3981–3992.","chicago":"Pavlogiannis, Andreas, Nico Schaumberger, Ulrich Schmid, and Krishnendu Chatterjee. “Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling.” <i>IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems</i>. IEEE, 2020. <a href=\"https://doi.org/10.1109/TCAD.2020.3012803\">https://doi.org/10.1109/TCAD.2020.3012803</a>."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","month":"11","department":[{"_id":"KrCh"}],"page":"3981-3992","quality_controlled":"1","doi":"10.1109/TCAD.2020.3012803","article_processing_charge":"No","publisher":"IEEE","date_updated":"2023-08-22T13:27:05Z","_id":"8788","type":"journal_article","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"status":"public","publication":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","acknowledgement":"This work was supported by the Austrian Science Foundation (FWF) under the NFN RiSE/SHiNE under Grant S11405 and Grant S11407. This article was presented in the International Conference on Embedded Software 2020 and appears as part of the ESWEEK-TCAD special issue. ","date_published":"2020-11-01T00:00:00Z","year":"2020","isi":1,"external_id":{"isi":["000587712700069"]}},{"month":"01","arxiv":1,"article_number":"e1007494","file":[{"file_id":"7441","date_created":"2020-02-03T07:32:42Z","file_size":1817531,"creator":"dernst","date_updated":"2020-07-14T12:47:53Z","relation":"main_file","checksum":"ce32ee2d2f53aed832f78bbd47e882df","file_name":"2020_PlosCompBio_Tkadlec.pdf","content_type":"application/pdf","access_level":"open_access"}],"department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Limits on amplifiers of natural selection under death-Birth updating. <i>PLoS computational biology</i>. 2020;16. doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1007494\">10.1371/journal.pcbi.1007494</a>","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, PLoS Computational Biology 16 (2020).","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Limits on amplifiers of natural selection under death-Birth updating,” <i>PLoS computational biology</i>, vol. 16. Public Library of Science, 2020.","ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2020. Limits on amplifiers of natural selection under death-Birth updating. PLoS computational biology. 16, e1007494.","chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Limits on Amplifiers of Natural Selection under Death-Birth Updating.” <i>PLoS Computational Biology</i>. Public Library of Science, 2020. <a href=\"https://doi.org/10.1371/journal.pcbi.1007494\">https://doi.org/10.1371/journal.pcbi.1007494</a>.","mla":"Tkadlec, Josef, et al. “Limits on Amplifiers of Natural Selection under Death-Birth Updating.” <i>PLoS Computational Biology</i>, vol. 16, e1007494, Public Library of Science, 2020, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1007494\">10.1371/journal.pcbi.1007494</a>.","apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2020). Limits on amplifiers of natural selection under death-Birth updating. <i>PLoS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.1007494\">https://doi.org/10.1371/journal.pcbi.1007494</a>"},"title":"Limits on amplifiers of natural selection under death-Birth updating","oa_version":"Published Version","author":[{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","first_name":"Josef"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"day":"17","scopus_import":"1","article_type":"original","date_created":"2019-12-23T13:45:11Z","volume":16,"intvolume":"        16","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"text":"The fixation probability of a single mutant invading a population of residents is among the most widely-studied quantities in evolutionary dynamics. Amplifiers of natural selection are population structures that increase the fixation probability of advantageous mutants, compared to well-mixed populations. Extensive studies have shown that many amplifiers exist for the Birth-death Moran process, some of them substantially increasing the fixation probability or even guaranteeing fixation in the limit of large population size. On the other hand, no amplifiers are known for the death-Birth Moran process, and computer-assisted exhaustive searches have failed to discover amplification. In this work we resolve this disparity, by showing that any amplification under death-Birth updating is necessarily bounded and transient. Our boundedness result states that even if a population structure does amplify selection, the resulting fixation probability is close to that of the well-mixed population. Our transience result states that for any population structure there exists a threshold r⋆ such that the population structure ceases to amplify selection if the mutant fitness advantage r is larger than r⋆. Finally, we also extend the above results to δ-death-Birth updating, which is a combination of Birth-death and death-Birth updating. On the positive side, we identify population structures that maintain amplification for a wide range of values r and δ. These results demonstrate that amplification of natural selection depends on the specific mechanisms of the evolutionary process.","lang":"eng"}],"has_accepted_license":"1","publication_identifier":{"eissn":["15537358"]},"publication_status":"published","file_date_updated":"2020-07-14T12:47:53Z","external_id":{"arxiv":["1906.02785"],"isi":["000510916500025"]},"related_material":{"record":[{"id":"7196","status":"public","relation":"part_of_dissertation"}]},"year":"2020","isi":1,"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"publication":"PLoS computational biology","status":"public","date_published":"2020-01-17T00:00:00Z","ec_funded":1,"publisher":"Public Library of Science","doi":"10.1371/journal.pcbi.1007494","article_processing_charge":"No","type":"journal_article","date_updated":"2023-10-17T12:29:47Z","_id":"7212","ddc":["000"],"quality_controlled":"1"},{"publication_identifier":{"issn":["1751-570X"]},"publication_status":"published","file_date_updated":"2022-05-16T22:30:04Z","has_accepted_license":"1","tmp":{"image":"/images/cc_by_nc_nd.png","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","short":"CC BY-NC-ND (4.0)"},"abstract":[{"lang":"eng","text":"This paper presents a novel abstraction technique for analyzing Lyapunov and asymptotic stability of polyhedral switched systems. A polyhedral switched system is a hybrid system in which the continuous dynamics is specified by polyhedral differential inclusions, the invariants and guards are specified by polyhedral sets and the switching between the modes do not involve reset of variables. A finite state weighted graph abstracting the polyhedral switched system is constructed from a finite partition of the state–space, such that the satisfaction of certain graph conditions, such as the absence of cycles with product of weights on the edges greater than (or equal) to 1, implies the stability of the system. However, the graph is in general conservative and hence, the violation of the graph conditions does not imply instability. If the analysis fails to establish stability due to the conservativeness in the approximation, a counterexample (cycle with product of edge weights greater than or equal to 1) indicating a potential reason for the failure is returned. Further, a more precise approximation of the switched system can be constructed by considering a finer partition of the state–space in the construction of the finite weighted graph. We present experimental results on analyzing stability of switched systems using the above method."}],"intvolume":"        36","volume":36,"article_type":"original","date_created":"2020-02-02T23:00:59Z","author":[{"first_name":"Miriam","orcid":"0000−0003−2936−5719","last_name":"Garcia Soto","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","full_name":"Garcia Soto, Miriam"},{"first_name":"Pavithra","full_name":"Prabhakar, Pavithra","last_name":"Prabhakar"}],"scopus_import":"1","day":"01","title":"Abstraction based verification of stability of polyhedral switched systems","oa_version":"Submitted Version","issue":"5","citation":{"apa":"Garcia Soto, M., &#38; Prabhakar, P. (2020). Abstraction based verification of stability of polyhedral switched systems. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2020.100856\">https://doi.org/10.1016/j.nahs.2020.100856</a>","mla":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification of Stability of Polyhedral Switched Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 36, no. 5, 100856, Elsevier, 2020, doi:<a href=\"https://doi.org/10.1016/j.nahs.2020.100856\">10.1016/j.nahs.2020.100856</a>.","ista":"Garcia Soto M, Prabhakar P. 2020. Abstraction based verification of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 36(5), 100856.","chicago":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification of Stability of Polyhedral Switched Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2020. <a href=\"https://doi.org/10.1016/j.nahs.2020.100856\">https://doi.org/10.1016/j.nahs.2020.100856</a>.","ieee":"M. Garcia Soto and P. Prabhakar, “Abstraction based verification of stability of polyhedral switched systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 36, no. 5. Elsevier, 2020.","short":"M. Garcia Soto, P. Prabhakar, Nonlinear Analysis: Hybrid Systems 36 (2020).","ama":"Garcia Soto M, Prabhakar P. Abstraction based verification of stability of polyhedral switched systems. <i>Nonlinear Analysis: Hybrid Systems</i>. 2020;36(5). doi:<a href=\"https://doi.org/10.1016/j.nahs.2020.100856\">10.1016/j.nahs.2020.100856</a>"},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa":1,"language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"article_number":"100856","file":[{"checksum":"560abfddb53f9fe921b6744f59f2cfaa","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2020_NAHS_GarciaSoto.pdf","file_id":"8688","date_updated":"2022-05-16T22:30:04Z","creator":"dernst","embargo":"2022-05-15","date_created":"2020-10-21T13:16:45Z","file_size":818774}],"month":"05","quality_controlled":"1","ddc":["000"],"date_updated":"2023-08-17T14:32:54Z","_id":"7426","type":"journal_article","doi":"10.1016/j.nahs.2020.100856","article_processing_charge":"No","publisher":"Elsevier","date_published":"2020-05-01T00:00:00Z","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"publication":"Nonlinear Analysis: Hybrid Systems","status":"public","year":"2020","isi":1,"external_id":{"isi":["000528828600003"]}},{"_id":"15055","date_updated":"2024-03-04T08:30:16Z","type":"journal_article","article_processing_charge":"No","doi":"10.1609/aaai.v34i06.6531","publisher":"Association for the Advancement of Artificial Intelligence","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2002.12086","open_access":"1"}],"quality_controlled":"1","page":"9794-9801","keyword":["General Medicine"],"year":"2020","external_id":{"arxiv":["2002.12086"]},"conference":{"location":"New York, NY, United States","start_date":"2020-02-07","end_date":"2020-02-12","name":"AAAI: Conference on Artificial Intelligence"},"acknowledgement":"Krishnendu Chatterjee is supported by the Austrian Science Fund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE), and COST Action GAMENET. Tomas Brazdil is supported by the Grant Agency of Masaryk University grant no. MUNI/G/0739/2017 and by the Czech Science Foundation grant No. 18-11193S. Petr Novotny and Jirı Vahala are supported by the Czech Science Foundation grant No. GJ19-15134Y.","date_published":"2020-04-03T00:00:00Z","status":"public","publication":"Proceedings of the 34th AAAI Conference on Artificial Intelligence","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"}],"volume":34,"date_created":"2024-03-04T08:07:22Z","article_type":"original","day":"03","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Petr","full_name":"Novotný, Petr","last_name":"Novotný"},{"first_name":"Jiří","last_name":"Vahala","full_name":"Vahala, Jiří"}],"oa_version":"Preprint","title":"Reinforcement learning of risk-constrained policies in Markov decision processes","publication_identifier":{"issn":["2374-3468"]},"publication_status":"published","abstract":[{"lang":"eng","text":"<jats:p>Markov decision processes (MDPs) are the defacto framework for sequential decision making in the presence of stochastic uncertainty. A classical optimization criterion for MDPs is to maximize the expected discounted-sum payoff, which ignores low probability catastrophic events with highly negative impact on the system. On the other hand, risk-averse policies require the probability of undesirable events to be below a given threshold, but they do not account for optimization of the expected payoff. We consider MDPs with discounted-sum payoff with failure states which represent catastrophic outcomes. The objective of risk-constrained planning is to maximize the expected discounted-sum payoff among risk-averse policies that ensure the probability to encounter a failure state is below a desired threshold. Our main contribution is an efficient risk-constrained planning algorithm that combines UCT-like search with a predictor learned through interaction with the MDP (in the style of AlphaZero) and with a risk-constrained action selection via linear programming. We demonstrate the effectiveness of our approach with experiments on classical MDPs from the literature, including benchmarks with an order of 106 states.</jats:p>"}],"intvolume":"        34","department":[{"_id":"KrCh"}],"arxiv":1,"month":"04","citation":{"apa":"Brázdil, T., Chatterjee, K., Novotný, P., &#38; Vahala, J. (2020). Reinforcement learning of risk-constrained policies in Markov decision processes. <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>. New York, NY, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v34i06.6531\">https://doi.org/10.1609/aaai.v34i06.6531</a>","mla":"Brázdil, Tomáš, et al. “Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes.” <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 06, Association for the Advancement of Artificial Intelligence, 2020, pp. 9794–801, doi:<a href=\"https://doi.org/10.1609/aaai.v34i06.6531\">10.1609/aaai.v34i06.6531</a>.","ista":"Brázdil T, Chatterjee K, Novotný P, Vahala J. 2020. Reinforcement learning of risk-constrained policies in Markov decision processes. Proceedings of the 34th AAAI Conference on Artificial Intelligence. 34(06), 9794–9801.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Petr Novotný, and Jiří Vahala. “Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes.” <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2020. <a href=\"https://doi.org/10.1609/aaai.v34i06.6531\">https://doi.org/10.1609/aaai.v34i06.6531</a>.","ieee":"T. Brázdil, K. Chatterjee, P. Novotný, and J. Vahala, “Reinforcement learning of risk-constrained policies in Markov decision processes,” <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 06. Association for the Advancement of Artificial Intelligence, pp. 9794–9801, 2020.","short":"T. Brázdil, K. Chatterjee, P. Novotný, J. Vahala, Proceedings of the 34th AAAI Conference on Artificial Intelligence 34 (2020) 9794–9801.","ama":"Brázdil T, Chatterjee K, Novotný P, Vahala J. Reinforcement learning of risk-constrained policies in Markov decision processes. <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>. 2020;34(06):9794-9801. doi:<a href=\"https://doi.org/10.1609/aaai.v34i06.6531\">10.1609/aaai.v34i06.6531</a>"},"issue":"06","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"language":[{"iso":"eng"}]},{"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"external_id":{"arxiv":["1901.06087"]},"year":"2019","status":"public","publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications ","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"date_published":"2019-10-01T00:00:00Z","conference":{"location":"Athens, Greece","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","end_date":"2019-10-25","start_date":"2019-10-23"},"ec_funded":1,"publisher":"ACM","article_processing_charge":"No","doi":"10.1145/3360555","type":"conference","_id":"6780","date_updated":"2025-06-02T08:53:47Z","ddc":["000"],"quality_controlled":"1","arxiv":1,"month":"10","file":[{"file_id":"6807","date_created":"2019-08-12T15:40:57Z","file_size":1024643,"date_updated":"2020-07-14T12:47:40Z","creator":"akafshda","relation":"main_file","checksum":"3482d8ace6fb4991eb7810e3b70f1b9f","file_name":"oopsla-2019.pdf","content_type":"application/pdf","access_level":"open_access"},{"file_id":"7821","creator":"dernst","date_updated":"2020-07-14T12:47:40Z","date_created":"2020-05-12T15:15:14Z","file_size":538579,"checksum":"4e5a6fb2b59a75222a4e8335a5a60eac","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_name":"2019_ACM_Huang.pdf"}],"article_number":"129","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"mla":"Huang, Mingzhang, et al. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>, vol. 3, 129, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3360555\">10.1145/3360555</a>.","apa":"Huang, M., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2019). Modular verification for almost-sure termination of probabilistic programs. In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i> (Vol. 3). Athens, Greece: ACM. <a href=\"https://doi.org/10.1145/3360555\">https://doi.org/10.1145/3360555</a>","chicago":"Huang, Mingzhang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>, Vol. 3. ACM, 2019. <a href=\"https://doi.org/10.1145/3360555\">https://doi.org/10.1145/3360555</a>.","ista":"Huang M, Fu H, Chatterjee K, Goharshady AK. 2019. Modular verification for almost-sure termination of probabilistic programs. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications . OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 129.","short":"M. Huang, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , ACM, 2019.","ieee":"M. Huang, H. Fu, K. Chatterjee, and A. K. Goharshady, “Modular verification for almost-sure termination of probabilistic programs,” in <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>, Athens, Greece, 2019, vol. 3.","ama":"Huang M, Fu H, Chatterjee K, Goharshady AK. Modular verification for almost-sure termination of probabilistic programs. In: <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>. Vol 3. ACM; 2019. doi:<a href=\"https://doi.org/10.1145/3360555\">10.1145/3360555</a>"},"oa_version":"Published Version","title":"Modular verification for almost-sure termination of probabilistic programs","day":"01","author":[{"first_name":"Mingzhang","last_name":"Huang","full_name":"Huang, Mingzhang"},{"last_name":"Fu","full_name":"Fu, Hongfei","first_name":"Hongfei"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady"}],"date_created":"2019-08-09T09:54:20Z","volume":3,"intvolume":"         3","tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","short":"CC BY-NC (4.0)"},"abstract":[{"lang":"eng","text":"In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a\r\ngiven probabilistic program terminates with probability 1. Scalable approaches for program analysis often\r\nrely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule)\r\nof Floyd-Hoare logic provides the foundation for modular analysis. Extension of this rule to almost-sure\r\ntermination of probabilistic programs is quite tricky, and a probabilistic variant was proposed in [16]. While the\r\nproposed probabilistic variant cautiously addresses the key issue of integrability, we show that the proposed\r\nmodular rule is still not sound for almost-sure termination of probabilistic programs.\r\nBesides establishing unsoundness of the previous rule, our contributions are as follows: First, we present a\r\nsound modular rule for almost-sure termination of probabilistic programs. Our approach is based on a novel\r\nnotion of descent supermartingales. Second, for algorithmic approaches, we consider descent supermartingales\r\nthat are linear and show that they can be synthesized in polynomial time. Finally, we present experimental\r\nresults on a variety of benchmarks and several natural examples that model various types of nested while\r\nloops in probabilistic programs and demonstrate that our approach is able to efficiently prove their almost-sure\r\ntermination property"}],"has_accepted_license":"1","file_date_updated":"2020-07-14T12:47:40Z","publication_status":"published"},{"month":"08","article_number":"27","file":[{"date_created":"2019-09-27T12:09:35Z","file_size":538120,"date_updated":"2020-07-14T12:47:43Z","creator":"kschuh","file_id":"6914","file_name":"2019_LIPIcs_Chatterjee.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"4985e26e1572d1575d64d38acabd71d6"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Henzinger TA, Otop J. 2019. Long-run average behavior of vector addition systems with states. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 27.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Long-Run Average Behavior of Vector Addition Systems with States,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.27\">https://doi.org/10.4230/LIPICS.CONCUR.2019.27</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2019). Long-run average behavior of vector addition systems with states (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.27\">https://doi.org/10.4230/LIPICS.CONCUR.2019.27</a>","mla":"Chatterjee, Krishnendu, et al. <i>Long-Run Average Behavior of Vector Addition Systems with States</i>. Vol. 140, 27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.27\">10.4230/LIPICS.CONCUR.2019.27</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Long-run average behavior of vector addition systems with states. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.27\">10.4230/LIPICS.CONCUR.2019.27</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Long-run average behavior of vector addition systems with states,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019."},"oa_version":"Published Version","title":"Long-run average behavior of vector addition systems with states","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"day":"01","scopus_import":1,"date_created":"2019-09-18T08:06:14Z","volume":140,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"text":"A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NP-complete for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open. ","lang":"eng"}],"intvolume":"       140","has_accepted_license":"1","publication_status":"published","file_date_updated":"2020-07-14T12:47:43Z","year":"2019","project":[{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"}],"status":"public","date_published":"2019-08-01T00:00:00Z","conference":{"location":"Amsterdam, Netherlands","name":"CONCUR: International Conference on Concurrency Theory","end_date":"2019-08-30","start_date":"2019-08-27"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPICS.CONCUR.2019.27","alternative_title":["LIPIcs"],"type":"conference","date_updated":"2021-01-12T08:09:27Z","_id":"6885","ddc":["000"],"quality_controlled":"1"},{"project":[{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"publication":"Leibniz International Proceedings in Informatics","status":"public","ec_funded":1,"date_published":"2019-08-01T00:00:00Z","conference":{"location":"Amsterdam, Netherlands","start_date":"2019-08-27","end_date":"2019-08-30","name":"CONCUR: International Conference on Concurrency Theory"},"year":"2019","ddc":["000"],"quality_controlled":"1","doi":"10.4230/LIPICS.CONCUR.2019.7","article_processing_charge":"No","alternative_title":["LIPIcs"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2022-08-12T10:54:34Z","_id":"6887","type":"conference","oa":1,"language":[{"iso":"eng"}],"citation":{"ama":"Chatterjee K, Dvorák W, Henzinger MH, Svozil A. Near-linear time algorithms for Streett objectives in graphs and MDPs. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.7\">10.4230/LIPICS.CONCUR.2019.7</a>","ieee":"K. Chatterjee, W. Dvorák, M. H. Henzinger, and A. Svozil, “Near-linear time algorithms for Streett objectives in graphs and MDPs,” in <i>Leibniz International Proceedings in Informatics</i>, Amsterdam, Netherlands, 2019, vol. 140.","short":"K. Chatterjee, W. Dvorák, M.H. Henzinger, A. Svozil, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","ista":"Chatterjee K, Dvorák W, Henzinger MH, Svozil A. 2019. Near-linear time algorithms for Streett objectives in graphs and MDPs. Leibniz International Proceedings in Informatics. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 7.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Alexander Svozil. “Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.7\">https://doi.org/10.4230/LIPICS.CONCUR.2019.7</a>.","apa":"Chatterjee, K., Dvorák, W., Henzinger, M. H., &#38; Svozil, A. (2019). Near-linear time algorithms for Streett objectives in graphs and MDPs. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 140). Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.7\">https://doi.org/10.4230/LIPICS.CONCUR.2019.7</a>","mla":"Chatterjee, Krishnendu, et al. “Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs.” <i>Leibniz International Proceedings in Informatics</i>, vol. 140, 7, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.7\">10.4230/LIPICS.CONCUR.2019.7</a>."},"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","month":"08","department":[{"_id":"KrCh"}],"file":[{"relation":"main_file","checksum":"e1f0e4061212454574f34a1368d018ec","file_name":"2019_LIPIcs_Chatterjee.pdf","content_type":"application/pdf","access_level":"open_access","file_id":"6922","file_size":730112,"date_created":"2019-10-01T08:20:30Z","creator":"kschuh","date_updated":"2020-07-14T12:47:43Z"}],"article_number":"7","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"       140","abstract":[{"text":"The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in the verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification. Consider graphs/MDPs with n vertices, m edges, and a Streett objectives with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants. The current best-known algorithm for the problem requires time O(min(n^2, m sqrt{m log n}) + b log n). In this work we present randomized near-linear time algorithms, with expected running time O~(m + b), where the O~ notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors. ","lang":"eng"}],"publication_status":"published","file_date_updated":"2020-07-14T12:47:43Z","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Wolfgang","full_name":"Dvorák, Wolfgang","last_name":"Dvorák"},{"first_name":"Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H"},{"last_name":"Svozil","full_name":"Svozil, Alexander","first_name":"Alexander"}],"scopus_import":"1","day":"01","title":"Near-linear time algorithms for Streett objectives in graphs and MDPs","oa_version":"Published Version","volume":140,"date_created":"2019-09-18T08:07:58Z"},{"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Nir","last_name":"Piterman","full_name":"Piterman, Nir"}],"day":"01","scopus_import":1,"oa_version":"Published Version","title":"Combinations of Qualitative Winning for Stochastic Parity Games","volume":140,"date_created":"2019-09-18T08:11:43Z","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"lang":"eng","text":"We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games. "}],"intvolume":"       140","publication_status":"published","file_date_updated":"2020-07-14T12:47:43Z","month":"08","department":[{"_id":"KrCh"}],"file":[{"file_id":"6923","date_created":"2019-10-01T08:49:45Z","file_size":509163,"creator":"kschuh","date_updated":"2020-07-14T12:47:43Z","relation":"main_file","checksum":"7b2ecfd4d9d02360308c0ca986fc10a7","file_name":"2019_LIPIcs_Chatterjee.pdf","content_type":"application/pdf","access_level":"open_access"}],"article_number":"6","oa":1,"language":[{"iso":"eng"}],"citation":{"ama":"Chatterjee K, Piterman N. Combinations of Qualitative Winning for Stochastic Parity Games. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.6\">10.4230/LIPICS.CONCUR.2019.6</a>","ieee":"K. Chatterjee and N. Piterman, “Combinations of Qualitative Winning for Stochastic Parity Games,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","short":"K. Chatterjee, N. Piterman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","chicago":"Chatterjee, Krishnendu, and Nir Piterman. “Combinations of Qualitative Winning for Stochastic Parity Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.6\">https://doi.org/10.4230/LIPICS.CONCUR.2019.6</a>.","ista":"Chatterjee K, Piterman N. 2019. Combinations of Qualitative Winning for Stochastic Parity Games. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 6.","apa":"Chatterjee, K., &#38; Piterman, N. (2019). Combinations of Qualitative Winning for Stochastic Parity Games (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.6\">https://doi.org/10.4230/LIPICS.CONCUR.2019.6</a>","mla":"Chatterjee, Krishnendu, and Nir Piterman. <i>Combinations of Qualitative Winning for Stochastic Parity Games</i>. Vol. 140, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.6\">10.4230/LIPICS.CONCUR.2019.6</a>."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","doi":"10.4230/LIPICS.CONCUR.2019.6","alternative_title":["LIPIcs"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2021-01-12T08:09:28Z","_id":"6889","type":"conference","ddc":["000"],"quality_controlled":"1","year":"2019","project":[{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"status":"public","date_published":"2019-08-01T00:00:00Z","conference":{"end_date":"2019-08-30","start_date":"2019-08-27","name":"CONCUR: International Conference on Concurrency Theory","location":"Amsterdam, Netherlands"}},{"external_id":{"isi":["000679281300007"],"arxiv":["1906.08178"]},"year":"2019","isi":1,"date_published":"2019-09-04T00:00:00Z","conference":{"name":"QEST: Quantitative Evaluation of Systems","start_date":"2019-09-10","end_date":"2019-09-12","location":"Glasgow, United Kingdom"},"publication":"16th International Conference on Quantitative Evaluation of Systems","status":"public","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"type":"conference","_id":"6942","date_updated":"2025-06-02T08:53:47Z","publisher":"Springer Nature","alternative_title":["LNCS"],"article_processing_charge":"No","doi":"10.1007/978-3-030-30281-8_7","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1906.08178"}],"page":"109-128","department":[{"_id":"KrCh"},{"_id":"ChLa"}],"month":"09","arxiv":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ama":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. Strategy representation by decision trees with linear classifiers. In: <i>16th International Conference on Quantitative Evaluation of Systems</i>. Vol 11785. Springer Nature; 2019:109-128. doi:<a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">10.1007/978-3-030-30281-8_7</a>","ieee":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, and V. Toman, “Strategy representation by decision trees with linear classifiers,” in <i>16th International Conference on Quantitative Evaluation of Systems</i>, Glasgow, United Kingdom, 2019, vol. 11785, pp. 109–128.","short":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, V. Toman, in:, 16th International Conference on Quantitative Evaluation of Systems, Springer Nature, 2019, pp. 109–128.","ista":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. 2019. Strategy representation by decision trees with linear classifiers. 16th International Conference on Quantitative Evaluation of Systems. QEST: Quantitative Evaluation of Systems, LNCS, vol. 11785, 109–128.","chicago":"Ashok, Pranav, Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský, Christoph Lampert, and Viktor Toman. “Strategy Representation by Decision Trees with Linear Classifiers.” In <i>16th International Conference on Quantitative Evaluation of Systems</i>, 11785:109–28. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">https://doi.org/10.1007/978-3-030-30281-8_7</a>.","apa":"Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C., &#38; Toman, V. (2019). Strategy representation by decision trees with linear classifiers. In <i>16th International Conference on Quantitative Evaluation of Systems</i> (Vol. 11785, pp. 109–128). Glasgow, United Kingdom: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">https://doi.org/10.1007/978-3-030-30281-8_7</a>","mla":"Ashok, Pranav, et al. “Strategy Representation by Decision Trees with Linear Classifiers.” <i>16th International Conference on Quantitative Evaluation of Systems</i>, vol. 11785, Springer Nature, 2019, pp. 109–28, doi:<a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">10.1007/978-3-030-30281-8_7</a>."},"language":[{"iso":"eng"}],"oa":1,"date_created":"2019-10-14T06:57:49Z","volume":11785,"title":"Strategy representation by decision trees with linear classifiers","oa_version":"Preprint","scopus_import":"1","day":"04","author":[{"first_name":"Pranav","last_name":"Ashok","full_name":"Ashok, Pranav"},{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Jan","full_name":"Křetínský, Jan","last_name":"Křetínský"},{"first_name":"Christoph","orcid":"0000-0001-8622-7887","full_name":"Lampert, Christoph","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","last_name":"Lampert"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","full_name":"Toman, Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X","first_name":"Viktor"}],"publication_identifier":{"isbn":["9783030302801"],"issn":["0302-9743"],"eisbn":["9783030302818"]},"publication_status":"published","abstract":[{"text":"Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of   𝜔 -regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.","lang":"eng"}],"intvolume":"     11785"},{"year":"2019","isi":1,"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"external_id":{"isi":["000564108400004"]},"ec_funded":1,"date_published":"2019-11-01T00:00:00Z","status":"public","publication":"ACM Transactions on Programming Languages and Systems","project":[{"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","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"_id":"7158","date_updated":"2024-03-25T23:30:19Z","type":"journal_article","article_processing_charge":"No","doi":"10.1145/3363525","publisher":"ACM","quality_controlled":"1","ddc":["000"],"department":[{"_id":"KrCh"}],"file":[{"content_type":"application/pdf","access_level":"open_access","file_name":"2019_ACMTransactions_Chatterjee.pdf","success":1,"checksum":"291cc86a07bd010d4815e177dac57b70","relation":"main_file","creator":"dernst","date_updated":"2020-10-08T12:58:10Z","date_created":"2020-10-08T12:58:10Z","file_size":667357,"file_id":"8632"}],"article_number":"23","month":"11","citation":{"apa":"Chatterjee, K., Goharshady, A. K., Goyal, P., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2019). Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 23, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>.","ista":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. 2019. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. ACM Transactions on Programming Languages and Systems. 41(4), 23.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Prateesh Goyal, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>.","ieee":"K. Chatterjee, A. K. Goharshady, P. Goyal, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4. ACM, 2019.","short":"K. Chatterjee, A.K. Goharshady, P. Goyal, R. Ibsen-Jensen, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 41 (2019).","ama":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>"},"issue":"4","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa":1,"language":[{"iso":"eng"}],"volume":41,"date_created":"2019-12-09T08:33:33Z","article_type":"original","scopus_import":"1","day":"01","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Goyal, Prateesh","last_name":"Goyal","first_name":"Prateesh"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"orcid":"0000-0002-8943-0722","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis"}],"oa_version":"Submitted Version","title":"Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth","file_date_updated":"2020-10-08T12:58:10Z","publication_status":"published","publication_identifier":{"issn":["0164-0925"]},"has_accepted_license":"1","abstract":[{"text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, and so on. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, and so on. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in an important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect we consider is that the control flow graphs for most programs have constant treewidth.\r\n\r\nOur main contributions are simple and implementable algorithms that support multiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing but can answer subsequent queries significantly faster as compared to the current algorithmic solutions for interprocedural dataflow analysis. We have also implemented our algorithms and evaluated their performance for performing on-demand interprocedural dataflow analysis on various domains, such as for live variable analysis and reaching definitions, on a standard benchmark set. Our experimental results align with our theoretical statements and show that after a lightweight preprocessing, on-demand queries are answered much faster than the standard existing algorithmic approaches.\r\n","lang":"eng"}],"intvolume":"        41"},{"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1907.11514"}],"quality_controlled":"1","page":"123-141","date_updated":"2023-09-06T14:55:15Z","_id":"7231","type":"conference","doi":"10.1007/978-3-030-29662-9_8","article_processing_charge":"No","alternative_title":["LNCS"],"publisher":"Springer Nature","date_published":"2019-08-13T00:00:00Z","conference":{"end_date":"2019-08-29","start_date":"2019-08-27","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","location":"Amsterdam, The Netherlands"},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"status":"public","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","isi":1,"year":"2019","external_id":{"arxiv":["1907.11514"],"isi":["000611677700008"]},"publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["978-3-0302-9661-2"]},"abstract":[{"lang":"eng","text":"Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature."}],"intvolume":"     11750","volume":11750,"date_created":"2020-01-05T23:00:47Z","author":[{"last_name":"Kong","full_name":"Kong, Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","first_name":"Hui"},{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"first_name":"Yu","last_name":"Jiang","full_name":"Jiang, Yu"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"scopus_import":"1","day":"13","title":"Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty","oa_version":"Preprint","citation":{"apa":"Kong, H., Bartocci, E., Jiang, Y., &#38; Henzinger, T. A. (2019). Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">https://doi.org/10.1007/978-3-030-29662-9_8</a>","mla":"Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">10.1007/978-3-030-29662-9_8</a>.","ista":"Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11750, 123–141.","chicago":"Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:123–41. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">https://doi.org/10.1007/978-3-030-29662-9_8</a>.","ieee":"H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 123–141.","short":"H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.","ama":"Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:123-141. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">10.1007/978-3-030-29662-9_8</a>"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa":1,"language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"month":"08","arxiv":1}]