The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete

기술 요약: 그래프 루프를 포함한 관계적 클레이니 대수의 등식 이론은 PSPACE-완전이다

문제 정의
본 논문은 그래프 루프 연산자(이하 $\cdot^\circlearrowleft$ 또는 fixset로 표기)가 확장된 관계적 클레이니 대수(Relational Kleene Algebra, RKA)의 등식 이론에 대한 계산 복잡도를 다룬다. 그래프 루프 연산자는 이진 관계를 항등 관계(즉, $R^\circlearrowleft = R \cap \Delta_X$)로 제한한다. 표준 RKA의 등식 이론은 PSpace-complete로 알려져 있고, 교집합(intersection)이 추가된 확장은 ExpSpace-complete이지만, 그래프 루프 연산자가 포함된 loop-RKA의 복잡도는 미해결 상태로 남아 있었다. 이전 연구들은 이 문제가 PSpace-hard이며 ExpTime에 속한다는 것을 입증했으나, 정확한 상한(upper bound)은 알려지지 않았다. 또한, 도메인(domain) 연산자($\cdot^d$)가 포함된 RKA의 복계 문제 역시, 안티도메인(antidomain, $\cdot^a$)이 포함된 RKA 이론이 ExpTime-complete임에도 불구하고 미해결 상태였다.

방법론
이러한 복잡도 문제를 해결하기 위해, 저자는 새로운 오토마타 모델인 **루프-오토마타(loop-automata)**를 도입한다. 이는 비결정적 유한 오토마타를 확장한 것으로, 현재 그래프 구조의 정점이 루프(즉, 자기 자신으로 향하는 에지)를 가지고 있는지 여부를 테스트하는 특정 전이 유형을 갖는다.

핵심적인 기술적 접근 방식은 다음 단계들을 포함한다:

1. 루프-오토마타 구성: 저자는 모든 loop-RKA 항(term)이 맥노턴-야마다-톰슨(McNaughton–Yamada–Thompson) 구성을 확장하여 동등한 루프-오토마타로 선형 시간 내에 변환될 수 있음을 보여준다.
2. 경로 폭(Pathwidth) 및 분해(Decomposition): 관련 논리들에 대해 확립된 "선형적으로 유계된 경로 폭 모델 속성(linearly bounded pathwidth model property)"을 활용하여, 입력 항의 크기에 의해 선형적으로 유계된 경로 폭을 가진 구조로 반례 모델의 탐색 공간을 제한한다. 유계된 폭을 가진 구조의 경로 분해는 문자열로 취급된다.
3. 2AFA로의 환원: loop-오토마타의 언어 포함(language inclusion) 문제를 **2-way 교대 유한 문자열 오토마타(2-way alternating finite string automata, 2AFA)**의 언어 포함 문제로 환원하는 과정을 구축한다. 이는 경로 분해를 문자열으로 인코딩하고, 루프-오토마타의 동작(루프 테스트 전이 포함)을 2AFA 프레임워크 내에서 시뮬레이션함으로써 달성된다.
4. 이진 인코딩(Binary Encoding): 환원이 PSpace 내에 머물도록 하기 위해, 저자는 그래프 구조(경로 분해의 bag들)의 이진 인코딩을 채택한다. 이는 구조를 원자적 기호로 취급할 때 발생할 수 있는 알파벳 크기의 지수적 팽창을 방방지하며, 이는 교집합 너비가 고정되지 않은 RKA를 위한 이전 알고리즘들과 차별화되는 결정적인 정교화 작업이다.
5. 추가 연산자로의 확장: 오토마타 구성은 top($\top$), 테스트(KAT의 경우처럼), 역(converse), 그리고 노미널(nominals)을 처리할 수 있도록 적응된다. 각 확장에 대해, 구조에 대한 특정 제약 조건(예: 테스트를 위한 항등의 분할, 역를 위한 대칭성 강제)은 보조 2AFA에 의해 거부되는 정규 언어로 인코딩된다.

주요 기여 및 결과
본 논문은 다음과 같은 주요 결과를 확립한다:

• 정리 1: loop-RKA의 등식 이론은 PSpace-complete이다. 이는 기존에 알려진 PSpace-hard/ExpTime 경계 사이의 간극을 좁힘으로써 loop-RKA의 복잡도 문제를 해결한다.
• 정리 2: top, 테스트, 역, 노미널이 확장된 loop-RKA의 등식 이론 또한 PSpace-complete이다.
• 따름정리 3: 직접적인 응용으로서, 도메인(및 범위/range) 연산자가 확장된 관계적 클레이니 테스트(RKAT)의 등식 이론은 PSpace-complete이다. 이는 RKAT의 도메인 복잡도에 관한 특정 미해결 문제(McLean [21, Problem 7.3] 및 Sedlár [36, p. 16])를 해결한다.

본 논문은 중요한 차이점을 언급한다: RKA에 안티도메인을 추가하면 복잡도가 ExpTime-complete로 증가하는 반면, 도메인(그래프 루프와 top을 사용하여 인코딩 가능)을 추가하는 것은 PSpace 상한을 유지한다.

의의
본 논문은 세 가지 주요 영역에서 그 의의를 주장한다:

1. 복잡도 해결: loop-RKA 및 도메인이 포함된 RKAT의 등식 이론이 PSpace-complete임을 증명하여 복잡도를 확정적으로 규명하였다. 이는 RKAT의 안티도메인 포함 시의 ExpTime-completeness 및 일반적인 교집합이 포함된 RKA의 ExpSpace-completeness와 대조된다.
2. 알고리즘 혁신: 루프-오토마타의 도입은 루프 제약이 있는 관계적 구조를 추론하기 위한 새로운 의미론적 도구를 제공한다. 경로 분해를 통한 2AFA로의 환원은, 교집합 너비가 고정되지 않았을 때 이전 방법들(예: PCoR*를 위한 방법)이 ExpSpace를 요구했던 것과 달리 PSpace 상한을 달성하는 정교한 알고리즘적 접근을 제공한다.
3. 논리적 연결: 본 결과는 loop-RKA와 명제 동적 논리(PDL) 사이의 관계를 명확히 한다. loop-PDL은 ExpTime-complete이지만, loop-RKA의 등식 이론은 PSpace-complete로 엄격히 더 쉬우며, 이는 방정식을 제한했을 때 논리와 그 대수적 대응물 사이의 복잡도 차이를 보여준다. 또한, 본 결과는 도메인 및 범위를 포함하는 부적절성 삼중항(incorrectness triples)의 타당성에 대한 직접적인 PSpace 상한을 제공하며, 이는 부적절성 논리(incorrectness logic)와 관련이 있다.

저자는 이 접근 방식이 선형적으로 유계된 경로 폭 모델 속성에 의존하며, 구조의 이진 인코딩이 특히 교집합 너비가 고정되지 않은 경우 PSpace 상한을 유지하는 데 매우 중요하다는 점을 강조한다. 마지막으로, loop-RKA의 유한 공리계(finite axiomatizability) 여부는 여전히 미해결 과제로 남아 있다고 밝히며 논문을 마친다.