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

TL;DR

This paper introduces a novel framework for accurately estimating safe domains of attraction in discrete-time nonlinear systems, leveraging a new Zubov equation and neural network approximations with verifiable guarantees.

Contribution

It derives a new Zubov equation for safe domain estimation and develops a neural network-based approach with verification tools for certifiable estimates.

Findings

The Zubov equation solution is unique and continuous.

Neural network approximations can effectively estimate safe domains.

Verification tools provide certifiable guarantees for the estimated domains.

Abstract

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., $\alpha,\!\beta$-CROWN and dReal). To illustrate its effectiveness, we demonstrate our approach through numerical examples concerning nonlinear systems with state constraints.