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

arXiv: https://arxiv.org/abs/2111.10330 · HTML: https://mlsanity.com/paper/2111.10330/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Nov 2021.

## Built on by (most cited first, 12 of 12)

- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems](https://mlsanity.com/paper/2512.11750/) (2025)
- [Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes](https://mlsanity.com/paper/2504.01007/) (2025)
- [Barrier Certificates for Unknown Systems with Latent States and Polynomial Dynamics using Bayesian Inference](https://mlsanity.com/paper/2504.01807/) (2025)
- [A Barrier Certificate-based Simplex Architecture for Systems with Approximate and Hybrid Dynamics](https://mlsanity.com/paper/2202.09710/) (2022)
- [Data-Driven Probabilistic Evaluation of Logic Properties with PAC-Confidence on Mealy Machines](https://mlsanity.com/paper/2508.14710/) (2025)
- [BarrierBench: Evaluating Large Language Models for Safety Verification in Dynamical Systems](https://mlsanity.com/paper/2511.09363/) (2025)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)
- [Safety Certification is Classification](https://mlsanity.com/paper/2605.06087/) (2026)
- [k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics](https://mlsanity.com/paper/2605.20108/) (2026)
- [Kernel-Based Safe Exploration in Deep Reinforcement Learning](https://mlsanity.com/paper/2605.22207/) (2026)

## Abstract (arXiv)

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.