We focus on switched systems with a parametric affine term and state-dependent switch logic. For these systems, we aim to synthesize a region of parameters for which we guarantee a formal proof of Global Asymptotic Stability (GAS). We propose a novel technique based on Piecewise Quadratic Lyapunov Functions that are either Locally Valid (LVPQLF) or Parametric (PPQLF), for which we can define the LMI problem for synthesis and the symbolic proof obligations for formal verification. We implement the technique and show that it scales up to industrial-size systems with 21 state variables.
Formal Verification of Stability for Parametric affine Switched Systems
Ludovico Battista
;Stefano Tonetta
2024-01-01
Abstract
We focus on switched systems with a parametric affine term and state-dependent switch logic. For these systems, we aim to synthesize a region of parameters for which we guarantee a formal proof of Global Asymptotic Stability (GAS). We propose a novel technique based on Piecewise Quadratic Lyapunov Functions that are either Locally Valid (LVPQLF) or Parametric (PPQLF), for which we can define the LMI problem for synthesis and the symbolic proof obligations for formal verification. We implement the technique and show that it scales up to industrial-size systems with 21 state variables.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
