Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems

Ahan Basu, Bhabani Shankar Dey, Pushpak Jagtap

TL;DR

This work addresses enforcing incremental stability for unknown discrete-time systems by jointly synthesizing a neural network controller and a $\delta$-ISS control Lyapunov function ($\delta$-ISS-CLF). The authors formulate a data-driven training framework that embeds a formal validity condition, leveraging Control Barrier Functions to ensure forward invariance of a compact state set and a robust scenario convex program to certify $\delta$-ISS properties. They provide theoretical proofs linking the SCP-derived conditions to deterministic guarantees and demonstrate the approach on four diverse case studies, including a scalar non-affine system, a one-link manipulator, a jet engine model, and a rotating spacecraft. The results show successful convergence to verifiably correct $\delta$-ISS-CLFs and neural controllers, suggesting scalable applicability to uncertain nonlinear discrete-time dynamics with practical safety and robustness implications.

Abstract

This work aims to synthesize a controller that ensures that an unknown discrete-time system is incrementally input-to-state stable ($δ$-ISS). In this work, we introduce the notion of $δ$-ISS control Lyapunov function ($δ$-ISS-CLF), which, in conjunction with the controller, ensures that the closed-loop system is incrementally ISS. To address the unknown dynamics of the system, we parameterize the controller as well as the $δ$-ISS-CLF as neural networks and learn them by utilizing the sampled data from the state space of the unknown system. To formally verify the obtained $δ$-ISS-CLF, we develop a validity condition and incorporate the condition into the training framework to ensure a provable correctness guarantee at the end of the training process. Finally, the usefulness of the proposed approach is proved using multiple case studies - the first one is a scalar system with a non-affine non-polynomial structure, the second example is a one-link manipulator system, the third system is a nonlinear Moore-Grietzer model of the jet engine and the final one is a rotating rigid spacecraft model.

Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems

TL;DR

This work addresses enforcing incremental stability for unknown discrete-time systems by jointly synthesizing a neural network controller and a -ISS control Lyapunov function (-ISS-CLF). The authors formulate a data-driven training framework that embeds a formal validity condition, leveraging Control Barrier Functions to ensure forward invariance of a compact state set and a robust scenario convex program to certify -ISS properties. They provide theoretical proofs linking the SCP-derived conditions to deterministic guarantees and demonstrate the approach on four diverse case studies, including a scalar non-affine system, a one-link manipulator, a jet engine model, and a rotating spacecraft. The results show successful convergence to verifiably correct -ISS-CLFs and neural controllers, suggesting scalable applicability to uncertain nonlinear discrete-time dynamics with practical safety and robustness implications.

Abstract

This work aims to synthesize a controller that ensures that an unknown discrete-time system is incrementally input-to-state stable (-ISS). In this work, we introduce the notion of -ISS control Lyapunov function (-ISS-CLF), which, in conjunction with the controller, ensures that the closed-loop system is incrementally ISS. To address the unknown dynamics of the system, we parameterize the controller as well as the -ISS-CLF as neural networks and learn them by utilizing the sampled data from the state space of the unknown system. To formally verify the obtained -ISS-CLF, we develop a validity condition and incorporate the condition into the training framework to ensure a provable correctness guarantee at the end of the training process. Finally, the usefulness of the proposed approach is proved using multiple case studies - the first one is a scalar system with a non-affine non-polynomial structure, the second example is a one-link manipulator system, the third system is a nonlinear Moore-Grietzer model of the jet engine and the final one is a rotating rigid spacecraft model.

Paper Structure

This paper contains 21 sections, 7 theorems, 29 equations, 4 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Formulation
  3. Incremental Input-to-State Stability
  4. Proof:
  5. Proof:
  6. Control Barrier Function
  7. Proof:
  8. Problem Formulation
  9. Neural $\delta$-ISS Control Lyapunov Function
  10. Construction of SOP and formal verification
  11. Proof:
  12. Formulation of Loss functions and Training procedure
  13. Proof:
  14. Case Studies
  15. Simple Nonlinear System
  16. ...and 6 more sections

Key Result

Theorem 2.4

The closed-loop discrete-time control system eq:system is said to be incrementally input-to-state stable with respect to input ${\mathsf{w}}$, if there exists a $\delta$-ISS control Lyapunov function as defined in Definition def:ISS-Lf_gen.

Figures (4)

  • Figure 1: (a)Trajectories starting from different initial conditions under same input signals, (b) Trajectories starting from different initial conditions under different input signals (${\mathsf{w}}(k) = 0.2$ for red curves, ${\mathsf{w}}(k) = -0.1$ for blue curves) (c) The $\delta$-ISS-CLF plot is greater than zero for all $(x, \hat{x}) \in {\mathbf{X}} \times {\mathbf{X}}, x \neq \hat{x}$ and equal to zero while $x = \hat{x}$, (d) The Lyapunov value over the trajectories is decaying with time with the heatmap showing Lyapunov level sets.
  • Figure 2: Top: Angular position (left) and velocity (right) of the manipulator, where the blue curve is influenced under input ${\mathsf{w}}(k) = 0.4 \in {\mathbf{W}}$, and the red curve is influenced under input ${\mathsf{w}}(k) = 0.3 \in {\mathbf{W}}$ for all $k \in {\mathbb{N}}_0$. Bottom: The difference in angular positions (left) and velocities (right) subjected to different initial conditions and input torques.
  • Figure 3: Top: Mass flow (left) and pressure rise (right) of the Jet-engine model, where the blue curve is influenced under input ${\mathsf{w}}(k) = -0.15 \in {\mathbf{W}}$, and the red curve is influenced under input ${\mathsf{w}}(k) = -0.3 \in {\mathbf{W}}$ for all $k \in {\mathbb{N}}_0$. Bottom: The difference in mass flow (left) and pressure rise (right) subjected to different initial conditions and input flows through the throttle.
  • Figure 4: Top: Trajectories ((a) $\omega_1$, (b) $\omega_2$, (c) $\omega_3$) starting from different initial conditions under different input signals (for all $k\in{\mathbb{N}}_0$, ${\mathsf{w}}(k)= -\sin(k)\in {\mathbf{W}}$ for blue curve and $\hat{{\mathsf{w}}}(k) = \cos^2(k/2) \in {\mathbf{W}}$ for red curve), Bottom: The difference between the trajectories corresponding to different states.

Theorems & Definitions (18)

  • Definition 2.1: Discrete-time Control Systems
  • Definition 2.2: $\delta$-ISS DT-ISS
  • Definition 2.3
  • Theorem 2.4
  • Definition 2.5: Robustly Forward Invariant Set liu2019compositional
  • Definition 2.6
  • Theorem 2.7
  • Definition 2.8: Neural_CBF
  • Lemma 2.9
  • Remark 3.1
  • ...and 8 more