Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Scalable Formal Verification of Incremental Stability in Large-Scale Systems Using Graph Neural Networks

Ahan Basu, Mahathi Anand, Pushpak Jagtap

TL;DR

This work tackles the scalable verification of incremental stability in large-scale interconnected systems with unknown subsystem dynamics but known interconnection topology. It introduces a distributed approach that learns local $\delta$-ISS Lyapunov functions for each subsystem and composes them to certify global stability, leveraging Graph Neural Networks to align with the network structure. A Lipschitz-based, sampling-based verification guarantees formal correctness of the learned certificates, enabling scalable validation over the full state-action space. The authors validate the framework on two nonlinear case studies, demonstrating the method's scalability from tens to thousands of subsystems and its potential for practical deployment in distributed settings.

Abstract

This work proposes a novel distributed framework for verifying the incremental stability of large-scale systems with unknown dynamics and known interconnection structures using graph neural networks. Our proposed approach relies on the construction of local incremental Lyapunov functions for subsystems, which are then composed together to obtain a suitable Lyapunov function for the interconnected system. Graph neural networks are used to synthesize these functions in a data-driven fashion. The formal correctness guarantee is then obtained by leveraging Lipschitz bounds of the trained neural networks. Finally, the effectiveness of our approach is validated through two nonlinear case studies.

Scalable Formal Verification of Incremental Stability in Large-Scale Systems Using Graph Neural Networks

TL;DR

This work tackles the scalable verification of incremental stability in large-scale interconnected systems with unknown subsystem dynamics but known interconnection topology. It introduces a distributed approach that learns local -ISS Lyapunov functions for each subsystem and composes them to certify global stability, leveraging Graph Neural Networks to align with the network structure. A Lipschitz-based, sampling-based verification guarantees formal correctness of the learned certificates, enabling scalable validation over the full state-action space. The authors validate the framework on two nonlinear case studies, demonstrating the method's scalability from tens to thousands of subsystems and its potential for practical deployment in distributed settings.

Abstract

This work proposes a novel distributed framework for verifying the incremental stability of large-scale systems with unknown dynamics and known interconnection structures using graph neural networks. Our proposed approach relies on the construction of local incremental Lyapunov functions for subsystems, which are then composed together to obtain a suitable Lyapunov function for the interconnected system. Graph neural networks are used to synthesize these functions in a data-driven fashion. The formal correctness guarantee is then obtained by leveraging Lipschitz bounds of the trained neural networks. Finally, the effectiveness of our approach is validated through two nonlinear case studies.

Paper Structure

This paper contains 16 sections, 4 theorems, 15 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Formulation
  3. Notations
  4. Incremental Stability for Interconnected Systems
  5. Proof:
  6. Problem Formulation
  7. Distributed Construction of $\delta$-ISS Lyapunov Functions
  8. Proof:
  9. Proof:
  10. GNN-based Lyapunov Functions for Unknown Interconnected Systems
  11. Graph Neural Network Architecture
  12. Training Procedure
  13. Formal Correctness Guarantees
  14. Proof:
  15. Case Study
  16. ...and 1 more sections

Key Result

Theorem 2.2

The interconnected dt-NHS $\Upsilon$ as in eq:complete is said to be incrementally input-to-state stable ($\delta$-ISS) if there exists a function $V:{\mathbb{R}}^{N\times n} \times {\mathbb{R}}^{N \times n} \rightarrow {\mathbb{R}}$ of degree $\kappa \in {\mathbb{N}}^+$ with class $\mathcal{K}_\inf

Figures (2)

  • Figure 1: (a) Trajectories of a subsystem starting from different initial conditions converge towards each other. (b) The Lyapunov value over the trajectory decays, indicating $\delta$-GAS in the absence of external input.
  • Figure 2: (a) Trajectories of a subsystem starting from different initial conditions converge towards each other. (b) The Lyapunov value over the trajectory decays, indicating $\delta$-GAS in the absence of external input.

Theorems & Definitions (10)

  • Definition 2.1
  • Theorem 2.2
  • Definition 3.1
  • Remark 3.2
  • Lemma 3.3
  • Theorem 3.4
  • Remark 4.1
  • Theorem 4.2
  • Remark 4.3
  • Remark 4.4