Parameterized linear temporal logics are extensions of Linear Temporal Logic (LTL) by temporal operators equipped with variables that bound their scope. In model-checking, such specifications were introduced as PLTL by Alur et al. and as PROMPT-LTL by Kupferman et al. We show how to determine in doubly-exponential time, whether a player wins a game with PLTL winning condition with respect to some, infinitely many, or all variable valuations. Hence, these problems are not harder than solving LTL games. Furthermore, we present an algorithm with triply-exponential running time to determine optimal variable valuations that allow a player to win a game. Finally, we give doubly-exponential upper and lower bounds on the values of such optimal variable valuations.

This work considers a finite-duration variant of Muller games, and their connection to infinite-duration Muller games. In particular, it studies the question of how long a finite- duration Muller game must be played before the winner of the finite-duration game is guaranteed to be able to win the corresponding infinite-duration game. Previous work by McNaughton has shown that this must occur after Pi_j=1ⁿ(j!+1) moves, and the reduction from Muller games to parity games gives a bound of n· n!+ 1 moves. We improve upon both of these results, by giving a bound of 3ⁿ moves.

We continue the investigation of finite-duration variants of infinite-duration games by extending known results for games played on finite graphs to those played on infinite ones. In particular, we establish an equivalence between pushdown parity games and a finite-duration variant. This allows us to determine the winner of a pushdown parity game by solving a reachability game on a finite tree.

We transform a Muller game with n vertices into a safety game with (n!)^3 vertices whose solution allows to determine the winning regions of the Muller game and to compute a finite-state winning strategy for one player. This yields a novel antichain-based memory structure and a natural notion of permissive strategies for Muller games. Moreover, we generalize our construction by presenting a new type of game reduction from infinite games to safety games and show its applicability to several other winning conditions.

We investigate the existence and the complexity of computing and implementing optimal winning strategies for graph games of infinite duration.

Parameterized linear temporal logics are extensions of Linear Temporal Logic (LTL) by temporal operators equipped with variables for time bounds. In model-checking, such specifications were introduced as PLTL by Alur et al. and as PROMPT-LTL by Kupferman et al. We show how to determine in doubly-exponential time, whether a player wins a game with PLTL winning condition with respect to some, infinitely many, or all variable valuations. Hence, these problems are not harder than solving LTL games. Furthermore, we present an algorithm with triply-exponential running time to determine optimal variable valuations that allow a player to win a game. Finally, we give doubly-exponential upper and lower bounds on the values of optimal variable valuations.

In Muller games, we measure the quality of a winning strategy using McNaughton's scoring functions. We construct winning strategies that bound the losing player's scores by two and show this to be optimal. This improves the previous best upper bound of n! in a game with n vertices, obtained by McNaughton. Using these strategies, we show how to transform a Muller game into a safety game whose solution allows to determine the winning regions of the Muller game and to compute a finite-state winning strategy for one player. This yields a novel antichain-based memory structure and the first definition of permissive strategies for Muller games. Moreover, we generalize our construction by presenting a new type of game reduction from infinite games to safety games and show its applicability to several other winning conditions.

We continue the investigation of delay games, infinite games in which one player may postpone her moves for some time to obtain a lookahead on her opponent's moves. We show that the problem of determining the winner of such a game is undecidable for deterministic context-free winning conditions. Furthermore, we show that the necessary lookahead to win a deterministic context-free delay game cannot be bounded by any elementary function. Both results hold already for restricted classes of deterministic context-free winning conditions.

We show how to transform a Muller game with n vertices into a safety game with (n!)^3 vertices whose solution allows to determine the winning regions of the Muller game and a winning strategy for one player.

We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as PLTL by Alur et al. and (in a different version called PROMPT-LTL) by Kupferman et al..

We present an algorithm to determine optimal variable valuations that allow a player to win a game. Furthermore, we show how to determine whether a player wins a game with respect to some, infinitely many, or all valuations. All our algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games.

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 wins the finite-duration version. A sound criterion is presented that stops a play after at most 3^n moves, where n is the size of the arena. This improves the bound (n!+1)^n obtained by McNaughton and the bound n!+1 derived from a reduction to parity games.

We continue the investigation of delay games, infinite games in which one player may postpone her moves for some time to obtain a lookahead on her opponents moves. We show that the problem of determining the winner of such a game is undecidable for context-free winning conditions. Furthermore, we show that the necessary lookahead to win a context-free delay game cannot be bounded by an elementary function.

We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as PLTL by Alur et al. and (in a different version called PROMPT-LTL) by Kupferman et al..

Our work lifts their results on model checking for PLTL and PROMPT-LTL to the level of games: we present algorithms that determine whether a player wins a game with respect to some, infinitely many, or all variable valuations. All these algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games. Furthermore, we show how to determine optimal valuations that allow a player to win a game.

We introduce a novel winning condition for infinite two-player games on graphs which extends the request-response condition and better matches concrete applications in scheduling or project planning. In a poset game, a request has to be responded by multiple events in an ordering over time that is compatible with a given partial ordering of the events. Poset games are zero-sum, but there are plays that are more desirable than others, i.e., those in which the requests are served quickly. We show that optimal strategies (with respect to long term average accumulated waiting times) exist. These strategies are implementable with finite memory and are effectively computable.

We introduce a novel winning condition for infinite two-player games on graphs which extends the request-response condition and better matches concrete applications in scheduling or project planning. In a poset game, a request has to be responded by multiple events in an ordering over time that is compatible with a given partial ordering of the events. Poset games are zero-sum, but there are plays that are more desirable than others, i.e., those in which the requests are served quickly. We show that optimal strategies (with respect to long term average accumulated waiting times) exist. These strategies are implementable with finite memory and are effectively computable.

Infinite Games are an important tool in the synthesis of finite-state controllers for reactive systems. The interaction between the environment and the system is modeled by a finite graph. The specification that has to be satisfied by the controlled system is translated into a winning condition on the infinite paths of the graph. Then, a winning strategy is a controller that is correct with respect to the given specification. Winning strategies are often finitely described by automata with output.

While classical optimization of synthesized controllers focuses on the size of the automaton we consider a different quality measure. Many winning conditions allow a natural definition of waiting times that reflect periods of waiting in the original system. We investigate time-optimal strategies for Request-Response Games, Poset Games - a novel type of infinite games that extends Request-Response Games - and games with winning conditions in Parametric Linear Temporal Logic. Here, the temporal operators of classical Temporal Logics can be subscribed with free variables that represent bounds on the satisfaction. Then, one is interested in winning strategies with respect to optimal valuations of the free variables. The optimization objective, maximization respectively minimization of the variable values, depends on the formula.

For Request-Response Games and Poset Games, we prove the existence of time-optimal finite-state winning strategies. For games with winning conditions in Parametric Linear Temporal Logic, we prove that optimal winning strategies are computable for solitary games.