PhD Defence: Pierre Vandenhove

Apr 26 16:00 ₂₀₂₃

Abstract: 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.

Jury:

• Véronique BRUYÈRE, Professor, Université de Mons (President)
• Christel BAIER, Professor, Technische Universität Dresden (Reviewer)
• Thomas COLCOMBET, Research Director, CNRS, Institut de Recherche en Informatique Fondamentale (Reviewer)
• Laurent DOYEN, Researcher, CNRS, Laboratoire Méthodes Formelles (Examiner)
• Benjamin MONMEGE, Associate Professor, Aix-Marseille Université, Laboratoire d’Informatique & Systèmes (Examiner)
• Patricia BOUYER-DECITRE, Research Director, CNRS, Laboratoire Méthodes Formelles (Supervisor)
• Mickael RANDOUR, Research Associate, F.R.S.-FNRS, Université de Mons (Supervisor)