397.49 뷔히 오토마타(Büchi Automaton) 기반 무한 수평 임무 계획

397.49 뷔히 오토마타(Büchi Automaton) 기반 무한 수평 임무 계획

1. 개요

뷔히 오토마타(Büchi automaton)는 무한 길이의 입력 문자열(infinite word)을 인식하는 오메가 오토마타(ω-automata)의 대표적 유형으로서, 로봇의 지속적·반복적 임무를 형식적으로 모델링하고 계획하는 데 핵심적으로 활용된다. 무한 수평(infinite horizon) 임무 계획에서는 순찰, 감시, 지속적 서비스 제공 등과 같이 종료 시점이 명시되지 않은 임무를 대상으로 하며, 뷔히 오토마타의 수락 조건(acceptance condition)을 통해 이러한 영구적 행동 패턴을 수학적으로 정의한다.

유한 수평(finite horizon) 임무 계획이 목표 상태에의 도달 가능성에 초점을 맞추는 반면, 무한 수평 임무 계획은 시스템이 영구적으로 특정 행동 패턴을 반복하면서 안전성(safety)과 활성(liveness)을 동시에 보장해야 한다. 뷔히 오토마타는 이러한 무한적 행동 요구사항을 수락 상태의 무한 반복 방문이라는 직관적 조건으로 포착한다.

2. 뷔히 오토마타의 수학적 기초

2.1 형식적 정의

뷔히 오토마타(Büchi automaton)는 Büchi(1962)에 의해 도입된 오메가 오토마타로서, 다음의 5-튜플로 정의된다.

\mathcal{B} = (Q, \Sigma, \delta, Q_0, F)

여기서 Q는 유한 상태 집합, \Sigma는 유한 입력 알파벳, \delta: Q \times \Sigma \rightarrow 2^Q는 전이 함수, Q_0 \subseteq Q는 초기 상태 집합, F \subseteq Q는 수락 상태(accepting state) 집합이다.

무한 입력 문자열(ω-word) w = \sigma_0 \sigma_1 \sigma_2 \ldots \in \Sigma^\omega에 대한 실행(run) \rho = q_0 q_1 q_2 \ldots는 다음 조건을 만족하는 무한 상태 시퀀스이다:

  1. q_0 \in Q_0 (초기 상태에서 출발)
  2. q_{i+1} \in \delta(q_i, \sigma_i) (모든 i \geq 0에 대해 전이 함수를 준수)

2.2 수락 조건

실행 \rho에 대해, 무한히 자주 방문하는 상태 집합을 다음과 같이 정의한다.

\text{Inf}(\rho) = \{q \in Q \mid \forall n \in \mathbb{N}, \exists m \geq n : q_m = q \}

뷔히 수락 조건(Büchi acceptance condition)에 따르면, 실행 \rho가 수락(accepting)되려면 다음을 만족해야 한다:

\text{Inf}(\rho) \cap F \neq \emptyset

즉, 수락 상태 집합 F에 속하는 상태 중 적어도 하나가 무한히 자주 방문되어야 한다. 이 조건은 “좋은 상태를 무한히 자주 경유한다“는 활성 속성을 자연스럽게 포착한다.

뷔히 오토마타가 인식하는 ω-언어(ω-language)는 다음과 같이 정의된다:

\mathcal{L}(\mathcal{B}) = \{w \in \Sigma^\omega \mid \exists \text{ accepting run of } \mathcal{B} \text{ on } w \}

2.3 결정론적 뷔히 오토마타와 비결정론적 뷔히 오토마타

결정론적 뷔히 오토마타(DBA: Deterministic Büchi Automaton)에서는 \lvert Q_0 \rvert = 1이고 모든 (q, \sigma) 쌍에 대해 \lvert \delta(q, \sigma) \rvert = 1이다. 중요한 이론적 사실은 DBA가 NBA보다 엄밀히 약한 표현력을 가진다는 것이다. 즉, 모든 ω-정규 언어(ω-regular language)를 인식할 수 있는 것은 NBA이며, DBA로는 인식할 수 없는 ω-정규 언어가 존재한다.

대표적 예로, 공식 \Diamond \square a (“결국 영원히 a가 성립한다”)에 대응하는 ω-언어는 DBA로 인식 가능하지만, \square \Diamond a (“a가 무한히 자주 성립한다”)에 대응하는 ω-언어는 DBA로 인식 가능하다. 반면, \Diamond \square a \vee \Diamond \square b와 같은 일부 공식은 DBA로 인식할 수 없으며, 이러한 경우 결정론적 라빈 오토마타(DRA) 등 더 강력한 오토마타가 필요하다.

3. LTL 명세에서 뷔히 오토마타로의 변환

3.1 변환의 이론적 기반

LTL(Linear Temporal Logic) 공식 \varphi는 동치의 비결정론적 뷔히 오토마타 \mathcal{B}_\varphi로 변환할 수 있으며, 이는 Vardi와 Wolper(1986)에 의해 증명되었다. 변환된 오토마타의 상태 수는 최악의 경우 2^{O(\lvert \varphi \rvert)}이다.

3.2 변환 알고리즘

LTL에서 NBA로의 변환은 다음의 주요 알고리즘을 통해 수행된다:

  1. Vardi-Wolper 구성법: 타블로(tableau) 기반 방법으로, LTL 공식의 부분 공식(subformula) 집합으로부터 최대 일관 집합(maximally consistent set)을 상태로 구성한다. 이론적 최악 복잡도를 달성하지만, 실용적으로는 불필요한 상태가 다수 생성될 수 있다.

  2. Gastin-Oddoux 알고리즘: 교대 오토마타(alternating automaton)를 중간 표현으로 사용하는 방법이다. LTL 공식을 먼저 매우 약한 교대 오토마타(VWAA: Very Weak Alternating Automaton)로 변환한 후, 이를 일반화된 뷔히 오토마타(GBA: Generalized Büchi Automaton)로 변환하고, 최종적으로 표준 NBA로 변환한다. LTL2BA 도구가 이 알고리즘을 구현한다.

  3. SPOT 라이브러리의 최적 변환: Duret-Lutz 등(2016)이 개발한 SPOT 라이브러리는 다중 전략을 결합한 최적화된 변환을 제공한다. 시뮬레이션 기반 축소(simulation-based reduction), SCC(Strongly Connected Component) 기반 간소화 등을 적용하여 최소한의 상태를 가지는 NBA를 생성한다.

3.3 일반화된 뷔히 오토마타

일반화된 뷔히 오토마타(GBA: Generalized Büchi Automaton)는 복수의 수락 상태 집합 \mathcal{F} = \{F_1, F_2, \ldots, F_k\}를 가지며, 수락 조건은 모든 수락 집합에 대해 무한히 자주 방문할 것을 요구한다:

\forall i \in \{1, \ldots, k\} : \text{Inf}(\rho) \cap F_i \neq \emptyset

GBA는 표준 NBA로 변환 가능하며, 변환된 NBA의 상태 수는 \lvert Q \rvert \cdot k이다. 변환 과정에서 카운터를 도입하여 각 수락 집합의 방문을 순환적으로 추적한다.

4. 무한 수평 임무 계획의 절차

4.1 전체 워크플로

뷔히 오토마타 기반 무한 수평 임무 계획의 전체 절차는 다음과 같다:

  1. 환경 모델링: 로봇의 작업 공간을 전이 시스템 \mathcal{T} = (S, s_0, \delta_T, AP, L)으로 모델링한다.
  2. 임무 명세: LTL 공식 \varphi로 무한 수평 임무를 형식적으로 기술한다.
  3. 오토마타 변환: LTL 공식 \varphi를 비결정론적 뷔히 오토마타 \mathcal{B}_\varphi로 변환한다.
  4. 제품 오토마톤 구성: 전이 시스템 \mathcal{T}와 뷔히 오토마타 \mathcal{B}_\varphi의 제품을 계산하여 제품 뷔히 오토마톤 \mathcal{P} = \mathcal{T} \otimes \mathcal{B}_\varphi를 구성한다.
  5. 수락 경로 탐색: 제품 오토마톤 \mathcal{P} 위에서 수락 실행을 탐색한다.
  6. 래소 경로 추출: 수락 실행을 접두사(prefix)와 주기(suffix) 부분으로 분해하여 래소(lasso) 형태의 실행 계획을 추출한다.

4.2 임무 명세 패턴

무한 수평 임무에서 흔히 사용되는 LTL 명세 패턴은 다음과 같다:

순환 방문(Cyclic visiting): 다수의 관심 영역을 무한히 자주 방문한다.

\varphi_{\text{patrol}} = \bigwedge_{i=1}^{n} \square \Diamond r_i

영구 회피(Permanent avoidance): 위험 영역을 영원히 회피한다.

\varphi_{\text{safety}} = \square \neg \text{obstacle}

순서 방문(Sequenced visiting): 특정 순서로 영역을 방문한 후 반복한다.

\varphi_{\text{seq}} = \square \Diamond (r_1 \wedge \Diamond (r_2 \wedge \Diamond r_3))

조건부 응답(Conditional response): 특정 사건 발생 시 일정 조건으로 응답한다.

\varphi_{\text{resp}} = \square (\text{request} \rightarrow \Diamond \text{service})

안정성(Stability): 결국 특정 영역에 영구적으로 머문다.

\varphi_{\text{stable}} = \Diamond \square \text{home}

4.3 수락 경로의 존재 판정

제품 뷔히 오토마톤 \mathcal{P} 위에서 수락 실행의 존재 여부는 다음의 그래프 이론적 조건과 동치이다:

초기 상태 s_{P,0}에서 도달 가능한(reachable) 강연결 성분(SCC: Strongly Connected Component) 중, 수락 상태를 포함하면서 사소하지 않은(non-trivial, 즉 적어도 하나의 간선을 포함하는) SCC가 존재한다.

이 조건을 검사하는 알고리즘은 다음과 같다:

  1. 제품 오토마톤의 도달 가능 부분 그래프를 구성한다.
  2. Tarjan 알고리즘 또는 Kosaraju 알고리즘을 사용하여 SCC를 식별한다.
  3. 수락 상태를 포함하는 사소하지 않은 SCC가 존재하는지 확인한다.

시간 복잡도는 O(\lvert S_P \rvert + \lvert \delta_P \rvert)로, 제품 오토마톤의 크기에 선형이다.

4.4 중첩 깊이 우선 탐색

비결정론적 뷔히 오토마타에 대한 대안적 공허성 검사 알고리즘으로, Courcoubetis, Vardi, Wolper, Yannakakis(1992)가 제안한 중첩 깊이 우선 탐색(nested DFS)이 있다. 이 알고리즘은 즉석 구성(on-the-fly construction)과 결합할 수 있어, 전체 제품 오토마톤을 사전에 구성하지 않고도 수락 실행을 탐색할 수 있다는 장점이 있다.

알고리즘 개요:

  • 외부 DFS: 초기 상태에서 출발하여 깊이 우선으로 탐색하되, 수락 상태에 도달하면 해당 상태를 기록한다.
  • 내부 DFS: 기록된 수락 상태에서 출발하여 다시 깊이 우선 탐색을 수행하고, 해당 수락 상태로 돌아오는 사이클이 발견되면 수락 실행이 존재한다고 판정한다.

5. 최적 무한 수평 임무 계획

5.1 비용 함수의 정의

최적 무한 수평 임무 계획에서는 래소 경로의 비용을 최소화하는 행동 시퀀스를 탐색한다. 비용 함수는 다음과 같이 정의된다:

J(\rho) = J_{\text{prefix}}(\rho) + \gamma \cdot J_{\text{cycle}}(\rho)

여기서 J_{\text{prefix}}는 접두사 비용, J_{\text{cycle}}은 주기 비용, \gamma > 0은 가중 계수이다. 주기가 무한히 반복되므로, 주기 비용에 대한 가중치가 높을수록 장기적 운용 효율이 강조된다.

5.2 최적 래소 탐색 알고리즘

Smith, Tumova, Belta, Rus(2011)는 다음의 2-Dijkstra 알고리즘을 제안하였다:

  1. 순방향 Dijkstra: 초기 상태에서 모든 수락 상태까지의 최단 경로를 계산한다.
  2. 역방향 Dijkstra: 각 수락 상태에서 자기 자신으로의 최단 사이클을 계산한다.
  3. 최적 래소 선택: J(\rho)를 최소화하는 수락 상태와 대응하는 접두사-주기 쌍을 선택한다.

이 알고리즘의 시간 복잡도는 O(\lvert F_P \rvert \cdot (\lvert S_P \rvert \log \lvert S_P \rvert + \lvert \delta_P \rvert))이다.

5.3 다중 비용 기준의 최적화

이동 거리, 에너지 소모, 지연 시간 등 복수의 비용 기준을 동시에 고려하는 다중 목적 최적화(multi-objective optimization)가 필요한 경우, 파레토 최적(Pareto-optimal) 래소 경로 집합을 계산한다. 가중합 방법 또는 ε-제약법을 적용하여 비열등 해(non-dominated solution)를 산출할 수 있다.

6. 확률적 환경에서의 확장

6.1 마르코프 결정 과정과의 결합

확률적 환경에서의 무한 수평 임무 계획은 마르코프 결정 과정(MDP: Markov Decision Process)과 뷔히 오토마타를 결합하여 수행된다. MDP \mathcal{M} = (S, A, P, s_0, AP, L)과 뷔히 오토마타 \mathcal{B}의 제품 MDP \mathcal{M} \otimes \mathcal{B}를 구성한 후, 수락 조건을 만족하는 확률을 최대화하는 정책을 계산한다.

\max_{\pi} \Pr^{\pi}_{\mathcal{M} \otimes \mathcal{B}} \left[ \text{Inf}(\rho) \cap F_P \neq \emptyset \right]

이 문제는 제품 MDP의 하단 SCC(bottom SCC) 분석과 선형 계획법(linear programming)을 통해 다항 시간 내에 해결된다. Baier, Katoen(2008)은 이러한 확률적 모델 검사(probabilistic model checking) 기법의 이론적 기반을 체계적으로 정립하였다.

6.2 수락 확률의 계산

제품 MDP에서 수락 조건을 만족하는 최대 확률은 다음 단계를 통해 계산된다:

  1. 하단 SCC 식별: 제품 MDP에서 모든 하단 SCC를 식별한다.
  2. 수락 하단 SCC 분류: 수락 상태를 포함하는 하단 SCC를 수락 하단 SCC로 분류한다.
  3. 도달 확률 계산: 초기 상태에서 수락 하단 SCC에 도달하는 최대 확률을 선형 계획법으로 계산한다.

7. 실용적 고려사항

7.1 환경 이산화

연속적 작업 공간을 유한 상태의 전이 시스템으로 이산화하는 과정은 임무 계획의 정확성에 직접적 영향을 미친다. 주요 이산화 기법은 다음과 같다:

  • 격자 분할(grid decomposition): 작업 공간을 균일한 격자 셀로 분할하는 가장 단순한 방법이다. 해상도가 높을수록 정밀하지만 상태 수가 급증한다.
  • 삼각 분할(triangulation): 볼록 다각형(convex polygon) 형태의 영역으로 분할하며, Kress-Gazit 등(2009)의 연구에서 로봇 임무 계획에 적용되었다.
  • 셀 분해(cell decomposition): 장애물의 형상에 따라 자유 공간을 비균일 셀로 분할하는 방법이다.

7.2 온라인 재계획

실제 환경에서는 사전 계획된 래소 경로가 환경 변화로 인해 실행 불가능해질 수 있다. 이 경우 현재 상태에서의 제품 오토마톤 상태를 유지하면서 남은 명세에 대해 재계획을 수행한다. 이러한 온라인 재계획(online replanning) 기법은 동적 환경에서의 뷔히 기반 임무 계획의 실용성을 높인다.

7.3 계산 복잡도와 확장성

뷔히 기반 무한 수평 임무 계획의 전체 계산 복잡도는 다음과 같다:

단계복잡도비고
LTL → NBA 변환2^{O(\lvert \varphi \rvert)}공식 크기에 지수적
제품 오토마톤 구성O(\lvert S \rvert \cdot \lvert Q \rvert)상태 수의 곱
수락 경로 탐색O(\lvert S_P \rvert + \lvert \delta_P \rvert)선형
최적 래소 탐색O(\lvert F_P \rvert \cdot \lvert S_P \rvert \log \lvert S_P \rvert)Dijkstra 기반

전체 파이프라인의 병목은 LTL에서 NBA로의 변환 단계에 있으며, 명세의 크기가 증가할수록 오토마타의 상태 수가 지수적으로 증가한다. 이를 완화하기 위해 GR(1) 합성, 기호적 방법(symbolic method), 또는 명세 분해(specification decomposition) 등의 기법이 적용된다.

8. 참고 문헌

  • Büchi, J.R. (1962). “On a Decision Method in Restricted Second-Order Arithmetic.” Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science, Stanford University Press, pp. 1–11.
  • Vardi, M.Y., Wolper, P. (1986). “An Automata-Theoretic Approach to Automatic Program Verification.” Proceedings of the 1st IEEE Symposium on Logic in Computer Science (LICS), pp. 332–344.
  • Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M. (1992). “Memory-Efficient Algorithms for the Verification of Temporal Properties.” Formal Methods in System Design, 1(2/3), pp. 275–288.
  • Baier, C., Katoen, J.-P. (2008). Principles of Model Checking. MIT Press.
  • Kress-Gazit, H., Fainekos, G.E., Pappas, G.J. (2009). “Temporal-Logic-Based Reactive Mission and Motion Planning.” IEEE Transactions on Robotics, 25(6), pp. 1370–1381.
  • Smith, S.L., Tumova, J., Belta, C., Rus, D. (2011). “Optimal Path Planning for Surveillance with Temporal-Logic Constraints.” The International Journal of Robotics Research, 30(14), pp. 1695–1708.
  • Duret-Lutz, A., Lewkowicz, A., Faez, A., Renault, E., Laurent, J. (2016). “Spot 2.0 — A Framework for LTL and ω-Automata Manipulation.” Proceedings of ATVA 2016, LNCS, vol. 9938, pp. 122–129.

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