Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis

이 논문은 자율 시스템의 제어 합성 (Control Synthesis) 을 위해 행동 트리 (Behavior Trees, BTs) 를 3 진 논리 (Ternary Logic) 기반의 시그널 시공간 논리 (Signal Temporal Logic, STL) 로 재형성하고, 이를 미분 정수 선형 부호화 (Mixed-Integer Linear Encodings) 를 통해 최적 제어 문제로 해결하는 방법을 제시합니다.

주요 내용은 다음과 같습니다.

1. 문제 정의 (Problem)

• 배경: 행동 트리 (BT) 는 자율 시스템의 장기 계획 수립에 직관적인 그래픽 인터페이스를 제공하지만, 안전성과 정확성을 보장하기 위한 엄격한 형식적 모델링과 검증이 필요합니다.
• 한계: 기존에 제안된 '시간적 행동 트리 (Temporal BTs, TBTs)'는 주로 오프라인 사후 분석 (post hoc analysis) 및 궤적 수정 (trace repair) 에 국한되어 있었습니다. 또한, 기존 STL 기반 접근법은 이진 논리 (True/False) 에 기반하여, 시스템이 명세를 완전히 만족하거나 위반하지 않는 '중간 상태'를 명확히 표현하거나 이를 제어 합성에 활용하기 어려웠습니다.
• 목표: TBT 를 3 진 논리 (True, False, Unknown) 를 지원하는 STL 로 재정의하고, 이를 **미분 정수 최적화 (Mixed-Integer Optimization)**를 통해 선형 동적 시스템에 대한 구현 가능 (correct-by-construction) 제어 전략을 자동으로 생성할 수 있도록 하는 것입니다.

2. 방법론 (Methodology)

A. 3 진 논리 (Kleene's Strong Logic, $K_3$) 기반 재형성

• 행동 트리의 노드 상태는 '성공 (Success)', '실패 (Failure)', '진행 중 (Running)'의 3 가지 상태가 존재하므로, 이를 표현하기 위해 3 진 논리 $K_3$를 도입했습니다.
  • True (T): 성공
  • False (F): 실패
  • Unknown (U): 진행 중 또는 불확실한 상태 (명세가 완전히 만족되거나 위반되지 않은 경우)
• 부분 궤적 (Partial Trajectory) STL: 무한한 궤적이 아닌 유한한 시간 구간 (부분 궤적) 에 대해 명세를 평가할 때, 정보가 부족하여 결정할 수 없는 경우 'Unknown' 값을 부여하여 논리적 결정을 가능하게 했습니다.
• 불확실성 모델링: 신호 예측 (Signal Predicate) 에 임계값 ($\delta$) 을 도입하여, $f(x_t)$가 특정 구간 내에 있을 때 True/False 대신 Unknown 으로 평가되도록 하여 측정 불확실성을 포착합니다.

B. 미분 정수 선형 부호화 (Mixed-Integer Linear Encodings)

• 3 진 부호화: 논리 값을 정수 변수로 매핑합니다.
  • True $\rightarrow +1$
  • Unknown $\rightarrow 0$
  • False $\rightarrow -1$
• STL 연산자 부호화:
  • 논리 연산자 ($\neg, \wedge, \vee$) 와 시공간 연산자 (Always $\square$, Eventually $\diamond$) 를 3 진 논리 규칙에 따라 선형 제약 조건으로 변환합니다.
  • 특히, 부분 궤적의 경우 검색 창 (search window) 이 궤적의 끝을 넘을 때 'Unknown'으로 평가되거나 단락 (short-circuit) 되는 논리를 수학적으로 인코딩했습니다.
• TBT 연산자 부호화:
  • Sequence (Seq): 자식 노드들이 순차적으로 성공해야 함.
  • Selector (Sel): 자식 노드 중 하나가 성공하면 됨 (실패 시 다음으로 이동).
  • 이 연산자들을 3 진 논리 기반의 미분 정수 제약 조건으로 변환하여, TBT 구조를 가진 복잡한 시간적 제약을 최적화 문제에 포함시켰습니다.

C. 최적 제어 문제 공식화

• 선형 이산 시간 동적 시스템 ($x_{t+1} = A_t x_t + B_t u_t$) 을 대상으로 합니다.
• 목적 함수는 제어 노력 (control effort) 의 2 차 함수로 설정하고, TBT 명세를 만족하는 궤적을 찾기 위해 미분 정수 2 차 계획법 (MIQP) 문제를 풉니다.
• 제어 입력과 상태 궤적이 TBT 명세를 만족하도록 하는 제약 조건을 미분 정수 선형 부등식으로 표현합니다.

3. 주요 기여 (Key Contributions)

1. 3 진 논리 ($K_3$) 를 통한 BT 형식화: 행동 트리의 '진행 중 (Running)' 상태를 포착하고 불확실성을 포함하는 3 진 논리 기반의 TBT 형식적 정의를 구체화했습니다.
2. 미분 정수 부호화 개발: 3 진 논리 기반의 STL 및 TBT 연산자 (Seq, Sel) 에 대한 미분 정수 선형 부호화를 제안하여, 이를 최적 제어 문제에 직접 적용 가능하게 했습니다.
3. 구현 가능한 제어 합성: 제안된 프레임워크를 사용하여 선형 이산 시간 시스템에 대한 최적 제어 문제를 해결하고, 명세를 만족하는 제어 입력을 자동으로 생성하는 것을 실증했습니다.

4. 실험 결과 (Results)

논문은 두 가지 사례 연구를 통해 프레임워크의 유효성을 입증했습니다.

• 사례 1: 이산 시간 더블 적분기 (이동 로봇)

  • 시나리오: 배터리 잔량에 따라 경로가 분기되는 BT 명세 (목표 A 도달 $\rightarrow$ 배터리 80% 이상이면 B 로, 아니면 C(충전소) 로 갔다가 B 로).
  • 결과: Gurobi 솔버를 사용하여 전역 최적해를 찾았습니다. 배터리 상태에 따라 로봇이 충전소 C 를 경유하거나 직접 B 로 이동하는 두 가지 다른 궤적이 성공적으로 합성되었습니다.
  • 성능: 25 시간 단계, 약 4,800 개의 정수 변수, 4,775 개의 선형 제약 조건을 가진 모델이 약 97 초 내에 해결되었습니다.

• 사례 2: 다중 에이전트 계획

  • 시나리오: 3 개의 로봇 에이전트가 서로 충돌하지 않고 장애물을 피하며 각자 목표 지점을 방문해야 하는 TBT 명세.
  • 결과: 에이전트 간의 최소 거리 유지 제약 조건으로 인해, 장애물 통로를 통과할 때 에이전트들이 순차적으로 통과하는 '대기 (Queuing)' 현상이 자연스럽게 발생했습니다. 이는 안전 명세가 엄격할 때 발생하는 현상을 TBT 를 통해 자연스럽게 모델링하고 해결할 수 있음을 보여줍니다.

5. 의의 및 결론 (Significance & Conclusion)

• 불확실성 처리: 기존 이진 논리 기반 접근법의 한계를 넘어, 시스템이 명세를 완전히 만족하지도 위반하지도 않는 '중간 상태'를 'Unknown'으로 처리함으로써 더 넓은 탐색 공간을 제공하고 불확실성을 포착할 수 있습니다.
• 자동화된 제어 합성: 복잡한 행동 트리 명세를 수학적으로 최적화 문제로 변환하여, 안전성과 행동 요구 사항을 동시에 만족하는 제어기를 자동으로 설계할 수 있는 길을 열었습니다.
• 확장성: 현재는 선형 시스템에 적용되었으나, 향후 비선형 시스템으로의 확장 및 검증 기술 개발을 통해 자율 시스템 제어의 신뢰성을 높이는 데 기여할 것으로 기대됩니다.

요약하자면, 이 논문은 행동 트리의 직관성과 3 진 논리의 유연성을 결합하여, 복잡한 시간적 제약을 가진 자율 시스템에 대해 수학적으로 엄밀하고 자동화된 제어 합성을 가능하게 하는 새로운 프레임워크를 제시했습니다.