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

TL;DR

The paper tackles the challenge of certifying closed-loop stability for systems controlled by neural networks by improving a semialgebraic-set-based verification framework. It introduces exact semialgebraic activation functions to reduce conservatism and extends the modeling to well-posed recurrent equilibrium networks (RENs), enabling a broader class of NNCs to be analyzed. A richer, explicit family of local Lyapunov candidates is developed, together with a novel sequence of SDPs that directly optimizes inner ROA estimates, improving local stability certificates. The method is validated on two numerical examples, demonstrating larger ROAs and applicability to REN-based controllers, thereby broadening the practical impact of SDP/SOS-based stability verification for neural-network-controlled dynamical systems.

Abstract

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.

Figures (6)

• Figure 1: Block diagram of a general discrete-time closed-loop dynamical system with a neural-network-based controller $\varphi$. The stability properties of systems of this form are examined in this work.
• Figure 2: Schematic of \ref{['subfig:NeuralNetworkGraph']} the neural network $\varphi$, which is modeled via its graph by the semialegbraic set $\mathbf{K}_\varphi$ and \ref{['subfig:OpenLoopGraph']} the composed loop $L = \varphi \circ f \circ (\textrm{id}, \varphi)$, which is modeled via its graph by the semialegbraic set $\mathbf{K}_{L}$.
• Figure 3: Comparison of \ref{['subfig:softplus_approximation']}$\text{softplus}(x)$ and the semialgebraic function $\hat{\phi}_{\textrm{sp}}(x)$ over the interval $[-5, 5]$ for $c_{\textrm{sp}} = \ln(2)^2 \approx 0.480$ and \ref{['subfig:tanh_approximation']}$\text{tanh}(x)$ and the semialgebraic function $\hat{\phi}_{\textrm{tanh}}(x)$ over the interval $[-5, 5]$ for $c_{\textrm{tanh}} = 1.171$.
• Figure 4: Block diagrams of \ref{['subfig:PreRENTransformation']} an open-loop system $x^+ = f(x,u)$ in closed-loop with a REN-based NNC shown via fractional transformation in the dotted box, and \ref{['subfig:PostRENTransformation']} the equivalent system obtained by augmenting the state of and input to the dynamical system with the REN's internal state variable $x_\varphi$ and hidden variable $\lambda$, respectively.
• Figure 5: Phase portrait of the closed-loop system under the neural network control law of \ref{['sec:ImplicitSpringMassDamper']}, shown in blue. Six level sets of the Lyapunov function $\tilde{V}$ solving SDP \ref{['eq:SDPFormulationGlobalAsymptoticStability']} are shown.

Theorems & Definitions (23)

• Definition II.1: Global Asymptotic Stability
• Definition II.2: Local Asymptotic Stability
• Definition II.3: Region of Attraction
• Definition II.4: Lyapunov Function, Def. B.12 mybibfile:Rawlings2017
• Definition II.5: Graph of a function
• Example 1
• Example 2
• Example 3
• Definition II.6: SOS polynomial
• Theorem II.7