Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formally Verified Neural Lyapunov Function for Incremental Input-to-State Stability of Unknown Systems

Ahan Basu, Bhabani Shankar Dey, Pushpak Jagtap

TL;DR

The paper addresses certifying $δ$-ISS for unknown discrete-time systems by learning a Lyapunov-like function parameterized as a neural network. It reframes the $δ$-ISS conditions into a robust optimization and then into a Scenario Convex Program (SCP) using sampled data, establishing a validity condition that connects SCP feasibility to the original Lyapunov inequalities. A training framework with Lyapunov-based loss terms and Lipschitz constraints yields provably correct neural $δ$-ISS Lyapunov functions without post-training verification. Validated on a scalar nonlinear system and a permanent magnet DC motor, the method demonstrates incremental stability under bounded inputs for systems with unknown dynamics.

Abstract

This work presents an approach to synthesize a Lyapunov-like function to ensure incrementally input-to-state stability ($δ$-ISS) property for an unknown discrete-time system. To deal with challenges posed by unknown system dynamics, we parameterize the Lyapunov-like function as a neural network, which we train using the data samples collected from the unknown system along with appropriately designed loss functions. We propose a validity condition to test the obtained function and incorporate it into the training framework to ensure provable correctness at the end of the training. Finally, the usefulness of the proposed technique is proved using two case studies: a scalar non-linear dynamical system and a permanent magnet DC motor.

Formally Verified Neural Lyapunov Function for Incremental Input-to-State Stability of Unknown Systems

TL;DR

The paper addresses certifying -ISS for unknown discrete-time systems by learning a Lyapunov-like function parameterized as a neural network. It reframes the -ISS conditions into a robust optimization and then into a Scenario Convex Program (SCP) using sampled data, establishing a validity condition that connects SCP feasibility to the original Lyapunov inequalities. A training framework with Lyapunov-based loss terms and Lipschitz constraints yields provably correct neural -ISS Lyapunov functions without post-training verification. Validated on a scalar nonlinear system and a permanent magnet DC motor, the method demonstrates incremental stability under bounded inputs for systems with unknown dynamics.

Abstract

This work presents an approach to synthesize a Lyapunov-like function to ensure incrementally input-to-state stability (-ISS) property for an unknown discrete-time system. To deal with challenges posed by unknown system dynamics, we parameterize the Lyapunov-like function as a neural network, which we train using the data samples collected from the unknown system along with appropriately designed loss functions. We propose a validity condition to test the obtained function and incorporate it into the training framework to ensure provable correctness at the end of the training. Finally, the usefulness of the proposed technique is proved using two case studies: a scalar non-linear dynamical system and a permanent magnet DC motor.
Paper Structure (13 sections, 3 theorems, 17 equations, 3 figures)

This paper contains 13 sections, 3 theorems, 17 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Incremental Stability
  3. Notations
  4. Definitions
  5. Problem Formulation
  6. Neural $\delta$-ISS Lyapunov Function
  7. Training Provably Correct Neural $\delta$-ISS Lyapunov Function
  8. Neural Network Structure
  9. Training with Formal Guarantees
  10. Case Study
  11. Numerical Example
  12. Permanent Magnet DC Motor
  13. Conclusion and Future work

Key Result

Theorem 2.4

The discrete-time control system $\Xi$ is $\delta$-ISS if it admits a $\delta$-ISS Lyapunov function.

Figures (3)

  • Figure 1: Top: State response of a simple nonlinear system as in \ref{['eq:case1']}, where the blue curve is influenced under input $u$ = 0.43, and the red curve is influenced under input $u$ = 0.45. Bottom: Difference between trajectories subjected to different initial conditions and inputs.
  • Figure 2: Top: Armature Current for DC motor, where the blue curve is influenced under input Vin = 0.17, and the red curve is influenced under input Vin = 0.18. Bottom: The difference in armature currents subjected to different initial conditions and input voltages.
  • Figure 3: Top: The rotor speed for DC motor, where the blue curve is influenced under input Vin = 0.17, and the red curve is influenced under input Vin = 0.18. Bottom: The difference in rotor speeds subjected to different initial conditions and input voltages.

Theorems & Definitions (10)

  • Definition 2.1: Discrete-time Systems
  • Definition 2.2: $\delta$-ISS Angeli
  • Definition 2.3: $\delta$-ISS Lyapunov function DT-ISS_prop
  • Theorem 2.4: DT-ISS
  • Remark 3.1
  • Theorem 3.2
  • Proof 3.3
  • Theorem 4.1
  • Remark 4.2
  • Remark 4.3