Verification Series

Strategy Complexity of Zero-Sum Games on Graphs

3rd July 2023, 11:00 add to calender
Pierre Vandenhove
LaBRI, Universite de Bordeaux

Abstract

We consider zero-sum turn-based games on graphs, which can be used to model the interaction between a computer system and its environment, assumed to be antagonistic. A crucial question in this framework is the complexity of strategies. A standard measure of strategy 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 talk, we review recent works on this topic. First, we show characterizations of a variant of finite-memory determinacy in multiple contexts. In particular, we show that understanding the memory requirements in one-player games (i.e., the simpler situation of games where the same player controls all the actions) leads to bounds on memory requirements in two-player zero-sum games. We also show a strong link between finite-memory determinacy and omega-regularity. Second, we show effective characterizations of the precise memory requirements of subclasses of the omega-regular objectives and discuss the related decision problems. We discuss that, perhaps surprisingly, the memory requirements of omega-regular objectives are not completely settled.
add to calender (including abstract)