A Bisimulation-Invariance-Based Approach to the Separation of Polynomial Complexity Classes

기술 요약: 다항 시간 복잡도 클래스 분리를 위한 비심뮬레이션 불변성 기반 접근법

1. 문제 정의
본 논문은 $P = NP$(그리고 더 나아가$P = PSPACE$)인지에 관한 근본적인 미해결 문제를 다룬다. 기술 복잡도 이론(descriptive complexity theory)은 논리적 형식주의(예: $NP = \exists SO$, $PSPACE = FO + PFP$)를 사용하여$NP$, $PSPACE$, $ExpTime$와 같은 복잡도 클래스를 성공적으로 특징지어 왔으나, 일반적이고 순서가 없는 구조(unordered structures)에 대한 $P$의 특징화는 여전히 난제로 남아 있다. 이는 "순서 문제(order problem)"로 알려져 있는데, $P$에 속하는 계산 문제들의 논리적 특징화는 대개 입력 구조에 대한 명시적인 전순서(total order)를 요구하지만, $P$ 내의 계산 문제들은 본질적으로 그러한 순서를 가지고 있지 않기 때문이다.

저자들은 비심뮬레이션 불변 분절(bisimulation-invariant fragments)인 복잡도 클래스들($P/\sim$ 대 $NP/\sim$ 및 $P/\sim$ 대 $PSPACE/\sim$)을 분리하는 것이 일반적인 $P=NP$문제를 해결하기 위한 실행 가능한 경로가 될 수 있는지 조사한다. 저자들은 만약 해당 클래스들이 비심뮬레이션 불변인 어려운 문제들을 포함하고 있다면,$P \neq NP$를 증명하는 것이$P/\sim \neq NP/\sim$를 증명하는 것과 동치라고 상정한다.

2. 방법론 및 이론적 프레임워크
본 논문은 문헌의 두 가지 확립된 결과에 기초한다:

1. Otto의 정리 [28]: 다항 시간 내에 계산 가능한 비심뮬레이션 불변 쿼리(bisimulation-invariant queries)의 클래스는 폴리아딕 $\mu$-계산법($L^\omega_\mu$)에 의해 정확히 포착된다.
2. 모델 체킹 환원 [4, 23]: 폴리아딕 $\mu$-계산법의 모델 체킹 문제는 "파워 그래프(power graphs)"라고 알려진 특정 곱 연산을 통해 일반적인(단항의) $\mu$-계산법($L_\mu$)으로 환원될 수 있다.

저자들은 이를 결합하여 **상대적 정규성(relative regularity)**에 기반한 프레임워크를 개발한다:

• 트리 언어로의 환원: 그래프와 그 트리 언폴딩(tree unfoldings)은 비심뮬레이션 관계에 있으므로, 비심뮬레이션 불변 논리에서의 정의 가능성은 트리 언어의 정의 가능성으로 환원된다.
• 파워 그래프: 그래프 $G$에 대하여, $G^d$는 $d$개의 $G$의 비동기적 곱(asynchronous product)이며, 구성 요소를 루트로 되돌리는 "리셋(reset)" 전이(transition)가 추가되어 있다.
• 모노피케이션(Monofication): 구문적 변환을 통해 폴리아딕 $\mu$-계산법의 공식(그래프 $G$ 위에서)을 $G^d$ 위의 일반적인 $\mu$-계산법 공식으로 변환한다.
• 상대적 정규성: 트리 언어 $L$이 컨텍스트 언어 $R$에 대해 *상대적으로 정규(regular relative to)*라는 것은, $L$의 원소와 비원소를 $R$ 내에서 올바르게 구별하는 $L_\mu$ 공식이 존재하며, $R$ 외부의 트리에 대해서는 임의의 주장을 할 수 있음을 의미한다.

3. 주요 기여 및 특징화
본 논문은 복잡도 클래스의 분리가 특정 트리 언어들의 **상대적 비정규성(relative non-regularity)**을 증명하는 문제로 환원됨을 입증한다.

• 분리의 동치성 (정리 1): 본 논문은 $P = NP$가$P/\sim = NP/\sim$와 동치이며,$PSPACE$의 경우도 마찬가지임을 증명한다. 이는 비심뮬레이션 불변인 어려운 문제들, 구체적으로는 1-문자($1NonUnivNFA$) 및 2-문자($2NonUnivNFA$) 알파벳에 대한 비결정적 유한 오토마타(NFA)의 비보편성(non-universality) 문제를 활용한 것이다.
• 파워 그래프의 특징화 (섹션 4): 저자들은 $d$-파워 그래프와 비심뮬러(bisimilar)한 그래프들에 대한 두 가지 특징화를 제공한다:
  1. 대수적 특징화: "지속성(persistence)"(한 구성 요소에서의 동작이 다른 구성 요소에 영향을 주지 않음)과 "리셋 속성(reset property)"을 만족하는 $d$-차원 비동기 비심뮬레이션(asynchronous bisimulation)을 통해 특징화된다.
  2. 논리적 특징화: 특정 공식들($\phi_{per}, \phi_{rst}, \phi_{pow}$)을 사용하는 이항 $\mu$-계산법($L^2_\mu$)을 통해 정의된다.
• 상대적 펌핑 렘마 (레마 13): 저자들은 정규 트리 언어에 대한 표준 펌핑 렘마를 상대적 정규성의 맥락에 맞게 수정한다. 만약 언어 $L$이 $R$에 대해 정규라면, $L \cap R$에 속하는 임의의 트리에 대하여, 결과 트리가 $R$ 내에 머무르는 한, 경로 세그먼트를 펌핑(pumping)해도 해당 트리가 $L$에 속하게 된다. 이로 인해 비정규성을 증명하는 작업이 훨씬 어려워지는데, 왜냐하면 펌핑이 파워 그래프의 구조적 제약 조건 내로 국한되어야 하기 때문이다.

4. 주요 결과
핵심 결과는 복잡도 분리를 NFA 비보편성 문제로부터 유도된 트리 언어들의 비정규성과 연결한다:

• 정리 26: $P \neq NP$인 것은 모든 $d \ge 1$에 대하여, $1NonUnivNFA_d$ 언어(그래프의 $d$-파워의 트리 언폴딩인 $1NonUnivNFA$의 트리 언어)가$Power_d$(파워 그래프의 트리 언어)에 대해 상대적으로 비정규적인 것과 동치이다.
• 정리 30: $P \neq PSPACE$인 것은 모든 $d \ge 1$에 대하여, $2NonUnivNFA_d$ 언어가 $Power_d$에 대해 상대적으로 비정규적인 것과 동치이다.

저자들은 이러한 언어들을 명시적으로 구축한다. 예를 들어, $1NonUnivNFA_d$는 모든 경로에 대하여, 특정 구성 요소에서의 동작 시퀀스(리셋을 무시할 때)가 결국 수용 색상 $f$가 없는 상태로 이어지는 트리들로 구성된다.

5. 의의 및 주장
본 논문은 $P=NP$ 문제에 대한 해결책이라기보다, 새로운 공격 경로를 제시한다는 점을 겸허히 주장한다. 본 논문의 의의는 다음과 같다:

• 순서 문제 완화: 구조에 대한 전순서를 요구하는 기존의 기술 복잡도 시도들의 주요 장애물을 우회하여, 비심뮬레이션 불변 쿼리에 초점을 맞춤으로써 이를 해결한다.
• 논리적 표현력: 복잡도 클래스의 분리를 특정 파워 그래프에 대한 상대적 논리적 비표현성(즉, 일반적인 $\mu$-계산법이 특정 트리 언어를 정의할 수 없는 능력)의 문제로 재구성한다.
• 실행 가능성 및 과제: 저자들은 이론적 환원은 확립되었으나, 상대적 비정규성을 증명하는 실제 과정은 "높은 조합론적 복잡성"을 수반한다고 인정한다. 표준적인 비정규성 증명만으로는 불충분하며, 파워 그래프의 구조적 특성을 엄격히 보존하는 펌핑 논증을 구축해야 한다고 지적한다.

결론적으로, 비록 이 경로는 험난하지만, 파워 그래프의 특징화(대수적 및 논리적 모두)는 이러한 증명을 시도하기 위한 필수적인 도구를 제공한다. 또한, 다른 주요 복잡도 클래스들과 달리, $NP/\sim$에 대한 논리적 특징화는 현재 알려져 있지 않으며, 이것이 이 비심뮬레이션 불변 접근법을 완전히 활용하는 데 있어 장벽으로 남아 있음을 강조한다.