The memory of $ω$-regular and BC($Σ_2^0$) objectives
For researchers in game theory and automata theory, this work provides decidability and complexity results for memory computation in ω-regular games, which was previously open.
The paper addresses the problem of computing the memory required for winning strategies in infinite-duration games with ω-regular and BC(Σ₂⁰) objectives. It shows that for ω-regular objectives, memory over finite and infinite games coincides and can be computed in NP, and provides a bound on memory for the union of prefix-independent objectives.
In the context of 2-player zero-sum infinite-duration games played on (potentially infinite) graphs, the memory of an objective is the smallest integer k such that in any game won by Eve, she has a strategy with <= k states of memory. For omega-regular objectives, checking whether the memory equals a given number k was not known to be decidable. In this work, we focus on objectives in BC(Sigma0^2), i.e. recognised by a potentially infinite deterministic parity automaton. We provide a class of automata that recognise objectives with memory <= k, leading to the following results: (1) For omega-regular objectives, the memory over finite and infinite games coincides and can be computed in NP. (2) Given two objectives W1 and W2 in BC(Sigma0^2) and assuming W1 is prefix-independent, the memory of W1 U W2 is at most the product of the memories of W1 and W2. Our results also apply to chromatic memory, the variant where strategies can update their memory state only depending on which colour is seen.