[{"project":[{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"page":"233-253","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":57,"publisher":"EasyChair","date_published":"2018-10-23T00:00:00Z","publication_status":"published","external_id":{"arxiv":["1909.04983"]},"abstract":[{"lang":"eng","text":"Solving parity games, which are equivalent to modal μ-calculus model checking, is a central algorithmic problem in formal methods, with applications in reactive synthesis, program repair, verification of branching-time properties, etc. Besides the standard compu- tation model with the explicit representation of games, another important theoretical model of computation is that of set-based symbolic algorithms. Set-based symbolic algorithms use basic set operations and one-step predecessor operations on the implicit description of games, rather than the explicit representation. The significance of symbolic algorithms is that they provide scalable algorithms for large finite-state systems, as well as for infinite-state systems with finite quotient. Consider parity games on graphs with n vertices and parity conditions with d priorities. While there is a rich literature of explicit algorithms for parity games, the main results for set-based symbolic algorithms are as follows: (a) the basic algorithm that requires O(nd) symbolic operations and O(d) symbolic space; and (b) an improved algorithm that requires O(nd/3+1) symbolic operations and O(n) symbolic space. In this work, our contributions are as follows: (1) We present a black-box set-based symbolic algorithm based on the explicit progress measure algorithm. Two important consequences of our algorithm are as follows: (a) a set-based symbolic algorithm for parity games that requires quasi-polynomially many symbolic operations and O(n) symbolic space; and (b) any future improvement in progress measure based explicit algorithms immediately imply an efficiency improvement in our set-based symbolic algorithm for parity games. (2) We present a set-based symbolic algorithm that requires quasi-polynomially many symbolic operations and O(d · log n) symbolic space. Moreover, for the important special case of d ≤ log n, our algorithm requires only polynomially many symbolic operations and poly-logarithmic symbolic space."}],"ddc":["000"],"file_date_updated":"2022-05-17T07:51:08Z","_id":"10883","doi":"10.29007/5z5k","citation":{"apa":"Chatterjee, K., Dvořák, W., Henzinger, M. H., &#38; Svozil, A. (2018). Quasipolynomial set-based symbolic algorithms for parity games. In <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i> (Vol. 57, pp. 233–253). Awassa, Ethiopia: EasyChair. <a href=\"https://doi.org/10.29007/5z5k\">https://doi.org/10.29007/5z5k</a>","mla":"Chatterjee, Krishnendu, et al. “Quasipolynomial Set-Based Symbolic Algorithms for Parity Games.” <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>, vol. 57, EasyChair, 2018, pp. 233–53, doi:<a href=\"https://doi.org/10.29007/5z5k\">10.29007/5z5k</a>.","ista":"Chatterjee K, Dvořák W, Henzinger MH, Svozil A. 2018. Quasipolynomial set-based symbolic algorithms for parity games. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing, vol. 57, 233–253.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvořák, Monika H Henzinger, and Alexander Svozil. “Quasipolynomial Set-Based Symbolic Algorithms for Parity Games.” In <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>, 57:233–53. EasyChair, 2018. <a href=\"https://doi.org/10.29007/5z5k\">https://doi.org/10.29007/5z5k</a>.","ama":"Chatterjee K, Dvořák W, Henzinger MH, Svozil A. Quasipolynomial set-based symbolic algorithms for parity games. In: <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>. Vol 57. EasyChair; 2018:233-253. doi:<a href=\"https://doi.org/10.29007/5z5k\">10.29007/5z5k</a>","ieee":"K. Chatterjee, W. Dvořák, M. H. Henzinger, and A. Svozil, “Quasipolynomial set-based symbolic algorithms for parity games,” in <i>22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>, Awassa, Ethiopia, 2018, vol. 57, pp. 233–253.","short":"K. Chatterjee, W. Dvořák, M.H. Henzinger, A. Svozil, in:, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair, 2018, pp. 233–253."},"date_created":"2022-03-18T12:46:32Z","acknowledgement":"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 an ERC Starting grant (279307: Graph Games). For M.H the research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013) /ERC Grant Agreement no. 340506.","year":"2018","ec_funded":1,"alternative_title":["EPiC Series in Computing"],"type":"conference","status":"public","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Dvořák","full_name":"Dvořák, Wolfgang","first_name":"Wolfgang"},{"orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"last_name":"Svozil","full_name":"Svozil, Alexander","first_name":"Alexander"}],"arxiv":1,"oa_version":"Published Version","day":"23","user_id":"72615eeb-f1f3-11ec-aa25-d4573ddc34fd","file":[{"file_size":720893,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","creator":"dernst","date_updated":"2022-05-17T07:51:08Z","date_created":"2022-05-17T07:51:08Z","file_id":"11392","checksum":"1229aa8640bd6db610c85decf2265480","file_name":"2018_EPiCs_Chatterjee.pdf","success":1}],"conference":{"end_date":"2018-11-21","location":"Awassa, Ethiopia","start_date":"2018-11-17","name":"LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"publication_identifier":{"issn":["2398-7340"]},"month":"10","language":[{"iso":"eng"}],"publication":"22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning","title":"Quasipolynomial set-based symbolic algorithms for parity games","oa":1,"date_updated":"2022-07-29T09:24:31Z","article_processing_charge":"No","intvolume":"        57","scopus_import":"1","has_accepted_license":"1"},{"type":"conference","status":"public","month":"07","conference":{"name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2018-07-13","location":"Stockholm, Sweden","end_date":"2018-07-19"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.10601"}],"day":"01","arxiv":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Elgyütt","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","first_name":"Adrian","full_name":"Elgyütt, Adrian"},{"full_name":"Novotny, Petr","first_name":"Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Owen","full_name":"Rouillé, Owen","last_name":"Rouillé"}],"language":[{"iso":"eng"}],"isi":1,"intvolume":"      2018","scopus_import":"1","article_processing_charge":"No","oa":1,"date_updated":"2025-06-02T08:53:48Z","title":"Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives","date_published":"2018-07-01T00:00:00Z","publisher":"IJCAI","quality_controlled":"1","volume":2018,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"4692 - 4699","project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"abstract":[{"lang":"eng","text":"Partially-observable Markov decision processes (POMDPs) with discounted-sum payoff are a standard framework to model a wide range of problems related to decision making under uncertainty. Traditionally, the goal has been to obtain policies that optimize the expectation of the discounted-sum payoff. A key drawback of the expectation measure is that even low probability events with extreme payoff can significantly affect the expectation, and thus the obtained policies are not necessarily risk-averse. An alternate approach is to optimize the probability that the payoff is above a certain threshold, which allows obtaining risk-averse policies, but ignores optimization of the expectation. We consider the expectation optimization with probabilistic guarantee (EOPG) problem, where the goal is to optimize the expectation ensuring that the payoff is above a given threshold with at least a specified probability. We present several results on the EOPG problem, including the first algorithm to solve it."}],"external_id":{"arxiv":["1804.10601"],"isi":["000764175404117"]},"publication_status":"published","doi":"10.24963/ijcai.2018/652","_id":"24","ec_funded":1,"year":"2018","acknowledgement":"This research was supported by the Vienna Science and Technology Fund (WWTF) grant ICT15-003; Austrian Science Fund (FWF): S11407-N23(RiSE/SHiNE);and an ERC Start Grant (279307:Graph Games).\r\n","date_created":"2018-12-11T11:44:13Z","publist_id":"8031","citation":{"ieee":"K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé, “Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives,” presented at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol. 2018, pp. 4692–4699.","ama":"Chatterjee K, Elgyütt A, Novotný P, Rouillé O. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. In: Vol 2018. IJCAI; 2018:4692-4699. doi:<a href=\"https://doi.org/10.24963/ijcai.2018/652\">10.24963/ijcai.2018/652</a>","short":"K. Chatterjee, A. Elgyütt, P. Novotný, O. Rouillé, in:, IJCAI, 2018, pp. 4692–4699.","mla":"Chatterjee, Krishnendu, et al. <i>Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives</i>. Vol. 2018, IJCAI, 2018, pp. 4692–99, doi:<a href=\"https://doi.org/10.24963/ijcai.2018/652\">10.24963/ijcai.2018/652</a>.","chicago":"Chatterjee, Krishnendu, Adrian Elgyütt, Petr Novotný, and Owen Rouillé. “Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives,” 2018:4692–99. IJCAI, 2018. <a href=\"https://doi.org/10.24963/ijcai.2018/652\">https://doi.org/10.24963/ijcai.2018/652</a>.","ista":"Chatterjee K, Elgyütt A, Novotný P, Rouillé O. 2018. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018, 4692–4699.","apa":"Chatterjee, K., Elgyütt, A., Novotný, P., &#38; Rouillé, O. (2018). Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives (Vol. 2018, pp. 4692–4699). Presented at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm, Sweden: IJCAI. <a href=\"https://doi.org/10.24963/ijcai.2018/652\">https://doi.org/10.24963/ijcai.2018/652</a>"}},{"publication":"Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence","language":[{"iso":"eng"}],"isi":1,"scopus_import":"1","oa":1,"date_updated":"2025-06-02T08:53:40Z","article_processing_charge":"No","title":"Goal-HSVI: Heuristic search value iteration for goal-POMDPs","status":"public","type":"conference","conference":{"location":"Stockholm, Sweden","end_date":"2018-07-19","name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2018-07-13"},"month":"07","oa_version":"Published Version","day":"01","main_file_link":[{"url":"https://doi.org/10.24963/ijcai.2018/662","open_access":"1"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"last_name":"Horák","first_name":"Karel","full_name":"Horák, Karel"},{"last_name":"Bošanský","full_name":"Bošanský, Branislav","first_name":"Branislav"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"doi":"10.24963/ijcai.2018/662","_id":"25","ec_funded":1,"acknowledgement":"∗This work has been supported by Vienna Science and Technology Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Starting grant (279307: Graph Games). This research was sponsored by the Army Research Laboratory and was accomplished under Cooperative Agreement Number W911NF-13-2-0045 (ARL Cyber Security CRA). ","year":"2018","publist_id":"8030","date_created":"2018-12-11T11:44:13Z","citation":{"mla":"Horák, Karel, et al. “Goal-HSVI: Heuristic Search Value Iteration for Goal-POMDPs.” <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, vol. 2018–July, IJCAI, 2018, pp. 4764–70, doi:<a href=\"https://doi.org/10.24963/ijcai.2018/662\">10.24963/ijcai.2018/662</a>.","ista":"Horák K, Bošanský B, Chatterjee K. 2018. Goal-HSVI: Heuristic search value iteration for goal-POMDPs. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018–July, 4764–4770.","chicago":"Horák, Karel, Branislav Bošanský, and Krishnendu Chatterjee. “Goal-HSVI: Heuristic Search Value Iteration for Goal-POMDPs.” In <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, 2018–July:4764–70. IJCAI, 2018. <a href=\"https://doi.org/10.24963/ijcai.2018/662\">https://doi.org/10.24963/ijcai.2018/662</a>.","ieee":"K. Horák, B. Bošanský, and K. Chatterjee, “Goal-HSVI: Heuristic search value iteration for goal-POMDPs,” in <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>, Stockholm, Sweden, 2018, vol. 2018–July, pp. 4764–4770.","ama":"Horák K, Bošanský B, Chatterjee K. Goal-HSVI: Heuristic search value iteration for goal-POMDPs. In: <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i>. Vol 2018-July. IJCAI; 2018:4764-4770. doi:<a href=\"https://doi.org/10.24963/ijcai.2018/662\">10.24963/ijcai.2018/662</a>","short":"K. Horák, B. Bošanský, K. Chatterjee, in:, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, 2018, pp. 4764–4770.","apa":"Horák, K., Bošanský, B., &#38; Chatterjee, K. (2018). Goal-HSVI: Heuristic search value iteration for goal-POMDPs. In <i>Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence</i> (Vol. 2018–July, pp. 4764–4770). Stockholm, Sweden: IJCAI. <a href=\"https://doi.org/10.24963/ijcai.2018/662\">https://doi.org/10.24963/ijcai.2018/662</a>"},"publisher":"IJCAI","date_published":"2018-07-01T00:00:00Z","department":[{"_id":"KrCh"}],"page":"4764 - 4770","quality_controlled":"1","volume":"2018-July","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"external_id":{"isi":["000764175404127"]},"abstract":[{"lang":"eng","text":"Partially observable Markov decision processes (POMDPs) are the standard models for planning under uncertainty with both finite and infinite horizon. Besides the well-known discounted-sum objective, indefinite-horizon objective (aka Goal-POMDPs) is another classical objective for POMDPs. In this case, given a set of target states and a positive cost for each transition, the optimization objective is to minimize the expected total cost until a target state is reached. In the literature, RTDP-Bel or heuristic search value iteration (HSVI) have been used for solving Goal-POMDPs. Neither of these algorithms has theoretical convergence guarantees, and HSVI may even fail to terminate its trials. We give the following contributions: (1) We discuss the challenges introduced in Goal-POMDPs and illustrate how they prevent the original HSVI from converging. (2) We present a novel algorithm inspired by HSVI, termed Goal-HSVI, and show that our algorithm has convergence guarantees. (3) We show that Goal-HSVI outperforms RTDP-Bel on a set of well-known examples."}],"publication_status":"published"},{"status":"public","type":"journal_article","author":[{"first_name":"Moshe","full_name":"Hoffman, Moshe","last_name":"Hoffman"},{"last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","first_name":"Christian","full_name":"Hilbe, Christian"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"file":[{"creator":"dernst","file_size":194734,"relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2018_NatureHumanBeh_Hoffman.pdf","file_id":"7051","checksum":"32efaf06a597495c184df91b3fbb19c0","date_updated":"2020-07-14T12:45:54Z","date_created":"2019-11-19T08:17:23Z"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"28","oa_version":"Submitted Version","month":"05","language":[{"iso":"eng"}],"publication":"Nature Human Behaviour","title":"The signal-burying game can explain why we obscure positive traits and good deeds","article_processing_charge":"No","oa":1,"date_updated":"2023-09-19T10:12:03Z","has_accepted_license":"1","scopus_import":"1","intvolume":"         2","isi":1,"project":[{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"}],"volume":2,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"397 - 404","date_published":"2018-05-28T00:00:00Z","publisher":"Nature Publishing Group","publication_status":"published","abstract":[{"lang":"eng","text":"People sometimes make their admirable deeds and accomplishments hard to spot, such as by giving anonymously or avoiding bragging. Such ‘buried’ signals are hard to reconcile with standard models of signalling or indirect reciprocity, which motivate costly pro-social behaviour by reputational gains. To explain these phenomena, we design a simple game theory model, which we call the signal-burying game. This game has the feature that senders can bury their signal by deliberately reducing the probability of the signal being observed. If the signal is observed, however, it is identified as having been buried. We show under which conditions buried signals can be maintained, using static equilibrium concepts and calculations of the evolutionary dynamics. We apply our analysis to shed light on a number of otherwise puzzling social phenomena, including modesty, anonymous donations, subtlety in art and fashion, and overeagerness."}],"external_id":{"isi":["000435551300009"]},"ddc":["000"],"article_type":"original","_id":"293","file_date_updated":"2020-07-14T12:45:54Z","doi":"10.1038/s41562-018-0354-z","citation":{"short":"M. Hoffman, C. Hilbe, M. Nowak, Nature Human Behaviour 2 (2018) 397–404.","ama":"Hoffman M, Hilbe C, Nowak M. The signal-burying game can explain why we obscure positive traits and good deeds. <i>Nature Human Behaviour</i>. 2018;2:397-404. doi:<a href=\"https://doi.org/10.1038/s41562-018-0354-z\">10.1038/s41562-018-0354-z</a>","ieee":"M. Hoffman, C. Hilbe, and M. Nowak, “The signal-burying game can explain why we obscure positive traits and good deeds,” <i>Nature Human Behaviour</i>, vol. 2. Nature Publishing Group, pp. 397–404, 2018.","mla":"Hoffman, Moshe, et al. “The Signal-Burying Game Can Explain Why We Obscure Positive Traits and Good Deeds.” <i>Nature Human Behaviour</i>, vol. 2, Nature Publishing Group, 2018, pp. 397–404, doi:<a href=\"https://doi.org/10.1038/s41562-018-0354-z\">10.1038/s41562-018-0354-z</a>.","chicago":"Hoffman, Moshe, Christian Hilbe, and Martin Nowak. “The Signal-Burying Game Can Explain Why We Obscure Positive Traits and Good Deeds.” <i>Nature Human Behaviour</i>. Nature Publishing Group, 2018. <a href=\"https://doi.org/10.1038/s41562-018-0354-z\">https://doi.org/10.1038/s41562-018-0354-z</a>.","ista":"Hoffman M, Hilbe C, Nowak M. 2018. The signal-burying game can explain why we obscure positive traits and good deeds. Nature Human Behaviour. 2, 397–404.","apa":"Hoffman, M., Hilbe, C., &#38; Nowak, M. (2018). The signal-burying game can explain why we obscure positive traits and good deeds. <i>Nature Human Behaviour</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/s41562-018-0354-z\">https://doi.org/10.1038/s41562-018-0354-z</a>"},"publist_id":"7588","date_created":"2018-12-11T11:45:39Z","year":"2018","acknowledgement":"This work was supported by a grant from the John Templeton Foundation and by the Office of Naval Research Grant N00014-16-1-2914 (M.A.N.). C.H. acknowledges generous support from the ISTFELLOW programme and by the Schrödinger scholarship of the Austrian Science Fund (FWF) J3475.","related_material":{"link":[{"description":"News on IST Homepage","url":"https://ist.ac.at/en/news/the-logic-of-modesty-why-it-pays-to-be-humble/","relation":"press_release"}]},"ec_funded":1},{"language":[{"iso":"eng"}],"oa":1,"date_updated":"2025-06-02T08:53:40Z","article_processing_charge":"No","title":"Strategy representation by decision trees in reactive synthesis","isi":1,"scopus_import":"1","has_accepted_license":"1","intvolume":"     10805","alternative_title":["LNCS"],"status":"public","type":"conference","author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8122-2881","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan"},{"first_name":"Viktor","full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman"}],"conference":{"start_date":"2018-04-14","name":"TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2018-04-20","location":"Thessaloniki, Greece"},"month":"04","oa_version":"Published Version","day":"12","file":[{"creator":"dernst","access_level":"open_access","relation":"main_file","file_size":1829940,"content_type":"application/pdf","file_name":"2018_LNCS_Brazdil.pdf","checksum":"b13874ffb114932ad9cc2586b7469db4","file_id":"5723","date_updated":"2020-07-14T12:45:57Z","date_created":"2018-12-17T16:29:08Z"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file_date_updated":"2020-07-14T12:45:57Z","_id":"297","doi":"10.1007/978-3-319-89960-2_21","year":"2018","citation":{"chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Jan Kretinsky, and Viktor Toman. “Strategy Representation by Decision Trees in Reactive Synthesis,” 10805:385–407. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">https://doi.org/10.1007/978-3-319-89960-2_21</a>.","mla":"Brázdil, Tomáš, et al. <i>Strategy Representation by Decision Trees in Reactive Synthesis</i>. Vol. 10805, Springer, 2018, pp. 385–407, doi:<a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">10.1007/978-3-319-89960-2_21</a>.","ista":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. 2018. Strategy representation by decision trees in reactive synthesis. TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10805, 385–407.","ieee":"T. Brázdil, K. Chatterjee, J. Kretinsky, and V. Toman, “Strategy representation by decision trees in reactive synthesis,” presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10805, pp. 385–407.","ama":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. Strategy representation by decision trees in reactive synthesis. In: Vol 10805. Springer; 2018:385-407. doi:<a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">10.1007/978-3-319-89960-2_21</a>","short":"T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.","apa":"Brázdil, T., Chatterjee, K., Kretinsky, J., &#38; Toman, V. (2018). Strategy representation by decision trees in reactive synthesis (Vol. 10805, pp. 385–407). Presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. <a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">https://doi.org/10.1007/978-3-319-89960-2_21</a>"},"publist_id":"7584","date_created":"2018-12-11T11:45:41Z","ec_funded":1,"project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"publisher":"Springer","date_published":"2018-04-12T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"385 - 407","volume":10805,"quality_controlled":"1","publication_status":"published","ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"isi":["000546326300021"]},"abstract":[{"text":"Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with ω -regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.","lang":"eng"}]},{"scopus_import":"1","isi":1,"title":"Lower bounds for symbolic computation on graphs: Strongly connected components, liveness, safety, and diameter","article_processing_charge":"No","oa":1,"date_updated":"2025-06-02T08:53:40Z","language":[{"iso":"eng"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Preprint","day":"01","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1711.09148"}],"month":"01","conference":{"end_date":"2018-01-10","location":"New Orleans, Louisiana, United States","start_date":"2018-01-07","name":"SODA: Symposium on Discrete Algorithms"},"arxiv":1,"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Dvorák","first_name":"Wolfgang","full_name":"Dvorák, Wolfgang"},{"orcid":"0000-0002-5008-6530","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"last_name":"Loitzenbauer","full_name":"Loitzenbauer, Veronika","first_name":"Veronika"}],"status":"public","type":"conference","ec_funded":1,"citation":{"short":"K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, ACM, 2018, pp. 2341–2356.","ama":"Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Lower bounds for symbolic computation on graphs: Strongly connected components, liveness, safety, and diameter. In: ACM; 2018:2341-2356. doi:<a href=\"https://doi.org/10.1137/1.9781611975031.151\">10.1137/1.9781611975031.151</a>","ieee":"K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Lower bounds for symbolic computation on graphs: Strongly connected components, liveness, safety, and diameter,” presented at the SODA: Symposium on Discrete Algorithms, New Orleans, Louisiana, United States, 2018, pp. 2341–2356.","ista":"Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2018. Lower bounds for symbolic computation on graphs: Strongly connected components, liveness, safety, and diameter. SODA: Symposium on Discrete Algorithms, 2341–2356.","mla":"Chatterjee, Krishnendu, et al. <i>Lower Bounds for Symbolic Computation on Graphs: Strongly Connected Components, Liveness, Safety, and Diameter</i>. ACM, 2018, pp. 2341–56, doi:<a href=\"https://doi.org/10.1137/1.9781611975031.151\">10.1137/1.9781611975031.151</a>.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika Loitzenbauer. “Lower Bounds for Symbolic Computation on Graphs: Strongly Connected Components, Liveness, Safety, and Diameter,” 2341–56. ACM, 2018. <a href=\"https://doi.org/10.1137/1.9781611975031.151\">https://doi.org/10.1137/1.9781611975031.151</a>.","apa":"Chatterjee, K., Dvorák, W., Henzinger, M. H., &#38; Loitzenbauer, V. (2018). Lower bounds for symbolic computation on graphs: Strongly connected components, liveness, safety, and diameter (pp. 2341–2356). Presented at the SODA: Symposium on Discrete Algorithms, New Orleans, Louisiana, United States: ACM. <a href=\"https://doi.org/10.1137/1.9781611975031.151\">https://doi.org/10.1137/1.9781611975031.151</a>"},"publist_id":"7555","date_created":"2018-12-11T11:45:45Z","year":"2018","doi":"10.1137/1.9781611975031.151","_id":"310","abstract":[{"lang":"eng","text":"A model of computation that is widely used in the formal analysis of reactive systems is symbolic algorithms. In this model the access to the input graph is restricted to consist of symbolic operations, which are expensive in comparison to the standard RAM operations. We give lower bounds on the number of symbolic operations for basic graph problems such as the computation of the strongly connected components and of the approximate diameter as well as for fundamental problems in model checking such as safety, liveness, and coliveness. Our lower bounds are linear in the number of vertices of the graph, even for constant-diameter graphs. For none of these problems lower bounds on the number of symbolic operations were known before. The lower bounds show an interesting separation of these problems from the reachability problem, which can be solved with O(D) symbolic operations, where D is the diameter of the graph. Additionally we present an approximation algorithm for the graph diameter which requires Õ(n/D) symbolic steps to achieve a (1 +ϵ)-approximation for any constant &gt; 0. This compares to O(n/D) symbolic steps for the (naive) exact algorithm and O(D) symbolic steps for a 2-approximation. Finally we also give a refined analysis of the strongly connected components algorithms of [15], showing that it uses an optimal number of symbolic steps that is proportional to the sum of the diameters of the strongly connected components."}],"external_id":{"isi":["000483921200152"],"arxiv":["1711.09148"]},"publication_status":"published","quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"2341 - 2356","date_published":"2018-01-01T00:00:00Z","publisher":"ACM","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}]},{"publication_status":"published","ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"abstract":[{"text":"Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i)~a simplified programming language for smart contracts; (ii)~an automatic translation of the programs to state-based games; (iii)~an abstraction-refinement approach to solve such games; and (iv)~experimental results on real-world-inspired smart contracts.","lang":"eng"}],"project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"publisher":"Springer","date_published":"2018-04-01T00:00:00Z","page":"739 - 767","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":10801,"acknowledgement":"The research was partially supported by Vienna Science and Technology Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Starting grant (279307: Graph Games).","year":"2018","citation":{"short":"K. Chatterjee, A.K. Goharshady, Y. Velner, in:, Springer, 2018, pp. 739–767.","ieee":"K. Chatterjee, A. K. Goharshady, and Y. Velner, “Quantitative analysis of smart contracts,” presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece, 2018, vol. 10801, pp. 739–767.","ama":"Chatterjee K, Goharshady AK, Velner Y. Quantitative analysis of smart contracts. In: Vol 10801. Springer; 2018:739-767. doi:<a href=\"https://doi.org/10.1007/978-3-319-89884-1_26\">10.1007/978-3-319-89884-1_26</a>","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Yaron Velner. “Quantitative Analysis of Smart Contracts,” 10801:739–67. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-89884-1_26\">https://doi.org/10.1007/978-3-319-89884-1_26</a>.","ista":"Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 739–767.","mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Analysis of Smart Contracts</i>. Vol. 10801, Springer, 2018, pp. 739–67, doi:<a href=\"https://doi.org/10.1007/978-3-319-89884-1_26\">10.1007/978-3-319-89884-1_26</a>.","apa":"Chatterjee, K., Goharshady, A. K., &#38; Velner, Y. (2018). Quantitative analysis of smart contracts (Vol. 10801, pp. 739–767). Presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece: Springer. <a href=\"https://doi.org/10.1007/978-3-319-89884-1_26\">https://doi.org/10.1007/978-3-319-89884-1_26</a>"},"publist_id":"7554","date_created":"2018-12-11T11:45:45Z","ec_funded":1,"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"file_date_updated":"2020-07-14T12:46:00Z","_id":"311","doi":"10.1007/978-3-319-89884-1_26","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Goharshady, Amir","first_name":"Amir","orcid":"0000-0003-1702-6584","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"conference":{"location":"Thessaloniki, Greece","end_date":"2018-04-19","name":"ESOP: European Symposium on Programming","start_date":"2018-04-16"},"month":"04","day":"01","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"dernst","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_size":1394993,"file_id":"5716","checksum":"9c8a8338c571903b599b6ca93abd2cce","file_name":"2018_ESOP_Chatterjee.pdf","date_created":"2018-12-17T15:45:49Z","date_updated":"2020-07-14T12:46:00Z"}],"alternative_title":["LNCS"],"type":"conference","status":"public","oa":1,"date_updated":"2025-06-02T08:53:41Z","article_processing_charge":"No","title":"Quantitative analysis of smart contracts","scopus_import":"1","intvolume":"     10801","has_accepted_license":"1","language":[{"iso":"eng"}]},{"_id":"325","doi":"10.1145/3158122","citation":{"chicago":"Agrawal, Sheshansh, Krishnendu Chatterjee, and Petr Novotný. “Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs,” Vol. 2. ACM, 2018. <a href=\"https://doi.org/10.1145/3158122\">https://doi.org/10.1145/3158122</a>.","mla":"Agrawal, Sheshansh, et al. <i>Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs</i>. Vol. 2, no. POPL, 34, ACM, 2018, doi:<a href=\"https://doi.org/10.1145/3158122\">10.1145/3158122</a>.","ista":"Agrawal S, Chatterjee K, Novotný P. 2018. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. POPL: Principles of Programming Languages vol. 2, 34.","short":"S. Agrawal, K. Chatterjee, P. Novotný, in:, ACM, 2018.","ama":"Agrawal S, Chatterjee K, Novotný P. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. In: Vol 2. ACM; 2018. doi:<a href=\"https://doi.org/10.1145/3158122\">10.1145/3158122</a>","ieee":"S. Agrawal, K. Chatterjee, and P. Novotný, “Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs,” presented at the POPL: Principles of Programming Languages, Los Angeles, CA, USA, 2018, vol. 2, no. POPL.","apa":"Agrawal, S., Chatterjee, K., &#38; Novotný, P. (2018). Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs (Vol. 2). Presented at the POPL: Principles of Programming Languages, Los Angeles, CA, USA: ACM. <a href=\"https://doi.org/10.1145/3158122\">https://doi.org/10.1145/3158122</a>"},"publist_id":"7540","date_created":"2018-12-11T11:45:50Z","year":"2018","article_number":"34","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"volume":2,"quality_controlled":"1","department":[{"_id":"KrCh"}],"date_published":"2018-01-01T00:00:00Z","publisher":"ACM","publication_status":"published","abstract":[{"lang":"eng","text":"Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks whether a given program program terminates with probability 1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). Although deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to programs of restricted control-flow structure. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on benchmarks adapted from previous work to demonstrate the effectiveness of our approach."}],"external_id":{"arxiv":["1709.04037"]},"language":[{"iso":"eng"}],"title":"Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs","issue":"POPL","oa":1,"date_updated":"2021-01-12T07:42:07Z","intvolume":"         2","status":"public","type":"conference","arxiv":1,"author":[{"first_name":"Sheshansh","full_name":"Agrawal, Sheshansh","last_name":"Agrawal"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr","first_name":"Petr"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","day":"01","main_file_link":[{"url":"https://arxiv.org/abs/1709.04037","open_access":"1"}],"month":"01","conference":{"location":"Los Angeles, CA, USA","end_date":"2018-01-13","name":"POPL: Principles of Programming Languages","start_date":"2018-01-07"}},{"language":[{"iso":"eng"}],"intvolume":"      2018","scopus_import":"1","isi":1,"title":"Sensor synthesis for POMDPs with reachability objectives","article_processing_charge":"No","oa":1,"date_updated":"2023-09-19T14:44:14Z","type":"conference","status":"public","alternative_title":["ICAPS"],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1710.00675"}],"day":"01","month":"06","conference":{"end_date":"2018-06-29","location":"Delft, Netherlands","start_date":"2018-06-24","name":"ICAPS: International Conference on Automated Planning and Scheduling"},"arxiv":1,"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Chemlík, Martin","first_name":"Martin","last_name":"Chemlík"},{"full_name":"Topcu, Ufuk","first_name":"Ufuk","last_name":"Topcu"}],"_id":"34","ec_funded":1,"date_created":"2018-12-11T11:44:16Z","publist_id":"8021","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Sensor Synthesis for POMDPs with Reachability Objectives</i>. Vol. 2018, AAAI Press, 2018, pp. 47–55.","ista":"Chatterjee K, Chemlík M, Topcu U. 2018. Sensor synthesis for POMDPs with reachability objectives. ICAPS: International Conference on Automated Planning and Scheduling, ICAPS, vol. 2018, 47–55.","chicago":"Chatterjee, Krishnendu, Martin Chemlík, and Ufuk Topcu. “Sensor Synthesis for POMDPs with Reachability Objectives,” 2018:47–55. AAAI Press, 2018.","short":"K. Chatterjee, M. Chemlík, U. Topcu, in:, AAAI Press, 2018, pp. 47–55.","ama":"Chatterjee K, Chemlík M, Topcu U. Sensor synthesis for POMDPs with reachability objectives. In: Vol 2018. AAAI Press; 2018:47-55.","ieee":"K. Chatterjee, M. Chemlík, and U. Topcu, “Sensor synthesis for POMDPs with reachability objectives,” presented at the ICAPS: International Conference on Automated Planning and Scheduling, Delft, Netherlands, 2018, vol. 2018, pp. 47–55.","apa":"Chatterjee, K., Chemlík, M., &#38; Topcu, U. (2018). Sensor synthesis for POMDPs with reachability objectives (Vol. 2018, pp. 47–55). Presented at the ICAPS: International Conference on Automated Planning and Scheduling, Delft, Netherlands: AAAI Press."},"year":"2018","quality_controlled":"1","volume":2018,"page":"47 - 55","department":[{"_id":"KrCh"}],"date_published":"2018-06-01T00:00:00Z","publisher":"AAAI Press","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"abstract":[{"lang":"eng","text":"Partially observable Markov decision processes (POMDPs) are widely used in probabilistic planning problems in which an agent interacts with an environment using noisy and imprecise sensors. We study a setting in which the sensors are only partially defined and the goal is to synthesize “weakest” additional sensors, such that in the resulting POMDP, there is a small-memory policy for the agent that almost-surely (with probability 1) satisfies a reachability objective. We show that the problem is NP-complete, and present a symbolic algorithm by encoding the problem into SAT instances. We illustrate trade-offs between the amount of memory of the policy and the number of additional sensors on a simple example. We have implemented our approach and consider three classical POMDP examples from the literature, and show that in all the examples the number of sensors can be significantly decreased (as compared to the existing solutions in the literature) without increasing the complexity of the policies."}],"external_id":{"isi":["000492986200006"],"arxiv":["1710.00675"]},"publication_status":"published"},{"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Dvorák","first_name":"Wolfgang","full_name":"Dvorák, Wolfgang"},{"orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","full_name":"Henzinger, Monika H","first_name":"Monika H"},{"first_name":"Alexander","full_name":"Svozil, Alexander","last_name":"Svozil"}],"arxiv":1,"conference":{"end_date":"2018-06-29","location":"Delft, Netherlands","start_date":"2018-06-24","name":"ICAPS: International Conference on Automated Planning and Scheduling"},"month":"06","main_file_link":[{"url":"https://arxiv.org/abs/1804.07031","open_access":"1"}],"oa_version":"None","day":"01","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","type":"conference","status":"public","date_updated":"2023-09-26T10:41:41Z","oa":1,"article_processing_charge":"No","title":"Algorithms and conditional lower bounds for planning problems","isi":1,"scopus_import":"1","language":[{"iso":"eng"}],"publication":"28th International Conference on Automated Planning and Scheduling ","publication_status":"published","external_id":{"arxiv":["1804.07031"],"isi":["000492986200007"]},"abstract":[{"text":"We consider planning problems for graphs, Markov decision processes (MDPs), and games on graphs. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems where there are k different target sets, and the problems are as follows: (a) the coverage problem asks whether there is a plan for each individual target set; and (b) the sequential target reachability problem asks whether the targets can be reached in sequence. For the coverage problem, we present a linear-time algorithm for graphs, and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs and for the sequential reachability problem games on graphs are harder than MDPs and graphs; and (ii) objective-separation results showing that for MDPs the coverage problem is harder than the sequential target problem.","lang":"eng"}],"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"publisher":"AAAI Press","date_published":"2018-06-01T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","year":"2018","publist_id":"8020","citation":{"apa":"Chatterjee, K., Dvorák, W., Henzinger, M. H., &#38; Svozil, A. (2018). Algorithms and conditional lower bounds for planning problems. In <i>28th International Conference on Automated Planning and Scheduling </i>. Delft, Netherlands: AAAI Press.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Alexander Svozil. “Algorithms and Conditional Lower Bounds for Planning Problems.” In <i>28th International Conference on Automated Planning and Scheduling </i>. AAAI Press, 2018.","ista":"Chatterjee K, Dvorák W, Henzinger MH, Svozil A. 2018. Algorithms and conditional lower bounds for planning problems. 28th International Conference on Automated Planning and Scheduling . ICAPS: International Conference on Automated Planning and Scheduling.","mla":"Chatterjee, Krishnendu, et al. “Algorithms and Conditional Lower Bounds for Planning Problems.” <i>28th International Conference on Automated Planning and Scheduling </i>, AAAI Press, 2018.","ieee":"K. Chatterjee, W. Dvorák, M. H. Henzinger, and A. Svozil, “Algorithms and conditional lower bounds for planning problems,” in <i>28th International Conference on Automated Planning and Scheduling </i>, Delft, Netherlands, 2018.","ama":"Chatterjee K, Dvorák W, Henzinger MH, Svozil A. Algorithms and conditional lower bounds for planning problems. In: <i>28th International Conference on Automated Planning and Scheduling </i>. AAAI Press; 2018.","short":"K. Chatterjee, W. Dvorák, M.H. Henzinger, A. Svozil, in:, 28th International Conference on Automated Planning and Scheduling , AAAI Press, 2018."},"date_created":"2018-12-11T11:44:17Z","ec_funded":1,"related_material":{"record":[{"status":"public","relation":"later_version","id":"9293"}]},"_id":"35"},{"status":"public","type":"journal_article","file":[{"checksum":"571b8cc0ba14e8d5d8b18e439a9835eb","file_id":"7052","file_name":"2018_NatureHumanBeh_Hilbe.pdf","date_updated":"2020-07-14T12:46:25Z","date_created":"2019-11-19T08:19:51Z","creator":"dernst","file_size":598033,"content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Submitted Version","day":"19","month":"03","author":[{"full_name":"Hilbe, Christian","first_name":"Christian","orcid":"0000-0001-5116-955X","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"publication":"Nature Human Behaviour","language":[{"iso":"eng"}],"has_accepted_license":"1","intvolume":"         2","scopus_import":"1","isi":1,"title":"Partners and rivals in direct reciprocity","article_processing_charge":"No","oa":1,"date_updated":"2023-09-13T09:38:54Z","volume":2,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"469–477","date_published":"2018-03-19T00:00:00Z","publisher":"Nature Publishing Group","project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"abstract":[{"text":"Reciprocity is a major factor in human social life and accounts for a large part of cooperation in our communities. Direct reciprocity arises when repeated interactions occur between the same individuals. The framework of iterated games formalizes this phenomenon. Despite being introduced more than five decades ago, the concept keeps offering beautiful surprises. Recent theoretical research driven by new mathematical tools has proposed a remarkable dichotomy among the crucial strategies: successful individuals either act as partners or as rivals. Rivals strive for unilateral advantages by applying selfish or extortionate strategies. Partners aim to share the payoff for mutual cooperation, but are ready to fight back when being exploited. Which of these behaviours evolves depends on the environment. Whereas small population sizes and a limited number of rounds favour rivalry, partner strategies are selected when populations are large and relationships stable. Only partners allow for evolution of cooperation, while the rivals’ attempt to put themselves first leads to defection. Hilbe et al. synthesize recent theoretical work on zero-determinant and ‘rival’ versus ‘partner’ strategies in social dilemmas. They describe the environments under which these contrasting selfish or cooperative strategies emerge in evolution.","lang":"eng"}],"external_id":{"isi":["000446612000016"]},"ddc":["000"],"publication_status":"published","doi":"10.1038/s41562-018-0320-9","article_type":"review","_id":"419","file_date_updated":"2020-07-14T12:46:25Z","related_material":{"link":[{"relation":"erratum","url":"http://doi.org/10.1038/s41562-018-0342-3"}]},"ec_funded":1,"date_created":"2018-12-11T11:46:22Z","publist_id":"7404","citation":{"apa":"Hilbe, C., Chatterjee, K., &#38; Nowak, M. (2018). Partners and rivals in direct reciprocity. <i>Nature Human Behaviour</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/s41562-018-0320-9\">https://doi.org/10.1038/s41562-018-0320-9</a>","short":"C. Hilbe, K. Chatterjee, M. Nowak, Nature Human Behaviour 2 (2018) 469–477.","ieee":"C. Hilbe, K. Chatterjee, and M. Nowak, “Partners and rivals in direct reciprocity,” <i>Nature Human Behaviour</i>, vol. 2. Nature Publishing Group, pp. 469–477, 2018.","ama":"Hilbe C, Chatterjee K, Nowak M. Partners and rivals in direct reciprocity. <i>Nature Human Behaviour</i>. 2018;2:469–477. doi:<a href=\"https://doi.org/10.1038/s41562-018-0320-9\">10.1038/s41562-018-0320-9</a>","mla":"Hilbe, Christian, et al. “Partners and Rivals in Direct Reciprocity.” <i>Nature Human Behaviour</i>, vol. 2, Nature Publishing Group, 2018, pp. 469–477, doi:<a href=\"https://doi.org/10.1038/s41562-018-0320-9\">10.1038/s41562-018-0320-9</a>.","chicago":"Hilbe, Christian, Krishnendu Chatterjee, and Martin Nowak. “Partners and Rivals in Direct Reciprocity.” <i>Nature Human Behaviour</i>. Nature Publishing Group, 2018. <a href=\"https://doi.org/10.1038/s41562-018-0320-9\">https://doi.org/10.1038/s41562-018-0320-9</a>.","ista":"Hilbe C, Chatterjee K, Nowak M. 2018. Partners and rivals in direct reciprocity. Nature Human Behaviour. 2, 469–477."},"year":"2018"},{"file_date_updated":"2020-07-14T12:46:31Z","_id":"454","doi":"10.1038/s41467-017-02721-8","acknowledgement":"This work was supported by the European Research Council (ERC) start grant 279307: Graph Games (C.K.), Austrian Science Fund (FWF) grant no P23499-N23 (C.K.), FWF\r\nNFN grant no S11407-N23 RiSE/SHiNE (C.K.), Office of Naval Research grant N00014-16-1-2914 (M.A.N.), National Cancer Institute grant CA179991 (M.A.N.) and by the John Templeton Foundation. J.G.R. is supported by an Erwin Schrödinger fellowship\r\n(Austrian Science Fund FWF J-3996). C.H. acknowledges generous support from the\r\nISTFELLOW program. The Program for Evolutionary Dynamics is supported in part by\r\na gift from B Wu and Eric Larson.","year":"2018","citation":{"ista":"Reiter J, Hilbe C, Rand D, Chatterjee K, Nowak M. 2018. Crosstalk in concurrent repeated games impedes direct reciprocity and requires stronger levels of forgiveness. Nature Communications. 9(1), 555.","chicago":"Reiter, Johannes, Christian Hilbe, David Rand, Krishnendu Chatterjee, and Martin Nowak. “Crosstalk in Concurrent Repeated Games Impedes Direct Reciprocity and Requires Stronger Levels of Forgiveness.” <i>Nature Communications</i>. Nature Publishing Group, 2018. <a href=\"https://doi.org/10.1038/s41467-017-02721-8\">https://doi.org/10.1038/s41467-017-02721-8</a>.","mla":"Reiter, Johannes, et al. “Crosstalk in Concurrent Repeated Games Impedes Direct Reciprocity and Requires Stronger Levels of Forgiveness.” <i>Nature Communications</i>, vol. 9, no. 1, 555, Nature Publishing Group, 2018, doi:<a href=\"https://doi.org/10.1038/s41467-017-02721-8\">10.1038/s41467-017-02721-8</a>.","ama":"Reiter J, Hilbe C, Rand D, Chatterjee K, Nowak M. Crosstalk in concurrent repeated games impedes direct reciprocity and requires stronger levels of forgiveness. <i>Nature Communications</i>. 2018;9(1). doi:<a href=\"https://doi.org/10.1038/s41467-017-02721-8\">10.1038/s41467-017-02721-8</a>","ieee":"J. Reiter, C. Hilbe, D. Rand, K. Chatterjee, and M. Nowak, “Crosstalk in concurrent repeated games impedes direct reciprocity and requires stronger levels of forgiveness,” <i>Nature Communications</i>, vol. 9, no. 1. Nature Publishing Group, 2018.","short":"J. Reiter, C. Hilbe, D. Rand, K. Chatterjee, M. Nowak, Nature Communications 9 (2018).","apa":"Reiter, J., Hilbe, C., Rand, D., Chatterjee, K., &#38; Nowak, M. (2018). Crosstalk in concurrent repeated games impedes direct reciprocity and requires stronger levels of forgiveness. <i>Nature Communications</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/s41467-017-02721-8\">https://doi.org/10.1038/s41467-017-02721-8</a>"},"publist_id":"7368","date_created":"2018-12-11T11:46:34Z","ec_funded":1,"article_number":"555","project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"}],"publisher":"Nature Publishing Group","date_published":"2018-02-07T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":9,"publication_status":"published","ddc":["004"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"isi":["000424318200001"]},"abstract":[{"lang":"eng","text":"Direct reciprocity is a mechanism for cooperation among humans. Many of our daily interactions are repeated. We interact repeatedly with our family, friends, colleagues, members of the local and even global community. In the theory of repeated games, it is a tacit assumption that the various games that a person plays simultaneously have no effect on each other. Here we introduce a general framework that allows us to analyze “crosstalk” between a player’s concurrent games. In the presence of crosstalk, the action a person experiences in one game can alter the person’s decision in another. We find that crosstalk impedes the maintenance of cooperation and requires stronger levels of forgiveness. The magnitude of the effect depends on the population structure. In more densely connected social groups, crosstalk has a stronger effect. A harsh retaliator, such as Tit-for-Tat, is unable to counteract crosstalk. The crosstalk framework provides a unified interpretation of direct and upstream reciprocity in the context of repeated games."}],"language":[{"iso":"eng"}],"publication":"Nature Communications","oa":1,"date_updated":"2023-09-11T12:51:03Z","pubrep_id":"964","issue":"1","article_processing_charge":"No","title":"Crosstalk in concurrent repeated games impedes direct reciprocity and requires stronger levels of forgiveness","isi":1,"has_accepted_license":"1","intvolume":"         9","scopus_import":"1","type":"journal_article","status":"public","author":[{"orcid":"0000-0002-0170-7353","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","first_name":"Johannes","full_name":"Reiter, Johannes"},{"orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","last_name":"Hilbe","first_name":"Christian","full_name":"Hilbe, Christian"},{"full_name":"Rand, David","first_name":"David","last_name":"Rand"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"month":"02","day":"07","oa_version":"Published Version","file":[{"creator":"system","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_size":843646,"file_id":"4741","file_name":"IST-2018-964-v1+1_2018_Hilbe_Crosstalk_in.pdf","checksum":"b6b90367545b4c615891c960ab0567f1","date_created":"2018-12-12T10:09:18Z","date_updated":"2020-07-14T12:46:31Z"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1"},{"status":"public","type":"journal_article","author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"full_name":"Kučera, Antonín","first_name":"Antonín","last_name":"Kučera"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"file_size":708657,"content_type":"application/pdf","relation":"main_file","access_level":"open_access","creator":"system","date_updated":"2020-07-14T12:44:42Z","date_created":"2018-12-12T10:11:30Z","checksum":"91271b23cf884d7c06d33bef0cd623b1","file_id":"4885","file_name":"IST-2016-717-v1+1_1-s2.0-S0022000016300897-main.pdf"}],"oa_version":"Published Version","day":"01","month":"03","language":[{"iso":"eng"}],"publication":"Journal of Computer and System Sciences","title":"Trading performance for stability in Markov decision processes","article_processing_charge":"No","oa":1,"date_updated":"2023-09-20T11:15:31Z","pubrep_id":"717","intvolume":"        84","scopus_import":"1","has_accepted_license":"1","isi":1,"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"volume":84,"quality_controlled":"1","page":"144 - 170","department":[{"_id":"KrCh"}],"date_published":"2017-03-01T00:00:00Z","publisher":"Elsevier","publication_status":"published","abstract":[{"lang":"eng","text":"We study controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize the expected mean-payoff performance and stability (also known as variability in the literature). We argue that the basic notion of expressing the stability using the statistical variance of the mean payoff is sometimes insufficient, and propose an alternative definition. We show that a strategy ensuring both the expected mean payoff and the variance below given bounds requires randomization and memory, under both the above definitions. We then show that the problem of finding such a strategy can be expressed as a set of constraints."}],"external_id":{"isi":["000388430000011"]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["004","006"],"_id":"1294","file_date_updated":"2020-07-14T12:44:42Z","doi":"10.1016/j.jcss.2016.09.009","citation":{"ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance for stability in Markov decision processes,” <i>Journal of Computer and System Sciences</i>, vol. 84. Elsevier, pp. 144–170, 2017.","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability in Markov decision processes. <i>Journal of Computer and System Sciences</i>. 2017;84:144-170. doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">10.1016/j.jcss.2016.09.009</a>","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, Journal of Computer and System Sciences 84 (2017) 144–170.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Trading Performance for Stability in Markov Decision Processes.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">https://doi.org/10.1016/j.jcss.2016.09.009</a>.","mla":"Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision Processes.” <i>Journal of Computer and System Sciences</i>, vol. 84, Elsevier, 2017, pp. 144–70, doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">10.1016/j.jcss.2016.09.009</a>.","ista":"Brázdil T, Chatterjee K, Forejt V, Kučera A. 2017. Trading performance for stability in Markov decision processes. Journal of Computer and System Sciences. 84, 144–170.","apa":"Brázdil, T., Chatterjee, K., Forejt, V., &#38; Kučera, A. (2017). Trading performance for stability in Markov decision processes. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2016.09.009\">https://doi.org/10.1016/j.jcss.2016.09.009</a>"},"date_created":"2018-12-11T11:51:12Z","publist_id":"6009","year":"2017","related_material":{"record":[{"status":"public","id":"2305","relation":"earlier_version"}]},"ec_funded":1},{"external_id":{"arxiv":["1701.05738"]},"abstract":[{"lang":"eng","text":"Transforming deterministic ω\r\n-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae."}],"publication_status":"published","page":"443-460","department":[{"_id":"KrCh"}],"volume":10205,"quality_controlled":"1","publisher":"Springer","date_published":"2017-03-31T00:00:00Z","date_created":"2023-06-21T13:21:14Z","citation":{"chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 10205:443–60. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">https://doi.org/10.1007/978-3-662-54577-5_26</a>.","mla":"Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 10205, Springer, 2017, pp. 443–60, doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">10.1007/978-3-662-54577-5_26</a>.","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance record for transforming Rabin automata into parity automata. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record for transforming Rabin automata into parity automata,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Uppsala, Sweden, 2017, vol. 10205, pp. 443–460.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record for transforming Rabin automata into parity automata. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 10205. Springer; 2017:443-460. doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">10.1007/978-3-662-54577-5_26</a>","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2017). Index appearance record for transforming Rabin automata into parity automata. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 10205, pp. 443–460). Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_26\">https://doi.org/10.1007/978-3-662-54577-5_26</a>"},"acknowledgement":"This work is partially funded by the DFG project “Verified Model Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.","year":"2017","doi":"10.1007/978-3-662-54577-5_26","_id":"13160","oa_version":"Preprint","day":"31","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1701.05738"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2017-04-22","location":"Uppsala, Sweden","end_date":"2017-04-29"},"publication_identifier":{"eissn":["1611-3349"],"eisbn":["9783662545775"],"isbn":["9783662545768"],"issn":["0302-9743"]},"month":"03","author":[{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165"},{"last_name":"Waldmann","first_name":"Clara","full_name":"Waldmann, Clara"},{"first_name":"Maximilian","full_name":"Weininger, Maximilian","last_name":"Weininger"}],"arxiv":1,"alternative_title":["LNCS"],"type":"conference","status":"public","intvolume":"     10205","title":"Index appearance record for transforming Rabin automata into parity automata","oa":1,"date_updated":"2023-06-21T13:29:46Z","article_processing_charge":"No","publication":"Tools and Algorithms for the Construction and Analysis of Systems","language":[{"iso":"eng"}]},{"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"page":"418","department":[{"_id":"KrCh"}],"publisher":"Institute of Science and Technology Austria","license":"https://creativecommons.org/licenses/by-nd/4.0/","supervisor":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"}],"date_published":"2017-08-09T00:00:00Z","publication_status":"published","abstract":[{"text":"This dissertation focuses on algorithmic aspects of program verification, and presents modeling and complexity advances on several problems related to the\r\nstatic analysis of programs, the stateless model checking of concurrent programs, and the competitive analysis of real-time scheduling algorithms.\r\nOur contributions can be broadly grouped into five categories.\r\n\r\nOur first contribution is a set of new algorithms and data structures for the quantitative and data-flow analysis of programs, based on the graph-theoretic notion of treewidth.\r\nIt has been observed that the control-flow graphs of typical programs have special structure, and are characterized as graphs of small treewidth.\r\nWe utilize this structural property to provide faster algorithms for the quantitative and data-flow analysis of recursive and concurrent programs.\r\nIn most cases we make an algebraic treatment of the considered problem,\r\nwhere several interesting analyses, such as the reachability, shortest path, and certain kind of data-flow analysis problems follow as special cases. \r\nWe exploit the constant-treewidth property to obtain algorithmic improvements for on-demand versions of the problems, \r\nand provide data structures with various tradeoffs between the resources spent in the preprocessing and querying phase.\r\nWe also improve on the algorithmic complexity of quantitative problems outside the algebraic path framework,\r\nnamely of the minimum mean-payoff, minimum ratio, and minimum initial credit for energy problems.\r\n\r\n\r\nOur second contribution is a set of algorithms for Dyck reachability with applications to data-dependence analysis and alias analysis.\r\nIn particular, we develop an optimal algorithm for Dyck reachability on bidirected graphs, which are ubiquitous in context-insensitive, field-sensitive points-to analysis.\r\nAdditionally, we develop an efficient algorithm for context-sensitive data-dependence analysis via Dyck reachability,\r\nwhere the task is to obtain analysis summaries of library code in the presence of callbacks.\r\nOur algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is (i)~linear in the number of call sites and (ii)~only logarithmic in the size of the whole library, as opposed to linear in the size of the whole library.\r\nFinally, we prove that Dyck reachability is Boolean Matrix Multiplication-hard in general, and the hardness also holds for graphs of constant treewidth.\r\nThis hardness result strongly indicates that there exist no combinatorial algorithms for Dyck reachability with truly subcubic complexity.\r\n\r\n\r\nOur third contribution is the formalization and algorithmic treatment of the Quantitative Interprocedural Analysis framework.\r\nIn this framework, the transitions of a recursive program are annotated as good, bad or neutral, and receive a weight which measures\r\nthe magnitude of their respective effect.\r\nThe Quantitative Interprocedural Analysis problem asks to determine whether there exists an infinite run of the program where the long-run ratio of the bad weights over the good weights is above a given threshold.\r\nWe illustrate how several quantitative problems related to static analysis of recursive programs can be instantiated in this framework,\r\nand present some case studies to this direction.\r\n\r\n\r\nOur fourth contribution is a new dynamic partial-order reduction for the stateless model checking of concurrent programs. Traditional approaches rely on the standard Mazurkiewicz equivalence between  traces, by means of partitioning the trace space into equivalence classes, and attempting to explore a few representatives from each class.\r\nWe present a new dynamic partial-order reduction method  called the Data-centric Partial Order Reduction (DC-DPOR).\r\nOur algorithm is based on a new equivalence between traces, called the observation equivalence.\r\nDC-DPOR explores a coarser partitioning of the trace space than any exploration method based on the standard Mazurkiewicz equivalence.\r\nDepending on the program, the new partitioning can be even exponentially coarser.\r\nAdditionally, DC-DPOR spends only polynomial time in each explored class.\r\n\r\n\r\nOur fifth contribution is the use of automata and game-theoretic verification techniques in the competitive analysis and synthesis of real-time scheduling algorithms for firm-deadline tasks.\r\nOn the analysis side, we leverage automata on infinite words to compute the competitive ratio of real-time schedulers subject to various environmental constraints.\r\nOn the synthesis side, we introduce a new instance of two-player mean-payoff partial-information games, and show\r\nhow the synthesis of an optimal real-time scheduler can be reduced to computing winning strategies in this new type of games.","lang":"eng"}],"ddc":["000"],"tmp":{"image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)"},"file_date_updated":"2020-07-14T12:48:10Z","_id":"821","doi":"10.15479/AT:ISTA:th_854","date_created":"2018-12-11T11:48:41Z","publist_id":"6828","citation":{"ieee":"A. Pavlogiannis, “Algorithmic advances in program analysis and their applications,” Institute of Science and Technology Austria, 2017.","ama":"Pavlogiannis A. Algorithmic advances in program analysis and their applications. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">10.15479/AT:ISTA:th_854</a>","short":"A. Pavlogiannis, Algorithmic Advances in Program Analysis and Their Applications, Institute of Science and Technology Austria, 2017.","mla":"Pavlogiannis, Andreas. <i>Algorithmic Advances in Program Analysis and Their Applications</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">10.15479/AT:ISTA:th_854</a>.","chicago":"Pavlogiannis, Andreas. “Algorithmic Advances in Program Analysis and Their Applications.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">https://doi.org/10.15479/AT:ISTA:th_854</a>.","ista":"Pavlogiannis A. 2017. Algorithmic advances in program analysis and their applications. Institute of Science and Technology Austria.","apa":"Pavlogiannis, A. (2017). <i>Algorithmic advances in program analysis and their applications</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">https://doi.org/10.15479/AT:ISTA:th_854</a>"},"acknowledgement":"First, I am thankful to my advisor, Krishnendu Chatterjee, for offering me the opportunity to\r\nmaterialize my scientific curiosity in a remarkably wide range of interesting topics, as well as for his constant availability and continuous support throughout my doctoral studies. I have had the privilege of collaborating with, discussing and getting inspired by all members of my committee: Thomas A. Henzinger, Ulrich Schmid and Martin A. Nowak. The role of the above four people has been very instrumental both to the research carried out for this dissertation, and to the researcher I evolved to in the process.\r\nI have greatly enjoyed my numerous brainstorming sessions with Rasmus Ibsen-Jensen, many\r\nof which led to results on low-treewidth graphs presented here.  I thank Alex Kößler for our\r\ndiscussions on modeling and analyzing real-time scheduling algorithms, Yaron Velner for our\r\ncollaboration on the Quantitative Interprocedural Analysis framework, and Nishant Sinha for our initial discussions on partial order reduction techniques in stateless model checking. I also thank Jan Otop, Ben Adlam, Bernhard Kragl and Josef Tkadlec for our fruitful collaborations on\r\ntopics outside the scope of this dissertation, as well as the interns Prateesh Goyal, Amir Kafshdar Goharshady, Samarth Mishra, Bhavya Choudhary and Marek Chalupa, with whom I have shared my excitement on various research topics. Together with my collaborators, I thank officemates and members of the Chatterjee and Henzinger groups throughout the years, Thorsten Tarrach, Ventsi Chonev, Roopsha Samanta, Przemek Daca, Mirco Giacobbe, Tanja Petrov, Ashutosh\r\nGupta,  Arjun Radhakrishna,  Petr Novontý,  Christian Hilbe,  Jakob Ruess,  Martin Chmelik,\r\nCezara Dragoi, Johannes Reiter, Andrey Kupriyanov, Guy Avni, Sasha Rubin, Jessica Davies, Hongfei Fu, Thomas Ferrère, Pavol Cerný, Ali Sezgin, Jan Kretínský, Sergiy Bogomolov, Hui\r\nKong, Benjamin Aminof, Duc-Hiep Chu, and Damien Zufferey.  Besides collaborations and office spaces, with many of the above people I have been fortunate to share numerous whiteboard\r\ndiscussions, as well as memorable long walks and amicable meals accompanied by stimulating\r\nconversations. I am highly indebted to Elisabeth Hacker for her continuous assistance in matters\r\nthat often exceeded her official duties, and who made my integration in Austria a smooth process.","year":"2017","ec_funded":1,"degree_awarded":"PhD","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"1071"},{"id":"1437","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"1602","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"1604"},{"status":"public","relation":"part_of_dissertation","id":"1607"},{"status":"public","relation":"part_of_dissertation","id":"1714"}]},"alternative_title":["ISTA Thesis"],"status":"public","type":"dissertation","author":[{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722"}],"day":"09","oa_version":"Published Version","file":[{"date_updated":"2020-07-14T12:48:10Z","date_created":"2018-12-12T10:11:44Z","file_name":"IST-2017-854-v1+1_Pavlogiannis_Thesis_PubRep.pdf","file_id":"4900","checksum":"3a3ec003f6ee73f41f82a544d63dfc77","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_size":4103115,"creator":"system"},{"creator":"dernst","access_level":"closed","relation":"source_file","file_size":14744374,"content_type":"application/zip","file_id":"6201","checksum":"bd2facc45ff8a2e20c5ed313c2ccaa83","file_name":"2017_thesis_Pavlogiannis.zip","date_created":"2019-04-05T07:59:31Z","date_updated":"2020-07-14T12:48:10Z"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"08","publication_identifier":{"issn":["2663-337X"]},"language":[{"iso":"eng"}],"title":"Algorithmic advances in program analysis and their applications","pubrep_id":"854","oa":1,"date_updated":"2023-09-07T12:01:59Z","article_processing_charge":"No","has_accepted_license":"1"},{"publication":"PNAS","language":[{"iso":"eng"}],"intvolume":"       114","scopus_import":1,"issue":"27","oa":1,"date_updated":"2021-01-12T08:11:21Z","title":"The red queen and king in finite populations","status":"public","type":"journal_article","pmid":1,"publication_identifier":{"issn":["00278424"]},"month":"07","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5502615/"}],"oa_version":"Submitted Version","day":"03","author":[{"full_name":"Veller, Carl","first_name":"Carl","last_name":"Veller"},{"full_name":"Hayward, Laura","first_name":"Laura","last_name":"Hayward"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"},{"last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","first_name":"Christian","full_name":"Hilbe, Christian"}],"doi":"10.1073/pnas.1702020114","_id":"699","year":"2017","citation":{"apa":"Veller, C., Hayward, L., Nowak, M., &#38; Hilbe, C. (2017). The red queen and king in finite populations. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1702020114\">https://doi.org/10.1073/pnas.1702020114</a>","short":"C. Veller, L. Hayward, M. Nowak, C. Hilbe, PNAS 114 (2017) E5396–E5405.","ieee":"C. Veller, L. Hayward, M. Nowak, and C. Hilbe, “The red queen and king in finite populations,” <i>PNAS</i>, vol. 114, no. 27. National Academy of Sciences, pp. E5396–E5405, 2017.","ama":"Veller C, Hayward L, Nowak M, Hilbe C. The red queen and king in finite populations. <i>PNAS</i>. 2017;114(27):E5396-E5405. doi:<a href=\"https://doi.org/10.1073/pnas.1702020114\">10.1073/pnas.1702020114</a>","chicago":"Veller, Carl, Laura Hayward, Martin Nowak, and Christian Hilbe. “The Red Queen and King in Finite Populations.” <i>PNAS</i>. National Academy of Sciences, 2017. <a href=\"https://doi.org/10.1073/pnas.1702020114\">https://doi.org/10.1073/pnas.1702020114</a>.","mla":"Veller, Carl, et al. “The Red Queen and King in Finite Populations.” <i>PNAS</i>, vol. 114, no. 27, National Academy of Sciences, 2017, pp. E5396–405, doi:<a href=\"https://doi.org/10.1073/pnas.1702020114\">10.1073/pnas.1702020114</a>.","ista":"Veller C, Hayward L, Nowak M, Hilbe C. 2017. The red queen and king in finite populations. PNAS. 114(27), E5396–E5405."},"date_created":"2018-12-11T11:48:00Z","publist_id":"7002","date_published":"2017-07-03T00:00:00Z","publisher":"National Academy of Sciences","volume":114,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"E5396 - E5405","abstract":[{"text":"In antagonistic symbioses, such as host–parasite interactions, one population’s success is the other’s loss. In mutualistic symbioses, such as division of labor, both parties can gain, but they might have different preferences over the possible mutualistic arrangements. The rates of evolution of the two populations in a symbiosis are important determinants of which population will be more successful: Faster evolution is thought to be favored in antagonistic symbioses (the “Red Queen effect”), but disfavored in certain mutualistic symbioses (the “Red King effect”). However, it remains unclear which biological parameters drive these effects. Here, we analyze the effects of the various determinants of evolutionary rate: generation time, mutation rate, population size, and the intensity of natural selection. Our main results hold for the case where mutation is infrequent. Slower evolution causes a long-term advantage in an important class of mutualistic interactions. Surprisingly, less intense selection is the strongest driver of this Red King effect, whereas relative mutation rates and generation times have little effect. In antagonistic interactions, faster evolution by any means is beneficial. Our results provide insight into the demographic evolution of symbionts. ","lang":"eng"}],"external_id":{"pmid":["28630336"]},"publication_status":"published"},{"volume":85,"quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2017-08-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","abstract":[{"lang":"eng","text":"Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts."}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["004","005"],"publication_status":"published","doi":"10.4230/LIPIcs.CONCUR.2017.5","_id":"711","file_date_updated":"2020-07-14T12:47:49Z","article_number":"5","date_created":"2018-12-11T11:48:04Z","citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Bidirectional nested weighted automata (Vol. 85). Presented at the 28th International Conference on Concurrency Theory, CONCUR, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.5</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Bidirectional nested weighted automata,” presented at the 28th International Conference on Concurrency Theory, CONCUR, Berlin, Germany, 2017, vol. 85.","ama":"Chatterjee K, Henzinger TA, Otop J. Bidirectional nested weighted automata. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">10.4230/LIPIcs.CONCUR.2017.5</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Bidirectional nested weighted automata. 28th International Conference on Concurrency Theory, CONCUR, LIPIcs, vol. 85, 5.","mla":"Chatterjee, Krishnendu, et al. <i>Bidirectional Nested Weighted Automata</i>. Vol. 85, 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">10.4230/LIPIcs.CONCUR.2017.5</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Bidirectional Nested Weighted Automata,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.5</a>."},"publist_id":"6976","year":"2017","type":"conference","status":"public","alternative_title":["LIPIcs"],"file":[{"file_id":"4661","checksum":"d2bda4783821a6358333fe27f11f4737","file_name":"IST-2017-886-v1+1_LIPIcs-CONCUR-2017-5.pdf","date_updated":"2020-07-14T12:47:49Z","date_created":"2018-12-12T10:08:02Z","creator":"system","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_size":570294}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","day":"01","month":"08","publication_identifier":{"issn":["18688969"]},"conference":{"name":"28th International Conference on Concurrency Theory, CONCUR","start_date":"2017-09-05","location":"Berlin, Germany","end_date":"2017-09-08"},"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"}],"language":[{"iso":"eng"}],"intvolume":"        85","has_accepted_license":"1","scopus_import":1,"title":"Bidirectional nested weighted automata","date_updated":"2021-01-12T08:11:53Z","oa":1,"pubrep_id":"886"},{"type":"journal_article","status":"public","month":"09","publication_identifier":{"issn":["00045411"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","day":"01","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1201.2829"}],"arxiv":1,"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"publication":"Journal of the ACM","language":[{"iso":"eng"}],"scopus_import":1,"intvolume":"        64","issue":"5","date_updated":"2021-01-12T08:12:08Z","oa":1,"title":"The complexity of mean-payoff pushdown games","date_published":"2017-09-01T00:00:00Z","publisher":"ACM","volume":64,"quality_controlled":"1","page":"34","department":[{"_id":"KrCh"}],"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"abstract":[{"lang":"eng","text":"Two-player games on graphs are central in many problems in formal verification and program analysis, such as synthesis and verification of open systems. In this work, we consider solving recursive game graphs (or pushdown game graphs) that model the control flow of sequential programs with recursion.While pushdown games have been studied before with qualitative objectives-such as reachability and ?-regular objectives- in this work, we study for the first time such games with the most well-studied quantitative objective, the mean-payoff objective. In pushdown games, two types of strategies are relevant: (1) global strategies, which depend on the entire global history; and (2) modular strategies, which have only local memory and thus do not depend on the context of invocation but rather only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity by showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games and memoryless modular strategies are sufficient in two-player pushdown games. Finally, we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded."}],"external_id":{"arxiv":["1201.2829"]},"publication_status":"published","doi":"10.1145/3121408","article_type":"original","_id":"716","ec_funded":1,"year":"2017","publist_id":"6964","citation":{"apa":"Chatterjee, K., &#38; Velner, Y. (2017). The complexity of mean-payoff pushdown games. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/3121408\">https://doi.org/10.1145/3121408</a>","ista":"Chatterjee K, Velner Y. 2017. The complexity of mean-payoff pushdown games. Journal of the ACM. 64(5), 34.","mla":"Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff Pushdown Games.” <i>Journal of the ACM</i>, vol. 64, no. 5, ACM, 2017, p. 34, doi:<a href=\"https://doi.org/10.1145/3121408\">10.1145/3121408</a>.","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff Pushdown Games.” <i>Journal of the ACM</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3121408\">https://doi.org/10.1145/3121408</a>.","short":"K. Chatterjee, Y. Velner, Journal of the ACM 64 (2017) 34.","ama":"Chatterjee K, Velner Y. The complexity of mean-payoff pushdown games. <i>Journal of the ACM</i>. 2017;64(5):34. doi:<a href=\"https://doi.org/10.1145/3121408\">10.1145/3121408</a>","ieee":"K. Chatterjee and Y. Velner, “The complexity of mean-payoff pushdown games,” <i>Journal of the ACM</i>, vol. 64, no. 5. ACM, p. 34, 2017."},"date_created":"2018-12-11T11:48:06Z"},{"oa":1,"date_updated":"2023-02-23T10:38:15Z","title":"Hyperplane separation technique for multidimensional mean-payoff games","intvolume":"        88","scopus_import":1,"language":[{"iso":"eng"}],"publication":"Journal of Computer and System Sciences","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"month":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","day":"01","main_file_link":[{"url":"https://arxiv.org/abs/1210.3141","open_access":"1"}],"status":"public","type":"journal_article","year":"2017","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No. P 23499-N23, FWF NFN Grant No. S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the RICH Model Toolkit (ICT COST Action IC0901), and was carried out in partial fulfillment of the requirements for the Ph.D. degree of the second author.","publist_id":"6963","citation":{"mla":"Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique for Multidimensional Mean-Payoff Games.” <i>Journal of Computer and System Sciences</i>, vol. 88, Academic Press, 2017, pp. 236–59, doi:<a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">10.1016/j.jcss.2017.04.005</a>.","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique for Multidimensional Mean-Payoff Games.” <i>Journal of Computer and System Sciences</i>. Academic Press, 2017. <a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">https://doi.org/10.1016/j.jcss.2017.04.005</a>.","ista":"Chatterjee K, Velner Y. 2017. Hyperplane separation technique for multidimensional mean-payoff games. Journal of Computer and System Sciences. 88, 236–259.","ieee":"K. Chatterjee and Y. Velner, “Hyperplane separation technique for multidimensional mean-payoff games,” <i>Journal of Computer and System Sciences</i>, vol. 88. Academic Press, pp. 236–259, 2017.","ama":"Chatterjee K, Velner Y. Hyperplane separation technique for multidimensional mean-payoff games. <i>Journal of Computer and System Sciences</i>. 2017;88:236-259. doi:<a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">10.1016/j.jcss.2017.04.005</a>","short":"K. Chatterjee, Y. Velner, Journal of Computer and System Sciences 88 (2017) 236–259.","apa":"Chatterjee, K., &#38; Velner, Y. (2017). Hyperplane separation technique for multidimensional mean-payoff games. <i>Journal of Computer and System Sciences</i>. Academic Press. <a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">https://doi.org/10.1016/j.jcss.2017.04.005</a>"},"date_created":"2018-12-11T11:48:07Z","related_material":{"record":[{"id":"2329","relation":"earlier_version","status":"public"}]},"ec_funded":1,"_id":"717","doi":"10.1016/j.jcss.2017.04.005","publication_status":"published","abstract":[{"text":"We consider finite-state and recursive game graphs with multidimensional mean-payoff objectives. In recursive games two types of strategies are relevant: global strategies and modular strategies. Our contributions are: (1) We show that finite-state multidimensional mean-payoff games can be solved in polynomial time if the number of dimensions and the maximal absolute value of weights are fixed; whereas for arbitrary dimensions the problem is coNP-complete. (2) We show that one-player recursive games with multidimensional mean-payoff objectives can be solved in polynomial time. Both above algorithms are based on hyperplane separation technique. (3) For recursive games we show that under modular strategies the multidimensional problem is undecidable. We show that if the number of modules, exits, and the maximal absolute value of the weights are fixed, then one-dimensional recursive mean-payoff games under modular strategies can be solved in polynomial time, whereas for unbounded number of exits or modules the problem is NP-hard.","lang":"eng"}],"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_published":"2017-09-01T00:00:00Z","publisher":"Academic Press","volume":88,"quality_controlled":"1","page":"236 - 259","department":[{"_id":"KrCh"}]},{"doi":"10.1007/s00236-017-0299-0","publication":"Acta Informatica","language":[{"iso":"eng"}],"_id":"719","scopus_import":1,"intvolume":"        54","title":"Special issue: Synthesis and SYNT 2014","date_created":"2018-12-11T11:48:07Z","citation":{"mla":"Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and SYNT 2014.” <i>Acta Informatica</i>, vol. 54, no. 6, Springer, 2017, pp. 543–44, doi:<a href=\"https://doi.org/10.1007/s00236-017-0299-0\">10.1007/s00236-017-0299-0</a>.","chicago":"Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and SYNT 2014.” <i>Acta Informatica</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s00236-017-0299-0\">https://doi.org/10.1007/s00236-017-0299-0</a>.","ista":"Chatterjee K, Ehlers R. 2017. Special issue: Synthesis and SYNT 2014. Acta Informatica. 54(6), 543–544.","short":"K. Chatterjee, R. Ehlers, Acta Informatica 54 (2017) 543–544.","ieee":"K. Chatterjee and R. Ehlers, “Special issue: Synthesis and SYNT 2014,” <i>Acta Informatica</i>, vol. 54, no. 6. Springer, pp. 543–544, 2017.","ama":"Chatterjee K, Ehlers R. Special issue: Synthesis and SYNT 2014. <i>Acta Informatica</i>. 2017;54(6):543-544. doi:<a href=\"https://doi.org/10.1007/s00236-017-0299-0\">10.1007/s00236-017-0299-0</a>","apa":"Chatterjee, K., &#38; Ehlers, R. (2017). Special issue: Synthesis and SYNT 2014. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-017-0299-0\">https://doi.org/10.1007/s00236-017-0299-0</a>"},"publist_id":"6961","year":"2017","issue":"6","date_updated":"2021-01-12T08:12:18Z","volume":54,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"543 - 544","date_published":"2017-09-01T00:00:00Z","status":"public","type":"journal_article","publisher":"Springer","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"The ubiquity of computation in modern machines and devices imposes a need to assert the correctness of their behavior. Especially in the case of safety-critical systems, their designers need to take measures that enforce their safe operation. Formal methods has emerged as a research field that addresses this challenge: by rigorously proving that all system executions adhere to their specifications, the correctness of an implementation under concern can be assured. To achieve this goal, a plethora of techniques are nowadays available, all of which are optimized for different system types and application domains.","lang":"eng"}],"day":"01","oa_version":"None","month":"09","publication_identifier":{"issn":["00015903"]},"publication_status":"published","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Ehlers, Rüdiger","first_name":"Rüdiger","last_name":"Ehlers"}]}]