From Formal Methods to Data-Driven Safety Certificates of Unknown Large-Scale Networks

TL;DR

This paper introduces a data-driven, decentralized method for designing safety controllers in large-scale unknown networks, leveraging noisy data and compositional reasoning to ensure safety with reduced computational complexity.

Contribution

It presents a novel compositional framework that uses noisy data from subsystems to construct safety certificates and controllers, scalable to large networks with unknown dynamics.

Findings

Successfully applied to physical networks with unknown models.

Reduces computational complexity from polynomial to linear in network size.

Ensures safety over infinite time horizon with correctness guarantees.

Abstract

In this work, we propose a data-driven scheme within a compositional framework with noisy data to design robust safety controllers in a fully decentralized fashion for large-scale interconnected networks with unknown mathematical dynamics. Despite the network's high dimensionality and the inherent complexity of its unknown model, which make it intractable, our approach effectively addresses these challenges by (i) treating the network as a composition of smaller subsystems, and (ii) collecting noisy data from each subsystem's trajectory to design a control sub-barrier certificate (CSBC) and its corresponding local controller. To achieve this, our proposed scheme only requires a noise-corrupted single input-state trajectory from each unknown subsystem up to a specified time horizon, satisfying a certain rank condition. Subsequently, under a small-gain compositional reasoning, we compose those CSBC, derived from noisy data, and formulate a control barrier certificate (CBC) for the unknown network, ensuring its safety over an infinite time horizon, while providing correctness guarantees. We offer a data-dependent sum-of-squares (SOS) optimization program for computing CSBC alongside local controllers of subsystems. We illustrate that while the computational complexity of designing a CBC and its safety controller grows polynomially with network dimension using SOS optimization, our compositional data-driven approach significantly reduces it to a linear scale concerning the number of subsystems. We demonstrate the capability of our data-driven approach on multiple physical networks involving unknown models and a range of interconnection topologies.