Strategy machines : representation and complexity of strategies in infinite games
Marcus Gelderie, Wolfgang H Thomas · RWTH Publications (RWTH Aachen) · 2014
This thesis studies the representation of winning strategies in infinite games as Turing machines. We show that Turing-machine-based strategy representation (by "strategy machines") - if compared to the standard setting of Mealy automata - allows for a finer classification of strategies, provides a better understanding of the structure of strategies, and can successfully be used in areas that are difficult to reason about with automaton strategies, such as composition of games and strategies. We give a formal definition of strategy machines and adapt the classical Turing-machine complexity measures to our setting - called latency, space requirement, and size. The latency is the number of computation steps that is required to produce a next move, the space requirement states how much memory is required for this computation and the size is the number of control states of the machine. These complexity measures are not present in representations of strategies that are based on automata and thus provide a finer view on strategies than currently used models. We show that strategy machines of polynomial size with a polynomial space requirement can be synthesized for Muller games. Moreover, we show that for Streett games a polynomial latency can be guaranteed in addition to these bounds. The synthesis procedure is an adaption of Zielonka's algorithm, now making use of the computational power of a Turing machine to spread costly computations across the infinite play. Turning to composition of games and strategies, we study reachability and Büchi games on arenas that are products of several component arenas. We focus on composing a winning strategy on the product arena from winning strategies in suitably chosen games on the components. We define strategy composition based on subroutine calls and show that as long as the component arenas cannot communicate, a composition of polynomial size and latency can be computed in polynomial time. If components may communicate, a similar composition result exists iff Pspace = Exptime. Finally, we study mean-payoff parity and mean-penalty parity games as examples of quantitative games. We prove that optimal and epsilon-optimal strategies in mean-payoff parity games have a very homogeneous structure and can can be composed of a linear number of positional strategies. Using this, we derive a strategy machine implementation of polynomial size of optimal and epsilon-optimal strategies. For epsilon-optimal strategies, the latency is moreover logarithmic in epsilon. This bound is optimal. We lift this result to mean-penalty parity games. For this we introduce permissive strategy machines and translate strategies via a reduction that does not allow for the transfer of automaton strategies. This again demonstrates the usefulness of Turing machine representations of strategies.