397.66 행동 트리와 형식 논리 기반 계획의 결합

397.66 행동 트리와 형식 논리 기반 계획의 결합

1. 개요

행동 트리(Behavior Tree, BT)는 로봇 행동의 모듈적 구성과 반응적 실행에 탁월한 프레임워크이나, 임무 명세의 형식적 정확성과 검증 가능성에서는 형식 논리(formal logic) 기반 접근법에 미치지 못한다. 반대로, 선형 시제 논리(LTL), 계산 트리 논리(CTL) 등의 형식 논리는 임무 요구사항을 엄밀하게 명세하고 자동 검증할 수 있지만, 생성된 제어 정책을 로봇에 직접 배포하고 실행하는 데에는 추가적인 변환이 필요하다.

본 절에서는 형식 논리 기반 임무 명세와 행동 트리 기반 실행 아키텍처를 결합하는 방법론을 다룬다. 이를 통해 형식적 정확성(formal correctness)과 실행적 유연성(execution flexibility)을 동시에 확보하는 통합 프레임워크를 구축한다.

2. 형식 논리와 행동 트리의 관계

2.1 표현력 비교

형식 논리와 행동 트리는 서로 다른 추상화 수준에서 로봇 행동을 기술한다.

측면형식 논리 (LTL/CTL)행동 트리 (BT)
명세 수준“무엇을 달성할 것인가” (선언적)“어떻게 행동할 것인가” (절차적)
표현 대상시간적 속성, 안전성/활동성행동 구성, 실행 흐름
형식 검증직접 지원 (모델 검사)간접 지원 (변환 후 검사)
실행 가능성오토마타 합성 후 실행직접 실행 가능
반응성환경 모델 의존내재적 반응성
모듈성논리식 결합서브트리 합성

두 프레임워크의 강점은 상호 보완적이므로, 결합을 통해 단독 사용 시의 한계를 극복할 수 있다.

2.2 의미론적 대응 관계

행동 트리의 기본 구성 요소는 형식 논리의 시간적 연산자와 다음과 같은 의미론적 대응을 가진다(Colledanchise & Ögren, 2017).

  • 시퀀스 노드: LTL의 순서 연산 \varphi_1 \,\mathbf{U}\, (\varphi_2 \,\mathbf{U}\, (\cdots \,\mathbf{U}\, \varphi_k))에 대응한다. 모든 자식이 순서대로 성공해야 한다.
  • 폴백 노드: 비결정적 선택(nondeterministic choice) \varphi_1 \lor \varphi_2 \lor \cdots \lor \varphi_k에 대응한다.
  • 데코레이터(반복): 항상성(always) 연산자 \mathbf{G}\,\varphi의 구현에 활용된다.

이러한 대응은 정확한 동치가 아니라 근사적 관계이며, 행동 트리의 실행 의미론(틱 기반 재평가)과 형식 논리의 선언적 의미론 사이에는 미묘한 차이가 존재한다.

3. LTL 명세로부터의 행동 트리 합성

3.1 오토마타 기반 변환 파이프라인

LTL 형식 명세 \varphi로부터 행동 트리를 자동 합성하는 표준 파이프라인은 다음 단계로 구성된다.

  1. LTL → 뷔히 오토마톤: LTL 명세 \varphi를 등가의 비결정적 뷔히 오토마톤(Nondeterministic Büchi Automaton, NBA) \mathcal{A}_\varphi로 변환한다.
  2. 환경 모델 구성: 로봇의 전이 시스템(Transition System) \mathcal{T}를 구성한다.
  3. 제품 오토마톤 구성: \mathcal{P} = \mathcal{T} \otimes \mathcal{A}_\varphi를 구성한다.
  4. 승인 실행 경로 탐색: \mathcal{P}에서 수용 조건을 만족하는 경로를 탐색한다.
  5. 행동 트리 변환: 탐색된 실행 경로를 행동 트리 구조로 변환한다.

마지막 단계의 변환 규칙은 다음과 같다.

순차 실행 경로: 상태 전이 시퀀스 (s_0, a_1, s_1, a_2, \ldots, s_k)는 시퀀스 노드로 변환된다.

Sequence
├── Condition(s₀)
├── Action(a₁)
├── Condition(s₁)
├── Action(a₂)
├── ...

분기 구조: 상태 s에서 복수의 전이가 가능한 경우, 폴백 노드로 변환된다.

Fallback
├── Sequence [분지 1]
│   ├── Condition(guard₁)
│   └── Action(a₁)
├── Sequence [분지 2]
│   ├── Condition(guard₂)
│   └── Action(a₂)

반복 구조: 뷔히 오토마톤의 수용 조건에 의한 무한 반복 패턴은 데코레이터의 반복 노드로 구현된다.

3.2 LTL 명세 분해에 의한 모듈적 합성

복잡한 LTL 명세 \varphi = \varphi_1 \land \varphi_2 \land \cdots \land \varphi_m을 부분 명세(sub-specification)로 분해하고, 각 부분 명세에 대해 독립적으로 행동 서브트리를 합성한 후, 이를 병렬 노드로 결합하는 방법이다.

T(\varphi) = \text{Parallel}\left(T(\varphi_1), T(\varphi_2), \ldots, T(\varphi_m)\right)

이 접근법의 장점은 각 부분 명세의 오토마톤 크기가 전체 명세에 비해 현저히 작으므로, 상태 공간 폭발(state-space explosion) 문제를 완화할 수 있다는 것이다. 그러나 부분 명세 간의 상호작용(예: 공유 자원)이 존재하는 경우, 합성된 행동 트리가 원래의 전체 명세를 만족하는지 별도의 검증이 필요하다.

4. STL 명세와 행동 트리의 결합

4.1 신호 시제 논리(STL)의 강건성 기반 행동 선택

신호 시제 논리(STL)는 연속 시간 신호에 대한 속성을 명세하며, 강건성 의미론(robustness semantics)을 통해 명세 만족의 정도를 정량적으로 평가할 수 있다. 행동 트리와의 결합에서는 STL 강건도를 행동 선택의 기준으로 활용한다.

폴백 노드의 자식 선택 시, 각 대안 행동 a_i의 예상 STL 강건도 \rho(\varphi, a_i)를 평가하여 강건도가 가장 높은 행동을 우선 선택한다.

a^* = \arg\max_{a_i} \rho(\varphi, \xi_{a_i})

여기서 \xi_{a_i}는 행동 a_i를 실행했을 때의 예상 신호 궤적이다. 이 방법은 이산적 만족/불만족 판정을 넘어, 명세 만족의 마진을 최대화하는 행동을 선택할 수 있게 한다.

4.2 강건도 기반 행동 트리 최적화

행동 트리의 구조와 파라미터를 STL 강건도로 최적화하는 문제를 다음과 같이 정식화할 수 있다.

\max_{\theta} \rho(\varphi, \xi_\theta)

여기서 \theta는 행동 트리의 파라미터(액션의 지속 시간, 이동 속도, 대기 시간 등)이고, \xi_\theta는 해당 파라미터로 실행된 신호 궤적이다.

경사 기반 최적화가 가능한 경우(미분 가능한 강건도 함수), 역전파(backpropagation)를 통해 효율적으로 최적 파라미터를 탐색할 수 있다(Gilpin et al., 2021).

5. 반응형 합성과 행동 트리의 결합

5.1 GR(1) 합성 기반 전략 생성

**일반화된 반응성 명세(Generalized Reactivity of rank 1, GR(1))**는 효율적인 반응형 합성이 가능한 LTL의 부분 클래스이다. GR(1) 합성은 환경의 적대적 행동에도 불구하고 명세를 만족하는 제어 전략을 다항 시간에 생성할 수 있다(Bloem et al., 2012).

GR(1) 명세는 다음 형태를 가진다.

\varphi = \left(\bigwedge_{i} \mathbf{G}\,\mathbf{F}\, \psi_i^{\text{env}}\right) \rightarrow \left(\bigwedge_{j} \mathbf{G}\,\mathbf{F}\, \psi_j^{\text{sys}}\right)

합성된 제어 전략을 행동 트리로 변환하는 과정은 다음과 같다.

  1. 합성 결과인 유한 상태 전략(finite-state strategy) \sigma: S_{\text{env}} \rightarrow A_{\text{sys}}를 추출한다.
  2. 각 상태-행동 쌍을 조건-액션 구조로 변환한다.
  3. 전략의 분기 구조를 폴백 노드로, 순차 구조를 시퀀스 노드로 매핑한다.

5.2 점진적 합성과 행동 트리 증분 구축

전체 명세에 대한 합성이 계산적으로 과중한 경우, 명세를 점진적으로 추가하면서 행동 트리를 증분적으로 확장하는 방법이 있다.

T_k = \text{Extend}(T_{k-1}, \varphi_k)

각 단계에서는 새로운 부분 명세 \varphi_k를 만족시키기 위한 서브트리를 합성하고, 기존 트리와의 충돌을 검사한 후 통합한다. 충돌이 발생하면 중재 메커니즘(mediation mechanism)을 통해 우선순위에 따라 해결한다.

6. 형식 보장(Formal Guarantee)의 실행 시 유지

6.1 실행 중 명세 만족 모니터링

행동 트리 실행 과정에서 형식 논리 명세의 만족 여부를 실시간으로 모니터링하는 런타임 검증(runtime verification) 시스템을 결합한다. 런타임 모니터는 로봇의 실행 궤적 \xi를 관찰하고, 각 시점에서 명세 \varphi에 대한 판정을 수행한다.

\text{verdict}(t) = \begin{cases} \top & \text{if } \xi[0:t] \models \varphi \\ \bot & \text{if } \xi[0:t] \not\models \varphi \\ ? & \text{if 판정 불가 (미래 의존)} \end{cases}

LTL 명세의 3-값 의미론(three-valued semantics)을 적용하여, 현재까지의 실행이 명세를 이미 위반했는지, 만족이 확정되었는지, 또는 미래의 행동에 따라 결정되는지를 구분한다(Bauer et al., 2011).

6.2 위반 감지 시 복구 전략

런타임 모니터가 명세 위반을 감지하면, 행동 트리에 삽입된 **복구 서브트리(recovery subtree)**가 활성화된다. 복구 전략의 유형은 다음과 같다.

  • 롤백(Rollback): 마지막으로 알려진 안전 상태로 복귀한다.
  • 대안 행동(Alternative Action): 폴백 노드를 통해 대안적 행동을 시도한다.
  • 재계획(Replanning): 심의 계층에 재계획을 요청하고, 새로운 행동 트리를 수신한다.
  • 안전 모드(Safe Mode): 최소한의 안전 행동(정지, 귀환 등)을 실행한다.

복구 서브트리의 구조:

Fallback
├── Condition(명세 만족 중)
├── Sequence [복구 시도]
│   ├── Action(복구 행동)
│   └── Condition(명세 회복 확인)
└── Action(안전 모드 전환)

7. 확장성과 계산 효율성

7.1 상태 공간 축소 기법

형식 논리 기반 합성의 주요 한계는 상태 공간의 지수적 증가이다. 행동 트리와의 결합에서는 다음 기법으로 이를 완화한다.

  • 추상화(Abstraction): 로봇의 연속 상태 공간을 유한 심볼릭 영역으로 추상화하여 오토마톤의 상태 수를 제한한다.
  • 합성 후 구체화(Synthesize-then-Refine): 추상화된 상태 공간에서 합성을 수행한 후, 행동 트리의 액션 노드 레벨에서 연속 제어를 구체화한다.
  • 게으른 합성(Lazy Synthesis): 실행 시점에 필요한 상태-전이만을 합성하여, 전체 상태 공간의 미리 합성(pre-synthesis)을 회피한다.

7.2 온라인 합성과 행동 트리의 동적 확장

실시간 임무 변경에 대응하기 위해, 런타임에 형식 논리 합성과 행동 트리 생성을 동적으로 수행하는 방법이 연구되고 있다. 이를 위해 합성 알고리즘의 병렬화, 증분 합성, 캐싱 기법 등이 적용된다.

8. 참고 문헌

  • Bauer, A., Leucker, M., & Schallhart, C. (2011). “Runtime Verification for Linear Temporal Logic.” Theoretical Computer Science, 412(12–14), 1382–1398.
  • 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), 911–938.
  • Colledanchise, M., & Ögren, P. (2017). “How Behavior Trees Modularize Hybrid Control Systems and Generalize Sequential Behavior Compositions, the Subsumption Architecture, and Decision Trees.” IEEE Transactions on Robotics, 33(2), 372–389.
  • Gilpin, Y., Kurtz, V., & Lin, H. (2021). “A Smooth Robustness Measure of Signal Temporal Logic for Symbolic-Geometric Planning.” IEEE Control Systems Letters, 5(1), 241–246.
  • Tumova, J., & Dimarogonas, D. V. (2016). “Multi-Agent Planning Under Local LTL Specifications and Event-Based Synchronization.” Automatica, 70, 239–248.