Verifying Probabilistic Regions of Attraction with Neural Lyapunov Functions for Stochastic Systems

Fuente: arXiv
Salvato in:
Dettagli Bibliografici
Autori principali: Su, Yun, De Sterck, Hans, Liu, Jun
Natura: Preprint
Pubblicazione: 2025
Soggetti:
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866908509371629568
author Su, Yun
De Sterck, Hans
Liu, Jun
author_facet Su, Yun
De Sterck, Hans
Liu, Jun
contents Leveraging a stochastic extension of Zubov's equation, we develop a physics-informed neural network (PINN) approach for learning a neural Lyapunov function that captures the largest probabilistic region of attraction (ROA) for stochastic systems. We then provide sufficient conditions for the learned neural Lyapunov functions that can be readily verified by satisfiability modulo theories (SMT) solvers, enabling formal verification of both local stability analysis and probabilistic ROA estimates. By solving Zubov's equation for the maximal Lyapunov function, our method provides more accurate and larger probabilistic ROA estimates than traditional sum-of-squares (SOS) methods. Numerical experiments on nonlinear stochastic systems validate the effectiveness of our approach in training and verifying neural Lyapunov functions for probabilistic stability analysis and ROA estimates.
format Preprint
id arxiv_https___arxiv_org_abs_2508_21213
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Verifying Probabilistic Regions of Attraction with Neural Lyapunov Functions for Stochastic Systems
Su, Yun
De Sterck, Hans
Liu, Jun
Optimization and Control
Leveraging a stochastic extension of Zubov's equation, we develop a physics-informed neural network (PINN) approach for learning a neural Lyapunov function that captures the largest probabilistic region of attraction (ROA) for stochastic systems. We then provide sufficient conditions for the learned neural Lyapunov functions that can be readily verified by satisfiability modulo theories (SMT) solvers, enabling formal verification of both local stability analysis and probabilistic ROA estimates. By solving Zubov's equation for the maximal Lyapunov function, our method provides more accurate and larger probabilistic ROA estimates than traditional sum-of-squares (SOS) methods. Numerical experiments on nonlinear stochastic systems validate the effectiveness of our approach in training and verifying neural Lyapunov functions for probabilistic stability analysis and ROA estimates.
title Verifying Probabilistic Regions of Attraction with Neural Lyapunov Functions for Stochastic Systems
topic Optimization and Control
url https://arxiv.org/abs/2508.21213