Neural Vector Lyapunov-Razumikhin Certificates for Delayed Interconnected Systems

1. Problem Statement

The paper addresses the critical challenge of ensuring scalable input-to-state stability (sISS) for large-scale interconnected systems (e.g., vehicle platoons, drone formations, microgrids) operating under communication delays and external disturbances.

• Context: Modern cyber-physical systems are increasingly complex and tightly coupled. While learning-based controllers (e.g., Reinforcement Learning) offer strong empirical performance, their "black-box" nature prevents formal stability guarantees.
• The Gap: Existing stability analysis tools for delayed systems (like Lyapunov-Krasovskii functionals) often fail to scale with network size. Conversely, scalable stability methods for delay-free systems cannot be directly applied because delays introduce memory, breaking the "memoryless" assumption required for standard vector Lyapunov arguments.
• Goal: To develop a framework that synthesizes and formally verifies stability certificates for discrete-time, delayed, interconnected systems without requiring explicit knowledge of the system dynamics (model-free), while ensuring the verification complexity does not explode as the number of agents ($N$) increases.

2. Methodology

The authors propose a Neural Vector Lyapunov–Razumikhin Certificate framework. The methodology consists of three main pillars:

A. Theoretical Foundation: Discrete-Time sISS via Vector Lyapunov-Razumikhin

The authors establish a sufficient condition for sISS using Vector Lyapunov-Razumikhin functions.

• Vector Lyapunov Functions: Instead of a single global Lyapunov function, they use a set of local functions $\{V_i\}$ for each agent $i$.
• Razumikhin Condition: To handle delays, they introduce a conditional decrement. If the current Lyapunov value $V_i(x_{i,k})$ is sufficiently larger than the delayed values of its neighbors (i.e., $V_j(x_{j,k-s}) \le p \cdot V_i(x_{i,k})$), then the system must contract.
• Small-Gain Condition: The coupling between agents is governed by a gain matrix $\Gamma$ satisfying a network-size-independent small-gain condition ($\sum \gamma_{i,j} \le 1-\epsilon$).
• Result: This formulation proves that the system state remains uniformly bounded regardless of the network size $N$, provided the delays are bounded.

B. Synthesis and Verification Framework

The paper introduces a learning-based pipeline to find these certificates:

1. Neural Synthesis: Neural networks are trained to approximate the local Lyapunov functions $V_i$ and the coupling gains $\Gamma$. The training loss enforces the Razumikhin bounds and the conditional decrement inequalities.
2. Reachability-Constrained Verification: Directly verifying the conditions over the entire state space is intractable. The authors restrict verification to reachability-constrained delay domains. They compute over-approximations of reachable states from an initial set over a finite horizon.
3. Two-Stage Verification Strategy:
   • Stage 1 (Outside): Verifies the Razumikhin conditional logic for states where the Lyapunov function is large (outside a target level set).
   • Stage 2 (Inside): Verifies an unconditional contraction for states within a target level set (where the system is already stable).
4. Sampling-Based Guarantee: Using Lipschitz continuity assumptions, the infinite-dimensional verification problem is reduced to finite checks on a uniform grid, with margins added to ensure correctness for all continuous points.

C. Scalability via Structural Equivalence

To address the computational cost of large $N$, the framework leverages structural isomorphism:

• Substructure Isomorphism: If a large system contains a smaller system as a substructure, the certificate for the smaller system can be reused.
• Node Equivalence: Agents with identical dynamics, neighbor structures, and delay patterns are "structurally equivalent." They can share the same neural certificate.
• Impact: This allows the verification complexity to depend on the number of unique structural classes rather than the total number of agents, enabling linear or constant scaling with $N$.

3. Key Contributions

1. New Stability Condition: Established the first sufficient condition for discrete-time sISS in delayed interconnected systems using vector Lyapunov-Razumikhin functions, ensuring stability constants are independent of network size.
2. Scalable Synthesis & Verification Pipeline: Developed a framework that learns neural certificates and verifies them over reachability-constrained domains. It combines counterexample-guided inductive synthesis (CEGIS) with a two-stage verification strategy.
3. Scalability Mechanism: Proved that certificates can be reused across structurally equivalent nodes and substructures, drastically reducing verification complexity for large-scale networks.
4. Empirical Validation: Demonstrated the approach on three distinct benchmarks: mixed-autonomy platoons, drone formations, and microgrids.

4. Experimental Results

The method was evaluated against baselines including nominal controllers, predictor feedback, and other ISS/sISS certificate methods.

• Verification Efficiency:
  • The proposed method (combining reachability constraints and structural reuse) was the only approach that successfully verified large-scale systems (up to $N=50$) within a 5-hour timeout.
  • Baselines relying solely on reachability or scalability timed out for $N=50$.
  • Runtime remained nearly invariant as $N$ increased, confirming the scalability of the structural reuse approach.
• Control Performance (RMSE):
  • Platoons: Achieved the lowest Root-Mean-Square Error (RMSE) under sinusoidal disturbances, outperforming predictor feedback and other certificate-based methods by up to 22%.
  • Drones: Matched the performance of model-based predictor feedback while being model-free.
  • Microgrids: Showed superior disturbance attenuation compared to all baselines, reducing RMSE by ~12% compared to the best alternative.
• Visualization: Lyapunov function plots confirmed that the learned certificates act as valid energy-like measures, decreasing as the system converges to equilibrium.

5. Significance

This work bridges a critical gap between learning-based control and formal verification in the context of time-delayed systems.

• Safety Assurance: It provides the first formal, scalable stability guarantees for neural network controllers in large-scale delayed networks, a prerequisite for deploying AI in safety-critical infrastructure (transport, power grids).
• Model-Free Robustness: Unlike traditional delay-compensation methods (e.g., predictor feedback) that require accurate system models, this approach works with unknown dynamics, making it applicable to real-world systems where modeling is difficult.
• Scalability: By proving that stability certificates can be shared among structurally equivalent agents, the paper solves the "curse of dimensionality" often associated with verifying large multi-agent systems.

In summary, the paper presents a rigorous, scalable, and practical framework for certifying the stability of complex, delayed, interconnected systems controlled by neural networks, moving beyond empirical testing to formal guarantees.