Neural Cooperative Reach-While-Avoid Certificates for Interconnected Systems

TL;DR

This paper introduces neural certificates for large-scale interconnected systems that guarantee safety and stability through decentralized, scalable, and transferable methods, validated on multi-robot and vehicle platoon experiments.

Contribution

It proposes neural cooperative reach-while-avoid certificates with dynamic-localized Lyapunov and Barrier Functions, enabling scalable, decentralized guarantees for interconnected systems.

Findings

Ensures certified cooperative reach-while-avoid in experiments

Maintains strong control performance with formal guarantees

Introduces transfer mechanism for controllers and certificates

Abstract

Providing formal guarantees for neural network-based controllers in large-scale interconnected systems remains a fundamental challenge. In particular, using neural certificates to capture cooperative interactions and verifying these certificates at scale is crucial for the safe deployment of such controllers. However, existing approaches fall short on both fronts. To address these limitations, we propose neural cooperative reach-while-avoid certificates with Dynamic-Localized Vector Control Lyapunov and Barrier Functions, which capture cooperative dynamics through state-dependent neighborhood structures and provide decentralized certificates for global exponential stability and safety. Based on the certificates, we further develop a scalable training and verification framework that jointly synthesizes controllers and neural certificates via a constrained optimization objective, and leverages a sufficient condition to ensure formal guarantees considering modeling error. To improve scalability, we introduce a structural reuse mechanism to transfer controllers and certificates between substructure-isomorphic systems. The proposed methodology is validated with extensive experiments on multi-robot coordination and vehicle platoons. Results demonstrate that our framework ensures certified cooperative reach-while-avoid while maintaining strong control performance.