Computing Sound Lower and Upper Bounds on Hamilton-Jacobi Reach-Avoid Value Functions

이 논문은 비선형 제어 시스템의 안전성 검증 및 제어 합성을 위한 핵심 도구인 해밀턴-야코비 (Hamilton-Jacobi, HJ) 도달성 분석의 한계를 해결하고, 이를 개선한 새로운 알고리즘을 제안합니다. 기존 방법론이 가진 이산화 오차 (discretization errors) 로 인한 보장성 (soundness) 문제를 다루며, 도달 회피 (Reach-Avoid) 및 회피 (Avoid) 문제에 대해 신뢰할 수 있는 상한 및 하한 값 함수 (Value Function) 를 계산하는 프레임워크를 제시합니다.

다음은 논문의 상세한 기술적 요약입니다.

1. 문제 제기 (Problem Statement)

• 배경: 비선형 제어 시스템 (자율주행차, 수술 로봇 등) 의 안전성 검증과 제어 합성에는 HJ 도달성 분석이 필수적입니다. 이는 시스템이 실패 집합 (Failure Set, $F$) 에 도달하지 않도록 하거나, 목표 집합 (Target Set, $T$) 에 도달하면서 $F$를 피하는 상태 집합 (Reach-Avoid Set, RAS) 을 계산하는 것을 목표로 합니다.
• 기존 방법의 한계: 기존 HJ 분석 방법들은 연속 상태 공간을 그리드 (Grid) 로 이산화하여 수치적으로 편미분 방정식 (PDE) 을 풉니다.
  • 보장성 부재: 이산화 오차를 명시적으로 고려하지 않기 때문에, 계산된 집합이 실제 **역방향 도달 집합 (BRS) 을 과대평가 (Over-approximation)**하거나 **RAS 를 과소평가 (Under-approximation)**한다는 것을 보장하지 못합니다. 즉, 안전하지 않은 상태를 안전하다고 잘못 판단하거나, 그 반대의 오류가 발생할 수 있습니다.
  • 수렴 전 중단 문제: 값 반복 (Value Iteration) 알고리즘이 고정점에 수렴하기 전에 중단될 경우 발생하는 오차를 처리하는 방법이 부족합니다.

2. 제안된 방법론 (Methodology)

저자들은 이산화 오차와 값 반복의 조기 중단 (Early Termination) 오차를 모두 고려하여 신뢰할 수 있는 (Sound) 상한 및 하한 값 함수를 계산하는 알고리즘을 개발했습니다.

A. 이산 추상화 (Discrete Abstraction) 및 바인딩

• 그리드 기반 추상화: 연속 상태 공간을 유한한 그리드 셀로 분할하고, 각 셀을 이산 상태로 간주하는 추상화 모델을 구축합니다.
• 리프시츠 연속성 활용: 상태 전이 함수 $f$, 실패 함수 $l$, 보상 함수 $r$이 리프시츠 연속 (Lipschitz continuous) 임을 가정합니다. 이를 통해 각 그리드 셀 내의 모든 상태에 대해 $l$과 $r$의 **최소값과 최대값 (하한 및 상한)**을 계산합니다.
• 비결정적 전이 관계: 셀 간의 전이 관계를 비결정적으로 정의하여, 실제 시스템이 해당 셀에서 시작하여 특정 제어 입력을 가했을 때 도달할 수 있는 모든 상태가 포함되도록 **과대평가 (Over-approximation)**된 전이 관계를 만듭니다.

B. 값 함수의 상한 및 하한 계산

• 두 개의 값 함수 정의:
  • 하한 값 함수 ($\underline{V}_\gamma$): 최악의 시나리오를 가정하여 계산되며, 실제 HJ 값 함수의 하한을 보장합니다.
  • 상한 값 함수 ($\overline{V}_\gamma$): 최선의 시나리오를 가정하여 계산되며, 실제 HJ 값 함수의 상한을 보장합니다.
• 벨만 연산자 (Bellman Operator): 위 두 값 함수에 대해 각각의 벨만 연산자를 정의하고, 이들이 축소 사상 (Contraction Mapping) 임을 증명하여 고유한 고정점이 존재함을 보입니다.

C. 조기 중단 (Early Stopping) 보정

• 값 반복이 고정점에 완전히 수렴하기 전에 중단될 경우, **보정 항 (Correction Term)**을 도입하여 오차를 보정합니다.
• 할인 계수 ($\gamma \in (0, 1)$) 활용: $\gamma < 1$일 때, 반복 횟수 $k$와 최소 변화량 $\delta_k$를 기반으로 하한 값 함수에 $\frac{\gamma \delta_k}{1-\gamma}$ 항을 추가하여, 중단된 단계에서도 여전히 실제 값 함수의 하한을 보장하도록 만듭니다.
• $\gamma = 1$인 경우: 비할인 (Non-discounted) 경우, 값 반복이 유한 시간 내에 수렴함을 보장하므로 보정 없이도 고정점을 정확히 찾을 수 있습니다.

D. 적응형 정밀화 알고리즘 (Adaptive Refinement)

• 계산된 상한과 하한이 0 을 기준으로 명확하게 분류되지 않는 셀 (Unclassified Cells) 을 식별합니다.
• 이러한 셀을 가장 긴 변을 기준으로 분할하여 그리드를 세분화하고, 다시 값 함수를 재계산합니다.
• 이 과정을 사용자가 정의한 최소 해상도 ($\epsilon_{min}$) 에 도달하거나 모든 셀이 분류될 때까지 반복하여 BRS 와 RAS 의 근사 정확도를 높입니다.

3. 주요 기여 (Key Contributions)

1. 신뢰할 수 있는 경계 계산: 이산화 오차와 값 반복의 조기 중단 오차를 명시적으로 고려하여, BRS 의 과대평가와 RAS 의 과소평가를 보장하는 상/하한 값 함수를 계산하는 알고리즘을 제시했습니다.
2. 수렴 전 보장성 증명: 값 반복이 고정점에 수렴하기 전에 중단되더라도 (특히 $\gamma \in (0, 1)$인 경우), 계산된 하한이 여전히 유효함을 수학적으로 증명했습니다.
3. 적응형 정밀화: 분류가 불확실한 셀만 선택적으로 분할하여 계산 효율성을 높이면서도 정확한 근사치를 얻는 알고리즘을 개발했습니다.
4. 범용성: 회피 (Avoid-only) 문제와 도달 - 회피 (Reach-Avoid) 문제 모두에 적용 가능하며, 이산 시간 비선형 제어 시스템에 대한 이론적 기반을 제공합니다.

4. 실험 결과 (Results)

두 가지 사례 연구 (Dubins Car, 3D Evasion) 를 통해 알고리즘의 유효성을 검증했습니다.

• 기존 도구와의 비교:
  • HJ PDE 솔버 ([25]): 낮은 해상도에서 안전하지 않은 상태를 안전하다고 잘못 분류하는 등 이산화 오차로 인한 보장성 부재를 보였습니다.
  • ROCS 2.0 (Symbolic Control): 추상화 기반 제어 합성 도구로, 본 논문 방법보다 계산 시간이 길거나 더 보수적인 (작은) RAS 를 계산했습니다.
• 성능:
  • 제안된 방법 (Algorithm 1 및 2) 은 기존 도구들보다 더 넓은 RAS를 계산하면서도 **보장성 (Soundness)**을 유지했습니다.
  • 특히, 정밀화 (Refinement) 를 통해 분류되지 않은 셀을 줄임으로써 BRS 와 RAS 의 경계를 더 정밀하게 파악할 수 있었습니다.
  • 계산 시간은 그리드 크기에 비례하여 증가하지만, 기존 HJ 솔버보다 효율적이거나 동등한 수준을 보였습니다.
• 할인 계수 ($\gamma$) 의 영향: $\gamma$가 1 에 가까울수록 시간 해석적 의미가 명확해지지만, $\gamma < 1$일 때 조기 중단 보정을 통해 수렴 속도를 높일 수 있음을 확인했습니다.

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

이 논문은 HJ 도달성 분석 분야에서 수치적 근사의 불확실성을 엄밀하게 제어하는 중요한 진전을 이루었습니다.

• 안전성 검증의 신뢰도 향상: 자율 시스템과 같은 안전-중요 (Safety-critical) 시스템에서 "안전하다"는 결론을 내릴 때, 이산화 오차로 인한 오검출을 방지할 수 있는 이론적 근거를 제공합니다.
• 실용적 적용 가능성: 조기 중단과 적응형 그리드 정밀화를 통해 고차원 시스템에서도 계산 비용을 절감하면서 정확한 안전 마진 (Safety Margin) 을 분석할 수 있게 합니다.
• 미래 과제: GPU 병렬화, 더 정교한 전방향 도달성 도구 활용, 그리고 연속 시간 시스템으로의 확장이 향후 연구 과제로 제시되었습니다.

요약하자면, 이 연구는 이산화 오차와 알고리즘적 오차를 모두 고려하여 수학적으로 엄밀한 (Provable) 안전성 경계를 제공하는 최초의 HJ 기반 프레임워크 중 하나로 평가됩니다.