@inproceedings{12101,
  abstract     = {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.},
  author       = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Jecker, Ismael R and Svoboda, Jakub},
  booktitle    = {42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  isbn         = {9783959772617},
  issn         = {1868-8969},
  location     = {Madras, India},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Complexity of spatial games}},
  doi          = {10.4230/LIPIcs.FSTTCS.2022.11},
  volume       = {250},
  year         = {2022},
}

@article{9393,
  abstract     = {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.},
  author       = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  issn         = {1572-8102},
  journal      = {Formal Methods in System Design},
  pages        = {401--428},
  publisher    = {Springer},
  title        = {{Faster algorithms for quantitative verification in bounded treewidth graphs}},
  doi          = {10.1007/s10703-021-00373-5},
  volume       = {57},
  year         = {2021},
}

@inproceedings{10629,
  abstract     = {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.
Our 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^{-λ}).},
  author       = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  booktitle    = {41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  isbn         = {978-3-9597-7215-0},
  issn         = {1868-8969},
  location     = {Virtual},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Quantitative verification on product graphs of small treewidth}},
  doi          = {10.4230/LIPIcs.FSTTCS.2021.42},
  volume       = {213},
  year         = {2021},
}

@inproceedings{7810,
  abstract     = {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.
In 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.},
  author       = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  booktitle    = {European Symposium on Programming},
  isbn         = {9783030449131},
  issn         = {16113349},
  location     = {Dublin, Ireland},
  pages        = {112--140},
  publisher    = {Springer Nature},
  title        = {{Optimal and perfectly parallel algorithms for on-demand data-flow analysis}},
  doi          = {10.1007/978-3-030-44914-8_5},
  volume       = {12075},
  year         = {2020},
}

@inproceedings{8533,
  abstract     = {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.},
  author       = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Jecker, Ismael R and Svoboda, Jakub},
  booktitle    = {45th International Symposium on Mathematical Foundations of Computer Science},
  isbn         = {9783959771597},
  issn         = {18688969},
  location     = {Prague, Czech Republic},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Simplified game of life: Algorithms and complexity}},
  doi          = {10.4230/LIPIcs.MFCS.2020.22},
  volume       = {170},
  year         = {2020},
}

@article{9197,
  abstract     = {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.},
  author       = {Avni, Guy and Ibsen-Jensen, Rasmus and Tkadlec, Josef},
  isbn         = {9781577358350},
  issn         = {2374-3468},
  journal      = {Proceedings of the AAAI Conference on Artificial Intelligence},
  location     = {New York, NY, United States},
  number       = {02},
  pages        = {1798--1805},
  publisher    = {Association for the Advancement of Artificial Intelligence},
  title        = {{All-pay bidding games on graphs}},
  doi          = {10.1609/aaai.v34i02.5546},
  volume       = {34},
  year         = {2020},
}

@misc{9814,
  abstract     = {Data and mathematica notebooks for plotting figures from Language learning with communication between learners},
  author       = {Ibsen-Jensen, Rasmus and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin},
  publisher    = {Royal Society},
  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},
  year         = {2020},
}

@inproceedings{6822,
  abstract     = {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
bidder 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 
 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.},
  author       = {Avni, Guy and Henzinger, Thomas A and Ibsen-Jensen, Rasmus and Novotny, Petr},
  booktitle    = { Proceedings of the 13th International Conference of Reachability Problems},
  isbn         = {978-303030805-6},
  issn         = {0302-9743},
  location     = {Brussels, Belgium},
  pages        = {1--12},
  publisher    = {Springer},
  title        = {{Bidding games on Markov decision processes}},
  doi          = {10.1007/978-3-030-30806-3_1},
  volume       = {11674},
  year         = {2019},
}

@article{7158,
  abstract     = {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.

Our 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.
},
  author       = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Goyal, Prateesh and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  issn         = {0164-0925},
  journal      = {ACM Transactions on Programming Languages and Systems},
  number       = {4},
  publisher    = {ACM},
  title        = {{Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth}},
  doi          = {10.1145/3363525},
  volume       = {41},
  year         = {2019},
}

@article{198,
  abstract     = {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.},
  author       = {Ibsen-Jensen, Rasmus and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin},
  issn         = {1742-5662},
  journal      = {Journal of the Royal Society Interface},
  number       = {140},
  publisher    = {The Royal Society},
  title        = {{Language acquisition with communication between learners}},
  doi          = {10.1098/rsif.2018.0073},
  volume       = {15},
  year         = {2018},
}

@inproceedings{5788,
  abstract     = {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.},
  author       = {Avni, Guy and Henzinger, Thomas A and Ibsen-Jensen, Rasmus},
  isbn         = {9783030046118},
  issn         = {03029743},
  location     = {Oxford, UK},
  pages        = {21--36},
  publisher    = {Springer},
  title        = {{Infinite-duration poorman-bidding games}},
  doi          = {10.1007/978-3-030-04612-5_2},
  volume       = {11316},
  year         = {2018},
}

@inproceedings{5967,
  abstract     = {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.
Blackwell 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.
},
  author       = {Hansen, Kristoffer Arnsfelt and Ibsen-Jensen, Rasmus and Neyman, Abraham},
  booktitle    = {Proceedings of the 2018 ACM Conference on Economics and Computation  - EC '18},
  isbn         = {9781450358293},
  location     = {Ithaca, NY, United States},
  pages        = {149--150},
  publisher    = {ACM Press},
  title        = {{The Big Match with a clock and a bit of memory}},
  doi          = {10.1145/3219166.3219198},
  year         = {2018},
}

@article{6009,
  abstract     = {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.
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.
},
  author       = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Goharshady, Amir Kafshdar and Pavlogiannis, Andreas},
  issn         = {0164-0925},
  journal      = {ACM Transactions on Programming Languages and Systems},
  number       = {3},
  publisher    = {Association for Computing Machinery (ACM)},
  title        = {{Algorithms for algebraic path properties in concurrent systems of constant treewidth components}},
  doi          = {10.1145/3210257},
  volume       = {40},
  year         = {2018},
}

@inproceedings{66,
  abstract     = {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.},
  author       = {Chatterjee, Krishnendu and Goharshady, Amir and Ibsen-Jensen, Rasmus and Velner, Yaron},
  isbn         = {978-3-95977-087-3},
  location     = {Beijing, China},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Ergodic mean-payoff games for the analysis of attacks in crypto-currencies}},
  doi          = {10.4230/LIPIcs.CONCUR.2018.11},
  volume       = {118},
  year         = {2018},
}

@article{465,
  abstract     = {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. },
  author       = {Chatterjee, Krishnendu and Henzinger, Thomas A and Ibsen-Jensen, Rasmus and Otop, Jan},
  issn         = {18605974},
  journal      = {Logical Methods in Computer Science},
  number       = {3},
  publisher    = {International Federation of Computational Logic},
  title        = {{Edit distance for pushdown automata}},
  doi          = {10.23638/LMCS-13(3:23)2017},
  volume       = {13},
  year         = {2017},
}

@inproceedings{551,
  abstract     = {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. },
  author       = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Nowak, Martin},
  booktitle    = {Leibniz International Proceedings in Informatics},
  isbn         = {978-395977046-0},
  location     = {Aalborg, Denmark},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs}},
  doi          = {10.4230/LIPIcs.MFCS.2017.61},
  volume       = {83},
  year         = {2017},
}

@inproceedings{553,
  abstract     = {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. },
  author       = {Chatterjee, Krishnendu and Hansen, Kristofer and Ibsen-Jensen, Rasmus},
  booktitle    = {Leibniz International Proceedings in Informatics},
  isbn         = {978-395977046-0},
  location     = {Aalborg, Denmark},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Strategy complexity of concurrent safety games}},
  doi          = {10.4230/LIPIcs.MFCS.2017.55},
  volume       = {83},
  year         = {2017},
}

@inproceedings{1071,
  abstract     = {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. },
  author       = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  location     = {Aarhus, Denmark},
  publisher    = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik},
  title        = {{Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs}},
  doi          = {10.4230/LIPIcs.ESA.2016.28},
  volume       = {57},
  year         = {2016},
}

@inproceedings{478,
  abstract     = {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.},
  author       = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus},
  location     = {The Hague, Netherlands},
  pages        = {1432 -- 1439},
  publisher    = {IOS Press},
  title        = {{The complexity of deciding legality of a single step of magic: The gathering}},
  doi          = {10.3233/978-1-61499-672-9-1432},
  volume       = {285},
  year         = {2016},
}

@inproceedings{1437,
  abstract     = {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.},
  author       = {Chatterjee, Krishnendu and Goharshady, Amir and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  location     = {St. Petersburg, FL, USA},
  pages        = {733 -- 747},
  publisher    = {ACM},
  title        = {{Algorithms for algebraic path properties in concurrent systems of constant treewidth components}},
  doi          = {10.1145/2837614.2837624},
  volume       = {20-22},
  year         = {2016},
}