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

TL;DR

This paper introduces a scalable, data-driven framework using graph neural networks to verify incremental stability in large interconnected systems, providing formal guarantees and validated through nonlinear case studies.

Contribution

It presents a novel distributed approach combining graph neural networks and Lyapunov functions for stability verification of large-scale systems with unknown dynamics.

Findings

Successfully verified stability in two nonlinear case studies

Demonstrated scalability to large systems

Provided formal correctness guarantees via Lipschitz bounds

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.