Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light
For researchers in formal verification and control theory, this is an incremental combination of existing methods (Bernstein interpolation and HOL Light) applied to switched systems.
The paper proposes using Bernstein interpolation to transform switched systems into polynomial forms for constructing Lyapunov functions, and verifies them formally with HOL Light. Numerical examples are provided but no concrete performance numbers are given.
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.