[{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","year":"2022","date_updated":"2026-04-07T11:49:11Z","project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"has_accepted_license":"1","date_published":"2022-12-14T00:00:00Z","day":"14","type":"conference","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","doi":"10.4230/LIPIcs.FSTTCS.2022.11","ddc":["000"],"citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Complexity of spatial games,” in <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Madras, India, 2022, vol. 250.","short":"K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.","mla":"Chatterjee, Krishnendu, et al. “Complexity of Spatial Games.” <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 250, 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">10.4230/LIPIcs.FSTTCS.2022.11</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Complexity of Spatial Games.” In <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Vol. 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2022. Complexity of spatial games. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Foundations of Software Technology and Theoretical Computer Science vol. 250, 11:1-11:14.","ama":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Complexity of spatial games. In: <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">10.4230/LIPIcs.FSTTCS.2022.11</a>","apa":"Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., &#38; Svoboda, J. (2022). Complexity of spatial games. In <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 250). Madras, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11</a>"},"related_material":{"record":[{"id":"20138","relation":"dissertation_contains","status":"public"}]},"article_processing_charge":"No","conference":{"end_date":"2022-12-20","location":"Madras, India","start_date":"2022-12-18","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science"},"title":"Complexity of spatial games","month":"12","_id":"12101","ec_funded":1,"intvolume":"       250","publication":"42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","scopus_import":"1","file_date_updated":"2023-01-20T10:19:19Z","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"first_name":"Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","last_name":"Jecker","full_name":"Jecker, Ismael R"},{"orcid":"0000-0002-1419-3267","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","full_name":"Svoboda, Jakub"}],"oa":1,"publication_identifier":{"isbn":["9783959772617"],"issn":["1868-8969"]},"file":[{"success":1,"relation":"main_file","access_level":"open_access","date_created":"2023-01-20T10:19:19Z","file_id":"12323","creator":"dernst","file_name":"2022_LIPICs_Chatterjee.pdf","file_size":657396,"checksum":"a21e3ba2421e2c4a06aa2cb6d530ede1","content_type":"application/pdf","date_updated":"2023-01-20T10:19:19Z"}],"acknowledgement":"Krishnendu Chatterjee: The research was partially supported by the ERC CoG 863818\r\n(ForM-SMArt).\r\nIsmaël Jecker: The research was partially supported by the ERC grant 950398 (INFSYS).\r\nJakub Svoboda: The research was partially supported by the ERC CoG 863818 (ForM-SMArt)","corr_author":"1","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"date_created":"2023-01-01T23:00:50Z","publication_status":"published","abstract":[{"text":"Spatial games form a widely-studied class of games from biology and physics modeling the evolution of social behavior. Formally, such a game is defined by a square (d by d) payoff matrix M and an undirected graph G. Each vertex of G represents an individual, that initially follows some strategy i ∈ {1,2,…,d}. In each round of the game, every individual plays the matrix game with each of its neighbors: An individual following strategy i meeting a neighbor following strategy j receives a payoff equal to the entry (i,j) of M. Then, each individual updates its strategy to its neighbors' strategy with the highest sum of payoffs, and the next round starts. The basic computational problems consist of reachability between configurations and the average frequency of a strategy. For general spatial games and graphs, these problems are in PSPACE. In this paper, we examine restricted setting: the game is a prisoner’s dilemma; and G is a subgraph of grid. We prove that basic computational problems for spatial games with prisoner’s dilemma on a subgraph of a grid are PSPACE-hard.","lang":"eng"}],"article_number":"11:1-11:14","quality_controlled":"1","volume":250},{"article_processing_charge":"No","conference":{"start_date":"2021-12-15","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","end_date":"2021-12-17","location":"Virtual"},"citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Quantitative verification on product graphs of small treewidth. In <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 213). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42\">https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42</a>","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Quantitative verification on product graphs of small treewidth. In: <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 213. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2021. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42\">10.4230/LIPIcs.FSTTCS.2021.42</a>","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Quantitative verification on product graphs of small treewidth. 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 213, 42.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Quantitative Verification on Product Graphs of Small Treewidth.” In <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Vol. 213. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42\">https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Verification on Product Graphs of Small Treewidth.” <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 213, 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2021.42\">10.4230/LIPIcs.FSTTCS.2021.42</a>.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Quantitative verification on product graphs of small treewidth,” in <i>41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Virtual, 2021, vol. 213."},"_id":"10629","title":"Quantitative verification on product graphs of small treewidth","month":"11","doi":"10.4230/LIPIcs.FSTTCS.2021.42","alternative_title":["LIPIcs"],"ddc":["000"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","type":"conference","day":"29","status":"public","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","date_published":"2021-11-29T00:00:00Z","has_accepted_license":"1","year":"2021","oa_version":"Published Version","date_updated":"2024-10-09T21:01:23Z","abstract":[{"lang":"eng","text":"Product graphs arise naturally in formal verification and program analysis. For example, the analysis of two concurrent threads requires the product of two component control-flow graphs, and for language inclusion of deterministic automata the product of two automata is constructed. In many cases, the component graphs have constant treewidth, e.g., when the input contains control-flow graphs of programs. We consider the algorithmic analysis of products of two constant-treewidth graphs with respect to three classic specification languages, namely, (a) algebraic properties, (b) mean-payoff properties, and (c) initial credit for energy properties.\r\nOur main contributions are as follows. Consider a graph G that is the product of two constant-treewidth graphs of size n each. First, given an idempotent semiring, we present an algorithm that computes the semiring transitive closure of G in time Õ(n⁴). Since the output has size Θ(n⁴), our algorithm is optimal (up to polylog factors). Second, given a mean-payoff objective, we present an O(n³)-time algorithm for deciding whether the value of a starting state is non-negative, improving the previously known O(n⁴) bound. Third, given an initial credit for energy objective, we present an O(n⁵)-time algorithm for computing the minimum initial credit for all nodes of G, improving the previously known O(n⁸) bound. At the heart of our approach lies an algorithm for the efficient construction of strongly-balanced tree decompositions of constant-treewidth graphs. Given a constant-treewidth graph G' of n nodes and a positive integer λ, our algorithm constructs a binary tree decomposition of G' of width O(λ) with the property that the size of each subtree decreases geometrically with rate (1/2 + 2^{-λ})."}],"article_number":"42","volume":213,"quality_controlled":"1","department":[{"_id":"KrCh"}],"date_created":"2022-01-16T23:01:28Z","corr_author":"1","language":[{"iso":"eng"}],"publication_status":"published","file":[{"file_size":891566,"creator":"cchlebak","file_name":"2021_LIPIcs_Chatterjee.pdf","file_id":"10633","date_created":"2022-01-17T10:36:08Z","date_updated":"2022-01-17T10:36:08Z","checksum":"71141acdeffa9056f24d6dbef952d254","content_type":"application/pdf","success":1,"access_level":"open_access","relation":"main_file"}],"publication_identifier":{"isbn":["978-3-9597-7215-0"],"issn":["1868-8969"]},"oa":1,"file_date_updated":"2022-01-17T10:36:08Z","scopus_import":"1","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"}],"publication":"41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","intvolume":"       213"},{"month":"09","title":"Faster algorithms for quantitative verification in bounded treewidth graphs","_id":"9393","citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” <i>Formal Methods in System Design</i>, vol. 57. Springer, pp. 401–428, 2021.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>, vol. 57, Springer, 2021, pp. 401–28, doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 57, 401–428.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>. Springer, 2021. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. 2021;57:401-428. doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>"},"article_processing_charge":"No","arxiv":1,"article_type":"original","doi":"10.1007/s10703-021-00373-5","status":"public","type":"journal_article","publisher":"Springer","day":"01","date_updated":"2025-04-15T07:23:30Z","year":"2021","oa_version":"Preprint","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_published":"2021-09-01T00:00:00Z","page":"401-428","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","volume":57,"abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"publication_status":"published","language":[{"iso":"eng"}],"date_created":"2021-05-16T22:01:47Z","department":[{"_id":"KrCh"}],"external_id":{"arxiv":["1504.07384"],"isi":["000645490300001"]},"publication_identifier":{"eissn":["1572-8102"],"issn":["0925-9856"]},"oa":1,"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant (279307: Graph Games), and Microsoft faculty fellows award.","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.07384"}],"intvolume":"        57","isi":1,"ec_funded":1,"publication":"Formal Methods in System Design","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"scopus_import":"1"},{"publication_identifier":{"isbn":["9783959771597"],"issn":["1868-8969"]},"oa":1,"acknowledgement":"Krishnendu Chatterjee: The research was partially supported by the Vienna Science and\r\nTechnology Fund (WWTF) Project ICT15-003.\r\nIsmaël Jecker: This project has received funding from the European Union’s Horizon 2020 research\r\nand innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 754411.","file":[{"success":1,"relation":"main_file","access_level":"open_access","date_created":"2020-09-21T13:57:34Z","file_id":"8550","creator":"dernst","file_name":"2020_LIPIcs_Chatterjee.pdf","file_size":491374,"checksum":"bbd7c4f55d45f2ff2a0a4ef0e10a77b1","content_type":"application/pdf","date_updated":"2020-09-21T13:57:34Z"}],"ec_funded":1,"intvolume":"       170","scopus_import":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"last_name":"Jecker","full_name":"Jecker, Ismael R","first_name":"Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425"},{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","full_name":"Svoboda, Jakub"}],"publication":"45th International Symposium on Mathematical Foundations of Computer Science","file_date_updated":"2020-09-21T13:57:34Z","abstract":[{"lang":"eng","text":"Game of Life is a simple and elegant model to study dynamical system over networks. The model consists of a graph where every vertex has one of two types, namely, dead or alive. A configuration is a mapping of the vertices to the types. An update rule describes how the type of a vertex is updated given the types of its neighbors. In every round, all vertices are updated synchronously, which leads to a configuration update. While in general, Game of Life allows a broad range of update rules, we focus on two simple families of update rules, namely, underpopulation and overpopulation, that model several interesting dynamics studied in the literature. In both settings, a dead vertex requires at least a desired number of live neighbors to become alive. For underpopulation (resp., overpopulation), a live vertex requires at least (resp. at most) a desired number of live neighbors to remain alive. We study the basic computation problems, e.g., configuration reachability, for these two families of rules. For underpopulation rules, we show that these problems can be solved in polynomial time, whereas for overpopulation rules they are PSPACE-complete."}],"license":"https://creativecommons.org/licenses/by/3.0/","article_number":"22:1-22:13","quality_controlled":"1","volume":170,"language":[{"iso":"eng"}],"external_id":{"arxiv":["2007.02894"]},"department":[{"_id":"KrCh"}],"date_created":"2020-09-20T22:01:36Z","publication_status":"published","day":"18","type":"conference","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","short":"CC BY (3.0)"},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2020","oa_version":"Published Version","date_updated":"2025-07-10T11:57:06Z","date_published":"2020-08-18T00:00:00Z","has_accepted_license":"1","project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2020. Simplified game of life: Algorithms and complexity. 45th International Symposium on Mathematical Foundations of Computer Science. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 170, 22:1-22:13.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Simplified Game of Life: Algorithms and Complexity.” In <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, Vol. 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.22\">https://doi.org/10.4230/LIPIcs.MFCS.2020.22</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., &#38; Svoboda, J. (2020). Simplified game of life: Algorithms and complexity. In <i>45th International Symposium on Mathematical Foundations of Computer Science</i> (Vol. 170). Prague, Czech Republic: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.22\">https://doi.org/10.4230/LIPIcs.MFCS.2020.22</a>","ama":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Simplified game of life: Algorithms and complexity. In: <i>45th International Symposium on Mathematical Foundations of Computer Science</i>. Vol 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.22\">10.4230/LIPIcs.MFCS.2020.22</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Simplified game of life: Algorithms and complexity,” in <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, Prague, Czech Republic, 2020, vol. 170.","mla":"Chatterjee, Krishnendu, et al. “Simplified Game of Life: Algorithms and Complexity.” <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, vol. 170, 22:1-22:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.22\">10.4230/LIPIcs.MFCS.2020.22</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 45th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020."},"article_processing_charge":"No","conference":{"location":"Prague, Czech Republic","end_date":"2020-08-28","name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2020-08-24"},"title":"Simplified game of life: Algorithms and complexity","month":"08","_id":"8533","doi":"10.4230/LIPIcs.MFCS.2020.22","alternative_title":["LIPIcs"],"arxiv":1,"ddc":["000"]},{"year":"2020","oa_version":"Preprint","date_updated":"2025-07-03T11:44:58Z","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369"}],"date_published":"2020-04-03T00:00:00Z","page":"1798-1805","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","day":"03","publisher":"Association for the Advancement of Artificial Intelligence","type":"journal_article","issue":"02","arxiv":1,"OA_place":"repository","doi":"10.1609/aaai.v34i02.5546","article_type":"original","OA_type":"green","title":"All-pay bidding games on graphs","month":"04","_id":"9197","citation":{"ieee":"G. Avni, R. Ibsen-Jensen, and J. Tkadlec, “All-pay bidding games on graphs,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 02. Association for the Advancement of Artificial Intelligence, pp. 1798–1805, 2020.","mla":"Avni, Guy, et al. “All-Pay Bidding Games on Graphs.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 02, Association for the Advancement of Artificial Intelligence, 2020, pp. 1798–805, doi:<a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">10.1609/aaai.v34i02.5546</a>.","short":"G. Avni, R. Ibsen-Jensen, J. Tkadlec, Proceedings of the AAAI Conference on Artificial Intelligence 34 (2020) 1798–1805.","ista":"Avni G, Ibsen-Jensen R, Tkadlec J. 2020. All-pay bidding games on graphs. Proceedings of the AAAI Conference on Artificial Intelligence. 34(02), 1798–1805.","chicago":"Avni, Guy, Rasmus Ibsen-Jensen, and Josef Tkadlec. “All-Pay Bidding Games on Graphs.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2020. <a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">https://doi.org/10.1609/aaai.v34i02.5546</a>.","apa":"Avni, G., Ibsen-Jensen, R., &#38; Tkadlec, J. (2020). All-pay bidding games on graphs. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. New York, NY, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">https://doi.org/10.1609/aaai.v34i02.5546</a>","ama":"Avni G, Ibsen-Jensen R, Tkadlec J. All-pay bidding games on graphs. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2020;34(02):1798-1805. doi:<a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">10.1609/aaai.v34i02.5546</a>"},"article_processing_charge":"No","conference":{"start_date":"2020-02-07","name":"AAAI: Conference on Artificial Intelligence","end_date":"2020-02-12","location":"New York, NY, United States"},"intvolume":"        34","author":[{"orcid":"0000-0001-5588-8287","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy","last_name":"Avni"},{"full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684"}],"publication":"Proceedings of the AAAI Conference on Artificial Intelligence","scopus_import":"1","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"],"isbn":["9781577358350"]},"oa":1,"acknowledgement":"This research was supported by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner fellowship).","main_file_link":[{"url":"https://arxiv.org/abs/1911.08360","open_access":"1"}],"publication_status":"published","language":[{"iso":"eng"}],"external_id":{"arxiv":["1911.08360"]},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_created":"2021-02-25T09:05:18Z","quality_controlled":"1","volume":34,"abstract":[{"lang":"eng","text":"In this paper we introduce and study all-pay bidding games, a class of two player, zero-sum games on graphs. The game proceeds as follows. We place a token on some vertex in the graph and assign budgets to the two players. Each turn, each player submits a sealed legal bid (non-negative and below their remaining budget), which is deducted from their budget and the highest bidder moves the token onto an adjacent vertex. The game ends once a sink is reached, and Player 1 pays Player 2 the outcome that is associated with the sink. The players attempt to maximize their expected outcome. Our games model settings where effort (of no inherent value) needs to be invested in an ongoing and stateful manner. On the negative side, we show that even in simple games on DAGs, optimal strategies may require a distribution over bids with infinite support. A central quantity in bidding games is the ratio of the players budgets. On the positive side, we show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation for the optimal strategy for that ratio. We also implement it, show that it performs well, and suggests interesting properties of these games. Then, given an outcome c, we show an algorithm for finding the necessary and sufficient initial ratio for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally, while the general case has not previously been studied, solving the specific game in which Player 1 wins iff he wins the first two auctions, has been long stated as an open question, which we solve."}]},{"type":"research_data_reference","day":"15","main_file_link":[{"url":"https://doi.org/10.6084/m9.figshare.5973013.v1","open_access":"1"}],"publisher":"Royal Society","status":"public","oa":1,"author":[{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389"},{"orcid":"0000-0002-1097-9684","last_name":"Tkadlec","full_name":"Tkadlec, Josef","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"user_id":"0043cee0-e5fc-11ee-9736-f83bc23afbf0","date_published":"2020-10-15T00:00:00Z","year":"2020","oa_version":"Published Version","date_updated":"2025-04-15T08:12:20Z","abstract":[{"lang":"eng","text":"Data and mathematica notebooks for plotting figures from Language learning with communication between learners"}],"article_processing_charge":"No","citation":{"chicago":"Ibsen-Jensen, Rasmus, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Data and Mathematica Notebooks for Plotting Figures from Language Learning with Communication between Learners from Language Acquisition with Communication between Learners.” Royal Society, 2020. <a href=\"https://doi.org/10.6084/m9.figshare.5973013.v1\">https://doi.org/10.6084/m9.figshare.5973013.v1</a>.","ista":"Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. 2020. Data and mathematica notebooks for plotting figures from language learning with communication between learners from language acquisition with communication between learners, Royal Society, <a href=\"https://doi.org/10.6084/m9.figshare.5973013.v1\">10.6084/m9.figshare.5973013.v1</a>.","ama":"Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. Data and mathematica notebooks for plotting figures from language learning with communication between learners from language acquisition with communication between learners. 2020. doi:<a href=\"https://doi.org/10.6084/m9.figshare.5973013.v1\">10.6084/m9.figshare.5973013.v1</a>","apa":"Ibsen-Jensen, R., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2020). Data and mathematica notebooks for plotting figures from language learning with communication between learners from language acquisition with communication between learners. Royal Society. <a href=\"https://doi.org/10.6084/m9.figshare.5973013.v1\">https://doi.org/10.6084/m9.figshare.5973013.v1</a>","ieee":"R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, and M. Nowak, “Data and mathematica notebooks for plotting figures from language learning with communication between learners from language acquisition with communication between learners.” Royal Society, 2020.","short":"R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, M. Nowak, (2020).","mla":"Ibsen-Jensen, Rasmus, et al. <i>Data and Mathematica Notebooks for Plotting Figures from Language Learning with Communication between Learners from Language Acquisition with Communication between Learners</i>. Royal Society, 2020, doi:<a href=\"https://doi.org/10.6084/m9.figshare.5973013.v1\">10.6084/m9.figshare.5973013.v1</a>."},"related_material":{"record":[{"id":"198","relation":"used_in_publication","status":"public"}]},"_id":"9814","title":"Data and mathematica notebooks for plotting figures from language learning with communication between learners from language acquisition with communication between learners","month":"10","department":[{"_id":"KrCh"}],"date_created":"2021-08-06T13:09:57Z","OA_place":"publisher","doi":"10.6084/m9.figshare.5973013.v1","OA_type":"hybrid"},{"month":"04","title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","_id":"7810","related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"citation":{"chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” In <i>European Symposium on Programming</i>, 12075:112–40. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">https://doi.org/10.1007/978-3-030-44914-8_5</a>.","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2020. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. European Symposium on Programming. ESOP: Programming Languages and Systems, LNCS, vol. 12075, 112–140.","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In: <i>European Symposium on Programming</i>. Vol 12075. Springer Nature; 2020:112-140. doi:<a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">10.1007/978-3-030-44914-8_5</a>","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2020). Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In <i>European Symposium on Programming</i> (Vol. 12075, pp. 112–140). Dublin, Ireland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">https://doi.org/10.1007/978-3-030-44914-8_5</a>","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal and perfectly parallel algorithms for on-demand data-flow analysis,” in <i>European Symposium on Programming</i>, Dublin, Ireland, 2020, vol. 12075, pp. 112–140.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 112–140.","mla":"Chatterjee, Krishnendu, et al. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” <i>European Symposium on Programming</i>, vol. 12075, Springer Nature, 2020, pp. 112–40, doi:<a href=\"https://doi.org/10.1007/978-3-030-44914-8_5\">10.1007/978-3-030-44914-8_5</a>."},"conference":{"start_date":"2020-04-25","name":"ESOP: Programming Languages and Systems","end_date":"2020-04-30","location":"Dublin, Ireland"},"article_processing_charge":"No","ddc":["000"],"alternative_title":["LNCS"],"doi":"10.1007/978-3-030-44914-8_5","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","publisher":"Springer Nature","day":"18","type":"conference","date_updated":"2026-04-28T22:31:04Z","year":"2020","oa_version":"Published Version","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies"}],"has_accepted_license":"1","date_published":"2020-04-18T00:00:00Z","page":"112-140","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","quality_controlled":"1","volume":12075,"abstract":[{"lang":"eng","text":"Interprocedural data-flow analyses form an expressive and useful paradigm of numerous static analysis applications, such as live variables analysis, alias analysis and null pointers analysis. The most widely-used framework for interprocedural data-flow analysis is IFDS, which encompasses distributive data-flow functions over a finite domain. On-demand data-flow analyses restrict the focus of the analysis on specific program locations and data facts. This setting provides a natural split between (i) an offline (or preprocessing) phase, where the program is partially analyzed and analysis summaries are created, and (ii) an online (or query) phase, where analysis queries arrive on demand and the summaries are used to speed up answering queries.\r\nIn this work, we consider on-demand IFDS analyses where the queries concern program locations of the same procedure (aka same-context queries). We exploit the fact that flow graphs of programs have low treewidth to develop faster algorithms that are space and time optimal for many common data-flow analyses, in both the preprocessing and the query phase. We also use treewidth to develop query solutions that are embarrassingly parallelizable, i.e. the total work for answering each query is split to a number of threads such that each thread performs only a constant amount of work. Finally, we implement a static analyzer based on our algorithms, and perform a series of on-demand analysis experiments on standard benchmarks. Our experimental results show a drastic speed-up of the queries after only a lightweight preprocessing phase, which significantly outperforms existing techniques."}],"publication_status":"published","language":[{"iso":"eng"}],"corr_author":"1","date_created":"2020-05-10T22:00:50Z","external_id":{"isi":["000681656800005"]},"department":[{"_id":"KrCh"}],"oa":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783030449131"]},"file":[{"access_level":"open_access","relation":"main_file","creator":"dernst","file_name":"2020_LNCS_Chatterjee.pdf","file_id":"7895","date_created":"2020-05-26T13:34:48Z","file_size":651250,"content_type":"application/pdf","checksum":"8618b80f4cf7b39a60e61a6445ad9807","date_updated":"2020-07-14T12:48:03Z"}],"isi":1,"intvolume":"     12075","publication":"European Symposium on Programming","scopus_import":"1","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"}],"file_date_updated":"2020-07-14T12:48:03Z"},{"isi":1,"intvolume":"     11674","publication":" Proceedings of the 13th International Conference of Reachability Problems","file_date_updated":"2020-07-14T12:47:41Z","scopus_import":"1","author":[{"full_name":"Avni, Guy","last_name":"Avni","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr"}],"publication_identifier":{"isbn":["978-303030805-6"],"issn":["0302-9743"]},"oa":1,"file":[{"file_size":436635,"file_name":"prob.pdf","creator":"gavni","date_created":"2019-08-19T07:56:40Z","file_id":"6823","date_updated":"2020-07-14T12:47:41Z","content_type":"application/pdf","checksum":"45ebbc709af2b247d28c7c293c01504b","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"date_created":"2019-08-19T07:58:10Z","external_id":{"isi":["001333747500001"]},"department":[{"_id":"ToHe"}],"publication_status":"published","abstract":[{"lang":"eng","text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the qualitative winner or quantitative payoff of the game. In bidding games, in each turn, we hold an auction between the two players to determine which player moves the token. Bidding games have largely been studied with concrete bidding mechanisms that are variants of a first-price auction: in each turn both players simultaneously submit bids, the higher\r\nbidder moves the token, and pays his bid to the lower bidder in Richman bidding, to the bank in poorman bidding, and in taxman bidding, the bid is split between the other player and the bank according to a predefined constant factor. Bidding games are deterministic games. They have an intriguing connection with a fragment of stochastic games called \r\n randomturn games. We study, for the first time, a combination of bidding games with probabilistic behavior; namely, we study bidding games that are played on Markov decision processes, where the players bid for the right to choose the next action, which determines the probability distribution according to which the next vertex is chosen. We study parity and meanpayoff bidding games on MDPs and extend results from the deterministic bidding setting to the probabilistic one."}],"quality_controlled":"1","volume":11674,"page":"1-12","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_updated":"2025-09-10T10:39:56Z","oa_version":"Submitted Version","year":"2019","date_published":"2019-09-06T00:00:00Z","has_accepted_license":"1","project":[{"grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"publisher":"Springer","day":"06","type":"conference","status":"public","alternative_title":["LNCS"],"doi":"10.1007/978-3-030-30806-3_1","ddc":["000"],"citation":{"chicago":"Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding Games on Markov Decision Processes.” In <i> Proceedings of the 13th International Conference of Reachability Problems</i>, 11674:1–12. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">https://doi.org/10.1007/978-3-030-30806-3_1</a>.","ista":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. 2019. Bidding games on Markov decision processes.  Proceedings of the 13th International Conference of Reachability Problems. RP: Reachability Problems, LNCS, vol. 11674, 1–12.","ama":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision processes. In: <i> Proceedings of the 13th International Conference of Reachability Problems</i>. Vol 11674. Springer; 2019:1-12. doi:<a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">10.1007/978-3-030-30806-3_1</a>","apa":"Avni, G., Henzinger, T. A., Ibsen-Jensen, R., &#38; Novotny, P. (2019). Bidding games on Markov decision processes. In <i> Proceedings of the 13th International Conference of Reachability Problems</i> (Vol. 11674, pp. 1–12). Brussels, Belgium: Springer. <a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">https://doi.org/10.1007/978-3-030-30806-3_1</a>","ieee":"G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games on Markov decision processes,” in <i> Proceedings of the 13th International Conference of Reachability Problems</i>, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.","short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, P. Novotny, in:,  Proceedings of the 13th International Conference of Reachability Problems, Springer, 2019, pp. 1–12.","mla":"Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” <i> Proceedings of the 13th International Conference of Reachability Problems</i>, vol. 11674, Springer, 2019, pp. 1–12, doi:<a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">10.1007/978-3-030-30806-3_1</a>."},"conference":{"start_date":"2019-09-11","name":"RP: Reachability Problems","end_date":"2019-09-13","location":"Brussels, Belgium"},"article_processing_charge":"No","month":"09","title":"Bidding games on Markov decision processes","_id":"6822"},{"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Game Theory","_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"}],"date_published":"2019-11-01T00:00:00Z","has_accepted_license":"1","date_updated":"2026-04-28T22:31:03Z","year":"2019","oa_version":"Submitted Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","issue":"4","day":"01","type":"journal_article","publisher":"ACM","ddc":["000"],"article_type":"original","doi":"10.1145/3363525","_id":"7158","month":"11","title":"Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth","article_processing_charge":"No","related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"citation":{"mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 23, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>.","short":"K. Chatterjee, A.K. Goharshady, P. Goyal, R. Ibsen-Jensen, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 41 (2019).","ieee":"K. Chatterjee, A. K. Goharshady, P. Goyal, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4. ACM, 2019.","ama":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>","apa":"Chatterjee, K., Goharshady, A. K., Goyal, P., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2019). Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Prateesh Goyal, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>.","ista":"Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. 2019. Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. ACM Transactions on Programming Languages and Systems. 41(4), 23."},"scopus_import":"1","publication":"ACM Transactions on Programming Languages and Systems","file_date_updated":"2020-10-08T12:58:10Z","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-1702-6584","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Goyal","full_name":"Goyal, Prateesh","first_name":"Prateesh"},{"orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"}],"isi":1,"intvolume":"        41","ec_funded":1,"file":[{"success":1,"access_level":"open_access","relation":"main_file","file_name":"2019_ACMTransactions_Chatterjee.pdf","creator":"dernst","date_created":"2020-10-08T12:58:10Z","file_id":"8632","file_size":667357,"content_type":"application/pdf","checksum":"291cc86a07bd010d4815e177dac57b70","date_updated":"2020-10-08T12:58:10Z"}],"publication_identifier":{"issn":["0164-0925"]},"oa":1,"publication_status":"published","date_created":"2019-12-09T08:33:33Z","department":[{"_id":"KrCh"}],"external_id":{"isi":["000564108400004"]},"language":[{"iso":"eng"}],"volume":41,"quality_controlled":"1","article_number":"23","abstract":[{"lang":"eng","text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, and so on. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, and so on. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in an important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect we consider is that the control flow graphs for most programs have constant treewidth.\r\n\r\nOur main contributions are simple and implementable algorithms that support multiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing but can answer subsequent queries significantly faster as compared to the current algorithmic solutions for interprocedural dataflow analysis. We have also implemented our algorithms and evaluated their performance for performing on-demand interprocedural dataflow analysis on various domains, such as for live variable analysis and reaching definitions, on a standard benchmark set. Our experimental results align with our theoretical statements and show that after a lightweight preprocessing, on-demand queries are answered much faster than the standard existing algorithmic approaches.\r\n"}]},{"related_material":{"link":[{"url":"https://dx.doi.org/10.6084/m9.figshare.c.4028971","relation":"supplementary_material"}],"record":[{"id":"9814","status":"public","relation":"research_data"}]},"citation":{"ieee":"R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, and M. Nowak, “Language acquisition with communication between learners,” <i>Journal of the Royal Society Interface</i>, vol. 15, no. 140. The Royal Society, 2018.","short":"R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, M. Nowak, Journal of the Royal Society Interface 15 (2018).","mla":"Ibsen-Jensen, Rasmus, et al. “Language Acquisition with Communication between Learners.” <i>Journal of the Royal Society Interface</i>, vol. 15, no. 140, 20180073, The Royal Society, 2018, doi:<a href=\"https://doi.org/10.1098/rsif.2018.0073\">10.1098/rsif.2018.0073</a>.","chicago":"Ibsen-Jensen, Rasmus, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Language Acquisition with Communication between Learners.” <i>Journal of the Royal Society Interface</i>. The Royal Society, 2018. <a href=\"https://doi.org/10.1098/rsif.2018.0073\">https://doi.org/10.1098/rsif.2018.0073</a>.","ista":"Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. 2018. Language acquisition with communication between learners. Journal of the Royal Society Interface. 15(140), 20180073.","ama":"Ibsen-Jensen R, Tkadlec J, Chatterjee K, Nowak M. Language acquisition with communication between learners. <i>Journal of the Royal Society Interface</i>. 2018;15(140). doi:<a href=\"https://doi.org/10.1098/rsif.2018.0073\">10.1098/rsif.2018.0073</a>","apa":"Ibsen-Jensen, R., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2018). Language acquisition with communication between learners. <i>Journal of the Royal Society Interface</i>. The Royal Society. <a href=\"https://doi.org/10.1098/rsif.2018.0073\">https://doi.org/10.1098/rsif.2018.0073</a>"},"article_processing_charge":"No","month":"03","title":"Language acquisition with communication between learners","_id":"198","article_type":"original","publist_id":"7715","doi":"10.1098/rsif.2018.0073","ddc":["000"],"issue":"140","type":"journal_article","publisher":"The Royal Society","day":"01","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-04-15T07:26:26Z","year":"2018","oa_version":"Submitted Version","has_accepted_license":"1","project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"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":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"date_published":"2018-03-01T00:00:00Z","article_number":"20180073","abstract":[{"lang":"eng","text":"We consider a class of students learning a language from a teacher. The situation can be interpreted as a group of child learners receiving input from the linguistic environment. The teacher provides sample sentences. The students try to learn the grammar from the teacher. In addition to just listening to the teacher, the students can also communicate with each other. The students hold hypotheses about the grammar and change them if they receive counter evidence. The process stops when all students have converged to the correct grammar. We study how the time to convergence depends on the structure of the classroom by introducing and evaluating various complexity measures. We find that structured communication between students, although potentially introducing confusion, can greatly reduce some of the complexity measures. Our theory can also be interpreted as applying to the scientific process, where nature is the teacher and the scientists are the students."}],"quality_controlled":"1","volume":15,"language":[{"iso":"eng"}],"date_created":"2018-12-11T11:45:09Z","department":[{"_id":"KrCh"}],"external_id":{"pmid":["29593089"],"isi":["000428576200023"]},"publication_status":"published","publication_identifier":{"eissn":["1742-5662"]},"oa":1,"pmid":1,"file":[{"date_created":"2019-02-12T07:54:37Z","file_id":"5955","creator":"dernst","file_name":"2018_RS_IbsenJensen.pdf","file_size":219837,"content_type":"application/pdf","checksum":"444e1a9d98eb0e780671be82b13025f3","date_updated":"2020-07-14T12:45:22Z","relation":"main_file","access_level":"open_access"}],"isi":1,"intvolume":"        15","ec_funded":1,"file_date_updated":"2020-07-14T12:45:22Z","publication":"Journal of the Royal Society Interface","scopus_import":"1","author":[{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","last_name":"Tkadlec","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}]},{"file":[{"file_size":302539,"creator":"dernst","file_name":"2018_EC18_Hansen.pdf","date_created":"2019-11-19T08:24:24Z","file_id":"7054","date_updated":"2020-07-14T12:47:14Z","content_type":"application/pdf","checksum":"bb52683e349cfd864f4769a8f38f2798","access_level":"open_access","relation":"main_file"}],"publication_identifier":{"isbn":["9781450358293"]},"oa":1,"author":[{"first_name":"Kristoffer Arnsfelt","last_name":"Hansen","full_name":"Hansen, Kristoffer Arnsfelt"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Neyman","full_name":"Neyman, Abraham","first_name":"Abraham"}],"scopus_import":"1","file_date_updated":"2020-07-14T12:47:14Z","publication":"Proceedings of the 2018 ACM Conference on Economics and Computation  - EC '18","isi":1,"quality_controlled":"1","abstract":[{"lang":"eng","text":"The Big Match is a multi-stage two-player game. In each stage Player 1 hides one or two pebbles in his hand, and his opponent has to guess that number; Player 1 loses a point if Player 2 is correct, and otherwise he wins a point. As soon as Player 1 hides one pebble, the players cannot change their choices in any future stage.\r\nBlackwell and Ferguson (1968) give an ε-optimal strategy for Player 1 that hides, in each stage, one pebble with a probability that depends on the entire past history. Any strategy that depends just on the clock or on a finite memory is worthless. The long-standing natural open problem has been whether every strategy that depends just on the clock and a finite memory is worthless. We prove that there is such a strategy that is ε-optimal. In fact, we show that just two states of memory are sufficient.\r\n"}],"publication_status":"published","date_created":"2019-02-13T10:31:41Z","department":[{"_id":"KrCh"}],"external_id":{"isi":["000492755100020"]},"language":[{"iso":"eng"}],"status":"public","day":"18","publisher":"ACM","type":"conference","date_published":"2018-06-18T00:00:00Z","has_accepted_license":"1","date_updated":"2025-05-14T11:24:35Z","oa_version":"Submitted Version","year":"2018","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"149-150","_id":"5967","month":"06","title":"The Big Match with a clock and a bit of memory","conference":{"location":"Ithaca, NY, United States","end_date":"2018-06-22","name":"EC: Conference on Economics and Computation","start_date":"2018-06-18"},"article_processing_charge":"No","citation":{"short":"K.A. Hansen, R. Ibsen-Jensen, A. Neyman, in:, Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18, ACM, 2018, pp. 149–150.","mla":"Hansen, Kristoffer Arnsfelt, et al. “The Big Match with a Clock and a Bit of Memory.” <i>Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18</i>, ACM, 2018, pp. 149–50, doi:<a href=\"https://doi.org/10.1145/3219166.3219198\">10.1145/3219166.3219198</a>.","ieee":"K. A. Hansen, R. Ibsen-Jensen, and A. Neyman, “The Big Match with a clock and a bit of memory,” in <i>Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18</i>, Ithaca, NY, United States, 2018, pp. 149–150.","ama":"Hansen KA, Ibsen-Jensen R, Neyman A. The Big Match with a clock and a bit of memory. In: <i>Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18</i>. ACM; 2018:149-150. doi:<a href=\"https://doi.org/10.1145/3219166.3219198\">10.1145/3219166.3219198</a>","apa":"Hansen, K. A., Ibsen-Jensen, R., &#38; Neyman, A. (2018). The Big Match with a clock and a bit of memory. In <i>Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18</i> (pp. 149–150). Ithaca, NY, United States: ACM. <a href=\"https://doi.org/10.1145/3219166.3219198\">https://doi.org/10.1145/3219166.3219198</a>","chicago":"Hansen, Kristoffer Arnsfelt, Rasmus Ibsen-Jensen, and Abraham Neyman. “The Big Match with a Clock and a Bit of Memory.” In <i>Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18</i>, 149–50. ACM, 2018. <a href=\"https://doi.org/10.1145/3219166.3219198\">https://doi.org/10.1145/3219166.3219198</a>.","ista":"Hansen KA, Ibsen-Jensen R, Neyman A. 2018. The Big Match with a clock and a bit of memory. Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18. EC: Conference on Economics and Computation, 149–150."},"ddc":["000"],"doi":"10.1145/3219166.3219198"},{"status":"public","publisher":"Springer","type":"conference","day":"21","date_published":"2018-11-21T00:00:00Z","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369"}],"date_updated":"2026-04-16T09:54:39Z","oa_version":"Preprint","year":"2018","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","page":"21-36","_id":"5788","month":"11","title":"Infinite-duration poorman-bidding games","conference":{"location":"Oxford, UK","end_date":"2018-12-17","name":"14th International Conference on Web and Internet Economics, WINE","start_date":"2018-12-15"},"article_processing_charge":"No","citation":{"short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, in:, Springer, 2018, pp. 21–36.","mla":"Avni, Guy, et al. <i>Infinite-Duration Poorman-Bidding Games</i>. Vol. 11316, Springer, 2018, pp. 21–36, doi:<a href=\"https://doi.org/10.1007/978-3-030-04612-5_2\">10.1007/978-3-030-04612-5_2</a>.","ieee":"G. Avni, T. A. Henzinger, and R. Ibsen-Jensen, “Infinite-duration poorman-bidding games,” presented at the 14th International Conference on Web and Internet Economics, WINE, Oxford, UK, 2018, vol. 11316, pp. 21–36.","ama":"Avni G, Henzinger TA, Ibsen-Jensen R. Infinite-duration poorman-bidding games. In: Vol 11316. Springer; 2018:21-36. doi:<a href=\"https://doi.org/10.1007/978-3-030-04612-5_2\">10.1007/978-3-030-04612-5_2</a>","apa":"Avni, G., Henzinger, T. A., &#38; Ibsen-Jensen, R. (2018). Infinite-duration poorman-bidding games (Vol. 11316, pp. 21–36). Presented at the 14th International Conference on Web and Internet Economics, WINE, Oxford, UK: Springer. <a href=\"https://doi.org/10.1007/978-3-030-04612-5_2\">https://doi.org/10.1007/978-3-030-04612-5_2</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Rasmus Ibsen-Jensen. “Infinite-Duration Poorman-Bidding Games,” 11316:21–36. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-030-04612-5_2\">https://doi.org/10.1007/978-3-030-04612-5_2</a>.","ista":"Avni G, Henzinger TA, Ibsen-Jensen R. 2018. Infinite-duration poorman-bidding games. 14th International Conference on Web and Internet Economics, WINE, LNCS, vol. 11316, 21–36."},"arxiv":1,"alternative_title":["LNCS"],"doi":"10.1007/978-3-030-04612-5_2","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030046118"]},"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.04372"}],"scopus_import":"1","author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","last_name":"Avni","full_name":"Avni, Guy"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389"}],"intvolume":"     11316","isi":1,"volume":11316,"quality_controlled":"1","abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner or payoff of the game. Such games are central in formal verification since they model the interaction between a non-terminating system and its environment. We study bidding games in which the players bid for the right to move the token. Two bidding rules have been defined. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the “bank” rather than the other player. While poorman reachability games have been studied before, we present, for the first time, results on infinite-duration poorman games. A central quantity in these games is the ratio between the two players’ initial budgets. The questions we study concern a necessary and sufficient ratio with which a player can achieve a goal. For reachability objectives, such threshold ratios are known to exist for both bidding rules. We show that the properties of poorman reachability games extend to complex qualitative objectives such as parity, similarly to the Richman case. Our most interesting results concern quantitative poorman games, namely poorman mean-payoff games, where we construct optimal strategies depending on the initial ratio, by showing a connection with random-turn based games. The connection in itself is interesting, because it does not hold for reachability poorman games. We also solve the complexity problems that arise in poorman bidding games.","lang":"eng"}],"date_created":"2018-12-30T22:59:14Z","external_id":{"isi":["000865933000002"],"arxiv":["1804.04372"]},"department":[{"_id":"ToHe"}],"language":[{"iso":"eng"}]},{"type":"conference","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","day":"01","status":"public","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2018-09-01T00:00:00Z","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"has_accepted_license":"1","year":"2018","oa_version":"Published Version","date_updated":"2026-04-28T22:31:03Z","article_processing_charge":"No","conference":{"end_date":"2018-09-07","location":"Beijing, China","start_date":"2018-09-04","name":"CONCUR: Conference on Concurrency Theory"},"citation":{"short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","mla":"Chatterjee, Krishnendu, et al. <i>Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies</i>. Vol. 118, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">10.4230/LIPIcs.CONCUR.2018.11</a>.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and Y. Velner, “Ergodic mean-payoff games for the analysis of attacks in crypto-currencies,” presented at the CONCUR: Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., &#38; Velner, Y. (2018). Ergodic mean-payoff games for the analysis of attacks in crypto-currencies (Vol. 118). Presented at the CONCUR: Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.11</a>","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">10.4230/LIPIcs.CONCUR.2018.11</a>","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. 2018. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 118, 11.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Yaron Velner. “Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.11</a>."},"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"_id":"66","title":"Ergodic mean-payoff games for the analysis of attacks in crypto-currencies","month":"09","publist_id":"7988","doi":"10.4230/LIPIcs.CONCUR.2018.11","alternative_title":["LIPIcs"],"arxiv":1,"ddc":["000"],"file":[{"file_size":1078309,"file_id":"5696","date_created":"2018-12-17T12:08:00Z","file_name":"2018_CONCUR_Chatterjee.pdf","creator":"dernst","date_updated":"2020-07-14T12:47:34Z","checksum":"68a055b1aaa241cc38375083cf832a7d","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"oa":1,"publication_identifier":{"isbn":["978-3-95977-087-3"]},"scopus_import":"1","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Goharshady","full_name":"Goharshady, Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir","orcid":"0000-0003-1702-6584"},{"first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"file_date_updated":"2020-07-14T12:47:34Z","ec_funded":1,"intvolume":"       118","abstract":[{"lang":"eng","text":"Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payo games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions."}],"article_number":"11","volume":118,"quality_controlled":"1","department":[{"_id":"KrCh"}],"external_id":{"arxiv":["1806.03108"]},"date_created":"2018-12-11T11:44:27Z","language":[{"iso":"eng"}],"publication_status":"published"},{"intvolume":"        40","isi":1,"ec_funded":1,"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722"}],"scopus_import":"1","publication":"ACM Transactions on Programming Languages and Systems","publication_identifier":{"issn":["0164-0925"]},"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.07565"}],"publication_status":"published","corr_author":"1","language":[{"iso":"eng"}],"date_created":"2019-02-14T14:31:52Z","external_id":{"isi":["000444694800001"],"arxiv":["1510.07565"]},"department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":40,"article_number":"9","abstract":[{"text":"We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.\r\n","lang":"eng"}],"date_updated":"2026-04-28T22:31:04Z","oa_version":"Preprint","year":"2018","date_published":"2018-08-01T00:00:00Z","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"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"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","issue":"3","type":"journal_article","day":"01","publisher":"Association for Computing Machinery","arxiv":1,"doi":"10.1145/3210257","month":"08","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","_id":"6009","related_material":{"record":[{"id":"5441","status":"public","relation":"earlier_version"},{"id":"5442","relation":"earlier_version","status":"public"},{"id":"1437","status":"public","relation":"earlier_version"},{"id":"8934","status":"public","relation":"dissertation_contains"}]},"citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3. Association for Computing Machinery, 2018.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).","mla":"Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3, 9, Association for Computing Machinery, 2018, doi:<a href=\"https://doi.org/10.1145/3210257\">10.1145/3210257</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Transactions on Programming Languages and Systems. 40(3), 9.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery, 2018. <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., &#38; Pavlogiannis, A. (2018). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>. 2018;40(3). doi:<a href=\"https://doi.org/10.1145/3210257\">10.1145/3210257</a>"},"article_processing_charge":"No"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2017-11-01T00:00:00Z","has_accepted_license":"1","date_updated":"2025-07-10T11:52:51Z","oa_version":"Published Version","year":"2017","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","day":"01","type":"conference","status":"public","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"alternative_title":["LIPIcs"],"publist_id":"7263","doi":"10.4230/LIPIcs.MFCS.2017.61","ddc":["004"],"pubrep_id":"924","conference":{"start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science","end_date":"2017-08-25","location":"Aalborg, Denmark"},"article_processing_charge":"No","citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, “Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","mla":"Chatterjee, Krishnendu, et al. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 61, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">10.4230/LIPIcs.MFCS.2017.61</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2017. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 83, 61.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Nowak, M. (2017). Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">10.4230/LIPIcs.MFCS.2017.61</a>"},"_id":"551","month":"11","title":"Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs","file_date_updated":"2020-07-14T12:47:00Z","scopus_import":"1","publication":"Leibniz International Proceedings in Informatics","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"intvolume":"        83","file":[{"content_type":"application/pdf","checksum":"2eed5224c0e4e259484a1d71acb8ba6a","date_updated":"2020-07-14T12:47:00Z","file_name":"IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf","creator":"system","date_created":"2018-12-12T10:18:04Z","file_id":"5322","file_size":535077,"access_level":"open_access","relation":"main_file"}],"oa":1,"publication_identifier":{"isbn":["978-395977046-0"]},"date_created":"2018-12-11T11:47:08Z","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"corr_author":"1","publication_status":"published","article_number":"61","abstract":[{"lang":"eng","text":"Evolutionary graph theory studies the evolutionary dynamics in a population structure given as a connected graph. Each node of the graph represents an individual of the population, and edges determine how offspring are placed. We consider the classical birth-death Moran process where there are two types of individuals, namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates the reproductive strength. The evolutionary dynamics happens as follows: in the initial step, in a population of all resident individuals a mutant is introduced, and then at each step, an individual is chosen proportional to the fitness of its type to reproduce, and the offspring replaces a neighbor uniformly at random. The process stops when all individuals are either residents or mutants. The probability that all individuals in the end are mutants is called the fixation probability, which is a key factor in the rate of evolution. We consider the problem of approximating the fixation probability. The class of algorithms that is extremely relevant for approximation of the fixation probabilities is the Monte-Carlo simulation of the process. Previous results present a polynomial-time Monte-Carlo algorithm for undirected graphs when r is given in unary. First, we present a simple modification: instead of simulating each step, we discard ineffective steps, where no node changes type (i.e., either residents replace residents, or mutants replace mutants). Using the above simple modification and our result that the number of effective steps is concentrated around the expected number of effective steps, we present faster polynomial-time Monte-Carlo algorithms for undirected graphs. Our algorithms are always at least a factor O(n2/ log n) faster as compared to the previous algorithms, where n is the number of nodes, and is polynomial even if r is given in binary. We also present lower bounds showing that the upper bound on the expected number of effective steps we present is asymptotically tight for undirected graphs. "}],"volume":83,"quality_controlled":"1"},{"type":"conference","day":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","year":"2017","date_updated":"2025-06-04T09:37:06Z","has_accepted_license":"1","date_published":"2017-11-01T00:00:00Z","citation":{"ama":"Chatterjee K, Hansen K, Ibsen-Jensen R. Strategy complexity of concurrent safety games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">10.4230/LIPIcs.MFCS.2017.55</a>","apa":"Chatterjee, K., Hansen, K., &#38; Ibsen-Jensen, R. (2017). Strategy complexity of concurrent safety games. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>","chicago":"Chatterjee, Krishnendu, Kristofer Hansen, and Rasmus Ibsen-Jensen. “Strategy Complexity of Concurrent Safety Games.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>.","ista":"Chatterjee K, Hansen K, Ibsen-Jensen R. 2017. Strategy complexity of concurrent safety games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 83, 55.","short":"K. Chatterjee, K. Hansen, R. Ibsen-Jensen, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","mla":"Chatterjee, Krishnendu, et al. “Strategy Complexity of Concurrent Safety Games.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 55, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">10.4230/LIPIcs.MFCS.2017.55</a>.","ieee":"K. Chatterjee, K. Hansen, and R. Ibsen-Jensen, “Strategy complexity of concurrent safety games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83."},"article_processing_charge":"No","conference":{"end_date":"2017-08-25","location":"Aalborg, Denmark","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science"},"title":"Strategy complexity of concurrent safety games","month":"11","_id":"553","publist_id":"7261","doi":"10.4230/LIPIcs.MFCS.2017.55","alternative_title":["LIPIcs"],"pubrep_id":"922","arxiv":1,"ddc":["004"],"main_file_link":[{"url":"https://arxiv.org/abs/1506.02434","open_access":"1"}],"oa":1,"publication_identifier":{"isbn":["978-395977046-0"]},"file":[{"file_size":549967,"file_name":"IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf","creator":"system","file_id":"4753","date_created":"2018-12-12T10:09:29Z","date_updated":"2020-07-14T12:47:00Z","content_type":"application/pdf","checksum":"7101facb56ade363205c695d72dbd173","access_level":"open_access","relation":"main_file"}],"intvolume":"        83","scopus_import":"1","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Hansen","full_name":"Hansen, Kristofer","first_name":"Kristofer"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389"}],"publication":"Leibniz International Proceedings in Informatics","file_date_updated":"2020-07-14T12:47:00Z","abstract":[{"lang":"eng","text":"We consider two player, zero-sum, finite-state concurrent reachability games, played for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. Player 1 wins iff a designated goal state is eventually visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest non-zero probability employed. Our main results are as follows: We show that: (i) the optimal bound on the patience of optimal and -optimal strategies, for both players is doubly exponential; and (ii) even in games with a single non-absorbing state exponential (in the number of actions) patience is necessary. "}],"article_number":"55","quality_controlled":"1","volume":83,"corr_author":"1","language":[{"iso":"eng"}],"external_id":{"arxiv":["1506.02434"]},"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:47:08Z","publication_status":"published"},{"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>"},"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5438"},{"status":"public","relation":"earlier_version","id":"1610"}]},"article_processing_charge":"No","title":"Edit distance for pushdown automata","month":"09","_id":"465","publist_id":"7356","doi":"10.23638/LMCS-13(3:23)2017","pubrep_id":"955","ddc":["004"],"publisher":"International Federation of Computational Logic","day":"13","type":"journal_article","issue":"3","tmp":{"name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"status":"public","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"Published Version","year":"2017","date_updated":"2026-04-29T06:14:48Z","date_published":"2017-09-13T00:00:00Z","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"}],"has_accepted_license":"1","abstract":[{"lang":"eng","text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. "}],"license":"https://creativecommons.org/licenses/by-nd/4.0/","quality_controlled":"1","volume":13,"language":[{"iso":"eng"}],"corr_author":"1","external_id":{"isi":["000419163000005"]},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_created":"2018-12-11T11:46:37Z","publication_status":"published","publication_identifier":{"issn":["1860-5974"]},"oa":1,"file":[{"relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:46:33Z","content_type":"application/pdf","checksum":"08041379ba408d40664f449eb5907a8f","file_size":279071,"file_id":"5090","date_created":"2018-12-12T10:14:37Z","creator":"system","file_name":"IST-2015-321-v1+1_main.pdf"},{"access_level":"open_access","relation":"main_file","checksum":"08041379ba408d40664f449eb5907a8f","content_type":"application/pdf","date_updated":"2020-07-14T12:46:33Z","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","creator":"system","date_created":"2018-12-12T10:14:38Z","file_id":"5091","file_size":279071}],"ec_funded":1,"intvolume":"        13","isi":1,"author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"publication":"Logical Methods in Computer Science","file_date_updated":"2020-07-14T12:46:33Z","scopus_import":"1"},{"status":"public","type":"conference","day":"01","publisher":"AAAI Press","date_updated":"2025-04-22T13:42:22Z","year":"2016","oa_version":"Preprint","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"date_published":"2016-01-01T00:00:00Z","page":"172 - 179","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","title":"Robust draws in balanced knockout tournaments","_id":"1182","related_material":{"link":[{"url":"https://www.ijcai.org/proceedings/2016","relation":"table_of_contents"}]},"citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Josef Tkadlec. “Robust Draws in Balanced Knockout Tournaments,” 2016–January:172–79. AAAI Press, 2016.","ista":"Chatterjee K, Ibsen-Jensen R, Tkadlec J. 2016. Robust draws in balanced knockout tournaments. IJCAI: International Joint Conference on Artificial Intelligence vol. 2016–January, 172–179.","ama":"Chatterjee K, Ibsen-Jensen R, Tkadlec J. Robust draws in balanced knockout tournaments. In: Vol 2016-January. AAAI Press; 2016:172-179.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Tkadlec, J. (2016). Robust draws in balanced knockout tournaments (Vol. 2016–January, pp. 172–179). Presented at the IJCAI: International Joint Conference on Artificial Intelligence, New York, NY, USA: AAAI Press.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and J. Tkadlec, “Robust draws in balanced knockout tournaments,” presented at the IJCAI: International Joint Conference on Artificial Intelligence, New York, NY, USA, 2016, vol. 2016–January, pp. 172–179.","short":"K. Chatterjee, R. Ibsen-Jensen, J. Tkadlec, in:, AAAI Press, 2016, pp. 172–179.","mla":"Chatterjee, Krishnendu, et al. <i>Robust Draws in Balanced Knockout Tournaments</i>. Vol. 2016–January, AAAI Press, 2016, pp. 172–79."},"conference":{"end_date":"2016-07-15","location":"New York, NY, USA","start_date":"2016-07-09","name":"IJCAI: International Joint Conference on Artificial Intelligence"},"article_processing_charge":"No","arxiv":1,"publist_id":"6171","oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1604.05090","open_access":"1"}],"ec_funded":1,"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"orcid":"0000-0002-1097-9684","last_name":"Tkadlec","full_name":"Tkadlec, Josef","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":"1","quality_controlled":"1","volume":"2016-January","abstract":[{"text":"Balanced knockout tournaments are ubiquitous in sports competitions and are also used in decisionmaking and elections. The traditional computational question, that asks to compute a draw (optimal draw) that maximizes the winning probability for a distinguished player, has received a lot of attention. Previous works consider the problem where the pairwise winning probabilities are known precisely, while we study how robust is the winning probability with respect to small errors in the pairwise winning probabilities. First, we present several illuminating examples to establish: (a) there exist deterministic tournaments (where the pairwise winning probabilities are 0 or 1) where one optimal draw is much more robust than the other; and (b) in general, there exist tournaments with slightly suboptimal draws that are more robust than all the optimal draws. The above examples motivate the study of the computational problem of robust draws that guarantee a specified winning probability. Second, we present a polynomial-time algorithm for approximating the robustness of a draw for sufficiently small errors in pairwise winning probabilities, and obtain that the stated computational problem is NP-complete. We also show that two natural cases of deterministic tournaments where the optimal draw could be computed in polynomial time also admit polynomial-time algorithms to compute robust optimal draws.","lang":"eng"}],"publication_status":"published","corr_author":"1","language":[{"iso":"eng"}],"date_created":"2018-12-11T11:50:35Z","department":[{"_id":"KrCh"}],"external_id":{"arxiv":["1604.05090"]}},{"conference":{"location":"Liverpool, United Kingdom","end_date":"2016-09-21","name":"SAGT: Symposium on Algorithmic Game Theory","start_date":"2016-09-19"},"article_processing_charge":"No","citation":{"ama":"Hansen K, Ibsen-Jensen R, Koucký M. The big match in small space. In: Vol 9928. Springer; 2016:64-76. doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_6\">10.1007/978-3-662-53354-3_6</a>","apa":"Hansen, K., Ibsen-Jensen, R., &#38; Koucký, M. (2016). The big match in small space (Vol. 9928, pp. 64–76). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_6\">https://doi.org/10.1007/978-3-662-53354-3_6</a>","chicago":"Hansen, Kristoffer, Rasmus Ibsen-Jensen, and Michal Koucký. “The Big Match in Small Space,” 9928:64–76. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_6\">https://doi.org/10.1007/978-3-662-53354-3_6</a>.","ista":"Hansen K, Ibsen-Jensen R, Koucký M. 2016. The big match in small space. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 64–76.","mla":"Hansen, Kristoffer, et al. <i>The Big Match in Small Space</i>. Vol. 9928, Springer, 2016, pp. 64–76, doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_6\">10.1007/978-3-662-53354-3_6</a>.","short":"K. Hansen, R. Ibsen-Jensen, M. Koucký, in:, Springer, 2016, pp. 64–76.","ieee":"K. Hansen, R. Ibsen-Jensen, and M. Koucký, “The big match in small space,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 64–76."},"_id":"1340","month":"09","title":"The big match in small space","alternative_title":["LNCS"],"publist_id":"5927","doi":"10.1007/978-3-662-53354-3_6","arxiv":1,"type":"conference","publisher":"Springer","day":"01","status":"public","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","page":"64 - 76","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"date_published":"2016-09-01T00:00:00Z","date_updated":"2025-09-22T08:18:27Z","year":"2016","oa_version":"Preprint","abstract":[{"text":"We study repeated games with absorbing states, a type of two-player, zero-sum concurrent mean-payoff games with the prototypical example being the Big Match of Gillete (1957). These games may not allow optimal strategies but they always have ε-optimal strategies. In this paper we design ε-optimal strategies for Player 1 in these games that use only O(log log T) space. Furthermore, we construct strategies for Player 1 that use space s(T), for an arbitrary small unbounded non-decreasing function s, and which guarantee an ε-optimal value for Player 1 in the limit superior sense. The previously known strategies use space Ω(log T) and it was known that no strategy can use constant space if it is ε-optimal even in the limit superior sense. We also give a complementary lower bound. Furthermore, we also show that no Markov strategy, even extended with finite memory, can ensure value greater than 0 in the Big Match, answering a question posed by Neyman [11].","lang":"eng"}],"volume":9928,"quality_controlled":"1","date_created":"2018-12-11T11:51:28Z","department":[{"_id":"KrCh"}],"external_id":{"isi":["000389020400006"],"arxiv":["1604.07634"]},"language":[{"iso":"eng"}],"publication_status":"published","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.07634"}],"oa":1,"author":[{"first_name":"Kristoffer","full_name":"Hansen, Kristoffer","last_name":"Hansen"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389"},{"first_name":"Michal","last_name":"Koucký","full_name":"Koucký, Michal"}],"scopus_import":"1","intvolume":"      9928","isi":1,"ec_funded":1},{"file":[{"date_updated":"2020-07-14T12:46:35Z","checksum":"848043c812ace05e459579c923f3d3cf","content_type":"application/pdf","file_size":2116225,"creator":"system","file_name":"IST-2018-950-v1+1_2016_Chatterjee_The_complexity.pdf","date_created":"2018-12-12T10:07:59Z","file_id":"4658","access_level":"open_access","relation":"main_file"}],"oa":1,"file_date_updated":"2020-07-14T12:46:35Z","scopus_import":"1","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"}],"intvolume":"       285","isi":1,"abstract":[{"lang":"eng","text":"Magic: the Gathering is a game about magical combat for any number of players. Formally it is a zero-sum, imperfect information stochastic game that consists of a potentially unbounded number of steps. We consider the problem of deciding if a move is legal in a given single step of Magic. We show that the problem is (a) coNP-complete in general; and (b) in P if either of two small sets of cards are not used. Our lower bound holds even for single-player Magic games. The significant aspects of our results are as follows: First, in most real-life game problems, the task of deciding whether a given move is legal in a single step is trivial, and the computationally hard task is to find the best sequence of legal moves in the presence of multiple players. In contrast, quite uniquely our hardness result holds for single step and with only one-player. Second, we establish efficient algorithms for important special cases of Magic."}],"volume":285,"quality_controlled":"1","date_created":"2018-12-11T11:46:41Z","external_id":{"isi":["000385793700166"]},"department":[{"_id":"KrCh"}],"corr_author":"1","language":[{"iso":"eng"}],"publication_status":"published","publisher":"IOS Press","day":"01","type":"conference","status":"public","tmp":{"short":"CC BY-NC (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","image":"/images/cc_by_nc.png"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","page":"1432 - 1439","date_published":"2016-01-01T00:00:00Z","has_accepted_license":"1","date_updated":"2025-09-22T14:26:27Z","oa_version":"Published Version","year":"2016","conference":{"end_date":"2016-09-02","location":"The Hague, Netherlands","start_date":"2016-08-29","name":"ECAI: European Conference on Artificial Intelligence"},"article_processing_charge":"No","citation":{"chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Complexity of Deciding Legality of a Single Step of Magic: The Gathering,” 285:1432–39. IOS Press, 2016. <a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">https://doi.org/10.3233/978-1-61499-672-9-1432</a>.","ista":"Chatterjee K, Ibsen-Jensen R. 2016. The complexity of deciding legality of a single step of magic: The gathering. ECAI: European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 285, 1432–1439.","ama":"Chatterjee K, Ibsen-Jensen R. The complexity of deciding legality of a single step of magic: The gathering. In: Vol 285. IOS Press; 2016:1432-1439. doi:<a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">10.3233/978-1-61499-672-9-1432</a>","apa":"Chatterjee, K., &#38; Ibsen-Jensen, R. (2016). The complexity of deciding legality of a single step of magic: The gathering (Vol. 285, pp. 1432–1439). Presented at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands: IOS Press. <a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">https://doi.org/10.3233/978-1-61499-672-9-1432</a>","ieee":"K. Chatterjee and R. Ibsen-Jensen, “The complexity of deciding legality of a single step of magic: The gathering,” presented at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands, 2016, vol. 285, pp. 1432–1439.","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. <i>The Complexity of Deciding Legality of a Single Step of Magic: The Gathering</i>. Vol. 285, IOS Press, 2016, pp. 1432–39, doi:<a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">10.3233/978-1-61499-672-9-1432</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, in:, IOS Press, 2016, pp. 1432–1439."},"_id":"478","month":"01","title":"The complexity of deciding legality of a single step of magic: The gathering","alternative_title":["Frontiers in Artificial Intelligence and Applications"],"publist_id":"7342","doi":"10.3233/978-1-61499-672-9-1432","ddc":["004"],"pubrep_id":"950"}]