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.

翻译：本文针对数据驱动的控制器计算问题展开研究，这类控制器可确保安全关键系统在设计中具备正确性，并能为（复杂）功能需求提供可证明的满足性。聚焦于存在参数不确定性的连续空间随机系统，我们提出一种两阶段方法，将问题分解为学习阶段与鲁棒形式控制器综合阶段。第一阶段利用现有贝叶斯回归结果，为系统真实参数计算鲁棒置信集。针对第二阶段，我们引入同时处理随机与参数不确定性的系统方法。通过基于子概率测度耦合随机系统不确定性的方式，提出支持正确性设计控制精化过程的仿真关系。所提出的关系对于构建不仅关联单一模型、而是关联一组参数化模型的抽象模型至关重要。研究成果通过三个案例（包含非线性系统与高维系统）进行验证。