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.
翻译:在基于(可能无限的)图进行的两人零和无限时长博弈中,一个目标的内存需求是指满足以下条件的最小整数k:在任何由Eve获胜的博弈中,她都能使用一个内存状态数≤k的策略。对于ω-正则目标,检验其内存需求是否等于给定数值k的可判定性此前未知。在本工作中,我们聚焦于BC(Σ₂⁰)类中的目标,即由可能无限的确定性奇偶自动机识别的目标。我们提出了一类能识别内存需求≤k的目标的自动机,并由此得到以下结果:(1)对于ω-正则目标,其在有限与无限博弈中的内存需求一致,且可在NP时间内计算。(2)给定BC(Σ₂⁰)中的两个目标W₁与W₂,并假设W₁具有前缀无关性,则W₁∪W₂的内存需求至多为W₁与W₂内存需求的乘积。我们的结论同样适用于色记忆变体,即策略仅能根据观测到的颜色更新其内存状态的情形。