Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations

TL;DR

This paper presents a Bayesian approach for synthesizing robust controllers for uncertain stochastic systems, combining learning and formal methods to ensure safety and correctness in complex, real-world applications.

Contribution

It introduces a two-stage framework that integrates Bayesian credible sets with simulation relations for robust control synthesis under uncertainty.

Findings

Successfully applied to nonlinear and high-dimensional systems

Provides formal guarantees for safety-critical control

Demonstrates effectiveness through three case studies

Abstract

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.