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

TL;DR

This paper introduces a PDE-based framework using neural networks to learn and verify Lyapunov-barrier functions, enabling stability and safety certification for nonlinear systems with improved domain of attraction estimation.

Contribution

It proposes a novel Zubov PDE formulation with boundary conditions on the safe set, extending Lyapunov-barrier theorems with a neural network approach for nonlinear system safety verification.

Findings

Neural network solutions can serve as Lyapunov-barrier functions after formal verification.

The PDE framework provides near-optimal safe domain under-approximations.

The method extends existing theorems to nonlinear systems with safety constraints.

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.