Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light

기술 요약: 스위칭 시스템의 안정성 및 형식 검증을 위한 베른슈타인 기반 다항식 접근법

문제 정의
여러 개의 하위 시스템이 스위칭 신호에 의해 제어되는 스위칭 시스템은 안정성 분석에 있어 상당한 어려움을 안겨준다. 전통적인 방법들은 시스템의 전체 거동을 하나의 통일된 수학적 기술로 표현하는 데 어려움을 겪는 경우가 많으며, 특히 스위칭 신호가 복잡할 때(예: 상태 의존적 또는 시간 의존적 스위칭) 더욱 그러하다. 다양한 분석 방법이 존재하지만, 스위칭 로직을 연속적인 다항식 표현으로 변환하여 리아푸노프 함수(Lyapunov function)의 구축을 용이하게 하고 엄격한 형식 검증을 가능하게 하는 통합된 수학적 정식화가 필요하다.

방법론
본 논문은 **베른슈타인 보간법(Bernstein interpolation)**을 사용하여 스위칭 시스템을 재정식화하는 전략을 제안한다. 핵심 접근 방식은 다음과 같은 단계로 구성된다:

1. 다항식 재정식화: 하위 시스템 $f_i$의 활성화를 결정하는 스위칭 신호 $\sigma$를 베른슈타인 다항식을 사용하여 근사한다. 스위칭 신호를 베른슈타인 기저 함수의 선형 결합으로 표현함으로써, 원래의 조각별 미분 방정식(piecewise differential equations)으로 정의된 전체 스위칭 시스템을 단일하고 통합된 다항식 표현으로 변환한다.

   • 시스템은 처음에 하위 시스템들의 볼록 결합(convex combination)으로 기술된다: $\dot{x} = \sum f_i(x)\sigma_i$, 여기서 $\sum \sigma_i = 1$ 이고 $\sigma_i \geq 0$ 이다.
   • 스위칭 신호 $\sigma_i$는 $\sigma$의 베른슈타인 급수 근사인 $B_{i,m}^\sigma(\sigma(\nu), \nu)$로 대체되며, 결과적으로 "B-스위칭 시스템(B-switched system)"은 단일 다항식 미분 방정식으로 기술된다.

2. 스위칭 유형 처리: 이 방법은 다양한 스위칭 동작을 수용한다:

   • 상태 의존적 스위칭(State-dependent switching): 부호 함수(예: $\sigma \equiv \text{sign}(\delta x_1 x_2)$)를 사용하여 모델링하며, 특정 차수 $m$의 베른슈타인 다항식으로 근사한다.
   • 시간 의존적 스위칭(Time-dependent switching): 주기적 활성화를 나타내기 위해 펄스 함수(pulse functions)를 사용하여 모델링한다.
   • 유연성: 베른슈타인 다항식의 차수 $m$을 조정하여 근사를 정밀하게 만들거나, 더 높은 정밀도를 위해 합성 규칙(composition rules)을 적용할 수 있으나, 이는 결과 식의 복잡성을 증가시킨다.

3. 형식 검증(Formal Verification): 시스템이 다항식으로 표현되면, 저자들은 **HOL Light 증명 보조기(proof assistant)**를 사용하여 시스템의 안정성 속성을 형식적으로 검증할 것을 제안한다.

   • 다항식 시스템에 대한 후보 리아푸노프 함수 $V(x)$가 식별된다.
   • 검증 작업은 정의된 영역 $D$에서 부등식 $\dot{V}(x) < \epsilon$ (여기서 $\epsilon$은 작은 양의 상수)을 증명하는 문제로 축소된다.
   • 이는 Flyspeck 프로젝트에서 이미 검증된 방법인 **테일러 근사를 이용한 구간 산술(interval arithmetic with Taylor approximations)**을 사용하여 달성된다. 이를 통해 리아푸노프 도함수가 지정된 범위 내에서 음수이거나(또는 0에 충분히 가까운) 상태임을 엄격하게 인증할 수 있다.

주요 결과
논문은 기존 문헌에서 추출한 두 가지 수치 예제를 통해 제안된 접근 방식을 설명하며, "B-스위칭" 다항식 표현을 "표준" 스위칭 시스템과 비교한다:

• 예제 1 (안정적인 시스템): 두 개의 안정적인 하위 시스템을 가진 선형 스위칭 시스템을 분석하였다. 베른슈타인 근사는 표준 시스템의 안정화 거동을 성공적으로 모사하였다.
• 예제 2 (불안정한 시스템): 불안정한 하위 시스템을 가진 선형 스위칭 시스템을 분석하였다. 이 방법은 발산하는 거동을 정확하게 포착하였으며, 상태 곱 $x_1 x_2$가 구간 $[0, 1]$을 벗어나 성장함에 따라 베른슈타인 급수가 자연스럽게 발산함을 보여줌으로써 시스템의 불안정성을 반영하였다.
• 형식 검증: 기본적인 선형 안정 시스템을 사용하여 HOL Light 검증 과정을 시연하였다. 저자들은 이차 리아푸노프 함수의 도함수가 구간 $[0, 1]$ 내에서 임계값($\epsilon = 0.01$) 미만임을 확인하는 형식 증명 인증서를 성공적으로 생성하였다.

의의 및 주장
저자들은 본 연구를 다음과 같은 구체적인 기여와 한계를 가진 **예비 연구(preliminary study)**로 제시한다:

• 통합: 주요 기여는 베른슈타인 보간을 통해 여러 스위칭 하위 시스템을 단일 다항식 표현으로 "통합"할 수 있다는 점이다. 이는 리아푸노프 후보 함수를 찾는 과정을 단순화한다.
• 형식적 인증: 이 접근법은 수치 시뮬레이션과 형식 증명 사이의 간극을 메워, HOL Light 보조기가 도출된 리아푸노프 함수의 안정성 속성을 검증할 수 있도록 한다.
• 제한된 범위: 저자들은 B-스위칭 시스템의 안정성 속성이 표준 스위칭 시스템과 동일하다고 가정한다는 점을 명시하였으나(적어도 리아푸노프 안정성 측면에서), 아직 이 등가성을 엄격하게 증명했다고 주장하지는 않는다.
• 향후 과제: 저자들은 다음과 같은 향후 연구 분야를 식별하였다:
  • 표준 표현과 B-스위칭 표현 사이의 완전한 수학적 등가성 증명.
  • 비선형 및 비다항식 시스템으로의 확장.
  • 단순히 식별된 후보를 검증하는 것을 넘어, "최적의" 리아푸노프 함수를 계산하기 위한 SOS(Sum-of-Squares) 도구의 활용.

결론적으로, 본 논문은 베른슈타인 다항식을 활용하여 스위칭 시스템 분석을 형식 검증 도구로 해결 가능한 다항식 문제로 변환하는 새로운 프레임워크를 제안하며, 이는 엄격한 안정성 인증을 위한 잠재적인 경로를 제공한다.