[{"publication_identifier":{"isbn":["9783959772617"],"issn":["1868-8969"]},"publication_status":"published","file_date_updated":"2023-01-20T10:19:19Z","has_accepted_license":"1","abstract":[{"lang":"eng","text":"Spatial games form a widely-studied class of games from biology and physics modeling the evolution of social behavior. Formally, such a game is defined by a square (d by d) payoff matrix M and an undirected graph G. Each vertex of G represents an individual, that initially follows some strategy i ∈ {1,2,…,d}. In each round of the game, every individual plays the matrix game with each of its neighbors: An individual following strategy i meeting a neighbor following strategy j receives a payoff equal to the entry (i,j) of M. Then, each individual updates its strategy to its neighbors' strategy with the highest sum of payoffs, and the next round starts. The basic computational problems consist of reachability between configurations and the average frequency of a strategy. For general spatial games and graphs, these problems are in PSPACE. In this paper, we examine restricted setting: the game is a prisoner’s dilemma; and G is a subgraph of grid. We prove that basic computational problems for spatial games with prisoner’s dilemma on a subgraph of a grid are PSPACE-hard."}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"       250","volume":250,"date_created":"2023-01-01T23:00:50Z","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Jecker","full_name":"Jecker, Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","first_name":"Ismael R"},{"first_name":"Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","last_name":"Svoboda"}],"day":"14","scopus_import":"1","title":"Complexity of spatial games","oa_version":"Published Version","citation":{"mla":"Chatterjee, Krishnendu, et al. “Complexity of Spatial Games.” <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 250, 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">10.4230/LIPIcs.FSTTCS.2022.11</a>.","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>","ista":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2022. Complexity of spatial games. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTC: Foundations of Software Technology and Theoretical Computer Science vol. 250, 11:1-11:14.","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>.","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.","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.","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>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"article_number":"11:1-11:14","file":[{"file_name":"2022_LIPICs_Chatterjee.pdf","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"a21e3ba2421e2c4a06aa2cb6d530ede1","file_size":657396,"date_created":"2023-01-20T10:19:19Z","date_updated":"2023-01-20T10:19:19Z","creator":"dernst","file_id":"12323"}],"month":"12","quality_controlled":"1","ddc":["000"],"date_updated":"2025-07-14T09:09:55Z","_id":"12101","type":"conference","doi":"10.4230/LIPIcs.FSTTCS.2022.11","article_processing_charge":"No","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","ec_funded":1,"date_published":"2022-12-14T00:00:00Z","conference":{"name":"FSTTC: Foundations of Software Technology and Theoretical Computer Science","start_date":"2022-12-18","end_date":"2022-12-20","location":"Madras, India"},"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)","project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"publication":"42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","status":"public","year":"2022"},{"publisher":"Springer","article_processing_charge":"No","doi":"10.1007/s10703-021-00373-5","type":"journal_article","_id":"9393","date_updated":"2023-10-10T11:13:20Z","page":"401-428","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.07384"}],"external_id":{"arxiv":["1504.07384"],"isi":["000645490300001"]},"year":"2021","isi":1,"status":"public","publication":"Formal Methods in System Design","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_published":"2021-09-01T00:00:00Z","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.","ec_funded":1,"title":"Faster algorithms for quantitative verification in bounded treewidth graphs","oa_version":"Preprint","scopus_import":"1","day":"01","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"}],"date_created":"2021-05-16T22:01:47Z","article_type":"original","volume":57,"intvolume":"        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_identifier":{"issn":["0925-9856"],"eissn":["1572-8102"]},"publication_status":"published","month":"09","arxiv":1,"department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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>","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.","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>","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>."}},{"volume":213,"date_created":"2022-01-16T23:01:28Z","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"scopus_import":"1","day":"29","title":"Quantitative verification on product graphs of small treewidth","oa_version":"Published Version","publication_status":"published","publication_identifier":{"isbn":["978-3-9597-7215-0"],"issn":["1868-8969"]},"file_date_updated":"2022-01-17T10:36:08Z","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"lang":"eng","text":"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^{-λ})."}],"intvolume":"       213","department":[{"_id":"KrCh"}],"file":[{"file_id":"10633","date_updated":"2022-01-17T10:36:08Z","creator":"cchlebak","file_size":891566,"date_created":"2022-01-17T10:36:08Z","checksum":"71141acdeffa9056f24d6dbef952d254","relation":"main_file","access_level":"open_access","content_type":"application/pdf","success":1,"file_name":"2021_LIPIcs_Chatterjee.pdf"}],"article_number":"42","month":"11","citation":{"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>.","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>.","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>","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.","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."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa":1,"language":[{"iso":"eng"}],"date_updated":"2022-01-17T10:39:40Z","_id":"10629","type":"conference","doi":"10.4230/LIPIcs.FSTTCS.2021.42","article_processing_charge":"No","alternative_title":["LIPIcs"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","ddc":["000"],"year":"2021","date_published":"2021-11-29T00:00:00Z","conference":{"name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","start_date":"2021-12-15","end_date":"2021-12-17","location":"Virtual"},"status":"public","publication":"41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science"},{"year":"2020","isi":1,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"external_id":{"isi":["000681656800005"]},"conference":{"location":"Dublin, Ireland","name":"ESOP: Programming Languages and Systems","start_date":"2020-04-25","end_date":"2020-04-30"},"date_published":"2020-04-18T00:00:00Z","publication":"European Symposium on Programming","status":"public","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"_id":"7810","date_updated":"2025-06-02T08:53:42Z","type":"conference","article_processing_charge":"No","alternative_title":["LNCS"],"doi":"10.1007/978-3-030-44914-8_5","publisher":"Springer Nature","quality_controlled":"1","page":"112-140","ddc":["000"],"department":[{"_id":"KrCh"}],"file":[{"file_size":651250,"date_created":"2020-05-26T13:34:48Z","date_updated":"2020-07-14T12:48:03Z","creator":"dernst","file_id":"7895","file_name":"2020_LNCS_Chatterjee.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"8618b80f4cf7b39a60e61a6445ad9807"}],"month":"04","citation":{"short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 112–140.","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.","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>","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>.","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>","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.","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>."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa":1,"language":[{"iso":"eng"}],"volume":12075,"date_created":"2020-05-10T22:00:50Z","scopus_import":"1","day":"18","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas"}],"oa_version":"Published Version","title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","file_date_updated":"2020-07-14T12:48:03Z","publication_identifier":{"issn":["03029743"],"isbn":["9783030449131"],"eissn":["16113349"]},"publication_status":"published","has_accepted_license":"1","abstract":[{"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.","lang":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"     12075"},{"year":"2020","external_id":{"arxiv":["2007.02894"]},"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"status":"public","publication":"45th International Symposium on Mathematical Foundations of Computer Science","ec_funded":1,"conference":{"location":"Prague, Czech Republic","start_date":"2020-08-24","end_date":"2020-08-28","name":"MFCS: Symposium on Mathematical Foundations of Computer Science"},"date_published":"2020-08-18T00:00:00Z","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.","doi":"10.4230/LIPIcs.MFCS.2020.22","alternative_title":["LIPIcs"],"article_processing_charge":"No","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2025-06-02T08:53:42Z","_id":"8533","type":"conference","ddc":["000"],"quality_controlled":"1","arxiv":1,"month":"08","department":[{"_id":"KrCh"}],"article_number":"22:1-22:13","file":[{"file_id":"8550","date_created":"2020-09-21T13:57:34Z","file_size":491374,"date_updated":"2020-09-21T13:57:34Z","creator":"dernst","relation":"main_file","checksum":"bbd7c4f55d45f2ff2a0a4ef0e10a77b1","success":1,"file_name":"2020_LIPIcs_Chatterjee.pdf","access_level":"open_access","content_type":"application/pdf"}],"oa":1,"language":[{"iso":"eng"}],"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: Symposium on 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>.","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>.","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>","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.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"first_name":"Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","full_name":"Jecker, Ismael R","last_name":"Jecker"},{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","orcid":"0000-0002-1419-3267","first_name":"Jakub"}],"scopus_import":"1","day":"18","oa_version":"Published Version","title":"Simplified game of life: Algorithms and complexity","volume":170,"date_created":"2020-09-20T22:01:36Z","has_accepted_license":"1","intvolume":"       170","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","short":"CC BY (3.0)"},"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."}],"publication_status":"published","publication_identifier":{"issn":["18688969"],"isbn":["9783959771597"]},"file_date_updated":"2020-09-21T13:57:34Z"},{"type":"journal_article","date_updated":"2023-09-05T12:40:00Z","_id":"9197","publisher":"Association for the Advancement of Artificial Intelligence","doi":"10.1609/aaai.v34i02.5546","article_processing_charge":"No","quality_controlled":"1","page":"1798-1805","external_id":{"arxiv":["1911.08360"]},"year":"2020","conference":{"location":"New York, NY, United States","end_date":"2020-02-12","start_date":"2020-02-07","name":"AAAI: Conference on Artificial Intelligence"},"date_published":"2020-04-03T00:00:00Z","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).","project":[{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF"}],"publication":"Proceedings of the AAAI Conference on Artificial Intelligence","status":"public","article_type":"original","date_created":"2021-02-25T09:05:18Z","volume":34,"title":"All-pay bidding games on graphs","oa_version":"Preprint","author":[{"full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"first_name":"Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":"1","day":"03","publication_status":"published","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"],"isbn":["9781577358350"]},"intvolume":"        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."}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"month":"04","arxiv":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","issue":"02","citation":{"short":"G. Avni, R. Ibsen-Jensen, J. Tkadlec, Proceedings of the AAAI Conference on Artificial Intelligence 34 (2020) 1798–1805.","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.","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>","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>.","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>","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>."},"language":[{"iso":"eng"}]},{"department":[{"_id":"KrCh"}],"related_material":{"record":[{"relation":"used_in_publication","status":"public","id":"198"}]},"month":"10","year":"2020","date_published":"2020-10-15T00:00:00Z","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","citation":{"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>","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>.","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>.","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>.","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).","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>"},"status":"public","oa":1,"type":"research_data_reference","date_created":"2021-08-06T13:09:57Z","date_updated":"2023-10-18T06:36:00Z","_id":"9814","publisher":"Royal Society","oa_version":"Published Version","title":"Data and mathematica notebooks for plotting figures from language learning with communication between learners from language acquisition with communication between learners","doi":"10.6084/m9.figshare.5973013.v1","author":[{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389"},{"first_name":"Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"day":"15","article_processing_charge":"No","main_file_link":[{"url":"https://doi.org/10.6084/m9.figshare.5973013.v1","open_access":"1"}],"abstract":[{"text":"Data and mathematica notebooks for plotting figures from Language learning with communication between learners","lang":"eng"}]},{"month":"09","department":[{"_id":"ToHe"}],"file":[{"file_name":"prob.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"45ebbc709af2b247d28c7c293c01504b","file_size":436635,"date_created":"2019-08-19T07:56:40Z","creator":"gavni","date_updated":"2020-07-14T12:47:41Z","file_id":"6823"}],"oa":1,"language":[{"iso":"eng"}],"citation":{"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>.","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>","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.","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>.","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.","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.","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>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"day":"06","author":[{"full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287","first_name":"Guy"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr"}],"title":"Bidding games on Markov decision processes","oa_version":"Submitted Version","volume":11674,"date_created":"2019-08-19T07:58:10Z","has_accepted_license":"1","intvolume":"     11674","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."}],"file_date_updated":"2020-07-14T12:47:41Z","publication_identifier":{"isbn":["978-303030805-6"],"issn":["0302-9743"]},"publication_status":"published","year":"2019","status":"public","publication":" Proceedings of the 13th International Conference of Reachability Problems","project":[{"call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"conference":{"location":"Brussels, Belgium","start_date":"2019-09-11","end_date":"2019-09-13","name":"RP: Reachability Problems"},"date_published":"2019-09-06T00:00:00Z","alternative_title":["LNCS"],"doi":"10.1007/978-3-030-30806-3_1","publisher":"Springer","_id":"6822","date_updated":"2021-01-12T08:09:12Z","type":"conference","page":"1-12","ddc":["000"],"quality_controlled":"1"},{"volume":41,"date_created":"2019-12-09T08:33:33Z","article_type":"original","scopus_import":"1","day":"01","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","orcid":"0000-0003-1702-6584","first_name":"Amir Kafshdar"},{"last_name":"Goyal","full_name":"Goyal, Prateesh","first_name":"Prateesh"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"}],"oa_version":"Submitted Version","title":"Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth","file_date_updated":"2020-10-08T12:58:10Z","publication_status":"published","publication_identifier":{"issn":["0164-0925"]},"has_accepted_license":"1","intvolume":"        41","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"}],"department":[{"_id":"KrCh"}],"article_number":"23","file":[{"file_id":"8632","creator":"dernst","date_updated":"2020-10-08T12:58:10Z","date_created":"2020-10-08T12:58:10Z","file_size":667357,"checksum":"291cc86a07bd010d4815e177dac57b70","relation":"main_file","access_level":"open_access","content_type":"application/pdf","success":1,"file_name":"2019_ACMTransactions_Chatterjee.pdf"}],"month":"11","citation":{"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>","ieee":"K. Chatterjee, A. K. Goharshady, P. Goyal, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4. ACM, 2019.","short":"K. Chatterjee, A.K. Goharshady, P. Goyal, R. Ibsen-Jensen, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 41 (2019).","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.","apa":"Chatterjee, K., Goharshady, A. K., Goyal, P., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2019). Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href=\"https://doi.org/10.1145/3363525\">https://doi.org/10.1145/3363525</a>","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 23, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3363525\">10.1145/3363525</a>."},"issue":"4","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa":1,"language":[{"iso":"eng"}],"_id":"7158","date_updated":"2024-03-25T23:30:19Z","type":"journal_article","article_processing_charge":"No","doi":"10.1145/3363525","publisher":"ACM","quality_controlled":"1","ddc":["000"],"isi":1,"year":"2019","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"external_id":{"isi":["000564108400004"]},"ec_funded":1,"date_published":"2019-11-01T00:00:00Z","publication":"ACM Transactions on Programming Languages and Systems","status":"public","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}]},{"publisher":"The Royal Society","article_processing_charge":"No","doi":"10.1098/rsif.2018.0073","type":"journal_article","_id":"198","date_updated":"2023-10-18T06:36:00Z","ddc":["000"],"quality_controlled":"1","related_material":{"link":[{"relation":"supplementary_material","url":"https://dx.doi.org/10.6084/m9.figshare.c.4028971"}],"record":[{"status":"public","relation":"research_data","id":"9814"}]},"external_id":{"isi":["000428576200023"],"pmid":["29593089"]},"isi":1,"year":"2018","publist_id":"7715","publication":"Journal of the Royal Society Interface","status":"public","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_published":"2018-03-01T00:00:00Z","ec_funded":1,"pmid":1,"oa_version":"Submitted Version","title":"Language acquisition with communication between learners","day":"01","scopus_import":"1","author":[{"last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","first_name":"Josef","orcid":"0000-0002-1097-9684"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"date_created":"2018-12-11T11:45:09Z","article_type":"original","volume":15,"abstract":[{"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.","lang":"eng"}],"intvolume":"        15","has_accepted_license":"1","file_date_updated":"2020-07-14T12:45:22Z","publication_identifier":{"eissn":["1742-5662"]},"publication_status":"published","month":"03","article_number":"20180073","file":[{"relation":"main_file","checksum":"444e1a9d98eb0e780671be82b13025f3","file_name":"2018_RS_IbsenJensen.pdf","access_level":"open_access","content_type":"application/pdf","file_id":"5955","date_created":"2019-02-12T07:54:37Z","file_size":219837,"date_updated":"2020-07-14T12:45:22Z","creator":"dernst"}],"department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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>","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).","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.","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>.","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>","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>."},"issue":"140"},{"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory"}],"status":"public","conference":{"start_date":"2018-12-15","end_date":"2018-12-17","name":"14th International Conference on Web and Internet Economics, WINE","location":"Oxford, UK"},"date_published":"2018-11-21T00:00:00Z","external_id":{"isi":["000865933000002"],"arxiv":["1804.04372"]},"isi":1,"year":"2018","page":"21-36","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.04372"}],"publisher":"Springer","doi":"10.1007/978-3-030-04612-5_2","alternative_title":["LNCS"],"article_processing_charge":"No","type":"conference","date_updated":"2023-09-12T07:44:01Z","_id":"5788","language":[{"iso":"eng"}],"oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, in:, Springer, 2018, pp. 21–36.","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>","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>.","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>","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.","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>."},"month":"11","arxiv":1,"department":[{"_id":"ToHe"}],"intvolume":"     11316","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 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."}],"publication_identifier":{"issn":["03029743"],"isbn":["9783030046118"]},"oa_version":"Preprint","title":"Infinite-duration poorman-bidding games","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy","last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"}],"scopus_import":"1","day":"21","date_created":"2018-12-30T22:59:14Z","volume":11316},{"ddc":["000"],"page":"149-150","quality_controlled":"1","publisher":"ACM Press","article_processing_charge":"No","doi":"10.1145/3219166.3219198","type":"conference","_id":"5967","date_updated":"2023-09-19T10:45:15Z","status":"public","publication":"Proceedings of the 2018 ACM Conference on Economics and Computation  - EC '18","conference":{"end_date":"2018-06-22","start_date":"2018-06-18","name":"EC: Conference on Economics and Computation","location":"Ithaca, NY, United States"},"date_published":"2018-06-18T00:00:00Z","external_id":{"isi":["000492755100020"]},"year":"2018","isi":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"}],"has_accepted_license":"1","file_date_updated":"2020-07-14T12:47:14Z","publication_identifier":{"isbn":["9781450358293"]},"publication_status":"published","title":"The Big Match with a clock and a bit of memory","oa_version":"Submitted Version","scopus_import":"1","day":"18","author":[{"first_name":"Kristoffer Arnsfelt","full_name":"Hansen, Kristoffer Arnsfelt","last_name":"Hansen"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"last_name":"Neyman","full_name":"Neyman, Abraham","first_name":"Abraham"}],"date_created":"2019-02-13T10:31:41Z","language":[{"iso":"eng"}],"oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"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 Press, 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.","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 Press, 2018, pp. 149–50, 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 Press. <a href=\"https://doi.org/10.1145/3219166.3219198\">https://doi.org/10.1145/3219166.3219198</a>","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 Press; 2018:149-150. doi:<a href=\"https://doi.org/10.1145/3219166.3219198\">10.1145/3219166.3219198</a>","short":"K.A. Hansen, R. Ibsen-Jensen, A. Neyman, in:, Proceedings of the 2018 ACM Conference on Economics and Computation  - EC ’18, ACM Press, 2018, pp. 149–150.","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."},"month":"06","file":[{"relation":"main_file","checksum":"bb52683e349cfd864f4769a8f38f2798","file_name":"2018_EC18_Hansen.pdf","content_type":"application/pdf","access_level":"open_access","file_id":"7054","file_size":302539,"date_created":"2019-11-19T08:24:24Z","date_updated":"2020-07-14T12:47:14Z","creator":"dernst"}],"department":[{"_id":"KrCh"}]},{"status":"public","publication":"ACM Transactions on Programming Languages and Systems","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"ec_funded":1,"date_published":"2018-08-01T00:00:00Z","year":"2018","isi":1,"related_material":{"record":[{"id":"1437","status":"public","relation":"earlier_version"},{"id":"5441","status":"public","relation":"earlier_version"},{"id":"5442","status":"public","relation":"earlier_version"},{"status":"public","relation":"dissertation_contains","id":"8934"}]},"external_id":{"isi":["000444694800001"],"arxiv":["1510.07565"]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.07565"}],"quality_controlled":"1","article_processing_charge":"No","doi":"10.1145/3210257","publisher":"Association for Computing Machinery (ACM)","_id":"6009","date_updated":"2024-03-25T23:30:19Z","type":"journal_article","oa":1,"language":[{"iso":"eng"}],"citation":{"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>","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).","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 (ACM), 2018.","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 (ACM), 2018. <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/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.","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 (ACM), 2018, doi:<a href=\"https://doi.org/10.1145/3210257\">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 (ACM). <a href=\"https://doi.org/10.1145/3210257\">https://doi.org/10.1145/3210257</a>"},"issue":"3","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","arxiv":1,"month":"08","department":[{"_id":"KrCh"}],"article_number":"9","abstract":[{"lang":"eng","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"}],"intvolume":"        40","publication_identifier":{"issn":["0164-0925"]},"publication_status":"published","day":"01","scopus_import":"1","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584"},{"orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"}],"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","oa_version":"Preprint","volume":40,"date_created":"2019-02-14T14:31:52Z"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","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.","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>","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>.","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>","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>."},"language":[{"iso":"eng"}],"oa":1,"file":[{"creator":"dernst","date_updated":"2020-07-14T12:47:34Z","date_created":"2018-12-17T12:08:00Z","file_size":1078309,"file_id":"5696","access_level":"open_access","content_type":"application/pdf","file_name":"2018_CONCUR_Chatterjee.pdf","checksum":"68a055b1aaa241cc38375083cf832a7d","relation":"main_file"}],"article_number":"11","department":[{"_id":"KrCh"}],"arxiv":1,"month":"09","file_date_updated":"2020-07-14T12:47:34Z","publication_identifier":{"isbn":["978-3-95977-087-3"]},"publication_status":"published","intvolume":"       118","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"text":"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.","lang":"eng"}],"has_accepted_license":"1","date_created":"2018-12-11T11:44:27Z","volume":118,"title":"Ergodic mean-payoff games for the analysis of attacks in crypto-currencies","oa_version":"Published Version","day":"01","scopus_import":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir","last_name":"Goharshady","first_name":"Amir","orcid":"0000-0003-1702-6584"},{"full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"date_published":"2018-09-01T00:00:00Z","conference":{"location":"Beijing, China","start_date":"2018-09-04","end_date":"2018-09-07","name":"CONCUR: Conference on Concurrency Theory"},"ec_funded":1,"status":"public","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"publist_id":"7988","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"external_id":{"arxiv":["1806.03108"]},"year":"2018","quality_controlled":"1","ddc":["000"],"type":"conference","_id":"66","date_updated":"2025-06-02T08:53:46Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","alternative_title":["LIPIcs"],"article_processing_charge":"No","doi":"10.4230/LIPIcs.CONCUR.2018.11"},{"quality_controlled":"1","ddc":["004"],"type":"journal_article","_id":"465","date_updated":"2023-02-23T12:26:25Z","publisher":"International Federation of Computational Logic","doi":"10.23638/LMCS-13(3:23)2017","date_published":"2017-09-13T00:00:00Z","ec_funded":1,"publication":"Logical Methods in Computer Science","status":"public","project":[{"call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"}],"publist_id":"7356","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1610"},{"id":"5438","relation":"earlier_version","status":"public"}]},"year":"2017","file_date_updated":"2020-07-14T12:46:33Z","publication_status":"published","publication_identifier":{"issn":["18605974"]},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"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. "}],"intvolume":"        13","has_accepted_license":"1","date_created":"2018-12-11T11:46:37Z","volume":13,"oa_version":"Published Version","title":"Edit distance for pushdown automata","scopus_import":1,"day":"13","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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>","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).","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>","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>."},"issue":"3","pubrep_id":"955","language":[{"iso":"eng"}],"oa":1,"file":[{"file_id":"5090","creator":"system","date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-12T10:14:37Z","file_size":279071,"checksum":"08041379ba408d40664f449eb5907a8f","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_name":"IST-2015-321-v1+1_main.pdf"},{"file_id":"5091","date_updated":"2020-07-14T12:46:33Z","creator":"system","date_created":"2018-12-12T10:14:38Z","file_size":279071,"checksum":"08041379ba408d40664f449eb5907a8f","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"month":"09"},{"type":"conference","_id":"551","date_updated":"2021-01-12T08:02:34Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","alternative_title":["LIPIcs"],"doi":"10.4230/LIPIcs.MFCS.2017.61","quality_controlled":"1","ddc":["004"],"publist_id":"7263","year":"2017","conference":{"location":"Aalborg, Denmark","start_date":"2017-08-21","end_date":"2017-08-25","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"date_published":"2017-11-01T00:00:00Z","publication":"Leibniz International Proceedings in Informatics","status":"public","date_created":"2018-12-11T11:47:08Z","volume":83,"oa_version":"Published Version","title":"Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs","scopus_import":1,"day":"01","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"file_date_updated":"2020-07-14T12:47:00Z","publication_identifier":{"isbn":["978-395977046-0"]},"publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"abstract":[{"lang":"eng","text":"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. "}],"intvolume":"        83","has_accepted_license":"1","article_number":"61","file":[{"creator":"system","date_updated":"2020-07-14T12:47:00Z","date_created":"2018-12-12T10:18:04Z","file_size":535077,"file_id":"5322","content_type":"application/pdf","access_level":"open_access","file_name":"IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf","checksum":"2eed5224c0e4e259484a1d71acb8ba6a","relation":"main_file"}],"department":[{"_id":"KrCh"}],"month":"11","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"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>.","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 (SG), LIPIcs, vol. 83, 61.","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>","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>.","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>","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.","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017."},"language":[{"iso":"eng"}],"pubrep_id":"924","oa":1},{"ddc":["004"],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1506.02434"}],"quality_controlled":"1","alternative_title":["LIPIcs"],"doi":"10.4230/LIPIcs.MFCS.2017.55","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","_id":"553","date_updated":"2021-01-12T08:02:35Z","type":"conference","publication":"Leibniz International Proceedings in Informatics","status":"public","date_published":"2017-11-01T00:00:00Z","conference":{"name":"MFCS: Mathematical Foundations of Computer Science (SG)","end_date":"2017-08-25","start_date":"2017-08-21","location":"Aalborg, Denmark"},"year":"2017","publist_id":"7261","has_accepted_license":"1","abstract":[{"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. ","lang":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"        83","file_date_updated":"2020-07-14T12:47:00Z","publication_identifier":{"isbn":["978-395977046-0"]},"publication_status":"published","day":"01","scopus_import":1,"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Kristofer","last_name":"Hansen","full_name":"Hansen, Kristofer"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389"}],"oa_version":"Published Version","title":"Strategy complexity of concurrent safety games","volume":83,"date_created":"2018-12-11T11:47:08Z","oa":1,"language":[{"iso":"eng"}],"pubrep_id":"922","citation":{"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 (SG), LIPIcs, vol. 83, 55.","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>.","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>","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>","short":"K. Chatterjee, K. Hansen, R. Ibsen-Jensen, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","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."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"11","department":[{"_id":"KrCh"}],"file":[{"file_name":"IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"7101facb56ade363205c695d72dbd173","date_created":"2018-12-12T10:09:29Z","file_size":549967,"date_updated":"2020-07-14T12:47:00Z","creator":"system","file_id":"4753"}],"article_number":"55"},{"file":[{"file_id":"5084","file_size":579225,"date_created":"2018-12-12T10:14:31Z","creator":"system","date_updated":"2018-12-12T10:14:31Z","relation":"main_file","file_name":"IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf","access_level":"open_access","content_type":"application/pdf"}],"article_number":"28","department":[{"_id":"KrCh"}],"month":"08","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. In: Vol 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">10.4230/LIPIcs.ESA.2016.28</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs,” presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark, 2016, vol. 57.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs,” Vol. 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">https://doi.org/10.4230/LIPIcs.ESA.2016.28</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2016. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. ESA: European Symposium on Algorithms, LIPIcs, vol. 57, 28.","mla":"Chatterjee, Krishnendu, et al. <i>Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs</i>. Vol. 57, 28, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">10.4230/LIPIcs.ESA.2016.28</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2016). Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs (Vol. 57). Presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">https://doi.org/10.4230/LIPIcs.ESA.2016.28</a>"},"pubrep_id":"777","language":[{"iso":"eng"}],"oa":1,"date_created":"2018-12-11T11:49:59Z","volume":57,"oa_version":"Published Version","title":"Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722"}],"scopus_import":1,"day":"01","publication_status":"published","file_date_updated":"2018-12-12T10:14:31Z","abstract":[{"text":"We consider data-structures for answering reachability and distance queries on constant-treewidth graphs with n nodes, on the standard RAM computational model with wordsize W=Theta(log n). Our first contribution is a data-structure that after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time; and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. The data-structure uses at all times O(n) space. Our second contribution is a space-time tradeoff data-structure for distance queries. For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing time that allows pair queries in O(n^{1-\\epsilon} alpha(n)) time, where alpha is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space. The input graph G is not considered in the space complexity. ","lang":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"        57","has_accepted_license":"1","publist_id":"6312","related_material":{"record":[{"id":"821","status":"public","relation":"dissertation_contains"}]},"year":"2016","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE) and ERC Start grant (279307: Graph Games).","date_published":"2016-08-01T00:00:00Z","conference":{"name":"ESA: European Symposium on Algorithms","end_date":"2016-08-24","start_date":"2016-08-22","location":"Aarhus, Denmark"},"ec_funded":1,"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"status":"public","type":"conference","date_updated":"2023-09-07T12:01:58Z","_id":"1071","publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik","doi":"10.4230/LIPIcs.ESA.2016.28","alternative_title":["LIPIcs"],"quality_controlled":"1","ddc":["004","006"]},{"date_published":"2016-01-01T00:00:00Z","conference":{"location":"The Hague, Netherlands","end_date":"2016-09-02","start_date":"2016-08-29","name":"ECAI: European Conference on Artificial Intelligence"},"status":"public","publist_id":"7342","year":"2016","quality_controlled":"1","ddc":["004"],"page":"1432 - 1439","type":"conference","date_updated":"2021-01-12T08:00:54Z","_id":"478","publisher":"IOS Press","doi":"10.3233/978-1-61499-672-9-1432","alternative_title":["Frontiers in Artificial Intelligence and Applications"],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"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>.","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>","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.","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>.","short":"K. Chatterjee, R. Ibsen-Jensen, in:, IOS Press, 2016, pp. 1432–1439.","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.","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>"},"language":[{"iso":"eng"}],"pubrep_id":"950","oa":1,"file":[{"relation":"main_file","checksum":"848043c812ace05e459579c923f3d3cf","file_name":"IST-2018-950-v1+1_2016_Chatterjee_The_complexity.pdf","content_type":"application/pdf","access_level":"open_access","file_id":"4658","date_created":"2018-12-12T10:07:59Z","file_size":2116225,"creator":"system","date_updated":"2020-07-14T12:46:35Z"}],"department":[{"_id":"KrCh"}],"month":"01","publication_status":"published","file_date_updated":"2020-07-14T12:46:35Z","intvolume":"       285","tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","short":"CC BY-NC (4.0)"},"abstract":[{"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.","lang":"eng"}],"has_accepted_license":"1","date_created":"2018-12-11T11:46:41Z","volume":285,"title":"The complexity of deciding legality of a single step of magic: The gathering","oa_version":"Published Version","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"}],"day":"01","scopus_import":1},{"volume":"20-22","date_created":"2018-12-11T11:52:01Z","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir","orcid":"0000-0003-1702-6584","first_name":"Amir"},{"first_name":"Rasmus","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722"}],"day":"11","scopus_import":1,"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","oa_version":"Preprint","publication_status":"published","abstract":[{"lang":"eng","text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. 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. Our 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."}],"department":[{"_id":"KrCh"}],"month":"01","arxiv":1,"citation":{"ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2016. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. POPL: Principles of Programming Languages, POPL, vol. 20–22, 733–747.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components,” 20–22:733–47. ACM, 2016. <a href=\"https://doi.org/10.1145/2837614.2837624\">https://doi.org/10.1145/2837614.2837624</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components</i>. Vol. 20–22, ACM, 2016, pp. 733–47, doi:<a href=\"https://doi.org/10.1145/2837614.2837624\">10.1145/2837614.2837624</a>.","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2016). Algorithms for algebraic path properties in concurrent systems of constant treewidth components (Vol. 20–22, pp. 733–747). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. <a href=\"https://doi.org/10.1145/2837614.2837624\">https://doi.org/10.1145/2837614.2837624</a>","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In: Vol 20-22. ACM; 2016:733-747. doi:<a href=\"https://doi.org/10.1145/2837614.2837624\">10.1145/2837614.2837624</a>","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, ACM, 2016, pp. 733–747.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 733–747."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"language":[{"iso":"eng"}],"date_updated":"2024-03-25T23:30:18Z","_id":"1437","type":"conference","doi":"10.1145/2837614.2837624","alternative_title":["POPL"],"publisher":"ACM","main_file_link":[{"url":"http://arxiv.org/abs/1510.07565","open_access":"1"}],"quality_controlled":"1","page":"733 - 747","publist_id":"5761","year":"2016","external_id":{"arxiv":["1510.07565"]},"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5441"},{"status":"public","relation":"earlier_version","id":"5442"},{"id":"821","relation":"dissertation_contains","status":"public"},{"id":"6009","relation":"later_version","status":"public"},{"status":"public","relation":"dissertation_contains","id":"8934"}]},"ec_funded":1,"conference":{"name":"POPL: Principles of Programming Languages","end_date":"2016-01-22","start_date":"2016-01-20","location":"St. Petersburg, FL, USA"},"date_published":"2016-01-11T00:00:00Z","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"status":"public"}]