Compositionally Verifiable Vector Neural Lyapunov Functions for Stability Analysis of Interconnected Nonlinear Systems
While there has been increasing interest in using neural networks to compute Lyapunov functions, verifying that these functions satisfy the Lyapunov conditions and certifying stability regions remain challenging due to the curse of dimensionality. In this paper, we demonstrate that by leveraging the compositional structure of interconnected nonlinear systems, it is possible to verify neural Lyapunov functions for high-dimensional systems beyond the capabilities of current satisfiability modulo theories (SMT) solvers using a monolithic approach. Our numerical examples employ neural Lyapunov functions trained by solving Zubov's partial differential equation (PDE), which characterizes the domain of attraction for individual subsystems. These examples show a performance advantage over sums-of-squares (SOS) polynomial Lyapunov functions derived from semidefinite programming.
Code (1)
Similar Papers 제목 키워드 기반
Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions
We investigate the formal synthesis of global polynomial Lyapunov functions for polynomial vector fields. We establish that a sign-definite polynomial must satisfy specific algebraic constraints, which we leverage to dev…
Design SynthesisvalidStability Analysis for Stochastic Hybrid Inclusions
Stochastic hybrid inclusions (SHIs) address situations with the stochastic continuous evolution in a stochastic differential inclusions and random jumps in the difference inclusions due to the forced (the state reaching …
Construction of Lyapunov Functions Using Vector Field Decomposition
In the present paper, a novel vector field decomposition based approach for constructing Lyapunov functions is proposed. For a given dynamical system, if the defining vector field admits a decomposition into two mutually…
Learning Koopman-based Stability Certificates for Unknown Nonlinear Systems
Koopman operator theory has gained significant attention in recent years for identifying discrete-time nonlinear systems by embedding them into an infinite-dimensional linear vector space. However, providing stability gu…
Construction of time-varying ISS-Lyapunov Functions for Impulsive Systems
Time-varying ISS-Lyapunov functions for impulsive systems provide a necessary and sufficient condition for ISS. This property makes them a more powerful tool for stability analysis than classical candidate ISS-Lyapunov f…