Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Neural Vector Lyapunov-Razumikhin Certificates for Delayed Interconnected Systems

Jingyuan Zhou, Yuexuan Wang, Kaidi Yang

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.

Neural Vector Lyapunov-Razumikhin Certificates for Delayed Interconnected 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.

Paper Structure

This paper contains 30 sections, 5 theorems, 79 equations, 4 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Stability of Delayed Dynamic Systems
  4. Neural Certificates and Formal Verification
  5. Problem Statement
  6. Discrete-time sISS Vector Lyapunov Razumikhin Function Formulation
  7. Synthesis and Verification Framework
  8. Synthesis of Neural Certificates
  9. Verification Formulation
  10. Scalability Analysis
  11. Numerical Simulation
  12. Verification Performance
  13. Control Performance
  14. Simulation Demonstration
  15. Conclusion
  16. ...and 15 more sections

Key Result

Theorem 4.1

The discrete-time delayed system in Eq. eq: system is sISS if there exist scalars $p > 1$, $\epsilon \in (0,1)$, $\psi \ge 0$, class-$\mathcal{K}_\infty$ functions $\alpha_1, \alpha_2 \in \mathcal{K}_\infty$, Lyapunov functions $V_i: \mathbb{R}^{n_i} \to \mathbb{R}_{\ge 0},~i \in \mathcal{N}$, posit such that the following conditions hold: (i) Class-$\mathcal{K}_\infty$ Bounds: For all $i \in \mat

Figures (4)

  • Figure 1: Two-stage verification framework.
  • Figure 2: Lyapunov function evolution on three benchmarks under the proposed delayed-sISS framework.
  • Figure 3: System trajectories on three benchmarks under the proposed delayed-sISS framework.
  • Figure 4: Representative network topologies demonstrating structural equivalence among nodes. Highlighted nodes are the selected representatives to verify.

Theorems & Definitions (18)

  • Remark 3.1
  • Definition 3.2: Discrete-Time Scalable Input-to-State Stability Under Bounded Delay
  • Theorem 4.1: Discrete-Time sISS via Vector Lyapunov-Razumikhin Functions
  • Remark 4.2
  • Remark 5.1
  • Remark 5.2
  • Theorem 5.3: Two-stage verification
  • Remark 5.7
  • Theorem 5.8: Sampling-Based Verification of Vector Lyapunov-Razumikhin Conditions
  • Definition 5.9: Substructure Isomorphism for Delayed Systems
  • ...and 8 more