The memory of $\omega$-regular and BC($\Sigma_2^0$) objectives

TL;DR

This paper investigates the memory requirements for winning strategies in infinite-duration games with omega-regular and BC(Sigma_2^0) objectives, providing decidability results and bounds on memory size.

Contribution

It introduces automata recognizing objectives with bounded memory and establishes complexity and bounds for memory in these game objectives.

Findings

Memory for omega-regular objectives can be computed in NP.

Memory of combined objectives is at most the product of individual memories.

Results apply to chromatic memory strategies.

Abstract

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.