397.48 제품 오토마톤(Product Automaton) 구성

397.48 제품 오토마톤(Product Automaton) 구성

1. 개요

제품 오토마톤(product automaton)은 로봇의 동작 모델과 임무 명세 오토마타를 결합하여, 임무 만족 가능한 로봇 행동 시퀀스를 체계적으로 탐색하기 위한 합성 구조물이다. 이 구성은 오토마타 기반 임무 계획의 핵심 단계로서, 시스템의 물리적 전이 가능성과 논리적 임무 요구사항을 단일 오토마톤 내에 동시 인코딩한다. 제품 오토마톤 위에서의 경로 탐색은 곧 임무를 만족하는 실행 가능한 제어 정책의 도출과 동치이다.

형식적으로, 제품 오토마톤은 전이 시스템(transition system)과 명세 오토마타의 동기적 곱(synchronous product)으로 정의되며, 이를 통해 로봇이 특정 행동을 수행할 때 임무 명세의 어떤 상태로 전이하는지를 추적할 수 있다. 이러한 합성 과정은 모델 검사(model checking)에서의 곱 구성과 유사하나, 임무 계획에서는 검증이 아닌 합성 목적으로 활용된다는 점에서 차이가 있다.

2. 수학적 정의

2.1 전이 시스템

로봇의 동작 환경을 모델링하는 전이 시스템(transition system)은 다음과 같이 정의된다.

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

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

전이 시스템의 각 상태는 로봇이 위치할 수 있는 이산화된 영역(region)에 대응하며, 전이 관계는 물리적으로 이동 가능한 영역 쌍을 나타낸다. 레이블링 함수 L은 각 상태에서 관찰되는 환경 속성(예: 목표 지점, 장애물, 충전소 등)을 원자 명제의 집합으로 할당한다.

2.2 명세 오토마타

임무 명세를 표현하는 오토마타는 일반적으로 비결정론적 뷔히 오토마타(NBA: Nondeterministic Büchi Automaton) 또는 결정론적 라빈 오토마타(DRA: Deterministic Rabin Automaton) 형태를 취한다. 뷔히 오토마타의 경우 다음과 같이 정의된다.

\mathcal{B} = (Q, 2^{AP}, \delta_B, q_0, F)

여기서 Q는 유한 상태 집합, 2^{AP}는 입력 알파벳(원자 명제 집합의 멱집합), \delta_B: Q \times 2^{AP} \rightarrow 2^Q는 전이 함수, q_0 \in Q는 초기 상태, F \subseteq Q는 수락 상태 집합이다.

명세 오토마타는 LTL(Linear Temporal Logic) 공식으로부터 자동 변환되며, Vardi-Wolper 구성법(1986) 또는 Gastin-Oddoux 알고리즘(2001) 등이 사용된다.

2.3 제품 오토마톤의 정의

전이 시스템 \mathcal{T}와 뷔히 오토마타 \mathcal{B}의 제품 오토마톤 \mathcal{P}는 다음과 같이 정의된다.

\mathcal{P} = \mathcal{T} \otimes \mathcal{B} = (S_P, s_{P,0}, \delta_P, F_P)

여기서 각 구성 요소는 다음과 같다:

  • 상태 집합: S_P = S \times Q. 각 상태 (s, q)는 로봇이 물리적 상태 s에 있으면서 명세 오토마타가 논리적 상태 q에 있는 상황을 표현한다.
  • 초기 상태: s_{P,0} = (s_0, q_0). 로봇과 명세 오토마타가 각각의 초기 상태에 있는 경우이다.
  • 전이 관계: (s, q) \xrightarrow{\delta_P} (s', q')는 다음 두 조건이 동시에 성립할 때 정의된다:
  1. (s, s') \in \delta_T (로봇이 s에서 s'로 물리적으로 이동 가능)
  2. q' \in \delta_B(q, L(s')) (명세 오토마타가 s'의 레이블 L(s')를 입력으로 받아 q에서 q'로 전이)
  • 수락 상태 집합: F_P = S \times F. 제품 상태의 명세 오토마타 성분이 수락 상태에 해당하는 모든 상태의 집합이다.

3. 제품 오토마톤 구성 알고리즘

3.1 기본 구성 절차

제품 오토마톤의 구성은 다음의 알고리즘적 절차를 따른다.

입력: 전이 시스템 \mathcal{T} = (S, s_0, \delta_T, AP, L), 뷔히 오토마타 \mathcal{B} = (Q, 2^{AP}, \delta_B, q_0, F)

출력: 제품 오토마톤 \mathcal{P} = (S_P, s_{P,0}, \delta_P, F_P)

절차:

  1. 초기 상태를 (s_0, q_0)로 설정하고, 이를 미탐색 대기열(unexplored queue)에 삽입한다.
  2. 대기열이 비어 있지 않은 동안 다음을 반복한다:
  • 대기열에서 현재 상태 (s, q)를 추출한다.
  • s의 모든 후속 상태 s' \in \text{Post}(s)에 대해:
  • 레이블 \sigma = L(s')를 계산한다.
  • q' \in \delta_B(q, \sigma)를 만족하는 모든 q'에 대해:
  • (s', q')가 새로운 상태이면 S_P에 추가하고 대기열에 삽입한다.
  • 전이 ((s, q), (s', q'))를 \delta_P에 추가한다.
  1. F_P = \{(s, q) \in S_P \mid q \in F\}로 수락 상태 집합을 설정한다.

이 알고리즘의 시간 복잡도는 O(\lvert S \rvert \cdot \lvert Q \rvert \cdot \lvert \delta_T \rvert \cdot \lvert \delta_B \rvert)이며, 공간 복잡도는 O(\lvert S \rvert \cdot \lvert Q \rvert)이다.

3.2 비결정론적 명세 오토마타의 처리

비결정론적 뷔히 오토마타(NBA)를 사용하는 경우, 하나의 전이 시스템 전이에 대해 복수의 명세 오토마타 전이가 발생할 수 있다. 이는 제품 오토마톤에서 분기(branching)를 초래하며, 결과적으로 비결정론적 제품 오토마톤이 생성된다.

비결정론성을 제거하기 위해 다음의 접근법이 사용된다:

  1. 사전 결정화: 명세 오토마타를 결정론적 형태(예: DRA)로 변환한 후 제품 오토마톤을 구성한다. 이 경우 제품 오토마톤은 결정론적이 되나, 명세 오토마타의 상태 수가 지수적으로 증가할 수 있다.
  2. 사후 탐색: 비결정론적 제품 오토마톤 위에서 중첩 깊이 우선 탐색(nested DFS) 등의 알고리즘을 적용하여 수락 경로를 탐색한다.

4. 제품 오토마톤 위에서의 경로 탐색

4.1 수락 경로의 존재 판정

제품 오토마톤 \mathcal{P} 위에서 임무를 만족하는 로봇 행동 시퀀스의 존재는, 초기 상태 s_{P,0}에서 출발하여 수락 상태 집합 F_P를 무한히 자주 경유하는 무한 경로(infinite run)의 존재와 동치이다.

뷔히 수락 조건 하에서, 수락 실행(accepting run) \rho = (s_0, q_0), (s_1, q_1), (s_2, q_2), \ldots는 다음 조건을 만족한다:

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

여기서 \text{Inf}(\rho)는 실행 \rho에서 무한히 자주 방문하는 상태 집합이다.

4.2 중첩 깊이 우선 탐색 알고리즘

수락 경로의 존재를 판정하는 표준적 알고리즘은 Courcoubetis, Vardi, Wolper, Yannakakis(1992)에 의해 제안된 중첩 깊이 우선 탐색(nested DFS) 알고리즘이다. 이 알고리즘은 두 단계의 깊이 우선 탐색을 수행한다:

외부 DFS: 초기 상태에서 출발하여 수락 상태에 도달하는 경로를 탐색한다.

내부 DFS: 발견된 수락 상태에서 출발하여 자기 자신으로 돌아오는 사이클을 탐색한다. 사이클이 존재하면 수락 상태를 무한히 자주 방문할 수 있으므로 수락 경로가 존재한다.

이 알고리즘의 시간 및 공간 복잡도는 모두 O(\lvert S_P \rvert + \lvert \delta_P \rvert), 즉 제품 오토마톤의 크기에 선형이다.

4.3 래소 형태의 실행 추출

수락 경로가 존재하는 경우, 로봇의 임무 수행 계획은 래소(lasso) 형태로 추출된다. 래소는 다음 두 부분으로 구성된다:

\rho = \underbrace{(s_0, q_0), (s_1, q_1), \ldots, (s_{k-1}, q_{k-1})}_{\text{접두사 (prefix)}} \cdot \underbrace{(s_k, q_k), (s_{k+1}, q_{k+1}), \ldots, (s_{k+l-1}, q_{k+l-1})}_{\text{주기 부분 (cycle)}}^\omega

접두사(prefix)는 초기 상태에서 사이클 시작점까지의 유한 경로이며, 주기 부분(cycle)은 수락 상태를 포함하는 유한 경로로서 무한히 반복된다. 로봇은 먼저 접두사에 해당하는 행동을 순차적으로 실행한 후, 주기 부분을 영구적으로 반복함으로써 임무 명세를 만족한다.

5. 최적 경로 탐색

5.1 가중 제품 오토마톤

단순한 임무 만족 여부를 넘어 최적의 행동 시퀀스를 도출하기 위해, 제품 오토마톤의 전이에 비용(cost) 또는 가중치(weight)를 부여한 가중 제품 오토마톤(weighted product automaton)을 구성할 수 있다.

\mathcal{P}_w = (S_P, s_{P,0}, \delta_P, F_P, w)

여기서 w: \delta_P \rightarrow \mathbb{R}_{\geq 0}는 각 전이에 대한 비용 함수이다. 비용은 통상적으로 물리적 이동 거리, 에너지 소모량, 또는 소요 시간에 대응한다.

5.2 최적 접두사와 최적 주기의 결합

최적 래소 경로를 탐색하기 위해서는 접두사 비용과 주기 비용을 동시에 고려해야 한다. Smith, Tumova, Belta, Rus(2011)는 다음과 같은 2단계 최적화 전략을 제안하였다:

  1. 최적 접두사 탐색: 초기 상태에서 각 수락 상태까지의 최단 경로를 Dijkstra 알고리즘 또는 A* 알고리즘으로 계산한다. 비용 c_{\text{prefix}}(s, q)를 각 수락 상태 (s, q) \in F_P에 대해 산출한다.

  2. 최적 주기 탐색: 각 수락 상태 (s, q) \in F_P에서 자기 자신으로 돌아오는 최단 경로의 비용 c_{\text{cycle}}(s, q)를 계산한다.

  3. 전체 최적 래소: 총 비용을 다음과 같이 정의하고 최소화하는 수락 상태를 선택한다.

(s^*, q^*) = \arg\min_{(s, q) \in F_P} \left( c_{\text{prefix}}(s, q) + \alpha \cdot c_{\text{cycle}}(s, q) \right)

여기서 \alpha \geq 0은 접두사와 주기 간 상대적 중요도를 조절하는 가중 계수이다. \alpha가 큰 경우 반복 실행의 효율성이 강조되며, \alpha = 0이면 초기 도달 비용만 고려된다.

6. 상태 폭발 문제와 완화 기법

6.1 상태 공간 크기 분석

제품 오토마톤의 상태 수는 전이 시스템과 명세 오토마타의 상태 수의 곱으로 결정된다:

\lvert S_P \rvert = \lvert S \rvert \cdot \lvert Q \rvert

LTL 공식 \varphi에서 변환된 NBA의 상태 수는 최악의 경우 2^{O(\lvert \varphi \rvert)}이므로, 제품 오토마톤의 상태 수는 \lvert S \rvert \cdot 2^{O(\lvert \varphi \rvert)}에 달할 수 있다. 다중 로봇 시스템에서 각 로봇이 k개의 영역을 가질 경우, 전이 시스템의 상태 수가 k^n으로 증가하여 상태 폭발 문제가 심화된다.

6.2 주요 완화 기법

  1. 지연 구성(on-the-fly construction): 제품 오토마톤의 전체 상태 공간을 사전에 구성하지 않고, 탐색 과정에서 필요한 상태와 전이만 점진적으로 생성한다. 이 기법은 도달 불가능한 상태의 불필요한 생성을 방지하여 메모리 사용을 절감한다.

  2. 기호적 구성(symbolic construction): 이진 결정 다이어그램(BDD: Binary Decision Diagram) 또는 만족 가능성 검사기(SAT solver)를 활용하여, 상태 집합과 전이 관계를 명시적으로 열거하지 않고 기호적으로 표현한다.

  3. 부분 순서 축소(partial order reduction): 동시에 발생하는 독립적 전이의 순서를 고정하여 탐색해야 할 인터리빙(interleaving)의 수를 감소시킨다.

  4. 추상화 기반 구성(abstraction-based construction): 전이 시스템을 추상화하여 상태 수를 줄인 후 제품 오토마톤을 구성하고, 필요 시 추상화를 정제하는 CEGAR(Counterexample-Guided Abstraction Refinement) 루프를 적용한다.

  5. 분산 제품 구성(distributed product construction): 다중 로봇 시스템에서 전체 곱 전이 시스템 대신 각 로봇의 개별 전이 시스템과 명세 오토마타의 부분 곱을 구성하여, 통합 제품 오토마톤의 크기를 감소시킨다.

7. 확장된 수락 조건의 제품 오토마톤

7.1 일반화된 뷔히 수락 조건

다수의 수락 상태 집합 F_1, F_2, \ldots, F_k를 가지는 일반화된 뷔히 오토마타(GBA: Generalized Büchi Automaton)에 대한 제품 오토마톤은 추가적인 카운터(counter)를 도입하여 구성된다.

\mathcal{P}_{\text{GBA}} = (S \times Q \times \{1, 2, \ldots, k\}, (s_0, q_0, 1), \delta_{P,\text{GBA}}, F_{P,\text{GBA}})

카운터 i는 현재 충족해야 할 수락 집합의 인덱스를 추적한다. 상태 (s, q, i)에서 경로가 수락 집합 F_i에 해당하는 상태를 방문하면 카운터가 (i \mod k) + 1로 순환적으로 증가한다. 수락 상태 집합은 F_{P,\text{GBA}} = S \times F_1 \times \{1\}로 설정된다.

7.2 라빈 수락 조건

결정론적 라빈 오토마타(DRA)를 사용하는 경우, 수락 조건은 라빈 쌍(Rabin pair) \{(L_i, U_i)\}_{i=1}^{k}으로 주어진다. 무한 실행 \rho가 수락되려면, 적어도 하나의 라빈 쌍 (L_i, U_i)에 대해 \text{Inf}(\rho) \cap L_i = \emptyset이고 \text{Inf}(\rho) \cap U_i \neq \emptyset이어야 한다. 라빈 제품 오토마톤에서의 수락 경로 탐색은 뷔히 경우보다 복잡하나, 결정론성이 보장되므로 전략 추출이 직접적으로 가능하다.

8. 로봇 임무 계획에의 적용 사례

8.1 단일 로봇 순찰 임무

로봇이 n개의 관심 영역 \{r_1, r_2, \ldots, r_n\}을 순환적으로 방문하면서 위험 영역 D를 회피해야 하는 순찰 임무를 고려하자. 임무 명세는 다음과 같이 기술된다:

\varphi = \bigwedge_{i=1}^{n} \square \Diamond r_i \wedge \square \neg D

이 명세를 뷔히 오토마타로 변환하면 n+1개의 상태를 가지는 일반화된 뷔히 오토마타가 생성된다. 작업 공간이 m개의 이산 영역으로 분할된 경우, 제품 오토마톤의 상태 수는 O(m \cdot (n+1))이다.

8.2 다중 로봇 협력 임무

다중 로봇 시스템에서는 각 로봇의 전이 시스템을 합성하여 전체 팀의 합성 전이 시스템(composite transition system)을 구성한 후, 이를 명세 오토마타와 곱하여 제품 오토마톤을 생성한다.

N대의 로봇이 각각 m개의 영역을 가질 때, 합성 전이 시스템의 상태 수는 m^N이며, 제품 오토마톤의 상태 수는 m^N \cdot \lvert Q \rvert로 급격히 증가한다. 이 문제를 해결하기 위해 Kloetzer와 Belta(2010)는 명세 분해(specification decomposition) 기법을 제안하여, 전체 명세를 각 로봇의 지역 명세로 분할하고 개별적으로 제품 오토마톤을 구성하는 방법을 개발하였다.

9. 구현 도구와 라이브러리

제품 오토마톤의 구성과 경로 탐색을 지원하는 대표적 도구는 다음과 같다:

  • SPOT (Synthesis of Omega-automata from Temporal logic): LTL 공식을 다양한 유형의 오메가 오토마타로 변환하고, 제품 오토마톤의 구성 및 공허성 검사(emptiness check)를 수행하는 C++ 기반 라이브러리이다(Duret-Lutz et al., 2016).
  • TuLiP: Python 기반의 임무 계획 도구로, 전이 시스템 모델링, 명세 오토마타 변환, 제품 오토마톤 구성 및 최적 경로 탐색을 통합적으로 지원한다.
  • LTLMoP: MATLAB 기반의 로봇 임무 계획 프레임워크로, 제품 오토마톤 기반 제어기 자동 합성 기능을 제공한다.
  • lomap (LTL Optimal Multi-Agent Planner): Python과 NetworkX 기반의 다중 로봇 임무 계획 라이브러리로, 가중 제품 오토마톤 위에서의 최적 경로 탐색 알고리즘을 구현한다(Ulusoy et al., 2013).

10. 참고 문헌

  • 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.
  • Gastin, P., Oddoux, D. (2001). “Fast LTL to Büchi Automata Translation.” Proceedings of CAV 2001, LNCS, vol. 2102, pp. 53–65.
  • Kloetzer, M., Belta, C. (2010). “Automatic Deployment of Distributed Teams of Robots from Temporal Logic Motion Specifications.” IEEE Transactions on Robotics, 26(1), pp. 48–63.
  • 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.
  • Ulusoy, A., Smith, S.L., Ding, X.C., Belta, C., Rus, D. (2013). “Optimality and Robustness in Multi-Robot Path Planning with Temporal Logic Constraints.” The International Journal of Robotics Research, 32(8), pp. 889–911.
  • 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