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

기술적 요약: $\omega$-정규 및 $BC(\Sigma^0_2)$ 목적 함수의 메모리

문제 정의
(잠재적으로 무한한) 그래프 상의 2인 제로섬 무한 지속 게임의 맥락에서, 목적 함수 $W$의 **메모리(memory)**는 Eve가 승리 전략을 가질 때, 그녀가 최대 $k$개의 메모리 상태를 가진 유한 오토마타에 의해 구현 가능한 승리 전략을 보유한다는 조건에 대한 최소 정수 $k$로 정의된다. $\omega$-정규 목적 함수의 위치성(positionality, 메모리 $k=1$)에 대한 결정 가능성은 최근 확립되었으나, 메모리 $k$를 결정하는 일반적인 문제는 미해결 상태로 남아 있었다. 구체적으로, 메모리 계산이 결정 가능한지 여부뿐만 아니라, 유한 게임 그래프에서의 메모리가 임의의 무한 그래프에서의 메모리와 일치하는지 여부도 알려져 있지 않았다. 또한, 메모리를 요구하는 목적 함수의 합집합에 따른 메모리의 거동(일반화된 Kopczyński 추측) 역시 미해결 문제였다.

방법론
저자들은 $k$-wise $\varepsilon$-completable 오토마타에 기반한 메모리 $\le k$인 목적 함수의 새로운 특징화를 도입한다. 이 접근 방식은 위치성(positionality)을 위해 이전에 사용되었던 유니버설 그래프(universal graphs)와 $\varepsilon$-completable 오토마타의 개념을 유한 메모리 설정으로 확장한 것이다.

1. $k$-wise $\varepsilon$-completable 오토마타: 오토마톤이 $k$-wise $\varepsilon$-complete하다는 것은, 그 상태들($k$개의 메모리 체인으로 분할됨)이 $\varepsilon$-전이를 통해 보강되어, 모든 짝수 우선순위 $x$와 메모리 상태 $m$에 대해, 메모리 $m$을 가진 상태들이 전순서(totally preordered)를 형성하는 구조를 만들 수 있음을 의미한다. 구체적으로, 임의의 상태 쌍 $(q, m)$과 $(q', m)$에 대해, $x$라는 우선순위를 가진 $q$에서 $q'$로의 $\varepsilon$-전이가 존재하거나, $x+1$이라는 우선순위를 가진 $q'$에서 $q$로의 전이가 존재한다.
2. 추출 렘마 (Extraction Lemmas): 핵심적인 기술적 혁신은 무한 또는 거대한 유한 그래프로부터 동형 부분 구조(homogeneous substructures)를 추출하는 것이다.
   • 무한의 경우 (섹션 3.1): 저자들은 유니버설 그래프 $S_\kappa^d$ (여기서 $\kappa = 2^{\aleph_0}$)로부터 "어디서나 코파이널(everywhere cofinal)"한 트리(tree)를 추출하기 위해 조합론적 렘마(Lemma 12)를 사용하며, 이를 통해 레벨 간의 지배 관계(domination relations)가 균일하게 유지되도록 한다.
   • 유한의 경우 (섹션 3.2): 저자들은 유한 오토마타에 이러한 추출 기법을 적응시키며, 유한 분기(finite branching)를 처리하고 $\varepsilon$-completable인 $k$-blowup의 존재를 보장하기 위해 "정규 단어(regular words)"와 동기화된 부분 단어(synchronised subwords)를 활용한다 (Lemma 24).
3. 캐스케이드 곱 (Cascade Products): 증명은 가능한 모든 수용 동작을 인코딩하기 위해 유니버설 그래프(또는 시그니처 트리)와 결정론적 오토마타의 캐스케이드 곱을 사용하는 과정과, 언어를 보존하면서 $\varepsilon$-완전성 조건을 만족하는 $k$-blowup을 구성하는 과정에 크게 의존한다.

주요 기여 및 결과

1. 특징화 정리 (Theorem 7): 본 논문은 ($BC(\Sigma^0_2)$ 목적 함수(잠재적으로 무한한 결정론적 패리티 오토마타에 의해 인식되는)가) 메모리 $\le k$를 갖기 위한 필요충분조건을 확립한다. 다음은 동치이다:

   • 해당 목적 함수가 크기가 $\le 2^{2^{\aleph_0}}$인 게임에서 메모리 $\le k$를 갖는다.
   • 목적 함수를 인식하는 모든 오토마타는 $k$-wise $\varepsilon$-complete한 $k$-blowup을 허용한다.
   • 목적 함수를 인식하면서 $k$-wise $\varepsilon$-completable한 결정론적 $k$-오토마톤이 존재한다.
   • 모든 카디널 $\kappa$에 대해, well-founded하고 $k$-wise $\varepsilon$-complete한 $(\kappa, W)$-유니버설 그래프가 존재한다.
   • 해당 목적 함수는 임의의 게임에서 메모리 $\le k$를 갖는다.

2. NP에서의 결정 가능성 (Corollary 9): $\omega$-정규 목적 함수(유한 오토마타)의 경우, 메모리(및 크로매틱 메모리)는 NP 내에서 계산될 수 있다. 알고리즘은 후보 메모리 크기 $k$, 크기가 $\le kn$인 결정론적 오토마타, 그리고 $\varepsilon$-완성을 가정(guess)한 후, 다항 시간 내에 언어 포함 관계를 검증한다. 이 연구 이전에는 오픈(open) $\omega$-정규 목적 함수의 메모리에 대한 결정 가능성이 알려져 있지 않았다.

3. 유한-무한 리프트 (Corollary 8): 본 논문은 $\omega$-정규 목적 함수의 경우, 유한 게임 그래프에서 요구되는 메모리가 임의의 (무한) 게임 그래프에서 요구되는 메모리와 동일함을 증명한다. 이는 $\omega$-정규 케이스에 대한 Vandenhove의 추측을 해결한다.

4. 합집합에 대한 폐쇄성 (Theorem 10): 저자들은 $BC(\Sigma^0_2)$ 목적 함수에 대한 일반화된 Kopczyński 추측의 강한 형태를 증명한다. 만약 $W_1$과 $W_2$가 각각 메모리 $k_1$과 $k_2$를 갖는 목적 함수이고, $W_2$가 접두사 증가(prefix-increasing) 성질을 갖는다면, $W_1 \cup W_2$의 메모리는 최대 $k_1 \cdot k_2$이다. 이 경계값은 타이트(tight)함이 입증되었다.

5. 크로매틱 메모리 (Chromatic Memory): 모든 결과는 전략이 엣지 자체보다는 관찰된 엣지의 색상에 기반하여 메모리 상태를 업데이트하는 크로매틱 메모리에도 동일하게 적용된다.

의의 및 주장
본 논문은 기존의 제한된 클래스(Muller 또는 closed 목적 함수 등)를 넘어 $\omega$-정규 목적 함수의 (크로매틱) 메모리에 대한 최초의 특징화를 제공한다고 주장한다. 메모리 계산이 NP에 속함을 확립함으로써, 이 문제를 미해결 결정 가능성 문제에서 다룰 수 있는 복잡도 클래스로 전환하였다. 저자들은 추출 렘마(extraction lemma)를 사용하는 증명 기법이 위치성(positionality) 연구(연속적인 오토마타 변환에 의존함)와는 구별되며, 현저히 짧다는 점을 강조한다.

이 결과는 메모리 분석의 범위를 에너지(energy) 및 평균 페이오프(mean-payoff) 게임과 같이 비$\omega$-정규 목적 함수 및 $\omega$-Turing 머신에 의해 인식되는 언어를 포함하는 더 넓은 $BC(\Sigma^0_2)$ 클래스로 확장한다. 본 논문은 $\omega$-정규 목적 함수에 대해 유한-무한 리프트를 복구하지만, 메모리 $k > 1$에 대해서는 비대칭 리프트(asymmetric lift)가 존재하지 않는 반례가 있으므로 이를 복구하지 못함을 명시적으로 밝힌다.

한계 및 미해결 과제
저자들은 NP 내에서 결정 가능성을 확립했으나, 정확한 복잡도(특히 P에 속하는지 여부)는 여전히 열려 있다고 인정한다. 또한, 추출 렘마를 일반화하는 데 어려움이 있어 현재 방법론이 $\Delta^0_3$ 클래스까지 확장되지 못함을 언급한다. $\omega$-정규 목적 함수의 크로매틱 메모리에 대해 비대칭 리프트가 존재하는지에 대한 질문은 여전히 남아 있다.