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

TL;DR

This paper introduces a Bernstein polynomial method to analyze the stability of switched systems and employs HOL Light for formal verification of Lyapunov functions, demonstrated through numerical examples.

Contribution

It presents a novel polynomial approach using Bernstein interpolation for stability analysis and formal verification with HOL Light.

Findings

Successful stability analysis of switched systems using Bernstein polynomials

Formal verification of Lyapunov functions with HOL Light

Numerical examples demonstrate the approach's effectiveness

Abstract

In this preliminary work, we propose to use a polynomial approach in order to study the stability of switched systems. The proposed strategy is based on the Bernstein interpolation method that may transform a switched system into a polynomial expression from which an associated "simple" Lyapunov function can be eventually built. The HOL Light proof assistant allows verifying formally the Lyapunov functions that are identified from the proposed switching structure. Our approach is illustrated by numerical examples.