Neural Vector Lyapunov-Razumikhin Certificates for Delayed Interconnected Systems

TL;DR

This paper introduces a scalable framework for synthesizing and verifying neural vector Lyapunov-Razumikhin certificates to ensure stability in large-scale delayed interconnected systems, addressing the challenge of formal guarantees.

Contribution

It establishes a sufficient stability condition, develops a scalable neural certificate synthesis method, and validates the approach on various large-scale systems with improved efficiency.

Findings

Validated on mixed-autonomy platoons, drone formations, and microgrids.

Achieved improved verification efficiency compared to baselines.

Demonstrated formal stability guarantees for large-scale delayed systems.

Abstract

Ensuring scalable input-to-state stability (sISS) is critical for the safety and reliability of large-scale interconnected systems, especially in the presence of communication delays. While learning-based controllers can achieve strong empirical performance, their black-box nature makes it difficult to provide formal and scalable stability guarantees. To address this gap, we propose a framework to synthesize and verify neural vector Lyapunov-Razumikhin certificates for discrete-time delayed interconnected systems. Our contributions are three-fold. First, we establish a sufficient condition for discrete-time sISS via vector Lyapunov-Razumikhin functions, which enables certification for large-scale delayed interconnected systems. Second, we develop a scalable synthesis and verification framework that learns the neural certificates and verifies the certificates on reachability-constrained delay domains with scalability analysis. Third, we validate our approach on mixed-autonomy platoons, drone formations, and microgrids against multiple baselines, showing improved verification efficiency with competitive control performance.