Finite Convergence of the Modal Mu-Calculus on Almost-Periodic Words

기술 요약: 준주기적 단어에 대한 모달 $\mu$-calculus의 유한 수렴성

문제 정의
본 논문은 무한 단어 상에서의 선형 시간 모달 $\mu$-calculus ($L_\mu$)에 관한 유한 수렴성(finite convergence) 문제를 다룬다. 어떤 구조(구체적으로는 무한 단어)가 유한 수렴성을 갖는다는 것은, 그 구조 상의 모든 $L_\mu$ 공식이 고정점 정의(fixpoint definitions)의 유한한 언폴딩(unfolding)과 동치임을 의미한다. 궁극적 주기적(ultimately periodic) 단어는 유한 수렴성을 갖는다는 것은 알려져 있으며, 유한 수렴성을 갖는 단어는 반드시 준주기적(almost-periodic)이어야 한다는 점 또한 알려져 있다. 그러나 유한 수렴성을 보이는 단어의 클래스를 정확히 규명하는 것은 미해결 과제로 남아 있었다. 즉, 모든 준주기적 단어가 유한 수렴성을 갖는지, 아니면 고정점 정의를 위해 무한한 언폴딩을 요구하는 준주기적 단어가 존재하는지는 알려지지 않았었다.

방법론
저자들은 유한 수렴성과 무한 단어 상에서의 *자명한 오토마타(trivial automata, TrA)*의 동작 사이의 동치 관계를 확립함으로써 이 문제에 접근한다. 단어가 유한 수렴성을 갖는다는 것은 모든 자명한 오토마타가 해당 단어 상에서 *유계된 실행(bounded runs)*을 갖는 것(즉, 실행이 유한한 단계 내에서 종료되거나, 특정 실행 경로에 따라 무제한으로 늘어나지 않고 영원히 실행됨)과 동치이다.

준주기적 단어가 이 조건을 만족함을 증명하기 위해, 본 논문은 비결정적 유한 오토마타와 정규 표현식($NFA_{reg}$)을 동등한 정규 표현식으로 변환하는 직접적인 증명 전략을 채택한다. 방법론은 다음 단계들에 의존한다:

1. 자명한 오토마타로의 축소: 문제를 임의의 준주기적 단어 $w$에 대해 모든 자명한 오토마타가 $w$ 상에서 유계된 실행을 갖는 것을 보여주는 것으로 축소한다.
2. 오토마타 변환: 저자들은 $NFA_{reg}$를 정규 표현식으로 변환하기 위해 표준적인 변환 과정(상태 제거와 유사한 방식)을 활용한다. 이 과정에서 저자들은 오토마타에 대한 특정 속성들을 도입한다: 최소성(minimality), 선함(goodness) (접두사 자유성 및 전이 언어의 상호 배타성 보장), 그리고 단어 $w$에 대한 단순성(simplicity).
3. 속성 보존: 저자들은 르마(Lemma) 12, 13, 14를 통해 변환 연산(병렬 엣지 병합 및 비 초기/비 최종 상태 제거)이 최소성, 선함, 단순성을 보존함을 증명한다.
4. 조합론적 논증: 핵심적인 기술적 요소는 르마 7이며, 이는 준주기적 단어 $w$와 접두사 자유적인 유한 언어 $L, L'$에 대하여 교집합 $L^*L \cap F(w)$ (여기서 $F(w)$는 $w$의 인자(factor)들의 집합)가 유한함을 확립한다. 이 르마는 자명한 오토마타로부터 유도된 정규 표현식에 적용되어, 오토마타에 의해 수용되는 $w$의 인자 집합이 유한함을 입증함으로써 실행 길이를 제한한다.

주요 기여 및 결과

• 유한 수렴성의 규명: 본 논문은 알려진 함축 관계의 역을 증명한다: 단어가 유한 수렴성을 갖는 것은 그 단어가 준주기적이기 위한 필요충분조건이다. 이는 $L_\mu$가 (유한 근사 측면에서) 교대 없는 파편(alternation-free fragment)으로 붕괴하는 단어의 클래스를 완전히 규명한다.
• 준주기적 단어 상의 유계된 실행: 핵심 결과(정리 15)는 모든 자명한 오토마타가 준주기적 단어 상에서 유계된 실행을 가짐을 보여준다. 이는 복잡한 기존 공식에 의존하지 않고 직접적인 증명을 통해 달성되었다.
• 결정 가능성 재증명: 이 결과는 효과적으로 준주기적인 단어에 대한 $L_\mu$의 결정 가능성에 관한 Semenov(1984)의 결과를 재증명한다. 본 논문은 결정 가능성이 이미 알려져 있었으나, 여기서 제공하는 직접적인 증명이 결과에 이르는 더 명확한 경로를 제공한다고 언급한다.
• $\omega$-정규 표현식의 표준형: 증명 기법은 새로운 표준형 결과(비고 17)를 도출한다. 이는 임의의 $\omega$-정규 표현식 $\sum r_i s_i^\omega$가 원래의 표현식과 준주기적 단어 집합 상에서 일치하는 형태 $r \Sigma^\omega$로 다시 쓰여질 수 있음을 보여준다.

의의 및 주장
본 논문은 이전 연구(특히 [8])에서 남겨진, 유한 수렴성을 갖는 단어의 정확한 성격에 관한 질문을 해결했다고 주장한다. 저자들은 자신들의 기여가 단순히 기존의 결정 가능성 결과를 재진술하는 것이 아니라, 유한 수렴성을 보장하는 구조적 속성(준주기성)에 대한 직접적인 규명임을 강조한다.

그 의의는 다음과 같다:

1. 완전성: 무한 단어 상에서의 유한 수렴성에 대한 필요조건과 충분조건 사이의 간극을 메운다.
2. 단순성: 증명은 "상대적으로 간단하며" "매우 기본적인 도구들"을 사용하며, 이는 기존의 "다루기 힘들거나" "직접적인 유도가 불충분했던" 공식들과 대조된다.
3. 구조적 통찰: 논리적 속성인 유한 수렴성을 조합론적 속성인 준주기성과 직접 연결함으로써, 오토마타의 동작과 단어 구조 사이의 관계를 강화한다.

논문은 결론에서, 본 결과가 무한 단어에 대해 확립되었음을 명시하며, 향후 연구 방향으로 분기 구조로 인해 폐쇄 서수(closure ordinals)의 동작이 달라질 수 있는 양방향 무한 단어 및 무한 트리로의 확장을 제시하며 겸허하게 마무리한다.