397.47 오토마타(Automata) 합성 기반 제어 정책 생성

1. 개요

오토마타 합성(automata synthesis) 기반 제어 정책 생성은 형식 언어 이론(formal language theory)과 제어 이론(control theory)을 결합하여, 주어진 형식 명세(formal specification)를 만족하는 제어 정책을 자동적으로 도출하는 방법론이다. 이 기법은 로봇의 임무 계획(mission planning) 분야에서 시제 논리(temporal logic)로 기술된 고수준 임무 명세를 유한 오토마타(finite automaton)로 변환한 후, 시스템 모델과의 합성(composition)을 통해 정확성이 보장된(correct-by-construction) 제어 전략을 산출한다.

자율 로봇 시스템에서 오토마타 합성은 단순한 상태 기반 제어를 넘어, 복잡한 시간적·논리적 제약 조건을 체계적으로 처리할 수 있는 수학적 기반을 제공한다. 특히 안전성(safety), 활성(liveness), 공정성(fairness) 등 다양한 속성을 동시에 고려하는 임무 계획에 유용하며, 합성 결과의 정확성을 형식적으로 검증할 수 있다는 점에서 확률적 또는 휴리스틱 기반 방법과 차별화된다.

2. 오토마타 합성의 이론적 기초

2.1 유한 오토마타의 정의

유한 오토마타(finite automaton)는 유한 개의 상태(state)와 상태 전이(transition)로 구성된 수학적 모델이며, 다음과 같은 5-튜플로 정의된다.

\mathcal{A} = (Q, \Sigma, \delta, q_0, F)

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

결정론적 유한 오토마타(DFA: Deterministic Finite Automaton)에서는 각 상태와 입력 기호의 조합에 대해 정확히 하나의 전이가 존재하며, 비결정론적 유한 오토마타(NFA: Nondeterministic Finite Automaton)에서는 동일 입력에 대해 복수의 가능한 전이가 허용된다. 임무 계획에서는 주로 NFA에서 DFA로의 부분집합 구성법(subset construction)을 통한 결정화(determinization) 과정이 활용된다.

2.2 오메가 오토마타와 무한 수평 행동

유한 길이의 단어(word)를 인식하는 고전적 유한 오토마타와 달리, 로봇의 지속적 운용을 모델링하기 위해서는 무한 길이의 입력 문자열(infinite word)을 처리할 수 있는 오메가 오토마타(ω-automata)가 필요하다. 대표적인 오메가 오토마타로는 뷔히 오토마타(Büchi automaton), 뮬러 오토마타(Muller automaton), 라빈 오토마타(Rabin automaton), 스트리트 오토마타(Streett automaton) 등이 있다.

뷔히 오토마타는 다음과 같이 정의된다.

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

여기서 구성 요소는 유한 오토마타와 동일하나, 수락 조건이 상이하다. 무한 실행(infinite run) \rho = q_0, q_1, q_2, \ldots에 대해, 무한히 자주 방문하는 상태 집합 \text{Inf}(\rho) = \{q \in Q \mid q = q_i \text{ for infinitely many } i\}가 수락 상태 집합 F와 교집합이 비어 있지 않을 때, 즉 \text{Inf}(\rho) \cap F \neq \emptyset일 때 해당 실행이 수락된다.

3. 합성 문제의 형식적 정의

3.1 합성 문제의 구조

오토마타 합성 문제(automata synthesis problem)는 Church(1957)에 의해 최초로 제기되었으며, Büchi와 Landweber(1969), 그리고 Rabin(1972)에 의해 해결 가능성이 증명되었다. 합성 문제는 다음과 같이 정식화된다.

주어진 것:

• 환경 변수(environment variable) 집합 \mathcal{X}: 환경이 제어하는 입력
• 시스템 변수(system variable) 집합 \mathcal{Y}: 제어기가 결정하는 출력
• 명세(specification) \varphi: \mathcal{X}와 \mathcal{Y} 위에서 정의된 시제 논리 공식

목표: 임의의 환경 행동 시퀀스 x_0, x_1, x_2, \ldots \in (2^{\mathcal{X}})^\omega에 대해 시스템 출력 시퀀스 y_0, y_1, y_2, \ldots \in (2^{\mathcal{Y}})^\omega를 결정하는 전략(strategy) f: (2^{\mathcal{X}})^+ \rightarrow 2^{\mathcal{Y}}를 찾되, 결합된 행동 시퀀스 (x_0 \cup y_0), (x_1 \cup y_1), \ldots가 명세 \varphi를 만족하도록 한다.

3.2 실현 가능성 판정

명세 \varphi가 실현 가능(realizable)하다 함은 환경의 임의의 행동에 대해 명세를 만족시키는 시스템 전략이 존재함을 의미한다. 이는 게임 이론(game theory)의 관점에서 2인 게임(two-player game)의 승리 전략(winning strategy) 존재 여부와 동치이다. 구체적으로, 환경(player 0)과 시스템(player 1) 간의 무한 게임에서 시스템이 승리 전략을 가지는 경우 명세는 실현 가능하다.

실현 가능성 판정의 계산 복잡도는 명세의 형식에 따라 달라진다. LTL 명세에 대한 합성 문제는 2EXPTIME-완전(2EXPTIME-complete)이며, 이는 명세의 크기에 대해 이중 지수적(doubly exponential) 시간이 소요됨을 의미한다. 반면, GR(1)(Generalized Reactivity(1)) 구조의 명세에 대해서는 다항 시간 내 합성이 가능하여, 실용적 응용에 적합하다.

4. 합성 기반 제어 정책 생성 절차

4.1 전체 절차 개관

오토마타 합성 기반 제어 정책 생성의 일반적 절차는 다음과 같다.

1. 임무 명세 작성: 시제 논리(LTL, CTL 등)를 사용하여 로봇의 임무 요구사항을 형식적으로 기술한다.
2. 오토마타 변환: 시제 논리 명세를 동치의 오토마타(통상 뷔히 오토마타 또는 결정론적 라빈 오토마타)로 변환한다.
3. 시스템 모델 구성: 로봇의 동작 가능 공간을 전이 시스템(transition system) 또는 유한 상태 기계(finite state machine)로 모델링한다.
4. 제품 오토마톤 구성: 시스템 모델과 명세 오토마타의 곱(product)을 계산하여 제품 오토마톤(product automaton)을 생성한다.
5. 게임 해석 및 승리 전략 계산: 제품 오토마톤을 2인 게임으로 해석하고, 고정점 반복(fixed-point iteration) 등의 알고리즘을 통해 승리 전략을 도출한다.
6. 제어 정책 추출: 승리 전략으로부터 로봇의 제어 정책(control policy)을 추출한다.

4.2 LTL에서 오토마타로의 변환

LTL 공식 \varphi를 비결정론적 뷔히 오토마타(NBA: Nondeterministic Büchi Automaton)로 변환하는 절차는 Vardi와 Wolper(1986)에 의해 제안되었으며, 변환된 오토마타의 상태 수는 최악의 경우 2^{O(\lvert\varphi\rvert)}이다.

LTL 공식에서 NBA로의 변환 알고리즘은 다음 단계를 포함한다:

1. 부분 공식 전개: LTL 공식의 모든 부분 공식(subformula)을 열거하여 클로저(closure) 집합 \text{cl}(\varphi)를 구성한다.
2. 원자 집합 구성: 클로저 집합의 원소에 대한 최대 일관 부분집합(maximally consistent subset)으로 원자(atom)를 구성한다.
3. 전이 관계 정의: 원자 간 전이 관계를 시제 연산자의 의미론에 기반하여 정의한다.
4. 수락 조건 설정: \text{Until} 연산자에 대한 의무(obligation) 충족을 보장하는 수락 조건을 설정한다.

합성 문제에서는 NBA를 결정론적 오토마타(예: 결정론적 라빈 오토마타(DRA) 또는 결정론적 파리티 오토마타(DPA))로 결정화하는 추가 단계가 필요하다. 이 결정화 과정에서 Safra 구성법(Safra’s construction)이 사용되며, 상태 수가 2^{O(n \log n)}으로 증가한다.

4.3 전이 시스템 모델링

로봇의 동작 환경과 가능한 행동을 다음과 같은 전이 시스템(transition system)으로 모델링한다.

\mathcal{T} = (S, s_0, A, \rightarrow, AP, L)

여기서 S는 상태 집합, s_0 \in S는 초기 상태, A는 행동(action) 집합, \rightarrow \subseteq S \times A \times S는 전이 관계, AP는 원자 명제(atomic proposition) 집합, L: S \rightarrow 2^{AP}는 레이블링 함수(labeling function)이다.

로봇의 작업 공간을 이산화하여 각 영역(region)을 상태로, 영역 간 이동 가능성을 전이로 모델링하는 것이 일반적이다. 예를 들어, 격자 세계(grid world)에서 각 셀이 하나의 상태에 대응하고, 인접 셀로의 이동이 전이에 해당한다.

5. 게임 이론적 해석

5.1 인 게임 구조

오토마타 합성은 본질적으로 시스템과 환경 사이의 2인 교대 게임(two-player alternating game)으로 모델링된다. 게임 그래프(game graph) \mathcal{G} = (V_0, V_1, E, v_0)에서 V_0는 환경이 선택하는 꼭짓점, V_1은 시스템이 선택하는 꼭짓점, E는 간선 집합, v_0는 초기 꼭짓점이다.

게임의 진행은 다음과 같다:

1. 현재 상태가 v \in V_0이면 환경이 후속 상태를 선택한다.
2. 현재 상태가 v \in V_1이면 시스템이 후속 상태를 선택한다.
3. 이 과정이 무한히 반복되어 무한 경로(infinite play) \pi = v_0, v_1, v_2, \ldots를 생성한다.

5.2 승리 조건과 전략 계산

승리 조건(winning condition)은 명세 오토마타의 수락 조건으로부터 도출된다. 대표적인 승리 조건 유형은 다음과 같다:

• 도달성 조건(Reachability): 특정 상태 집합에 도달하면 승리한다.
• 안전성 조건(Safety): 특정 상태 집합을 영원히 회피하면 승리한다.
• 뷔히 조건(Büchi): 수락 상태 집합을 무한히 자주 방문하면 승리한다.
• 파리티 조건(Parity): 각 상태에 우선순위(priority)가 부여되며, 무한히 자주 방문하는 상태 중 최소 우선순위가 짝수이면 승리한다.

뷔히 게임에서의 승리 영역(winning region) W_1은 다음의 중첩 고정점 반복(nested fixed-point iteration)으로 계산된다.

W_1 = \nu Z. \mu Y. \left( (F \cap \text{Pre}(Z)) \cup \text{Pre}(Y) \right)

여기서 \nu는 최대 고정점(greatest fixed-point), \mu는 최소 고정점(least fixed-point), \text{Pre}(X) = \{v \in V_1 \mid \exists (v, v') \in E, v' \in X\} \cup \{v \in V_0 \mid \forall (v, v') \in E, v' \in X\}는 전임자 연산자(predecessor operator)이다.

파리티 게임에서의 승리 전략은 Zielonka 알고리즘 또는 McNaughton-Zielonka 알고리즘을 통해 계산되며, 이 알고리즘의 시간 복잡도는 O(m \cdot n^{d/2})이다. 여기서 m은 간선 수, n은 꼭짓점 수, d는 우선순위 범위이다.

6. GR(1) 합성

6.1 GR(1) 명세의 구조

GR(1)(Generalized Reactivity(1)) 합성은 Piterman, Pnueli, Sa’ar(2006)에 의해 제안된 효율적 합성 프레임워크이다. GR(1) 명세는 다음의 형태를 갖는다.

\varphi = \varphi_e \rightarrow \varphi_s

여기서 환경 가정 \varphi_e와 시스템 보장 \varphi_s는 각각 다음의 구조를 따른다:

• 초기 조건: \theta_e (환경 초기 조건), \theta_s (시스템 초기 조건)
• 안전성 조건: \square \rho_e (환경 전이 제약), \square \rho_s (시스템 전이 제약)
• 활성 조건: \bigwedge_{i=1}^{m} \square \Diamond J_e^i (환경 공정성 가정), \bigwedge_{j=1}^{n} \square \Diamond J_s^j (시스템 활성 목표)

GR(1) 합성의 핵심적 장점은 3중 중첩 고정점 반복(triply nested fixed-point iteration)을 통해 O(\lvert S \rvert^2 \cdot n \cdot m) 시간 복잡도로 합성이 가능하다는 것이다. 여기서 \lvert S \rvert는 상태 수, n은 시스템 목표 수, m은 환경 가정 수이다.

6.2 GR(1) 합성 알고리즘

GR(1) 게임의 승리 영역은 다음의 3중 고정점으로 계산된다.

W_1 = \nu Z. \bigwedge_{j=1}^{n} \mu Y. \nu X. \left( (J_s^j \cap \text{Pre}(Z)) \cup \text{Pre}(Y) \cup ((\neg J_s^j) \cap \text{Pre}(X)) \right)

이 알고리즘은 각 시스템 목표 J_s^j에 대해 순환적으로 만족을 보장하는 전략을 구성한다. 구체적 절차는 다음과 같다:

1. 외부 최대 고정점 (\nu Z): 모든 시스템 목표를 순회하며 전체 승리 영역을 수렴시킨다.
2. 중간 최소 고정점 (\mu Y): 현재 목표 J_s^j에 도달하기까지의 유한 단계 도달성을 계산한다.
3. 내부 최대 고정점 (\nu X): 목표에 도달하지 않더라도 안전하게 유지 가능한 상태를 확인한다.

6.3 메모리 전략의 추출

GR(1) 합성에서 도출되는 제어 전략은 유한 메모리 전략(finite-memory strategy)이며, 시스템 목표의 인덱스 j를 메모리 상태로 사용한다. 추출된 전략은 Mealy 기계(Mealy machine) 형태로 표현되며, 현재 환경 입력과 내부 메모리 상태에 따라 시스템 출력을 결정한다.

\mathcal{M} = (M, m_0, \Sigma_I, \Sigma_O, \delta_M, \lambda_M)

여기서 M은 메모리 상태 집합, m_0는 초기 메모리 상태, \Sigma_I는 입력 알파벳, \Sigma_O는 출력 알파벳, \delta_M: M \times \Sigma_I \rightarrow M은 메모리 전이 함수, \lambda_M: M \times \Sigma_I \rightarrow \Sigma_O은 출력 함수이다.

7. 로봇 임무 계획에의 적용

7.1 이동 로봇의 내비게이션 임무

이동 로봇의 작업 공간을 유한 개의 영역으로 분할하고, 각 영역에 원자 명제를 부여하여 LTL 임무 명세를 작성할 수 있다. 예를 들어, 로봇이 영역 A, B, C를 순환적으로 방문하면서 장애물 영역 O를 회피해야 하는 임무는 다음과 같이 명세된다.

\varphi = \square \Diamond A \wedge \square \Diamond B \wedge \square \Diamond C \wedge \square \neg O

이 명세를 뷔히 오토마타로 변환하고, 로봇의 전이 시스템과 곱을 취하면 제품 뷔히 오토마톤이 생성된다. 이 제품 오토마톤 위에서 공정 경로(fair path)를 탐색하면 임무를 만족하는 로봇의 행동 시퀀스가 도출된다.

Kress-Gazit, Fainekos, Pappas(2009)의 연구에서는 이러한 기법을 실제 로봇 시스템에 적용하여, LTL 명세로부터 로봇 제어기를 자동으로 합성하는 프레임워크를 제시하였다. 이 프레임워크에서는 작업 공간의 삼각 분할(triangulation)을 통해 연속 공간을 이산화하고, 각 삼각형 영역에 대한 연속 제어기를 별도로 설계하여 하이브리드 제어 시스템을 구성한다.

7.2 다중 로봇 시스템에의 확장

다중 로봇 시스템에서의 오토마타 합성은 각 로봇의 상태 공간을 합성하여 전체 시스템의 상태 공간을 구성한다. n대의 로봇이 각각 k개의 상태를 가질 때, 전체 상태 공간의 크기는 k^n으로 지수적으로 증가하여 상태 폭발(state explosion) 문제가 발생한다.

이 문제를 완화하기 위한 대표적 접근법은 다음과 같다:

• 분산 합성(distributed synthesis): 각 로봇에 대해 독립적으로 또는 부분적 통신을 통해 합성을 수행한다.
• 단계적 분해(compositional synthesis): 전체 명세를 각 로봇별 부분 명세로 분해하여 개별적으로 합성한 후 결합한다.
• 대칭성 활용(symmetry reduction): 동질적(homogeneous) 로봇 그룹에서의 대칭성을 이용하여 탐색 공간을 축소한다.

7.3 반응형 합성과의 연계

반응형 합성(reactive synthesis)은 환경의 동적 변화에 실시간으로 대응하는 제어 전략을 생성하는 기법으로, 오토마타 합성의 중요한 응용 분야이다. Bloem, Jobstmann, Piterman, Pnueli, Sa’ar(2012)의 연구에서는 GR(1) 합성을 기반으로 로봇의 반응형 제어기를 효율적으로 합성하는 도구인 SLUGS(SmaLl bUt Complete GRone Synthesizer)를 개발하였다.

반응형 합성에서는 환경이 적대적(adversarial)으로 행동한다고 가정하므로, 생성된 제어 정책은 최악의 환경 행동에 대해서도 명세를 만족하는 강건한(robust) 특성을 보인다.

8. 계산 복잡도와 확장성 과제

8.1 복잡도 분석

오토마타 합성의 계산 복잡도는 사용되는 명세 형식과 오토마타 유형에 따라 상이하다:

8.2 상태 폭발 완화 기법

대규모 시스템에서의 상태 폭발 문제를 해결하기 위한 주요 기법은 다음과 같다:

1. 기호적 표현(symbolic representation): 이진 결정 다이어그램(BDD: Binary Decision Diagram)을 사용하여 상태 집합과 전이 관계를 압축적으로 표현한다. 기호적 합성 알고리즘은 명시적 열거 없이 고정점 계산을 수행할 수 있다.

2. 반례 유도 추상화 정제(CEGAR: Counterexample-Guided Abstraction Refinement): 초기에는 추상화된 모델에서 합성을 시도하고, 실패 시 반례를 분석하여 추상화를 정제하는 반복적 절차를 적용한다.

3. 지연 합성(lazy synthesis): 전체 상태 공간을 사전에 구성하지 않고, 필요에 따라 점진적으로 탐색하는 전략이다.

4. 계층적 합성(hierarchical synthesis): 임무를 계층적으로 분해하여 각 수준에서 개별적으로 합성을 수행한 후 통합한다.

9. 도구와 소프트웨어 프레임워크

9.1 합성 도구

오토마타 합성을 지원하는 대표적 소프트웨어 도구는 다음과 같다:

• SLUGS: SmaLl bUt Complete GRone Synthesizer. GR(1) 합성에 특화된 도구로, BDD 기반 기호적 알고리즘을 구현한다.
• Strix: LTL 명세로부터 파리티 게임 기반 합성을 수행하는 도구로, SYNTCOMP(Synthesis Competition)에서 우수한 성적을 기록하였다.
• LTLMoP: Linear Temporal Logic MissiOn Planning. LTL 기반 임무 계획 및 제어기 합성을 통합하는 로봇 공학 전용 프레임워크이다.
• TuLiP: Temporal Logic Planning Toolbox. Python 기반의 오픈 소스 도구로, GR(1) 합성과 로봇 제어기 생성을 지원한다.

9.2 로봇 미들웨어와의 통합

합성된 제어 정책은 로봇 미들웨어(예: ROS2)와 연동하여 실제 로봇 시스템에 배포될 수 있다. TuLiP에서 생성된 제어기를 ROS2 노드(node)로 래핑(wrapping)하여 토픽(topic) 기반 통신을 통해 센서 데이터를 수신하고 행동 명령을 발행하는 아키텍처가 대표적이다.

10. 한계와 향후 연구 방향

10.1 현재 한계

오토마타 합성 기반 제어 정책 생성은 다음과 같은 한계를 갖는다:

1. 계산 비용: 일반적 LTL 명세에 대한 합성은 이중 지수 시간 복잡도를 가져, 대규모 시스템에의 직접 적용이 어렵다.
2. 이산화 요구: 연속적인 로봇 동역학을 유한 상태 모델로 추상화하는 과정에서 정보 손실이 발생할 수 있다.
3. 환경 모델의 완전성 가정: 환경의 가능한 행동을 사전에 완전히 열거해야 하므로, 미지의 환경에 대한 적응이 어렵다.
4. 명세 작성의 난이도: 복잡한 임무를 시제 논리로 정확히 기술하는 것은 전문적 지식을 요구한다.

10.2 향후 연구 방향

• 학습 기반 합성(learning-based synthesis): 강화 학습(reinforcement learning)과 형식 합성을 결합하여, 데이터로부터 환경 모델을 학습하면서 동시에 올바른 제어 전략을 도출하는 연구가 진행되고 있다(Hasanbeig, Abate, Kroening, 2019).
• 다중 에이전트 분산 합성: 통신 제약 하에서 다수의 에이전트가 협력적으로 임무를 수행하기 위한 분산 합성 알고리즘의 개발이 활발하다.
• 확률적 합성(probabilistic synthesis): 확률적 환경 모델을 고려한 합성으로, 마르코프 결정 과정과 오토마타 기반 명세를 결합하는 기법이 연구되고 있다.
• 자연어 인터페이스: 대규모 언어 모델(LLM)을 통해 자연어 임무 지시를 자동으로 시제 논리 명세로 변환하고 합성하는 종단 간(end-to-end) 파이프라인의 개발이 탐색되고 있다.

11. 참고 문헌

• Church, A. (1957). “Application of Recursive Arithmetic to the Problem of Circuit Synthesis.” Summaries of Talks Presented at the Summer Institute for Symbolic Logic, Cornell University.
• Büchi, J.R., Landweber, L.H. (1969). “Solving Sequential Conditions by Finite-State Strategies.” Transactions of the American Mathematical Society, 138, pp. 295–311.
• Rabin, M.O. (1972). “Automata on Infinite Objects and Church’s Problem.” Regional Conference Series in Mathematics, No. 13, AMS.
• 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.
• Piterman, N., Pnueli, A., Sa’ar, Y. (2006). “Synthesis of Reactive(1) Designs.” Proceedings of VMCAI 2006, LNCS, vol. 3855, pp. 364–380.
• 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.
• Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y. (2012). “Synthesis of Reactive(1) Designs.” Journal of Computer and System Sciences, 78(3), pp. 911–938.
• Hasanbeig, M., Abate, A., Kroening, D. (2019). “Logically-Constrained Reinforcement Learning.” arXiv preprint arXiv:1801.08099.

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