Formal Synthesis of Lyapunov Stability Certificates for Linear Switched Systems using ReLU Neural Networks

Debauche, Virginie;Jungers, Raphaël;et.al.
(2024) 6th Annual Learning for Dynamics & Control Conference — Location: Oxford (15.July.2024)

Files

L4DC24_submission_Debauche_Edwards_Jungers_Abate.pdf
  • Restricted Access
  • Adobe PDF
  • 413.58 KB
Request a copy

Details

Authors
Abstract
This paper presents a neural network-based algorithm with soundness guarantees to study the stability of discrete-time linear switched systems. This algorithm is cast as a counterexample guided inductive synthesis (CEGIS) architecture: an iterative structure which alternates between the learner, which provides a candidate Lyapunov function, and the verifier which checks its validity over the whole domain. We choose a ReLU neural network as learner to take advantage of its expressivity power and flexibility, and a satisfiability module theories (SMT) solver as verifier. In addition, we introduce a post processing step to leverage a valid Lyapunov function from the neural network in case of failure of the CEGIS loop. We provide several examples to illustrate the entire algorithm.
Affiliations

Citations

  • APA
  • Chicago
  • FWB

Debauche, V., Jungers, R., & et al. (2024). Formal Synthesis of Lyapunov Stability Certificates for Linear Switched Systems using ReLU Neural Networks. 6th Annual Learning for Dynamics & Control Conference, Oxford. https://hdl.handle.net/2078.5/252034