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(Sigma0^2)类目标(即由潜在无限确定奇偶性自动机识别的语言),提出了一类可识别记忆不超过k的自动机,并得到以下结论:(1) 对ω-正则目标而言,有限博弈与无限博弈的记忆结果一致,且可在NP复杂度内计算;(2) 给定两个同属BC(Sigma0^2)的目标W1与W2,若W1满足前缀独立性,则W1∪W2的记忆不超过W1与W2记忆的乘积。本文结论同样适用于色记忆变体——该变体中策略仅能根据观测到的颜色更新记忆状态。