# Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Apr 2023.

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

- [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)
- [Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)](https://mlsanity.com/paper/2506.16971/) (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)

## Abstract (arXiv)

This paper addresses the problem of data-driven computation of controllers that are correct by design for safety-critical systems and can provably satisfy (complex) functional requirements. With a focus on continuous-space stochastic systems with parametric uncertainty, we propose a two-stage approach that decomposes the problem into a learning stage and a robust formal controller synthesis stage. The first stage utilizes available Bayesian regression results to compute robust credible sets for the true parameters of the system. For the second stage, we introduce methods for systems subject to both stochastic and parametric uncertainties. We provide simulation relations for enabling correct-by-design control refinement that are founded on coupling uncertainties of stochastic systems via sub-probability measures. The presented relations are essential for constructing abstract models that are related to not only one model but to a set of parameterized models. The results are demonstrated on three case studies, including a nonlinear and a high-dimensional system.