Strategy Complexity of Zero-Sum Games on Graphs

My PhD thesis is entitled Strategy Complexity of Zero-Sum Games on Graphs. It was conducted under the joint supervision of Patricia Bouyer (LMF, Université Paris-Saclay, CNRS, ENS Paris-Saclay) and Mickael Randour (Université de Mons). It was funded by the F.R.S.-FNRS Research Fellow project FrontieRS. The jury was composed of Christel Baier (Reviewer), Véronique Bruyère (President), Thomas Colcombet (Reviewer), Laurent Doyen (Examiner), and Benjamin Monmege (Examiner), as well as my supervisors Patricia Bouyer and Mickael Randour.

• The private defense happened on April 20, 2023 at the Université de Mons in the sole presence of the jury [slides].
• The public defense (intended to be a less technical and more accessible presentation) happened at the University of Mons (Room Vésale 30) on Wednesday, April 26, 2023 at 4 pm [slides].
• The manuscript is accessible here.

A public seminar about my thesis was also organized on March 14, 2023 at Laboratoire Méthodes Formelles, Université Paris-Saclay [slides].

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.