Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compositionally Verifiable Vector Neural Lyapunov Functions for Stability Analysis of Interconnected Nonlinear Systems

Jun Liu, Yiming Meng, Maxwell Fitzsimmons, Ruikun Zhou

TL;DR

By leveraging the compositional structure of interconnected nonlinear systems, it is demonstrated 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.

Abstract

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.

Compositionally Verifiable Vector Neural Lyapunov Functions for Stability Analysis of Interconnected Nonlinear Systems

TL;DR

By leveraging the compositional structure of interconnected nonlinear systems, it is demonstrated 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.

Abstract

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.
Paper Structure (19 sections, 2 theorems, 33 equations, 2 figures, 1 table)

This paper contains 19 sections, 2 theorems, 33 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Interconnected system
  4. Problem formulation
  5. Stability and reachability analysis using vector Lyapunov functions
  6. Local stability analysis
  7. Reachability analysis
  8. Training vector neural Lyapunov functions and SMT verification
  9. Training neural Lyapunov functions for subsystems
  10. Verification of stability and reachability using vector neural Lyapunov functions and SMT solvers
  11. Compositional nature of SMT verification
  12. Numerical results
  13. Networked Van der Pol oscillators
  14. Hyperparameters
  15. Results and discussions
  16. ...and 4 more sections

Key Result

Proposition 1

Let $P_i$ and $Q_i$ satisfy (eq:lyap). For each $i=1,\ldots,l$ and $p>0$, define the set Suppose that there exists a positive vector $c=(c_1,\ldots,c_l)\in\mathbb R^l$ and a matrix of nonnegative elements $R=(r_{ij})$ such that the following inequalities hold: for all $x_i\in \mathcal{P}_i(c_i)$ and $x_j\in \mathcal{P}_j(c_j)$. Define $\Lambda = (\lambda_{ij})$ by If there exists a positive vec

Figures (2)

  • Figure 1: Two networks with different densities of interconnections by varying the number of nonzero entries in the set ${ \mu_{ij} }$ for the Van der Pol network.
  • Figure 2: Neural stability analysis on a 20-dimensional interconnected system: sub-level sets of neural Lyapunov functions liu2023towards, which define regions of attraction, are verified by the SMT solver dReal gao2013dreal using the approach described in Section \ref{['sec:method:verify']}. The thick solid lines represent the regions of attraction for the interconnected system, while the thin dashed lines indicate those for individual subsystems.

Theorems & Definitions (6)

  • Definition 1: Domain of Attraction
  • Proposition 1
  • Proposition 2
  • proof
  • proof
  • proof