397.50 라빈 오토마타(Rabin Automaton) 기반 임무 계획

1. 개요

라빈 오토마타(Rabin automaton)는 오메가 오토마타(ω-automata)의 한 유형으로서, 뷔히 오토마타(Büchi automaton)보다 강력한 표현력을 갖는 결정론적 수락 조건을 제공한다. 로봇 임무 계획에서 라빈 오토마타는 LTL(Linear Temporal Logic) 명세를 결정론적 형태로 변환하여 합성(synthesis) 및 제어 정책 도출에 직접 활용할 수 있다는 핵심적 장점을 갖는다.

뷔히 오토마타의 경우, 비결정론적 형태(NBA)는 모든 ω-정규 언어(ω-regular language)를 인식할 수 있으나, 결정론적 형태(DBA)는 이보다 엄밀히 약한 표현력을 가진다. 반면, 결정론적 라빈 오토마타(DRA: Deterministic Rabin Automaton)는 ω-정규 언어의 완전한 클래스를 인식할 수 있으므로, 임의의 LTL 명세를 결정론적 오토마타로 변환할 수 있다. 이러한 결정론성은 게임 기반 합성(game-based synthesis)에서 승리 전략을 직접 추출하는 데 필수적이다.

2. 수학적 정의

2.1 라빈 오토마타의 형식적 정의

결정론적 라빈 오토마타(DRA)는 다음의 5-튜플로 정의된다.

\mathcal{R} = (Q, \Sigma, \delta, q_0, \text{Acc})

여기서 Q는 유한 상태 집합, \Sigma는 유한 입력 알파벳, \delta: Q \times \Sigma \rightarrow Q는 결정론적 전이 함수, q_0 \in Q는 초기 상태이다.

수락 조건 \text{Acc}는 라빈 쌍(Rabin pair)의 집합으로 표현된다:

\text{Acc} = \{(L_1, U_1), (L_2, U_2), \ldots, (L_k, U_k)\}

여기서 각 라빈 쌍 (L_i, U_i)에 대해 L_i \subseteq Q와 U_i \subseteq Q이다. L_i는 회피 집합(lower set 또는 forbidden set)이라 하며, U_i는 방문 집합(upper set 또는 accepting set)이라 한다.

2.2 수락 조건

무한 입력 문자열 w = \sigma_0 \sigma_1 \sigma_2 \ldots \in \Sigma^\omega에 대한 유일한 실행(결정론적이므로) \rho = q_0 q_1 q_2 \ldots가 수락되려면, 적어도 하나의 라빈 쌍 (L_i, U_i)에 대해 다음 두 조건이 동시에 성립해야 한다:

\text{Inf}(\rho) \cap L_i = \emptyset \quad \wedge \quad \text{Inf}(\rho) \cap U_i \neq \emptyset

즉, 회피 집합 L_i의 상태는 유한 횟수만 방문하고(결국 영원히 방문하지 않게 되고), 방문 집합 U_i의 상태는 무한히 자주 방문해야 한다. 이 조건은 “나쁜 상태를 결국 피하면서, 좋은 상태를 무한히 경유한다“는 직관을 형식화한 것이다.

2.3 뷔히 수락 조건과의 관계

뷔히 수락 조건은 라빈 수락 조건의 특수한 경우이다. 단일 라빈 쌍 (\emptyset, F)를 갖는 DRA는 DBA와 동치이다. 따라서 라빈 수락 조건은 뷔히 수락 조건을 일반화한다.

스트리트 수락 조건(Streett acceptance condition)은 라빈 수락 조건의 쌍대(dual)로서, 모든 스트리트 쌍에 대해 조건이 성립할 것을 요구한다:

\forall i \in \{1, \ldots, k\} : \text{Inf}(\rho) \cap L_i = \emptyset \implies \text{Inf}(\rho) \cap U_i \neq \emptyset

라빈 조건이 존재적(existential) 선택을 허용하는 반면, 스트리트 조건은 전칭적(universal) 충족을 요구한다.

3. LTL에서 결정론적 라빈 오토마타로의 변환

3.1 Safra 구성법

비결정론적 뷔히 오토마타(NBA)를 결정론적 라빈 오토마타(DRA)로 변환하는 가장 고전적 방법은 Safra(1988)가 제안한 Safra 구성법(Safra’s construction)이다.

NBA \mathcal{B} = (Q, \Sigma, \delta, Q_0, F)가 주어질 때, Safra 구성법은 다음과 같이 동작한다:

1. Safra 트리(Safra tree) 구조를 상태로 사용한다. 각 Safra 트리 노드는 Q의 부분집합을 레이블로 가지며, 트리의 깊이는 최대 \lvert Q \rvert이다.
2. 트리의 각 노드는 NBA 상태 집합의 추적 정보를 유지하며, 수락 상태 방문 시 새로운 자식 노드를 생성한다.
3. 노드의 레이블이 비어지면 해당 노드를 삭제하고, 자식 노드의 레이블이 부모와 합쳐지면 합병(merge)한다.

Safra 구성법의 결과 DRA는 다음의 복잡도를 갖는다:

• 상태 수: O((2n)^{2n}), 여기서 n = \lvert Q \rvert
• 라빈 쌍 수: O(n)

LTL 공식 \varphi에 대해 NBA의 상태 수가 2^{O(\lvert \varphi \rvert)}이므로, 최종 DRA의 상태 수는 이중 지수적(doubly exponential)이 된다. 이는 LTL 합성의 2EXPTIME 하한과 일치한다.

3.2 개선된 변환 알고리즘

Safra 구성법의 구현 난이도와 상태 폭발 문제를 개선하기 위해 다양한 대안적 알고리즘이 제안되었다:

1. Muller-Schupp 트리 오토마타 기법: 트리 오토마타를 경유하는 2단계 변환으로, 이론적 복잡도는 동일하나 구성의 모듈성이 향상된다.

2. Piterman의 개선된 Safra 구성법: Piterman(2006)은 Safra 트리의 변형인 Safra-Piterman 구성을 통해, 결정론적 파리티 오토마타(DPA)로의 직접 변환을 제안하였다. 이 방법은 상태 수 상한을 O(n! \cdot 2^n)으로 감소시킨다.

3. Esparza, Kretinsky, Sickert의 제한적 결정화: 특정 LTL 단편(fragment)에 대해 지수적 폭발 없이 결정론적 오토마타를 생성하는 기법이 개발되었다. 특히 안전성(safety)과 코뷔히(co-Büchi) 조건에 해당하는 명세에 대해서는 효율적 변환이 가능하다.

4. 라빈 게임과 임무 계획

4.1 라빈 게임의 정의

라빈 오토마타 기반 임무 계획에서, 로봇(시스템)과 환경 사이의 상호작용은 라빈 게임(Rabin game)으로 모델링된다. 2인 라빈 게임은 다음과 같이 정의된다:

\mathcal{G} = (V_0, V_1, E, v_0, \text{Acc})

여기서 V_0은 환경(player 0)의 꼭짓점 집합, V_1은 시스템(player 1)의 꼭짓점 집합, E는 간선 집합, v_0는 초기 꼭짓점, \text{Acc} = \{(L_1, U_1), \ldots, (L_k, U_k)\}는 라빈 수락 조건이다.

시스템이 라빈 게임에서 승리하려면, 환경의 임의의 전략에 대해 결과적 무한 경로가 라빈 수락 조건을 만족하는 시스템 전략이 존재해야 한다.

4.2 라빈 게임의 해법

라빈 게임의 승리 영역(winning region)과 승리 전략은 다음의 알고리즘을 통해 계산된다.

Zielonka 알고리즘(Zielonka’s algorithm): 이 알고리즘은 라빈 쌍에 대한 재귀적 분해를 통해 승리 영역을 계산한다. 각 라빈 쌍 (L_i, U_i)에 대해:

1. U_i에 속하는 꼭짓점을 무한히 자주 방문할 수 있는 유인 집합(attractor)을 계산한다.
2. L_i에 속하는 꼭짓점을 결국 영원히 회피할 수 있는지 검사한다.
3. 나머지 부분-게임(sub-game)에 대해 재귀적으로 문제를 해결한다.

라빈 게임의 시간 복잡도는 O(m \cdot n^{k+1} \cdot k!)이다. 여기서 m은 간선 수, n은 꼭짓점 수, k는 라빈 쌍의 수이다.

4.3 승리 전략의 메모리 요구량

라빈 게임에서 시스템의 승리 전략은 메모리(memory)를 필요로 한다. k개의 라빈 쌍을 가지는 라빈 게임에서, 승리 전략의 메모리 상한은 O(n \cdot k!)이다. 이는 뷔히 게임에서의 무기억(memoryless) 전략과 대비되는 특성이며, 도출된 제어기의 상태 수가 증가함을 의미한다.

5. 제품 라빈 오토마톤의 구성

5.1 전이 시스템과 DRA의 곱

로봇의 전이 시스템 \mathcal{T} = (S, s_0, \delta_T, AP, L)과 결정론적 라빈 오토마타 \mathcal{R} = (Q, 2^{AP}, \delta_R, q_0, \text{Acc})의 제품 오토마톤은 다음과 같이 구성된다:

\mathcal{P}_R = \mathcal{T} \otimes \mathcal{R} = (S \times Q, (s_0, q_0), \delta_{P_R}, \text{Acc}_P)

전이 관계는 다음과 같다:

(s, q) \xrightarrow{\delta_{P_R}} (s', q') \iff (s, s') \in \delta_T \wedge q' = \delta_R(q, L(s'))

DRA의 결정론성에 의해 각 전이에 대해 유일한 후속 명세 상태 q'가 결정되므로, 제품 오토마톤 역시 결정론적이다.

수락 조건은 다음과 같이 승격(lifting)된다:

\text{Acc}_P = \{(S \times L_i, S \times U_i) \mid (L_i, U_i) \in \text{Acc}\}

5.2 결정론적 제품의 장점

DRA 기반 제품 오토마톤의 핵심적 장점은 결정론성이 보장된다는 것이다. 비결정론적 뷔히 제품과 비교할 때:

• 유일한 실행: 각 로봇 행동 시퀀스에 대해 정확히 하나의 제품 실행이 존재하므로, 명세 만족 여부의 판정이 직접적이다.
• 전략 추출 용이성: 게임 해석 시 환경의 각 행동에 대해 시스템의 응답이 유일하게 결정되므로, 승리 전략에서 제어 정책으로의 변환이 간명하다.
• 온라인 모니터링 가능: 실행 중 현재 명세 상태를 유일하게 추적할 수 있어, 실시간 임무 진행 상황 모니터링이 가능하다.

6. 수락 경로 탐색 알고리즘

6.1 SCC 기반 분석

제품 라빈 오토마톤 \mathcal{P}_R 위에서의 수락 경로 존재 판정은 강연결 성분(SCC) 분석을 통해 수행된다. 도달 가능한 SCC C가 수락 SCC(accepting SCC)가 되려면, 적어도 하나의 라빈 쌍 (L_i, U_i)에 대해 다음을 만족해야 한다:

C \cap L_i = \emptyset \quad \wedge \quad C \cap U_i \neq \emptyset

즉, SCC 내에 회피 집합의 상태가 없으면서 방문 집합의 상태가 존재해야 한다.

알고리즘:

1. Tarjan 알고리즘으로 도달 가능 SCC를 식별한다.
2. 각 SCC에 대해 모든 라빈 쌍을 검사하여 수락 조건 충족 여부를 판정한다.
3. 초기 상태에서 수락 SCC에 도달 가능하면 수락 경로가 존재한다.

시간 복잡도는 O(k \cdot (\lvert S_P \rvert + \lvert \delta_P \rvert))이다.

6.2 최적 경로 탐색

최적 래소 경로의 탐색은 뷔히 경우와 유사하게, 최적 접두사와 최적 주기를 결합하는 2-Dijkstra 방법으로 수행된다. 다만, 라빈 수락 조건에서는 주기 부분이 특정 라빈 쌍의 회피 집합을 경유하지 않으면서 방문 집합을 포함해야 하므로, 탐색 공간에 추가적 제약이 부과된다.

7. 확률적 모델과의 결합

7.1 MDP 위의 라빈 수락 조건

마르코프 결정 과정(MDP) \mathcal{M}과 DRA \mathcal{R}의 제품 MDP에서, 라빈 수락 조건을 최대 확률로 만족하는 정책을 계산하는 문제는 다항 시간 내에 해결 가능하다.

제품 MDP의 하단 SCC 분석을 통해, 각 하단 SCC가 수락 조건을 만족하는지 판정하고, 수락 하단 SCC에 도달하는 최대 확률을 선형 계획법(LP)으로 계산한다.

\max_{\pi} \Pr^{\pi}_{\mathcal{M} \otimes \mathcal{R}} \left[ \exists i : \text{Inf}(\rho) \cap L_i = \emptyset \wedge \text{Inf}(\rho) \cap U_i \neq \emptyset \right]

이 결과는 Courcoubetis와 Yannakakis(1995)에 의해 최초로 체계화되었으며, PRISM 등의 확률적 모델 검사 도구에서 구현되어 있다.

8. 실용적 응용

8.1 복합 임무 명세 처리

라빈 오토마타의 복수 라빈 쌍 구조는 복합적 임무 명세를 자연스럽게 처리한다. 예를 들어, 다음과 같은 복합 명세:

\varphi = (\Diamond \square \text{safe\_zone}) \vee (\square \Diamond \text{patrol\_A} \wedge \square \Diamond \text{patrol\_B})

이 명세는 “결국 영원히 안전 구역에 머무르거나, 순찰 구역 A와 B를 무한히 자주 방문한다“를 의미하며, 두 개의 라빈 쌍으로 표현된다. 첫 번째 라빈 쌍은 안전 구역 도달 후 영구 체류를, 두 번째 라빈 쌍은 순환 순찰을 인코딩한다.

8.2 도구 지원

라빈 오토마타 기반 임무 계획을 지원하는 주요 도구는 다음과 같다:

• SPOT: LTL 공식에서 DRA로의 변환을 포함한 다양한 ω-오토마타 조작 기능을 제공한다.
• Rabinizer: LTL 공식에서 직접 DRA를 생성하는 전용 도구로, Safra 구성법을 우회하는 효율적 알고리즘을 구현한다(Komárková, Křetínský, 2014).
• ltl2dstar: LTL에서 DRA/DSA로의 변환을 수행하는 도구로, Safra 구성법의 최적화된 구현을 제공한다.
• PRISM: 확률적 모델 검사 도구로, MDP와 DRA의 제품 구성 및 확률적 최적 정책 계산을 지원한다.

9. 계산 복잡도와 한계

9.1 복잡도 분석

라빈 오토마타 기반 임무 계획의 주요 계산 복잡도는 다음과 같다:

9.2 실용적 한계와 대안

DRA의 이중 지수적 상태 폭발은 실용적 한계의 주요 원인이다. 이를 완화하기 위한 접근법은 다음과 같다:

1. GR(1) 합성으로의 제한: 명세를 GR(1) 단편으로 제한하여 다항 시간 합성을 가능하게 한다.
2. 결정론적 파리티 오토마타(DPA) 활용: DRA 대신 DPA를 사용하여 파리티 게임 해법의 효율적 알고리즘을 활용한다.
3. 기호적 합성: BDD 기반 기호적 표현을 통해 명시적 상태 열거를 방지한다.
4. 제한적 결정화: 특정 LTL 단편에 대해 최적화된 결정론적 변환을 적용한다.

10. 참고 문헌

• Rabin, M.O. (1969). “Decidability of Second-Order Theories and Automata on Infinite Trees.” Transactions of the American Mathematical Society, 141, pp. 1–35.
• Safra, S. (1988). “On the Complexity of ω-Automata.” Proceedings of the 29th IEEE Symposium on Foundations of Computer Science (FOCS), pp. 319–327.
• Courcoubetis, C., Yannakakis, M. (1995). “The Complexity of Probabilistic Verification.” Journal of the ACM, 42(4), pp. 857–907.
• Piterman, N. (2006). “From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata.” Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS), pp. 255–264.
• Komárková, Z., Křetínský, J. (2014). “Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata.” Proceedings of ATVA 2014, LNCS, vol. 8837, pp. 235–241.
• Baier, C., Katoen, J.-P. (2008). Principles of Model Checking. MIT Press.

버전: 2026-03-24
출처: Robotics Engineering 서적, Volume 9, Part 53, Chapter 397