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.
@article{arxiv.2511.09523,
title = {Towards Learning and Verifying Maximal Lyapunov-Barrier Functions with a Zubov PDE Formulation},
author = {Yiming Meng and Jun Liu},
journal= {arXiv preprint arXiv:2511.09523},
year = {2025}
}