Contributions to Semialgebraic-Set-Based Stability Verification of Dynamical Systems with Neural-Network-Based Controllers

Neural-network-based controllers (NNCs) can represent complex, highly nonlinear control laws, but verifying the closed-loop stability of dynamical systems using them remains challenging. This work presents contributions to a state-of-the-art stability verification procedure for NNC-controlled systems which relies on semialgebraic-set-based input-output modeling to pose the search for a Lyapunov function as an optimization problem. Specifically, this procedure's conservatism when analyzing NNCs using transcendental activation functions and the restriction to feedforward NNCs are addressed by a) introducing novel semialgebraic activation functions that preserve key properties of common transcendental activations and b) proving compatibility of NNCs from the broader class of recurrent equilibrium networks (RENs) with this procedure. Furthermore, the indirect optimization of a local region of attraction (RoA) estimate using a restricted set of candidate Lyapunov functions is greatly improved via c) the introduction of a richer parameterization of candidate Lyapunov functions than previously reported and d) the formulation of novel semidefinite programs (SDPs) that directly optimize the resulting RoA estimate. The value of these contributions is highlighted in two numerical examples.