SEROAISE: Advancing ROA Estimation for ReLU and PWA Dynamics through Estimating Certified Invariant Sets

TL;DR

The paper tackles estimating the Region of Attraction ($RoA$) for dynamics described by Piecewise Affine ($PWA$) models or ReLU-activated neural networks. It introduces SEROAISE, a two-stage approach that first constructs a certified invariant subset via Iterative Invariant Set Estimation ($IISE$) and Non-Uniform Growth of Invariant Sets ($NUGIS$), and then performs a Lyapunov-like, $PWA$-based verification inside that subset to certify the $RoA$. A key novelty is the $NUGIS$ concept, which enables non-uniform, guaranteed expansion of invariant sets to reduce conservatism and improve RoA size without resorting to expensive SMT/MIP verifications. The framework is demonstrated on path-following, inverted-pendulum, and cart-pole examples with NN controllers, showing substantial RoA improvements and providing public code for reproducibility.

Abstract

This paper presents a novel framework for constructing the Region of Attraction (RoA) for dynamics derived either from Piecewise Affine (PWA) functions or from Neural Networks (NNs) with Rectified Linear Units (ReLU) activation function. This method, described as Sequential Estimation of RoA based on Invariant Set Estimation (SEROAISE), computes a Lyapunov-like PWA function over a certified PWA invariant set. While traditional approaches search for Lyapunov functions by enforcing Lyapunov conditions over pre-selected domains, this framework enforces Lyapunov-like conditions over a certified invariant subset obtained using the Iterative Invariant Set Estimator(IISE). Compared to the state-of-the-art, IISE provides systematically larger certified invariant sets. In order to find a larger invariant subset, the IISE utilizes a novel concept known as the Non-Uniform Growth of Invariant Set (NUGIS). A number of examples illustrating the efficacy of the proposed methods are provided, including dynamical systems derived from learning algorithms. The implementation is publicly available at: https://github.com/PouyaSamanipour/SEROAISE.git.

Figures (8)

• Figure 1: Three different approaches for selection of the domain over which Lyapunov stability conditions are enforced when computationally searching for Lyapunov functions.
• Figure 2: Non-uniform Growth of the invariant set for points within the interior of the cells such as $\boldsymbol{x}$ and points on their boundary such as $v_7$ by creating simplex cells as described in Theorem \ref{['th:LGD']}. $\dot{x}_i$ represents the vector field at each vertex of these cells. The normal vector of the invariant set toward the origin is $s_i$ for cell $X_i$.
• Figure 3: If $E' \dot{x}(v_j) < 0$, the vertex $v_j$ cannot be included in any invariant set $S \subseteq \overline{\mathcal{D}}$.
• Figure 4: Vertex categorization for IISE, where blue region denotes a $\mathrm{PWA}$ certified invariant set interior, green segments show $\textbf{NUGIS}$ points, black segments show points that could stay on the boundary of the invariant set, and the red border marks the exclusion zone. The purple denotes the points that refer to the $I_{UC}$ as described in category \ref{['cat5:Unclass']}.
• Figure 5: The process of updating the $\mathcal{K}_{\infty}$ function $\alpha_m(x)$ in each iteration with learning rate $\gamma$.