Data-driven verification and synthesis of stochastic systems via barrier certificates

TL;DR

This paper introduces a data-driven method for verifying and synthesizing controllers for unknown stochastic systems using barrier certificates, by converting complex problems into scenario convex programs with probabilistic guarantees.

Contribution

It formulates barrier certificate computation as a robust convex program and develops a scenario convex program approach with confidence guarantees for unknown stochastic systems.

Findings

Provides probabilistic safety guarantees based on sample size

Demonstrates effectiveness through three case studies

Extends approach to non-convex robust programs

Abstract

In this work, we study verification and synthesis problems for safety specifications over unknown discrete-time stochastic systems. When a model of the system is available, barrier certificates have been successfully applied for ensuring the satisfaction of safety specifications. In this work, we formulate the computation of barrier certificates as a robust convex program (RCP). Solving the acquired RCP is hard in general because the model of the system that appears in one of the constraints of the RCP is unknown. We propose a data-driven approach that replaces the uncountable number of constraints in the RCP with a finite number of constraints by taking finitely many random samples from the trajectories of the system. We thus replace the original RCP with a scenario convex program (SCP) and show how to relate their optimizers. We guarantee that the solution of the SCP is a solution of the RCP with a priori guaranteed confidence when the number of samples is larger than a pre-computed value. This provides a lower bound on the safety probability of the original unknown system together with a controller in the case of synthesis. We also discuss an extension of our verification approach to a case where the associated robust program is non-convex and show how a similar methodology can be applied. Finally, the applicability of our proposed approach is illustrated through three case studies.