397.51 반응형 합성(Reactive Synthesis)과 임무 계획

397.51 반응형 합성(Reactive Synthesis)과 임무 계획

1. 개요

반응형 합성(reactive synthesis)은 동적으로 변화하는 환경에 실시간으로 대응하는 제어 전략을 형식 명세(formal specification)로부터 자동으로 생성하는 기법이다. 고전적 계획(classical planning)이 환경을 정적이고 완전히 예측 가능한 것으로 가정하는 반면, 반응형 합성은 환경을 적대적(adversarial) 또는 비결정론적 행위자로 간주하여, 환경의 임의의 행동에 대해서도 명세를 만족시키는 시스템 전략의 존재 여부를 판정하고 해당 전략을 추출한다.

로봇 임무 계획에서 반응형 합성의 적용은 환경의 불확실성에 대한 강건성(robustness)을 보장하면서도, 형식적 정확성(formal correctness)을 유지하는 제어기를 자동으로 도출할 수 있다는 점에서 의의가 있다. 특히, 합성된 제어기는 설계에 의해 정확(correct-by-construction)하므로, 사후 검증(post-hoc verification)이 불필요하다.

2. 반응형 합성의 이론적 기반

2.1 합성 문제의 정의

반응형 합성 문제는 Church(1957)가 최초로 제기한 합성 문제(synthesis problem)의 현대적 해석이다. 문제의 형식적 정의는 다음과 같다.

주어진 것:

  • 환경 변수 집합 \mathcal{X}: 로봇이 관측하는 센서 입력(환경이 결정)
  • 시스템 변수 집합 \mathcal{Y}: 로봇이 출력하는 행동 명령(시스템이 결정)
  • 명세 \varphi: \mathcal{X}와 \mathcal{Y} 위에 정의된 LTL 공식

목표: 전략 함수 f: (2^{\mathcal{X}})^+ \rightarrow 2^{\mathcal{Y}}를 찾되, 환경의 임의의 무한 입력 시퀀스 x_0, x_1, x_2, \ldots에 대해 시스템이 y_i = f(x_0, \ldots, x_i)를 출력할 때, 결합된 행동 시퀀스 (x_0 \cup y_0), (x_1 \cup y_1), \ldots가 \varphi를 만족하도록 한다.

2.2 실현 가능성과 결정 불가능성

명세 \varphi가 실현 가능(realizable)하다 함은 환경의 모든 전략에 대해 명세를 만족시키는 시스템 전략이 존재함을 의미한다. 실현 불가능(unrealizable)한 경우, 어떤 시스템 전략도 모든 환경 행동에 대해 명세를 보장할 수 없다.

일반적 LTL 명세에 대한 실현 가능성 판정은 2EXPTIME-완전(2EXPTIME-complete) 문제이다(Pnueli, Rosner, 1989). 명세의 크기에 대해 이중 지수적 시간이 소요되므로, 대규모 명세에 대한 직접적 합성은 실용적으로 제한된다.

2.3 게임 이론적 해석

반응형 합성은 환경(player 0)과 시스템(player 1) 사이의 2인 무한 게임(two-player infinite game)으로 모델링된다. 게임의 각 라운드에서:

  1. 환경이 입력 x_i \in 2^{\mathcal{X}}를 선택한다.
  2. 시스템이 출력 y_i \in 2^{\mathcal{Y}}를 선택한다.
  3. 이 과정이 무한히 반복된다.

시스템의 승리 조건은 결과적 무한 실행이 명세 \varphi를 만족하는 것이다. 명세가 실현 가능한 경우, 시스템에는 승리 전략(winning strategy)이 존재하며, 이 승리 전략이 반응형 제어기에 해당한다.

3. GR(1) 반응형 합성

3.1 GR(1) 명세의 형식

GR(1)(Generalized Reactivity(1)) 합성은 Piterman, Pnueli, Sa’ar(2006)에 의해 제안된 효율적 합성 프레임워크로서, 임무 계획에 실용적으로 적용 가능한 다항 시간 합성을 제공한다. GR(1) 명세는 다음의 구조를 갖는 가정-보장(assume-guarantee) 형태의 공식이다:

\varphi = \varphi_e \rightarrow \varphi_s

환경 가정 \varphi_e와 시스템 보장 \varphi_s는 각각 다음의 세 부분으로 구성된다:

환경 가정:

  • 초기 조건: \theta_e — 초기 시점에서 환경 변수가 만족해야 할 명제
  • 전이 조건: \square \rho_e — 매 시점에서의 환경 변수 전이 제약
  • 공정성 가정: \bigwedge_{i=1}^{m} \square \Diamond J_e^i — 환경이 무한히 자주 충족할 것으로 가정하는 조건

시스템 보장:

  • 초기 조건: \theta_s — 초기 시점에서 시스템 변수가 만족해야 할 명제
  • 전이 조건: \square \rho_s — 매 시점에서의 시스템 변수 전이 제약
  • 활성 목표: \bigwedge_{j=1}^{n} \square \Diamond J_s^j — 시스템이 무한히 자주 달성해야 하는 목표

3.2 GR(1) 합성 알고리즘

GR(1) 합성은 3중 중첩 고정점 반복(triply nested fixed-point iteration)을 통해 수행된다. 합성 게임의 승리 영역 W는 다음과 같이 계산된다:

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

여기서 \text{CPre}(X)는 제어 전임자(controllable predecessor) 연산자로, 환경의 임의의 행동에 대해 시스템이 집합 X로 전이할 수 있는 상태 집합이다:

\text{CPre}(X) = \{s \mid \forall x \in 2^{\mathcal{X}}, \exists y \in 2^{\mathcal{Y}} : \text{succ}(s, x, y) \in X\}

시간 복잡도: O(N^2 \cdot n \cdot m). 여기서 N은 게임 상태 수, n은 시스템 목표 수, m은 환경 가정 수이다. 이는 일반적 LTL 합성의 2EXPTIME과 비교하여 극적으로 효율적이다.

3.3 제어기 추출

고정점 계산 결과로부터 유한 상태 제어기(finite-state controller)가 Mealy 기계(Mealy machine) 형태로 추출된다:

\mathcal{C} = (M, m_0, 2^{\mathcal{X}}, 2^{\mathcal{Y}}, \delta_M, \lambda)

여기서 M은 내부 메모리 상태 집합(시스템 목표의 인덱스 \{1, \ldots, n\}에 대응), m_0는 초기 메모리 상태, \delta_M은 메모리 전이 함수, \lambda는 출력 함수이다.

제어기의 동작 원리는 다음과 같다:

  1. 현재 시스템 목표 J_s^j를 추적하는 메모리 상태 j를 유지한다.
  2. 각 시점에서 환경 입력 x_i를 관측한다.
  3. 현재 목표와 환경 입력, 현재 상태에 기반하여 시스템 출력 y_i를 생성한다.
  4. 목표 J_s^j가 달성되면 다음 목표 J_s^{(j \mod n) + 1}로 전환한다.

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

4.1 임무 명세의 GR(1) 인코딩

로봇 임무를 GR(1) 명세로 변환하는 과정은 다음과 같다:

시스템 변수: 로봇의 위치, 내부 상태(예: 적재 여부, 수집 여부)를 불리안 변수로 인코딩한다.

환경 변수: 동적 장애물의 위치, 요청 발생 여부, 문의 개폐 상태 등을 불리안 변수로 인코딩한다.

전이 제약: 로봇의 물리적 이동 가능성(인접 영역으로만 이동)과 환경의 동작 규칙(장애물 이동 패턴)을 전이 제약으로 명세한다.

활성 목표: “영역 A를 무한히 자주 방문하라”, “요청이 발생하면 서비스를 제공하라” 등의 임무를 활성 목표로 명세한다.

4.2 적용 사례: 자율 서비스 로봇

건물 내부를 순찰하면서 요청에 응답하는 자율 서비스 로봇의 임무를 GR(1) 명세로 표현한 사례를 고려하자.

환경 가정:

  • 동적 장애물은 인접 셀로만 이동한다: \square \rho_{\text{obstacle}}
  • 요청은 결국 발생한다: \square \Diamond \text{request}

시스템 보장:

  • 로봇은 인접 셀로만 이동한다: \square \rho_{\text{robot}}
  • 장애물이 있는 셀로는 이동하지 않는다: \square \neg \text{collision}
  • 순찰 지점 A, B, C를 무한히 자주 방문한다: \square \Diamond \text{at\_A} \wedge \square \Diamond \text{at\_B} \wedge \square \Diamond \text{at\_C}
  • 요청이 발생하면 결국 서비스를 제공한다: \square (\text{request} \rightarrow \Diamond \text{service})

이 명세에 대해 GR(1) 합성을 수행하면, 동적 장애물을 회피하면서 순찰과 서비스 제공을 동시에 수행하는 반응형 제어기가 자동으로 생성된다.

4.3 Kress-Gazit 프레임워크

Kress-Gazit, Fainekos, Pappas(2009)는 LTL 기반 반응형 임무 계획과 운동 계획(motion planning)을 결합한 통합 프레임워크를 제안하였다. 이 프레임워크의 구조는 다음과 같다:

  1. 고수준 계층: GR(1) 합성을 통해 이산적 임무 전략을 도출한다.
  2. 저수준 계층: 각 이산 전이에 대응하는 연속 제어기를 설계하여 로봇의 연속 동역학을 제어한다.
  3. 인터페이스: 이산 전략의 각 전이에 대해 연속 제어기의 실현 가능성을 보장하는 시뮬레이션 관계(simulation relation)를 확립한다.

5. 합성 도구

5.1 SLUGS

SLUGS(SmaLl bUt Complete GRone Synthesizer)는 Ehlers(2010)에 의해 개발된 GR(1) 합성 전용 도구이다. BDD(Binary Decision Diagram) 기반 기호적 알고리즘을 구현하여 대규모 상태 공간에 대한 합성을 효율적으로 수행한다.

주요 특징:

  • 기호적 고정점 계산을 통한 메모리 효율적 합성
  • 반례 기반 비실현 가능성 진단(unrealizability diagnosis)
  • 합성된 제어기의 자동 시뮬레이션 기능
  • 구조적 입력 형식(structuredSlugsPlus)을 통한 명세 작성 지원

5.2 LTLMoP

LTLMoP(Linear Temporal Logic MissiOn Planning)은 Finucane, Jing, Kress-Gazit(2010)이 개발한 로봇 임무 계획 전용 프레임워크이다. 자연어에 가까운 구조적 영어(structured English)로부터 GR(1) 명세를 자동 생성하고, SLUGS를 백엔드로 사용하여 합성을 수행한 후, 로봇 시뮬레이터 또는 실제 로봇에 제어기를 배포한다.

5.3 TuLiP

TuLiP(Temporal Logic Planning Toolbox)은 California Institute of Technology에서 개발한 Python 기반 오픈 소스 도구이다. GR(1) 합성을 핵심 기능으로 제공하며, 연속 동역학 시스템의 이산 추상화(discrete abstraction)와 합성된 제어기의 로봇 미들웨어(ROS2 등) 연동을 지원한다.

5.4 Strix

Strix는 Meyer, Sickert, Luttenberger(2018)에 의해 개발된 LTL 합성 도구로, 파리티 게임(parity game) 기반 합성 알고리즘을 구현한다. SYNTCOMP(Synthesis Competition)에서 다수의 우승을 기록하였으며, GR(1) 범위 밖의 일반적 LTL 명세에 대해서도 효율적 합성을 수행한다.

6. 반응형 합성의 확장

6.1 수량적 합성(Quantitative Synthesis)

순수한 불리안 만족/위반 판정을 넘어, 비용이나 성능의 수량적 최적화를 포함하는 수량적 합성이 연구되고 있다. 예를 들어, 명세를 만족하면서 이동 거리를 최소화하는 전략의 합성이 이에 해당한다. Bloem, Chatterjee, Henzinger, Jobstmann(2009)은 평균 비용 게임(mean-payoff game)과 시제 논리 명세를 결합하는 프레임워크를 제안하였다.

6.2 점진적 합성(Incremental Synthesis)

환경이나 임무 명세가 실행 중 변경될 때, 처음부터 합성을 재수행하는 대신 이전 합성 결과를 활용하여 점진적으로 제어기를 갱신하는 점진적 합성 기법이 개발되고 있다. Livingston, Murray(2013)는 새로운 환경 가정이나 시스템 목표가 추가될 때 기존 승리 영역을 점진적으로 갱신하는 알고리즘을 제안하였다.

6.3 다중 에이전트 반응형 합성

다수의 로봇이 협력적으로 임무를 수행하는 다중 에이전트 환경에서의 반응형 합성은 상태 공간의 지수적 증가로 인해 난해하다. 분산 합성(distributed synthesis)과 합성적 합성(compositional synthesis) 등의 접근법을 통해 각 에이전트의 전략을 개별적으로 또는 부분적으로 합성하고 이를 통합하는 방법이 연구되고 있다.

6.4 학습 기반 반응형 합성

환경 모델이 사전에 완전히 알려지지 않은 경우, 강화 학습(reinforcement learning)을 통해 환경 모델을 점진적으로 학습하면서 반응형 제어기를 합성하는 하이브리드 접근법이 탐색되고 있다. Hasanbeig, Abate, Kroening(2019)의 연구에서는 LTL 명세를 보상 신호(reward signal)로 변환하여, 형식적 보장과 학습의 적응성을 결합하는 프레임워크를 제안하였다.

7. 한계와 과제

7.1 명세 작성의 난이도

GR(1) 합성의 효율성에도 불구하고, 실제 로봇 임무를 GR(1) 형태로 정확히 인코딩하는 것은 전문적 지식을 요구한다. 환경 가정의 불완전성은 비현실적 제어기를, 과도한 가정은 불필요하게 보수적인 전략을 생성할 수 있다.

7.2 비실현 가능성 진단

명세가 비실현 가능한 경우, 그 원인을 진단하고 명세를 수정하는 과정이 필요하다. Konighofer, Hofferek, Bloem(2013)은 비실현 가능 명세에 대해 최소한의 환경 가정 완화(environment assumption weakening)를 통해 실현 가능성을 회복하는 기법을 제안하였다.

7.3 이산화 간극

연속 로봇 동역학과 이산 합성 결과 사이의 간극(abstraction gap)은 합성된 제어기의 실제 실행 가능성을 저해할 수 있다. 이산 추상화의 정확성을 형식적으로 보장하기 위해 시뮬레이션 관계(simulation relation) 또는 교대 시뮬레이션(alternating simulation)이 활용된다.

8. 참고 문헌

  • 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.
  • Pnueli, A., Rosner, R. (1989). “On the Synthesis of a Reactive Module.” Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 179–190.
  • 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., Chatterjee, K., Henzinger, T.A., Jobstmann, B. (2009). “Better Quality in Synthesis through Quantitative Objectives.” Proceedings of CAV 2009, LNCS, vol. 5643, pp. 140–156.
  • Finucane, C., Jing, G., Kress-Gazit, H. (2010). “LTLMoP: Experimenting with Language, Temporal Logic and Robot Control.” Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 1988–1993.
  • Ehlers, R. (2010). “Symbolic Bounded Synthesis.” Proceedings of CAV 2010, LNCS, vol. 6174, pp. 365–379.
  • 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.
  • Livingston, S.C., Murray, R.M. (2013). “Just-in-Time Synthesis for Reactive Motion Planning with Temporal Logic.” Proceedings of the IEEE International Conference on Robotics and Automation (ICRA), pp. 532–538.
  • Konighofer, R., Hofferek, G., Bloem, R. (2013). “Debugging Formal Specifications: A Practical Approach Using Model-Based Diagnosis and Counterstrategies.” International Journal on Software Tools for Technology Transfer, 15(5–6), pp. 563–583.
  • Meyer, P.J., Sickert, S., Luttenberger, M. (2018). “Strix: Explicit Reactive Synthesis Strikes Back!” Proceedings of CAV 2018, LNCS, vol. 10981, pp. 578–586.
  • 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