Searcharxiv⌕ Search

arXiv subjects

Rasmus Ibsen-Jensen

Publications and source records attributed to Rasmus Ibsen-Jensen.

At least 19 recordsLinked to original sources
arXiv2026

The Complexity of Games with Randomised Control

We study the complexity of solving two-player infinite duration games played on a fixed finite graph, where the control of a node is not predetermined but rather assigned randomly. In classic random-turn games, control of each node is assigned randomly every time the node is visited during a play. In this work, we study two natural variants of this where control of each node is assigned only once: (i) control is assigned randomly during a play when a node is visited for the first time and does not change for the rest of the play and (ii) control is assigned a priori before the game starts for every node by independent coin tosses and then the game is played. We investigate the complexity of computing the winning probability with three kinds of objectives-reachability, parity, and energy. We show that the qualitative questions on all variants and all objectives are NL-complete. For the quantitative questions, we show that deciding whether the maximiser can win with probability at least a given threshold for every objective is PSPACE-complete under the first mechanism, and that computing the exact winning probability for every objective is sharp-P-complete under the second. To complement our hardness results for the second mechanism, we propose randomised approximation schemes that efficiently estimate the winning probability for all three objectives, assuming a bounded number of parity colours and unary-encoded weights for energy objectives, and we empirically demonstrate their fast convergence.

cs.GT↗
arXiv2025

Games on Graphs: From Logic and Automata to Algorithms

The objective of this book is to give a comprehensive presentation of the research field concerned with infinite duration games on graphs. Historically, these game models appeared in the study of automata and logic, and they later became important for program verification and synthesis. They have many more applications, in particular some of the models investigated in this book were introduced and studied in neighbouring research communities such as optimisation, reinforcement learning, model theory, and set theory.

cs.GT↗
arXiv2025

Stochastic Games with Limited Public Memory

We study the memory resources required for near-optimal play in two-player zero-sum stochastic games with the long-run average payoff. Although optimal strategies may not exist in such games, near-optimal strategies always do. Mertens and Neyman (1981) proved that in any stochastic game, for any $\varepsilon>0$, there exist uniform $\varepsilon$-optimal memory-based strategies -- i.e., strategies that are $\varepsilon$-optimal in all sufficiently long $n$-stage games -- that use at most $O(n)$ memory states within the first $n$ stages. We improve this bound on the number of memory states by proving that in any stochastic game, for any $\varepsilon>0$, there exist uniform $\varepsilon$-optimal memory-based strategies that use at most $O(\log n)$ memory states in the first $n$ stages. Moreover, we establish the existence of uniform $\varepsilon$-optimal memory-based strategies whose memory updating and action selection are time-independent and such that, with probability close to 1, for all $n$, the number of memory states used up to stage $n$ is at most $O(\log n)$. This result cannot be extended to strategies with bounded public memory -- even if time-dependent memory updating and action selection are allowed. This impossibility is illustrated in the Big Match -- a well-known stochastic game where the stage payoffs to Player 1 are 0 or 1. Although for any $\varepsilon > 0$, there exist strategies of Player 1 that guarantee a payoff {exceeding} $1/2 - \varepsilon$ in all sufficiently long $n$-stage games, we show that any strategy of Player 1 that uses a finite public memory fails to guarantee a payoff greater than $\varepsilon$ in any sufficiently long $n$-stage game.

cs.GT↗
arXiv2024

The Power of Counting Steps in Quantitative Games

We study deterministic games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs. We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over infinite graphs, focusing on whether step-counter strategies (sometimes called Markov strategies) suffice to implement winning strategies. In particular, we show that over finitely branching arenas, three variants of limsup mean-payoff and total-payoff objectives admit winning strategies that are based either on a step counter or on a step counter and an additional bit of memory. Conversely, we show that for certain liminf total-payoff objectives, strategies resorting to a step counter and finite memory are not sufficient. For step-counter strategies, this settles the case of all classical quantitative objectives up to the second level of the Borel hierarchy.

cs.GT↗
arXiv2024

Bounded-Memory Strategies in Partial-Information Games

We study the computational complexity of solving stochastic games with mean-payoff objectives. Instead of identifying special classes in which simple strategies are sufficient to play $ε$-optimally, or form $ε$-Nash equilibria, we consider general partial-information multiplayer games and ask what can be achieved with (and against) finite-memory strategies up to a {given} bound on the memory. We show $NP$-hardness for approximating zero-sum values, already with respect to memoryless strategies and for 1-player reachability games. On the other hand, we provide upper bounds for solving games of any fixed number of players $k$. We show that one can decide in polynomial space if, for a given $k$-player game, $ε\ge 0$ and bound $b$, there exists an $ε$-Nash equilibrium in which all strategies use at most $b$ memory modes. For given $ε>0$, finding an $ε$-Nash equilibrium with respect to $b$-bounded strategies can be done in $FN[NP]$. Similarly for 2-player zero-sum games, finding a $b$-bounded strategy that, against all $b$-bounded opponent strategies, guarantees an outcome within $ε$ of a given value, can be done in $FNP[NP]$. Our constructions apply to parity objectives with minimal simplifications. Our results improve the status quo in several well-known special cases of games. In particular, for $2$-player zero-sum concurrent mean-payoff games, one can approximate ordinary zero-sum values (without restricting admissible strategies) in $FNP[NP]$.

cs.GT↗
arXiv2020

Simplified Game of Life: Algorithms and Complexity

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.

nlin.CG↗
arXiv2020

Optimal and Perfectly Parallel Algorithms for On-demand Data-flow Analysis

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.

cs.DS↗
arXiv2020

One-Clock Priced Timed Games are PSPACE-hard

The main result of this paper is that computing the value of a one-clock priced timed game (OCPTG) is PSPACE-hard. Along the way, we provide a family of OCPTGs that have an exponential number of event points. Both results hold even in very restricted classes of games such as DAGs with treewidth three. Finally, we provide a number of positive results, including polynomial-time algorithms for even more restricted classes of OCPTGs such as trees.

cs.GT↗
arXiv2020

Infinite-Duration Poorman-Bidding Games

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 {\em bidding games} in which the players bid for the right to move the token. Two bidding rules have been defined. In {\em Richman} bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. {\em 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 {\em infinite-duration} poorman games. A central quantity in these games is the {\em 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 {\em 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 {\em 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.

cs.GT↗
arXiv2019

All-Pay Bidding Games on Graphs

In this paper we introduce and study {\em 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 \PO pays \PT 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 {\em 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 \PO wins iff he wins the first two auctions, has been long stated as an open question, which we solve.

cs.GT↗
arXiv2018

Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies

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-payoff 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.

cs.CR↗
arXiv2017

Edit Distance for Pushdown Automata

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 $\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ to $\mathcal{L}_2$ is the minimal number $k$ such that for every word from $\mathcal{L}_1$ there exists a word in $\mathcal{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.

cs.FL↗
arXiv2017

Faster Monte-Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs

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. We present faster polynomial-time Monte-Carlo algorithms for finidng the fixation probability on undirected graphs. Our algorithms are always at least a factor O(n^2/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.

cs.NE↗
arXiv2016

The Big Match in Small Space

In this paper we study how to play (stochastic) games optimally using little space. We focus on repeated games with absorbing states, a type of two-player, zero-sum concurrent mean-payoff games. The prototypical example of these games is the well known Big Match of Gillete (1957). These games may not allow optimal strategies but they always have ε-optimal strategies. In this paper we design ε-optimal strategies for Player 1 in these games that use only O(log log T ) space. Furthermore, we construct strategies for Player 1 that use space s(T), for an arbitrary small unbounded non-decreasing function s, and which guarantee an ε-optimal value for Player 1 in the limit superior sense. The previously known strategies use space Ω(logT) and it was known that no strategy can use constant space if it is ε-optimal even in the limit superior sense. We also give a complementary lower bound. Furthermore, we also show that no Markov strategy, even extended with finite memory, can ensure value greater than 0 in the Big Match, answering a question posed by Abraham Neyman.

cs.GT↗
arXiv2016

Robust Draws in Balanced Knockout Tournaments

Balanced knockout tournaments are ubiquitous in sports competitions and are also used in decision-making and elections. The traditional computational question, that asks to compute a draw (optimal draw) that maximizes the winning probability for a distinguished player, has received a lot of attention. Previous works consider the problem where the pairwise winning probabilities are known precisely, while we study how robust is the winning probability with respect to small errors in the pairwise winning probabilities. First, we present several illuminating examples to establish: (a)~there exist deterministic tournaments (where the pairwise winning probabilities are~0 or~1) where one optimal draw is much more robust than the other; and (b)~in general, there exist tournaments with slightly suboptimal draws that are more robust than all the optimal draws. The above examples motivate the study of the computational problem of robust draws that guarantee a specified winning probability. Second, we present a polynomial-time algorithm for approximating the robustness of a draw for sufficiently small errors in pairwise winning probabilities, and obtain that the stated computational problem is NP-complete. We also show that two natural cases of deterministic tournaments where the optimal draw could be computed in polynomial time also admit polynomial-time algorithms to compute robust optimal draws.

cs.GT↗
arXiv2015

Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components

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, 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.

cs.PL↗
arXiv2015

Strategy Complexity of Concurrent Stochastic Games with Safety and Reachability Objectives

We consider finite-state concurrent stochastic games, played by k>=2 players 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. We consider reachability objectives that given a target set of states require that some state in the target is visited, and the dual safety objectives that given a target set require that only states in the target set are visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest nonzero probability employed. Our main results are as follows: We show that in two-player zero-sum concurrent stochastic games (with reachability objective for one player and the complementary safety objective for the other player): (i) the optimal bound on the patience of optimal and epsilon-optimal strategies, for both players is doubly exponential; and (ii) even in games with a single nonabsorbing state exponential (in the number of actions) patience is necessary. In general we study the class of non-zero-sum games admitting stationary epsilon-Nash equilibria. We show that if there is at least one player with reachability objective, then doubly-exponential patience may be needed for epsilon-Nash equilibrium strategies, whereas in contrast if all players have safety objectives, the optimal bound on patience for epsilon-Nash equilibrium strategies is only exponential.

cs.GT↗