Abstract EN:

In this thesis, we study games as a tool for the synthesis of controllers for reactive Systems. In this setting, a game is defined by an arena, representing the System and its evolution as a graph; and a winning condition, which models the specification that the controller must ensure In each state, the choice of the outgoing transition is done by either Eve (the controller), Adam (an hostile environment), or Random (uncontrollable evolution obeying a stochastic law). This process is repeated for an infinite number of times, leading to an infinite play whose winner depends on the winning condition. Our first object of study is the simplest case of Computing the optimal values of reachability games. We present a new effective approach, based on permutations of random states, to solve this classical problem. In terms of complexity, the resulting "permutation algorithm" is orthogonal to the classical, strategy-based algorithms: it is exponential in the number of random states, rather than in the number of controlled states. We also present an improvement heuristic for this algorithm, inspired by the "strategy improvement" algorithm. We turn next to a much more general class of problems, covering ail fie cases where the winning condition is prefix-independent. We prove the existence of optimal strategies for these games, and show that our permutation algorithm can be extended into a "meta-algorithm", changing any qualitative algorithm into a quantitative algorithm. Lastly, we study the complexity of optimal strategies for regular winning conditions represented as Muller games, and especially the amount of memory that can be saved by using randomised strategies. Using the Zielonka tree, we show tight bounds on the necessary and sufficient memory needed to define randomised optimal strategies for any single Muller condition.