  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.
