1292.3 행동 트리의 수학적 형식 정의

1292.3 행동 트리의 수학적 형식 정의

1. 형식 정의의 필요성

행동 트리의 구조와 실행 의미론을 엄밀하게 분석하고 검증하기 위해서는 수학적 형식 정의(formal definition)가 필수적이다. 직관적 이해에 기반한 비형식적 기술은 모호성을 수반하며, 특히 로봇 시스템과 같이 안전성이 중요한 응용 분야에서는 행동 트리의 동작에 대한 형식적 보장이 요구된다. Colledanchise와 Ögren(2018)은 행동 트리에 대한 수학적 형식 정의를 제시하여 이 분야의 이론적 기반을 확립하였다.

2. 행동 트리의 튜플 기반 정의

행동 트리는 다음의 4-튜플(4-tuple)로 형식적으로 정의한다.

\mathcal{T} = \langle f_i, r_i, \Delta t, N \rangle

각 구성 요소의 의미는 다음과 같다.

  • f_i: 노드 i의 실행 함수(execution function)로, Tick 신호를 수신했을 때 수행하는 연산을 정의하는 사상(mapping)이다.
  • r_i \in \{\text{Success}, \text{Failure}, \text{Running}\}: 노드 i의 반환 상태(return status)로, 실행 함수 f_i의 실행 결과를 나타낸다.
  • \Delta t: Tick 주기(tick period)로, 연속적인 두 Tick 신호 사이의 시간 간격을 나타내는 양의 실수값이다.
  • N: 트리를 구성하는 노드의 유한 집합이다.

3. 반환 상태 집합의 형식 정의

행동 트리의 모든 노드는 Tick 신호를 수신한 후 반드시 다음 반환 상태 집합 \mathcal{S}의 원소 하나를 반환해야 한다.

\mathcal{S} = \{\text{Success}, \text{Failure}, \text{Running}\}

각 상태의 형식적 의미는 다음과 같다.

  • \text{Success}: 노드가 할당된 과업(task)을 성공적으로 완료하였음을 나타낸다.
  • \text{Failure}: 노드가 할당된 과업의 수행에 실패하였음을 나타낸다.
  • \text{Running}: 노드가 할당된 과업을 아직 수행 중이며 완료되지 않았음을 나타낸다.

4. 노드 실행 함수의 형식 정의

각 노드 i \in N의 실행 함수 f_i는 다음과 같은 사상으로 정의한다.

f_i: \mathcal{X} \rightarrow \mathcal{S}

여기서 \mathcal{X}는 시스템의 상태 공간(state space)이며, \mathcal{S}는 반환 상태 집합이다. 실행 함수 f_i의 정의역(domain)은 노드 유형에 따라 다음과 같이 세분화된다.

4.1 리프 노드의 실행 함수

리프 노드(leaf node)의 실행 함수는 외부 환경 또는 시스템 상태를 입력으로 받아 반환 상태를 출력한다.

  • 액션 노드: f_{\text{action}}: \mathcal{X} \rightarrow \mathcal{S}로 정의되며, 실행 과정에서 상태 공간 \mathcal{X}에 부수 효과(side effect)를 발생시킬 수 있다.
  • 조건 노드: f_{\text{condition}}: \mathcal{X} \rightarrow \{\text{Success}, \text{Failure}\}로 정의되며, Running을 반환하지 않고 부수 효과를 발생시키지 않는다.

4.2 내부 노드의 실행 함수

내부 노드(internal node)의 실행 함수는 자식 노드들의 반환 상태를 입력으로 받아 자신의 반환 상태를 결정한다.

f_{\text{internal}}: \mathcal{S}^k \rightarrow \mathcal{S}

여기서 k는 해당 내부 노드의 자식 노드 수이며, \mathcal{S}^k는 k개 자식 노드의 반환 상태 벡터를 나타낸다.

5. 제어 흐름 노드의 형식적 실행 규칙

주요 제어 흐름 노드의 실행 함수를 형식적으로 정의하면 다음과 같다.

5.1 Sequence 노드

Sequence 노드 S가 자식 노드 c_1, c_2, \ldots, c_k를 가질 때, 실행 함수 f_S는 다음과 같이 정의한다.

f_S(r_{c_1}, r_{c_2}, \ldots, r_{c_k}) = \begin{cases} \text{Failure} & \text{if } \exists \, j : r_{c_j} = \text{Failure} \\ \text{Running} & \text{if } \exists \, j : r_{c_j} = \text{Running} \wedge \forall \, i < j : r_{c_i} = \text{Success} \\ \text{Success} & \text{if } \forall \, j : r_{c_j} = \text{Success} \end{cases}

여기서 자식 노드는 c_1부터 순서대로 평가하며, 첫 번째 Failure 또는 Running을 반환하는 자식에서 평가를 중단한다.

5.2 Fallback 노드

Fallback 노드 F가 자식 노드 c_1, c_2, \ldots, c_k를 가질 때, 실행 함수 f_F는 다음과 같이 정의한다.

f_F(r_{c_1}, r_{c_2}, \ldots, r_{c_k}) = \begin{cases} \text{Success} & \text{if } \exists \, j : r_{c_j} = \text{Success} \\ \text{Running} & \text{if } \exists \, j : r_{c_j} = \text{Running} \wedge \forall \, i < j : r_{c_i} = \text{Failure} \\ \text{Failure} & \text{if } \forall \, j : r_{c_j} = \text{Failure} \end{cases}

5.3 Parallel 노드

Parallel 노드 P가 성공 임계값 M을 가지며 자식 노드 c_1, c_2, \ldots, c_k를 가질 때, 실행 함수 f_P는 다음과 같이 정의한다.

f_P(r_{c_1}, r_{c_2}, \ldots, r_{c_k}) = \begin{cases} \text{Success} & \text{if } \lvert\{j : r_{c_j} = \text{Success}\}\rvert \geq M \\ \text{Failure} & \text{if } \lvert\{j : r_{c_j} = \text{Failure}\}\rvert > k - M \\ \text{Running} & \text{otherwise} \end{cases}

6. 데코레이터 노드의 형식적 정의

데코레이터 노드는 정확히 하나의 자식 노드 c를 가지며, 자식의 반환 상태를 변환하는 함수 \delta를 구현한다.

f_{\text{decorator}} = \delta \circ f_c

여기서 \delta: \mathcal{S} \rightarrow \mathcal{S}는 상태 변환 함수이다. 대표적인 데코레이터의 상태 변환 함수는 다음과 같다.

  • Inverter: \delta(\text{Success}) = \text{Failure}, \quad \delta(\text{Failure}) = \text{Success}, \quad \delta(\text{Running}) = \text{Running}
  • ForceSuccess: \delta(s) = \text{Success}, \quad \forall s \in \{\text{Success}, \text{Failure}\}, \quad \delta(\text{Running}) = \text{Running}
  • ForceFailure: \delta(s) = \text{Failure}, \quad \forall s \in \{\text{Success}, \text{Failure}\}, \quad \delta(\text{Running}) = \text{Running}

7. Tick 함수의 형식적 정의

행동 트리의 Tick 메커니즘을 형식적으로 정의하면, Tick 함수 \text{tick}은 트리 \mathcal{T}와 시간 단계 t를 입력으로 받아 트리 전체의 반환 상태를 출력하는 함수이다.

\text{tick}: \mathcal{T} \times \mathbb{N} \rightarrow \mathcal{S}

시간 단계 t에서의 Tick 함수 실행은 루트 노드의 실행 함수를 호출하는 것으로 시작하며, 루트의 실행 함수는 재귀적으로 자식 노드들의 실행 함수를 호출한다. 이 과정은 다음과 같이 재귀적으로 정의된다.

\text{tick}(\mathcal{T}, t) = f_{\text{root}}(\text{tick}(c_1, t), \text{tick}(c_2, t), \ldots, \text{tick}(c_k, t))

단, 제어 흐름 노드의 조기 종료(short-circuit) 규칙에 의해 모든 자식 노드가 반드시 평가되는 것은 아니다.

8. 행동 트리의 상태 공간 형식 정의

행동 트리의 전체 상태는 각 노드의 개별 상태와 블랙보드의 상태를 포함하여 다음과 같이 정의한다.

\mathcal{X}_{\mathcal{T}} = \prod_{i \in N} \mathcal{S}_i \times \mathcal{B}

여기서 \mathcal{S}_i는 노드 i의 상태 공간이고, \mathcal{B}는 블랙보드의 상태 공간이다. 시간 단계 t에서 t+1로의 상태 전이는 Tick 함수의 실행에 의해 결정되며, 이는 다음과 같이 표현된다.

x_{t+1} = g(x_t, \text{tick}(\mathcal{T}, t))

여기서 g는 상태 전이 함수(state transition function)이며, x_t \in \mathcal{X}_{\mathcal{T}}는 시간 단계 t에서의 전체 상태 벡터이다.

9. 형식 정의의 이론적 의의

행동 트리의 수학적 형식 정의는 다음과 같은 이론적 분석을 가능하게 한다.

첫째, 안전성(safety) 속성의 형식적 검증이 가능하다. 특정 위험 상태에 도달하지 않음을 형식적으로 증명할 수 있으며, 이는 \forall t \in \mathbb{N}: x_t \notin \mathcal{X}_{\text{unsafe}}의 형태로 표현된다.

둘째, 활성(liveness) 속성의 분석이 가능하다. 목표 상태에 유한 시간 내에 도달함을 보장하는 분석이 가능하며, 이는 \exists t \in \mathbb{N}: x_t \in \mathcal{X}_{\text{goal}}의 형태로 표현된다.

셋째, 합성성(compositionality)의 형식적 보장이 가능하다. 개별 서브트리에 대해 검증된 속성이 전체 트리에서도 보존됨을 형식적으로 증명할 수 있으며, 이는 행동 트리의 모듈적 설계를 이론적으로 뒷받침한다.

10. 참고 문헌

  • Colledanchise, M., & Ögren, P. (2018). Behavior Trees in Robotics and AI: An Introduction. CRC Press.
  • 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), 2435–2442.
  • 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.
  • Marzinotto, A., Colledanchise, M., Smith, C., & Ögren, P. (2014). Towards a Unified Behavior Trees Framework for Robot Control. Proceedings of the IEEE International Conference on Robotics and Automation (ICRA), 5420–5427.

본 절은 Version 1로 작성되었다.