Data-Driven Certificate Synthesis
Luke Rickard, Alessandro Abate, Kostas Margellos

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNeural Networks and Applications
MethodsSparse Evolutionary Training · ADaptive gradient method with the OPTimal convergence rate
