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:
File Dimensione Formato  
parametric_switched.pdf

accesso aperto

Licenza: PUBBLICO - Creative Commons 3.6
Dimensione 550.21 kB
Formato Adobe PDF
550.21 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/353429
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact