Constructive Preference Relations: Navigating Undecidability in Rational LTL Contraction

기술 요약: 합리적 LTL 축소에서의 구성적 선호 관계

문제 정의
본 논문은 선형 시제 논리(LTL) 내에서 합리적 믿음 축소(rational belief contraction)를 수행할 때 발생하는 계산적 도전 과제를 다룬다. AGM 믿음 변화 패러다임에서, 축소는 폐기될 믿음을 포기하는 동시에 남은 믿음 집합의 변화를 최소화하는 과정을 포함한다. 이 과정은 가장 그럴듯한 "역-흔적(contra-traces)"(축소하려는 믿음을 만족하지 않는 흔적들)을 선택하기 위해 인식론적 선호 관계에 의존한다. 이러한 관계를 구축하는 것이 고전 논리에서는 대개 사소한 것으로 간주되지만, 저자들은 믿음과 흔적이 뷔키 오토마타(Büchi automata) 및 뷔키-밀리 오토마타(Büchi-Mealy automata, BMA)를 통해 표현되는 LTL에서는 이 작업이 훨씬 더 복잡하다는 것을 입증한다. 구체적으로, 선호 관계가 BMA로 주어졌을 때, 성공적인 축소를 보장하기 위해 요구되는 핵심 조건인 **최대 컷(Maximal Cut)**이 결정 불가능(undecidable)하다는 것을 보여준다.

방법론
저자들은 무한한 흔적(원자 명제들의 시퀀스)에 대한 이진 선호 관계를 표현하기 위해 뷔키-밀리 오토마타 프레임워크를 활용한다. 저자들은 선호 관계가 완전히 합리적인 축소 함수를 유도하는 데 필요한 두 가지 핵심 속성의 결정 가능성을 분석한다:

1. 미러링(Mirroring): 두 흔적이 비교 불가능할 경우, 제3의 흔적에 대한 그들의 선호가 서로를 모방해야 함을 보장하는 구조적 조건.
2. 최대 컷(Maximal Cut): 비항진식(non-tautological formula)에 대하여, 그 식의 역-흔적 집합이 선호 관계 하에서 적어도 하나의 극대 원소(가장 그럴듯한 흔적)를 포함하도록 보장하는 조건.

결정 가능성을 조사하기 위해, 저자들은 오토마타 이론적 기법과 계산 이론의 결정 불가능한 문제, 특히 **선형 유계 오토마타(LBA)의 불멸성 문제(Immortality Problem)**로부터의 환원을 사용한다. 저자들은 LBA의 실행 단계(불멸의 구성 상태의 존재 여부)를 시뮬레이션하는 BMA를 구축하여, 이를 통해 잘-정형성(well-foundedness)과 최대 컷의 실패를 연결한다.

주요 기여 및 결과

1. 미러링의 결정 가능성:
   저자들은 BMA 관계가 미러링 속성을 만족하는지 확인하는 것이 결정 가능하다(구체적으로 ExpTime 내에 가능함)는 것을 증명한다. 이는 관계 연산자(보집합, 역, 합성)를 사용하여 미러링을 대수적으로 특징짓고, 뷔키 오토마타의 폐쇄 성질을 활용함으로써 달성된다.

2. 최대 컷의 결정 불가능성:
   본 논문은 주어진 BMA에 대해 최대 컷 속성을 검증하는 것이 결정 불가능함을 확립한다.

• 이 증명은 LBA 불멸성 문제를 잘-정형성(well-foundedness) 문제로 환원한다.
• 또한, LBA를 시뮬레이션하도록 구축된 특정 관계 클래스에 대해, 잘-정형성과 최대 컷이 일치함을 보여준다.
• 결과적으로, 임의의 BMA가 성공적인 축소를 유도하는지 확인할 수 있는 일반적인 알고리즘은 존재하지 않는다. 이 결과는 완전히 합리적인 LTL 축소를 위한 완전한 구성적 표현 정리(complete constructive representation theorem)가 불가능함을 의미한다; 즉, 모든 유효한 선호 관계를 생성할 수 있는 유한한 구축 시스템은 존재할 수 없다.

3. 랭킹으로서의 합리적 관계 특성화:
   미러링과 최대 컷을 모두 만족하는 BMA 관계는 본질적으로 **랭킹(ranking)**이어야 한다는 중요한 이론적 발견이 있다. 즉, 흔적들은 동일한 선호를 가진 동치류들로 분할되어야 하며, 이 클래스들은 전순서(totally ordered) 관계를 가져야 한다. 이는 고전 논리의 표현 결과를 "컴펜디어스 논리(compendious logics)"와 같은 LTL로 일반화한다.

4. 구성적 선호 관계 군(Families):
   일반적인 검증이 불가능하기 때문에, 저자들은 설계 단계에서부터 미러링과 최대 컷을 보장하는 특정 구성적 랭킹 군을 제안한다. 여기에는 다음이 포함된다:

• 유한 랭크 리스트(Finite Lists of Ranks): 서로 소인 뷔키 오토마타로 정의된 유한 개의 집합들로 흔적을 분할함.
• "빠를수록 좋다(The Sooner, the Better)": 특정 LTL 공식이 성립하는 가장 이른 시점(time point)을 기준으로 흔적의 순위를 매김 (예: 비가 더 빨리 오는 흔적을 선호함).
• 거리 기반 랭킹(Distance-Based Rankings): 시간 단계에 대한 체비쇼프 메트릭(Chebyshev metric)을 사용하여 무한한 흔적에 대한 고전적 거리 측정법(Dalal의 거리 등)을 일반화하고, 지식 베이스로부터의 거리에 따라 흔적의 순위를 매김.
• 계층적 합성(Hierarchical Composition): 여러 랭킹을 사전식(lexicographically)으로 합성하는 방법으로, 복잡하고 다층적인 선호 구조(예: 시간적 긴급성을 먼저 고려한 후 지식 베이스와의 거리를 고려)를 허용함.

의의 및 주장
본 논문은 자신의 결과가 LTL과 같이 표현력이 높고 비유한적(non-finitary)인 논리에서의 합리적 믿음 축소 접근 방식을 근본적으로 변화시킨다고 주장한다. 최대 컷의 결정 불가능성을 증명함으로써, 저자들은 임의의 선호 관계에 대한 자동화된 검증에 의존하여 합리성을 보장할 수 없음을 보여준다. 대신, 분야의 초점이 제안된 구성적 군을 사용하는 **맞춤형 설계(custom design)**로 이동해야 함을 강조한다.

저자들은 자신의 구성적 접근 방식이 효과적인 LTL 축소를 가능하게 할 뿐만 아니라, 고전적 설정에서도 더 풍부한 대안을 제공한다고 강조한다. Dalal의 거리 측정법이 고전 논리의 알려진 합리적 생성자이지만, 자신들의 프레임워크는 이를 일반화하며, 기존의 방법들(예: 유책성(culpability) 측정법)이 불일치하는 믿음에 국한되었던 한계를 극복하여 완전한 합리성을 달성하는 새롭고 더 풍부한 관계 군을 제공한다고 언급한다.

논문은 미러링과 최대 컷의 결합(conjunction)(미러링이 성립한다고 가정할 때)에 대한 결정 불가능성을 증명하지는 못했으나, 결정 불가능성이 지속될 것이라는 강력한 징후가 있음을 언급하며 겸허하게 결론을 맺는다. 저자들은 이 특정 교차점에 대한 완전한 해결을 향후 연구 과제로 남겨둔다.