Speaker: Pierre Vandenhove
Tuesday, 14 Mars 2023, 14:00, 1Z77
Abstract: In this seminar, I will present the results obtained as part of my PhD thesis cosupervised by Patricia Bouyer at LMF and Mickael Randour at Université de Mons (Belgium). This seminar precedes my thesis defense which will take place in Mons in April. I include here a short abstract; more details are available at my website.
We study zero-sum turn-based games on graphs. Such games can be used to model the interaction between a computer system and its environment, assumed to be antagonistic. The synthesis problem consists in automatically building a controller for the system that guarantees a given objective no matter what happens in the environment, that is, a winning strategy in the derived game.
A crucial question in this endeavor is the complexity of strategies. A standard measure of complexity is the amount of memory needed to implement winning strategies for a given objective; 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. 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 characterize a variant of finite-memory determinacy through properties of objectives in multiple contexts. 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 zero-sum games. Second, we identify natural classes of objectives for which precise memory requirements are not fully understood. We effectively characterize memory requirements of two subclasses of the omega-regular objectives and study the related decision problems. These results complement seminal results about memory requirements of classes of omega-regular objectives.