1291.83 행동 트리의 형식적 정의와 분석 연구

1291.83 행동 트리의 형식적 정의와 분석 연구

1. 개요

행동 트리(Behavior Tree, BT)의 형식적 정의와 분석 연구는 행동 트리를 엄밀한 수학적 객체로 정의하고, 그 실행 의미론(operational semantics), 표현력(expressiveness), 구성 가능성(compositionality) 등의 속성을 이론적으로 분석하는 학술 분야이다. 본 절에서는 행동 트리의 형식적 정의에 관한 주요 연구 성과와 분석 방법론을 체계적으로 기술한다.

2. 행동 트리의 형식적 수학 구조

행동 트리의 최초의 체계적 형식화는 Colledanchise와 Ögren(2018)의 저서 Behavior Trees in Robotics and AI: An Introduction에서 제시되었다. 이 연구에서 행동 트리는 다음과 같이 정의된다.

행동 트리 \mathcal{T}는 유한 방향 루트 트리(finite directed rooted tree)로서, 각 노드 n_i는 부모로부터 Tick 신호를 수신하면 실행되며, 실행 완료 후 부모에게 반환 상태 s \in \{Success, Failure, Running\} 중 하나를 반환한다. 루트 노드는 외부 제어 루프로부터 주기적으로 Tick 신호를 수신하며, 이 신호가 트리 전체에 깊이 우선(depth-first) 방식으로 전파된다.

형식적으로, 행동 트리는 다음의 4-튜플로 정의할 수 있다:

\mathcal{T} = (N, E, r, \tau)

여기서 N은 노드의 유한 집합, E \subseteq N \times N은 방향 간선의 집합, r \in N은 루트 노드, \tau: N \rightarrow \{Sequence, Fallback, Parallel, Action, Condition, Decorator\}는 각 노드의 타입을 결정하는 타입 함수이다.

3. 실행 의미론의 형식화

행동 트리의 실행 의미론은 구조적 조작 의미론(Structural Operational Semantics, SOS) 프레임워크를 통해 형식화된다. Colledanchise와 Ögren(2014)은 How Behavior Trees Modularize Hybrid Control Systems and Generalize Sequential Behavior Compositions, the Subsumption Architecture, and Decision Trees에서 행동 트리의 각 제어 노드(Sequence, Fallback, Parallel)에 대한 실행 규칙을 추론 규칙(inference rule) 형태로 명세하였다.

3.1 Sequence 노드의 실행 규칙

Sequence 노드는 자식 노드를 좌측부터 순차적으로 실행하며, 첫 번째로 Failure 또는 Running을 반환하는 자식을 만나면 해당 상태를 부모에게 반환한다. 모든 자식이 Success를 반환하면 Sequence 자체도 Success를 반환한다. 이를 추론 규칙으로 표현하면 다음과 같다:

\frac{\text{child}_i \rightarrow \text{Success} \quad \forall i \in \{1, \ldots, n\}}{\text{Sequence}(\text{child}_1, \ldots, \text{child}_n) \rightarrow \text{Success}}

\frac{\text{child}_i \rightarrow \text{Failure}}{\text{Sequence}(\text{child}_1, \ldots, \text{child}_n) \rightarrow \text{Failure}}

3.2 Fallback 노드의 실행 규칙

Fallback 노드(또는 Selector 노드)는 자식 노드를 좌측부터 순차적으로 실행하며, 첫 번째로 Success 또는 Running을 반환하는 자식을 만나면 해당 상태를 부모에게 반환한다. 모든 자식이 Failure를 반환하면 Fallback 자체도 Failure를 반환한다.

\frac{\text{child}_i \rightarrow \text{Success}}{\text{Fallback}(\text{child}_1, \ldots, \text{child}_n) \rightarrow \text{Success}}

\frac{\text{child}_i \rightarrow \text{Failure} \quad \forall i \in \{1, \ldots, n\}}{\text{Fallback}(\text{child}_1, \ldots, \text{child}_n) \rightarrow \text{Failure}}

4. 표현력 분석

행동 트리의 표현력(expressiveness)에 관한 형식적 분석은 행동 트리가 다른 행동 제어 아키텍처를 일반화할 수 있는지를 이론적으로 규명하는 연구이다. Colledanchise와 Ögren(2014)은 다음의 핵심적 결과를 형식적으로 증명하였다:

  1. 순차 행동 합성(Sequential Behavior Composition)의 일반화: 행동 트리의 Sequence 노드는 순차적 행동 합성을 자연스럽게 표현하며, 이는 명령형 프로그래밍의 순차 실행 구조와 형식적으로 동치이다.

  2. 포괄 아키텍처(Subsumption Architecture)의 일반화: 행동 트리의 Fallback 노드는 Brooks(1986)의 포괄 아키텍처에서 우선순위 기반 행동 선택을 일반화한다. 높은 우선순위 행동이 하위 행동을 억제(subsume)하는 메커니즘이 Fallback의 좌측 우선 실행과 형식적으로 대응한다.

  3. 의사 결정 트리(Decision Tree)의 일반화: 행동 트리는 조건 노드와 행동 노드의 조합을 통해 의사 결정 트리의 분기 구조를 표현할 수 있다.

5. 구성 가능성과 모듈성의 형식적 분석

행동 트리의 핵심적 이론적 장점 중 하나는 구성 가능성(compositionality)이다. Ögren(2012)은 Increasing Modularity of UAV Control Systems using Computer Game Behavior Trees에서 소프트웨어 공학의 결합도(coupling)와 응집도(cohesion) 지표를 활용하여 행동 트리의 모듈성을 정량적으로 분석하였다.

행동 트리에서 서브트리 \mathcal{T}_s를 독립적으로 설계하고 검증한 후, 상위 트리에 삽입하더라도 \mathcal{T}_s의 내부 동작이 변경되지 않는다는 속성은 형식적으로 다음과 같이 표현된다:

\forall \mathcal{T}_s \subseteq \mathcal{T}, \quad \text{Semantics}(\mathcal{T}_s) = \text{Semantics}(\mathcal{T}_s \mid \mathcal{T})

이 속성은 행동 트리가 유한 상태 머신에 비해 근본적으로 우수한 모듈성을 가지는 이유를 형식적으로 설명한다. 유한 상태 머신에서는 상태와 전이의 수정이 전역적 파급 효과를 유발하지만, 행동 트리에서는 서브트리의 수정이 해당 서브트리 외부에 영향을 미치지 않는다.

6. 시제 논리 기반 분석

Biggar, Zamani, Shames(2020)는 A Framework for Formal Verification of Behavior Trees with Linear Temporal Logic에서 행동 트리의 실행 궤적(execution trace)을 선형 시제 논리(Linear Temporal Logic, LTL) 공식으로 인코딩하는 체계적 프레임워크를 제안하였다. 이 프레임워크에서 행동 트리의 각 Tick 주기는 LTL의 시간 단계(time step)에 대응하며, 노드의 반환 상태 시퀀스를 LTL 원자 명제(atomic proposition)으로 인코딩한다.

이를 통해 다음과 같은 시간적 속성을 모델 검사 도구(예: NuSMV, SPIN)로 자동 검증할 수 있다:

  • 도달 가능성(Reachability): 특정 행동 노드가 결국 실행되는지 여부 (\Diamond \, \text{action\_executed})
  • 안전성(Safety): 위험 행동이 절대 실행되지 않는지 여부 (\square \, \neg \, \text{dangerous\_action})
  • 활성(Liveness): 시스템이 무한히 특정 상태에 머물지 않는지 여부 (\square \Diamond \, \text{progress})
  • 공정성(Fairness): 모든 행동이 무한히 자주 실행 기회를 얻는지 여부

7. 계약 기반 설계를 통한 합성적 분석

Sprague와 Ögren(2022)은 계약 기반 설계(contract-based design) 방법론을 행동 트리에 적용하였다. 각 행동 트리 노드 n_i에 대해 계약(contract) C_i = (A_i, G_i)를 정의하며, 여기서 A_i는 가정(assumption), G_i는 보증(guarantee)이다.

  • 가정 A_i: 노드 n_i가 올바르게 동작하기 위해 환경이 만족해야 하는 조건
  • 보증 G_i: 가정 A_i가 만족될 때 노드 n_i가 보장하는 사후 조건

이 프레임워크를 통해 행동 트리의 각 서브트리에 대해 독립적으로 계약을 검증한 후, 합성 규칙(composition rule)을 적용하여 전체 행동 트리의 속성을 도출할 수 있다. 이는 대규모 행동 트리 시스템의 점진적 검증(incremental verification)을 가능하게 하며, 전체 상태 공간 탐색의 계산 복잡도를 회피할 수 있다.

8. 하이브리드 동적 시스템으로서의 해석

Colledanchise와 Ögren(2018)은 행동 트리를 하이브리드 동적 시스템(hybrid dynamical system)으로 해석하는 관점을 제안하였다. 행동 트리의 Tick 기반 이산 제어 흐름과 각 행동 노드의 연속 시간 동작을 결합하면, 행동 트리 전체를 이산-연속 혼합 시스템으로 모델링할 수 있다.

이 해석에서 행동 트리의 상태 공간은 다음과 같이 정의된다:

\mathcal{X} = \mathcal{X}_d \times \mathcal{X}_c

여기서 \mathcal{X}_d는 각 노드의 반환 상태로 구성되는 이산 상태 공간이고, \mathcal{X}_c는 로봇의 물리적 상태(위치, 속도, 자세 등)로 구성되는 연속 상태 공간이다. 이 프레임워크는 제어 이론(control theory)의 안정성 분석 도구(Lyapunov 함수, 배리어 함수 등)를 행동 트리 기반 시스템에 적용할 수 있는 이론적 근거를 제공한다.

9. 형식적 분석 연구의 의의와 한계

행동 트리의 형식적 정의와 분석 연구는 다음과 같은 학술적 의의를 가진다:

  1. 이론적 기초 확립: 행동 트리를 직관적 설명에 의존하지 않고 엄밀한 수학적 대상으로 정의함으로써, 정밀한 추론과 증명의 토대를 마련하였다.
  2. 자동 검증 가능성: LTL 인코딩 및 모델 검사 도구와의 연계를 통해, 행동 트리 설계의 정확성을 자동으로 검증할 수 있는 경로를 개척하였다.
  3. 합성적 설계 지원: 계약 기반 설계를 통해 대규모 행동 트리의 점진적 검증 방법론을 확립하였다.

한편, 형식적 분석 연구의 한계로는 상태 공간 폭발(state space explosion) 문제로 인해 대규모 시스템에 대한 완전한 검증이 실질적으로 어렵다는 점, 그리고 연속 동역학과 이산 제어 흐름의 상호작용에 대한 형식적 분석이 아직 초기 단계에 있다는 점이 지적된다.

참고 문헌

  • Colledanchise, M., & Ögren, P. (2018). Behavior Trees in Robotics and AI: An Introduction. CRC Press.
  • Colledanchise, M., & Ögren, P. (2014). 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.
  • Biggar, O., Zamani, M., & Shames, I. (2020). A Framework for Formal Verification of Behavior Trees with Linear Temporal Logic. IEEE Robotics and Automation Letters, 5(2), 2089–2096.
  • Ögren, P. (2012). Increasing Modularity of UAV Control Systems using Computer Game Behavior Trees. AIAA Guidance, Navigation, and Control Conference.
  • Brooks, R. A. (1986). A Robust Layered Control System for a Mobile Robot. IEEE Journal on Robotics and Automation, 2(1), 14–23.

버전: 2026-04-01