Data-Driven Certificate Synthesis

TL;DR

This paper introduces a novel data-driven method for verifying properties of discrete time dynamical systems by learning certificates from system trajectories, providing probabilistic guarantees and scalable algorithms for property verification.

Contribution

It proposes a new algorithm that learns certificates from data, quantifies their generalization via PAC and scenario approach, and introduces a constructive compression set calculation method.

Findings

Effective verification of system properties using learned certificates.

Probabilistic guarantees on certificate validity and system property satisfaction.

Scalable and novel algorithm with demonstrated numerical case studies.

Abstract

We investigate the problem of verifying different properties of discrete time dynamical systems, namely, reachability, safety and reach-while-avoid. To achieve this, we adopt a data driven perspective and, using past system trajectories as data, we aim at learning a specific function termed certificate for each property we wish to verify. We seek to minimize a loss function, designed to encompass conditions on the certificate to be learned that encode the satisfaction of the associated property. Besides learning a certificate, we quantify probabilistically its generalization properties, namely, how likely it is for a certificate to be valid (and hence for the associated property to be satisfied) when it comes to a new system trajectory not included in the training data set. We view this problem under the realm of probably approximately correct (PAC) learning under the notion of compression, and use recent advancements of the so-called scenario approach to obtain scalable generalization bounds on the learned certificates. To achieve this, we design a novel algorithm that minimizes the loss function and hence constructs a certificate, and at the same time determines a quantity termed compression, which is instrumental in obtaining meaningful probabilistic guarantees. This process is novel per se and provides a constructive mechanism for compression set calculation, thus opening the road for its use to more general non-convex optimization problems. We verify the efficacy of our methodology on several numerical case studies, and compare it (both theoretically and numerically) with closely related results on data-driven property verification.