Formal safety verification of unknown continuous-time systems
Abolfazl Lavaei, Ameneh Nejati, Pushpak Jagtap, Majid Zamani · 2021
This work studies formal verification of continuous-time continuous-space systems with unknown dynamics against safety specifications. The proposed framework is based on a data-driven construction of barrier certificates using which the safety of unknown systems is verified via a finite set of data collected from trajectories of systems with a priori guaranteed confidence. In the proposed scheme, we first cast the original safety problem as a robust convex program (RCP). Since the unknown model appears in one of the constraints of the proposed RCP, we provide the scenario convex program (SCP) corresponding to the original RCP by collecting finite numbers of data from systems' evolutions. We then establish a probabilistic closeness between the optimal value of SCP and that of RCP. Accordingly, we formally quantify the safety guarantee of unknown systems based on the number of data and the required level of safety confidence.