Related papers: Playing Pushdown Parity Games in a Hurry

We consider two-player turn-based games with zero-reachability and zero-safety objectives generated by extended vector addition systems with states. Although the problem of deciding the winner in such games is undecidable in general, we…

Quantitative games are two-player zero-sum games played on directed weighted graphs. Total-payoff games (that can be seen as a refinement of the well-studied mean-payoff games) are the variant where the payoff of a play is computed as the…

Parity games are infinite two-player games played on directed graphs. Parity game solvers are used in the domain of formal verification. This paper defines parametrized parity games and introduces an operation, Justify, that determines a…

We consider two-player games played in real time on game structures with clocks and parity objectives. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the…

Parity games are two-player infinite-duration games on graphs that play a crucial role in various fields of theoretical computer science. Finding efficient algorithms to solve these games in practice is widely acknowledged as a core problem…

Two-player games on graphs is central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work we consider solving recursive game graphs (or pushdown game graphs) that can…

This work studies the following question: can plays in a Muller game be stopped after a finite number of moves and a winner be declared. A criterion to do this is sound if Player 0 wins an infinite-duration Muller game if and only if she…

Muller games are played by two players moving a token along a graph; the winner is determined by the set of vertices that occur infinitely often. The central algorithmic problem is to compute the winning regions for the players. Different…

Although mixed extensions of finite games always admit equilibria, this is not the case for countable games, the best-known example being Wald's pick-the-larger-integer game. Several authors have provided conditions for the existence of…

Two-player win/lose games of infinite duration are involved in several disciplines including computer science and logic. If such a game has deterministic winning strategies, one may ask how simple such strategies can get. The answer may…

We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety…

In this paper we investigate a differential game in which countably many dynamical objects pursue a single one. All the players perform simple motions. The duration of the game is fixed. The controls of a group of pursuers are subject to…

We consider two-player stochastic games played on a finite graph for infinitely many rounds. Stochastic games generalize both Markov decision processes (MDP) by adding an adversary player, and two-player deterministic games by adding…

Games on recursive game graphs can be used to reason about the control flow of sequential programs with recursion. In games over recursive game graphs, the most natural notion of strategy is the modular strategy, i.e., a strategy that is…

Infinite games where several players seek to coordinate under imperfect information are known to be intractable, unless the information flow is severely restricted. Examples of undecidable cases typically feature a situation where players…

We introduce and analyze several variations of Penney's game aimed to find a more equitable game.

Many analysis and verifications tasks, such as static program analyses and model-checking for temporal logics reduce to the solution of systems of equations over suitable lattices. Inspired by recent work on lattice-theoretic progress…

This paper discusses the problem of efficiently solving parity games where player Odd has to obey an additional 'strong transition fairness constraint' on its vertices -- given that a player Odd vertex $v$ is visited infinitely often, a…

Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several…

We give an algorithm for solving stochastic parity games with almost-sure winning conditions on {\it lossy channel systems}, under the constraint that both players are restricted to finite-memory strategies. First, we describe a general…