Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems

1. 문제 정의 (Problem Statement)

• 배경: 많은 공학 시스템은 미분 방정식과 대수적 방정식이 결합된 DAE 로 모델링됩니다. 대수적 제약 ($\phi(x)=0$) 은 시스템 상태가 특정 다양체 (Manifold) 상에서만 움직이도록 제한합니다.
• 기존 CBF 의 한계: 기존의 제어 장벽 함수 (CBF) 는 일반 미분 방정식 (ODE) 시스템에 효과적이지만, DAE 시스템에 직접 적용할 때 다음과 같은 근본적인 문제가 발생합니다.
  • 불일치 (Infeasibility): 표준 CBF 조건을 만족하는 제어 입력을 찾으려 할 때, 해당 입력이 대수적 제약 조건을 위반하여 시스템이 허용된 다양체 (Constraint Manifold) 에서 벗어나게 됩니다.
  • 안전성 위반: 제어 입력의 존재성 (Feasibility) 이 보장되지 않아 최적화 문제 (QP) 가 해를 찾지 못하게 되며, 이로 인해 시스템이 안전 영역을 이탈하게 됩니다.
• 목표: 대수적 제약과 CBF 조건을 동시에 만족하면서도, 안전 집합의 전방 불변성 (Forward Invariance) 을 보장하는 제어 입력을 설계하고 이를 검증하는 프레임워크를 개발하는 것입니다.

2. 방법론 (Methodology)

논문은 DAE 인지형 CBF (DAE-aware CBF) 프레임워크를 제안하며, 주요 방법은 다음과 같습니다.

가. 투영된 벡터장 (Projected Vector Fields)

• 대수적 제약으로 인해 시스템의 상태가 다양체 $M$ 위에 유지되도록 하기 위해, 투영된 벡터장을 정의합니다.
• 대수적 제약의 미분을 통해 얻은 호환성 조건 (Compatibility Condition) 을 만족하도록 제어 입력을 투영합니다.
• 이를 통해 DAE 시스템을 다양체 $M$ 위에서 정의된 동치인 ODE 시스템 ($\dot{x} = \hat{f}(x) + \hat{g}(x)u$) 으로 변환하여, 표준 CBF 이론을 적용할 수 있는 기반을 마련합니다.

나. 차수 (Index) 에 따른 확장

• Index-1 DAE: 대수적 제약의 1 차 미분만으로도 제어 입력이 명시적으로 나타나는 경우. 투영된 벡터장을 사용하여 표준 CBF 조건을 적용합니다.
• 고차 DAE (Higher-Index, $\nu \ge 2$): 대수적 제약이 숨겨진 동역학을 포함하는 경우.
  • 미분 지수 (Differentiation Index, $\nu$) 와 상대 차수 (Relative Degree) 의 관계를 정립합니다.
  • 대수적 제약의 $\nu$ 번 미분을 통해 숨겨진 제약을 드러내고, 이를 만족하는 고차 CBF (HOCBF) 조건을 유도합니다.
  • 제어 입력이 나타나기 전까지의 모든 미분 단계에서 호환성 조건을 만족해야 함을 보장합니다.

다. 형식적 검증 프레임워크 (Formal Verification)

후보 CBF 함수가 실제로 유효한지 검증하기 위해 두 가지 주요 조건을 확인합니다.

1. 기하학적 정확성 (Geometric Correctness): 제안된 장벽 집합 $D$가 실제 안전 집합 $C$ 내에 포함되는지 확인 ($D \cap M \subseteq C \cap M$).
2. 실현 가능성 (Feasibility): 모든 상태 $x \in D \cap M$ 에서 대수적 제약과 CBF 조건을 동시에 만족하는 제어 입력 $u$ 가 존재하는지 확인.

• 다항식 시스템: 합의 제곱 (Sum-of-Squares, SOS) 프로그래밍을 사용하여 증명 (Certificate) 을 생성합니다.
• 비다항식/신경망 시스템: SMT (Satisfiability Modulo Theories) 솔버 (Z3 등) 를 이용한 반증 (Falsification) 기법을 사용하여 안전성을 검증합니다.

3. 주요 기여 (Key Contributions)

1. DAE 인지형 CBF 조건 도출: 대수적 제약의 구조를 투영된 벡터장을 통해 명시적으로 반영하여, 안전 집합의 전방 불변성과 대수적 제약의 일관성을 동시에 보장하는 충분 조건을 제시했습니다.
2. 고차 DAE 시스템으로의 일반화: 미분 지수 (Differentiation Index) 와 장벽 함수의 상대 차수 간의 관계를 정립하여, 숨겨진 제약을 가진 고차 DAE 시스템에도 적용 가능한 고차 CBF 조건을 확장했습니다.
3. 체계적인 검증 방법론 개발:
   • 다항식 시스템에 대한 SOS 기반의 검증.
   • 비다항식 및 신경망 기반 CBF 에 대한 SMT 기반의 반증 (Falsification) 기법.
   • 기하학적 정확성과 실현 가능성 (내부 및 경계 조건) 을 모두 검증하는 통합 프레임워크.
4. 실증적 유효성 입증: 풍력 터빈 시스템 (Index-1) 과 유연 링크 매니퓰레이터 (Index-2) 에 대한 시뮬레이션을 통해 제안된 방법이 표준 CBF 의 실패 (QP 비실현성) 를 극복하고 안전성을 유지함을 보였습니다.

4. 실험 결과 (Results)

• 풍력 터빈 시스템 (Index-1 DAE):
  • 기존 표준 CBF 를 적용 시 대수적 제약과 충돌하여 QP 가 비실현성이 되고 안전성이 위반됨을 확인.
  • 제안된 DAE 인지형 CBF 를 적용 시, 시스템 궤적이 제약 다양체 위에 유지되며 안전 함수가 양수 값을 유지함을 확인.
  • SOS 및 SMT 를 통한 형식적 검증으로 후보 CBF 의 유효성을 수학적으로 증명.
• 유연 링크 매니퓰레이터 (Index-2 DAE):
  • 고차 DAE 시스템에서 제안된 고차 CBF 조건이 작동함을 입증.
  • 초기 각속도가 큰 상황에서도 엔드 이펙터가 안전 한계 (1.8m) 를 초과하지 않도록 제어 입력을 조절.
  • 신경망 (NN) 기반 CBF 후보에 대해 SMT 기반 반증 검증을 수행하여 안전성을 확인.

5. 의의 및 결론 (Significance)

• 이론적 기여: DAE 시스템의 안전 제어에 있어 "제어 입력의 존재성"과 "대수적 제약의 일관성" 사이의 모순을 해결하는 이론적 기반을 마련했습니다. 특히 고차 DAE 시스템에서의 CBF 설계와 검증에 대한 체계적인 접근법을 제시했습니다.
• 실용적 가치: 전력망, 로봇, 화학 공정 등 대수적 제약이 필수적인 실제 공학 시스템에 안전 제어 기술을 적용할 수 있는 길을 열었습니다.
• 한계 및 향후 과제:
  • SOS 및 SMT 기반 검증의 확장성 문제 (고차원 시스템 적용의 어려움).
  • 시스템 모델의 불확실성을 고려하지 않음.
  • 현재는 후보 CBF 함수의 검증에 집중되어 있으며, 안전 사양으로부터 CBF 를 자동 합성 (Synthesis) 하는 문제는 향후 과제로 남음.

결론적으로, 이 논문은 DAE 시스템의 고유한 구조적 특성을 고려하여 안전 제어 필터를 설계하고 검증하는 최초의 포괄적인 프레임워크를 제공하며, 안전 임계 (Safety-critical) 시스템 제어 분야에서 중요한 진전을 이룩했습니다.