Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes
Mohammed Adib Oumer, Amr Alanwar, Majid Zamani
TL;DR
The paper tackles safety verification for cyber-physical systems with unknown or uncertain dynamics by building a data-driven model set using matrix zonotopes that contains all models consistent with observed data and noise bounds. It then integrates this set into a barrier certificate framework and uses sum-of-squares (SOS) optimization to search for certificates that guarantee safety for all models in the set, providing infinite-horizon guarantees via an interval-matrix representation. The approach avoids relying on a single, potentially inaccurate model and demonstrates its viability through 2D and 5D numerical experiments, highlighting scalability and computational challenges. The work contributes a practical methodology for robust safety verification in real-world CPS and points to extensions for polynomial nonlinear systems and safe controller synthesis.
Abstract
Ensuring safety in cyber-physical systems (CPSs) is a critical challenge, especially when system models are difficult to obtain or cannot be fully trusted due to uncertainty, modeling errors, or environmental disturbances. Traditional model-based approaches rely on precise system dynamics, which may not be available in real-world scenarios. To address this, we propose a data-driven safety verification framework that leverages matrix zonotopes and barrier certificates to verify system safety directly from noisy data. Instead of trusting a single unreliable model, we construct a set of models that capture all possible system dynamics that align with the observed data, ensuring that the true system model is always contained within this set. This model set is compactly represented using matrix zonotopes, enabling efficient computation and propagation of uncertainty. By integrating this representation into a barrier certificate framework, we establish rigorous safety guarantees without requiring an explicit system model. Numerical experiments demonstrate the effectiveness of our approach in verifying safety for dynamical systems with unknown models, showcasing its potential for real-world CPS applications.