Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Learning and Verifying Maximal Lyapunov-Barrier Functions with a Zubov PDE Formulation

Yiming Meng, Jun Liu

TL;DR

This work addresses the challenge of jointly certifying stability and safety for autonomous nonlinear systems by formulating a Zubov-type PDE with Dirichlet boundary conditions on the safe set and solving it with physics-informed neural networks (PINNs) that are formally verified to yield a Lyapunov–barrier function. The authors construct a maximal Lyapunov function $V$ on the domain $\mathcal{D}$ via a proper indicator on the safe complement $\mathcal{D}_s=U^c$ and dynamic programming principles, then transform $V$ into a Lyapunov–barrier function $W$ through a Zubov transformation to obtain a Dirichlet-Zubov PDE whose unique viscosity solution certifies stability and safety. To facilitate learning, they introduce an extended-domain formulation with a modified vector field $\tilde{f}$ that ensures solvability on a larger ROI $\Omega$ while preserving $W$ on the original domain $\mathcal{D}_s$. Numerically, the approach is demonstrated on nonlinear systems (e.g., reversed Van der Pol and a two-machine power system) using LyZNet-PINNs, with formal verification via SMT solvers, demonstrating effective recovery of a near-maximal safe domain of attraction and providing a foundation for learning CLBFs through PDE formulations. These results offer a unified, verifiable certificate for both stability and safety and point to future work on unknown systems and broader applicability of PDE-based CLBF learning.

Abstract

Verifying stability and safety guarantees for nonlinear systems has received considerable attention in recent years. This property serves as a fundamental building block for specifying more complex system behaviors and control objectives. However, estimating the domain of attraction under safety constraints and constructing a Lyapunov-barrier function remain challenging tasks for nonlinear systems. To address this problem, we propose a Zubov PDE formulation with a Dirichlet boundary condition for autonomous nonlinear systems and show that a physics-informed neural network solution, once formally verified, can serve as a Lyapunov-barrier function that jointly certifies stability and safety. This approach extends existing converse Lyapunov-barrier theorems by introducing a PDE-based framework with boundary conditions defined on the safe set, yielding a near-optimal certified under-approximation of the true safe domain of attraction.

Towards Learning and Verifying Maximal Lyapunov-Barrier Functions with a Zubov PDE Formulation

TL;DR

This work addresses the challenge of jointly certifying stability and safety for autonomous nonlinear systems by formulating a Zubov-type PDE with Dirichlet boundary conditions on the safe set and solving it with physics-informed neural networks (PINNs) that are formally verified to yield a Lyapunov–barrier function. The authors construct a maximal Lyapunov function on the domain via a proper indicator on the safe complement and dynamic programming principles, then transform into a Lyapunov–barrier function through a Zubov transformation to obtain a Dirichlet-Zubov PDE whose unique viscosity solution certifies stability and safety. To facilitate learning, they introduce an extended-domain formulation with a modified vector field that ensures solvability on a larger ROI while preserving on the original domain . Numerically, the approach is demonstrated on nonlinear systems (e.g., reversed Van der Pol and a two-machine power system) using LyZNet-PINNs, with formal verification via SMT solvers, demonstrating effective recovery of a near-maximal safe domain of attraction and providing a foundation for learning CLBFs through PDE formulations. These results offer a unified, verifiable certificate for both stability and safety and point to future work on unknown systems and broader applicability of PDE-based CLBF learning.

Abstract

Verifying stability and safety guarantees for nonlinear systems has received considerable attention in recent years. This property serves as a fundamental building block for specifying more complex system behaviors and control objectives. However, estimating the domain of attraction under safety constraints and constructing a Lyapunov-barrier function remain challenging tasks for nonlinear systems. To address this problem, we propose a Zubov PDE formulation with a Dirichlet boundary condition for autonomous nonlinear systems and show that a physics-informed neural network solution, once formally verified, can serve as a Lyapunov-barrier function that jointly certifies stability and safety. This approach extends existing converse Lyapunov-barrier theorems by introducing a PDE-based framework with boundary conditions defined on the safe set, yielding a near-optimal certified under-approximation of the true safe domain of attraction.

Paper Structure

This paper contains 11 sections, 2 theorems, 25 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Dynamical Systems and Concept of Stability-with-Safety
  4. Converse Lyapunov–barrier Function Theorem from Previous Work
  5. Problem Formulation
  6. Converse Lyapunov-Barrier Function for Stability with Safety Guarantees
  7. Maximal Converse Lyapunov Function for Stability-with-Safety Specification
  8. Lyapunov–barrier Function via Zubov Equation and Dirichlet Boundary Value Problem
  9. Equivalent Formulation of the Dirichlet–Zubov Problem
  10. Numerical Examples
  11. Conclusion

Key Result

Proposition 1

Let $\overline{\mathbb R} = \mathbb R\cup\left\{-\infty, \infty\right\}$ denote the extended real number system, equipped with the standard extended real arithmetic $a + (+\infty) = +\infty$ for all $a\in\mathbb R\cup\left\{+\infty\right\}$. Then, for all $x\in \mathbb R^n$, Furthermore, for all $x\in\mathbb R^n$ and for all $t\geq 0$, $\tau(x)<\infty$ if and only if $\mathds{1}_{\left\{t\leq \ta

Figures (4)

  • Figure 1: Visualization of the safe domain of attraction for the reversed Van der Pol oscillator with artificial obstacles. The regions enclosed by the red curves represent the obstacles.
  • Figure 2: Learned Lyapunov–barrier functions and verified level sets (shown in solid blue) for the reversed Van der Pol oscillator with artificial obstacles. The dashed red curves represent the largest verifiable safe regions of attraction obtained using a quadratic Lyapunov function.
  • Figure 3: Visualization of the safe domain of attraction for the Two-Machine Power System with artificial obstacles. The regions enclosed by the red curves represent the obstacles.
  • Figure 4: Learned Lyapunov–barrier functions and verified level sets (shown in solid blue) for the two-machine power system with artificial obstacles. The dashed red curves represent the largest verifiable safe regions of attraction obtained using a quadratic Lyapunov function.

Theorems & Definitions (15)

  • Definition 1: Forward invariance
  • Definition 2: Domain of attraction
  • Definition 3: Stability-with-safety guarantee
  • Definition 4
  • Example 1
  • Proposition 1
  • proof
  • proof
  • proof
  • Example 2
  • ...and 5 more