# Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimation

arXiv: https://arxiv.org/abs/2506.13961 · HTML: https://mlsanity.com/paper/2506.13961/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 33 references that are in the map.
- First posted on arXiv 16 Jun 2025.

## Builds on (most cited first, 17 of 17)

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees](https://mlsanity.com/paper/2206.01913/) (2022)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [Neural Lyapunov Control for Discrete-Time Systems](https://mlsanity.com/paper/2305.06547/) (2023)
- [Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification](https://mlsanity.com/paper/2312.09131/) (2023)
- [Learning Region of Attraction for Nonlinear Systems](https://mlsanity.com/paper/2110.00731/) (2021)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction](https://mlsanity.com/paper/2403.10013/) (2024)
- [Underapproximating Safe Domains of Attraction for Discrete-Time Systems Using Implicit Representations of Backward Reachable Sets](https://mlsanity.com/paper/2409.10657/) (2024)

## Built on by (most cited first, 3 of 3)

- [Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers](https://mlsanity.com/paper/2605.25346/) (2026)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Safe and Robust Domains of Attraction for Discrete-Time Systems: A Set-Based Characterization and Certifiable Neural Network Estimation](https://mlsanity.com/paper/2603.03082/) (2026)

## Abstract (arXiv)

Analysis of nonlinear autonomous systems typically involves estimating domains of attraction, which have been a topic of extensive research interest for decades. Despite that, accurately estimating domains of attraction for nonlinear systems remains a challenging task, where existing methods are conservative or limited to low-dimensional systems. The estimation becomes even more challenging when accounting for state constraints. In this work, we propose a framework to accurately estimate safe (state-constrained) domains of attraction for discrete-time autonomous nonlinear systems. In establishing this framework, we first derive a new Zubov equation, whose solution corresponds to the exact safe domain of attraction. The solution to the aforementioned Zubov equation is shown to be unique and continuous over the whole state space. We then present a physics-informed approach to approximating the solution of the Zubov equation using neural networks. To obtain certifiable estimates of the domain of attraction from the neural network approximate solutions, we propose a verification framework that can be implemented using standard verification tools (e.g., α,!β-CROWN and dReal). To illustrate its effectiveness, we demonstrate our approach through numerical examples concerning nonlinear systems with state constraints.