Search

We study two-player zero-sum turn-based games on graphs, a framework of choice in theoretical computer science. Such games model the possibly infinite interaction between a computer system (often called reactive) and its environment. The system, seen as a player, wants to guarantee a specification (translated to a game objective) based on the interaction; its environment is seen as an antagonistic opponent. The aim is to automatically synthesize a controller for the system that guarantees the specification no matter what happens in the environment, that is, a winning strategy in the derived game.A crucial question in this synthesis quest is the complexity of strategies: when winning strategies exist for a game objective, how simple can they be, and how complex must they be? A standard measure of strategy complexity is the amount of memory needed to implement winning strategies for a given game objective. In other words, how much information should be remembered about the past to make optimal decisions about the future? Proving the existence of bounds on memory requirements has historically had a significant impact. Such bounds were, for instance, used to show the decidability of monadic second-order theories, and they are at the core of state-of-the-art synthesis algorithms. Particularly relevant are the finite-memory-determined objectives (for which winning strategies can be implemented with finite memory), as they allow for implementable controllers. In this thesis, we seek to further the understanding of finite-memory determinacy. We divide our contributions into two axes.First, we introduce arena-independent finite-memory determinacy, describing the objectives for which a single automatic memory structure suffices to implement winning strategies in all games. We characterize this property through language-theoretic and algebraic properties of objectives in multiple contexts (games played on finite or infinite graphs). We show in particular that understanding the memory requirements in one-player game graphs (i.e., the simpler situation of games where the same player controls all the actions) usually leads to bounds on memory requirements in two-player zero-sum games. We also show that if we consider games played on infinite game graphs, the arena-independent-finite-memory-determined objectives are exactly the omega-regular objectives, providing a converse to the landmark result on finite-memory determinacy of omega-regular objectives. These results generalize previous works about the class of objectives requiring no memory to implement winning strategies.Second, we identify natural classes of objectives for which precise memory requirements are surprisingly not fully understood. We introduce regular objectives (a subclass of the omega-regular objectives), which are simple objectives derived from regular languages. We effectively characterize their memory requirements for each player, and we study the computational complexity of deciding the existence of a small memory structure. We then move a step up in the complexity of the objectives and consider objectives definable with deterministic Büchi automata. We characterize the ones for which the first player needs no memory to implement winning strategies (a property called half-positionality). Thanks to this characterization, we show that half-positionality is decidable in polynomial time for this class of objectives. These results complement seminal results about memory requirements of classes of omega-regular objectives.; Les jeux sur graphes à deux joueurs et à somme nulle constituent un modèle central en informatique théorique. De tels jeux modélisent une interaction potentiellement infinie entre un système dit réactif et son environnement. Le système est considéré comme un joueur et souhaite garantir une spécification (traduite en un objectif de jeu). Son environnement est considéré comme un joueur antagoniste. Le but est de synthétiser automatiquement un contrôleur pour le système qui garantit la spécification peu importe le comportement de l'environnement, ce qui correspond à construire une stratégie gagnante dans le jeu dérivé.Une question cruciale dans cette problématique de synthèse est celle de la complexité des stratégies : si des stratégies gagnantes existent, à quel point peuvent-elles être simples et à quel point doivent-elles être complexes ? Une mesure standard de complexité des stratégies est la quantité de mémoire nécessaire pour implémenter des stratégies gagnantes pour un objectif donné. En d'autres termes, quelle quantité d'information faut-il retenir au sujet du passé pour prendre des décisions optimales concernant le futur ? Des preuves de l'existence de bornes sur les besoins en mémoire ont historiquement eu un impact important. Par exemple, de telles bornes ont mené à des preuves de décidabilité de théories monadiques du second ordre, et sont au cœur de nombreux algorithmes efficaces pour la synthèse. Les objectifs déterminés à mémoire finie (c'est-à-dire ceux qui admettent des stratégies gagnantes se limitant à une mémoire finie) sont particulièrement pertinents, car ils mènent à l'existence de contrôleurs pouvant être implémentés en pratique. Dans cette thèse, nous cherchons à améliorer la compréhension de la détermination à mémoire finie. Nous distinguons deux axes dans nos contributions.Premièrement, nous introduisons le concept de détermination à mémoire finie indépendante de l'arène, qui décrit les objectifs pour lesquels une unique structure automatique de mémoire suffit pour implémenter des stratégies gagnantes dans tous les jeux. Nous caractérisons cette propriété via des propriétés algébriques et de langages dans différents contextes (jeux joués sur des graphes finis ou infinis). Nous montrons en particulier que la compréhension des besoins en mémoire dans les jeux à un joueur (c'est-à-dire les jeux plus simples dans lesquels le même joueur contrôle toutes les actions) mène généralement à des bornes sur les besoins en mémoire dans les jeux à deux joueurs et à somme nulle. Nous montrons également que si l'on considère les jeux joués sur des graphes infinis, les objectifs déterminés à mémoire finie indépendante de l'arène sont exactement les objectifs oméga-réguliers, ce qui fournit une réciproque au célèbre théorème de détermination à mémoire finie de ces objectifs. Ces résultats généralisent des travaux précédents au sujet des objectifs pour lesquels aucune mémoire n'est nécessaire pour les stratégies gagnantes.Deuxièmement, nous identifions des classes naturelles d'objectifs pour lesquels les besoins en mémoire ne sont pas complètement établis. Nous introduisons les objectifs réguliers (une sous-classe des oméga-réguliers), qui sont des objectifs dérivés de langages réguliers. Nous donnons une caractérisation effective des besoins en mémoire de ces objectifs pour chacun des joueurs, et nous étudions la complexité de décider de l'existence d'une petite structure de mémoire. Nous considérons ensuite des objectifs plus complexes définissables avec des automates de Büchi déterministes. Nous caractérisons ceux pour lesquels le premier joueur n'a besoin d'aucune mémoire pour implémenter des stratégies gagnantes (une propriété appelée semi-positionnalité). Grâce à cette caractérisation, nous montrons que la semi-positionnalité est décidable en temps polynomial pour ces objectifs. Ces résultats complètent des travaux fondateurs sur les besoins en mémoire des objectifs oméga-réguliers.