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 focus on continuous-state uncertain systems, 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 for the first time 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 a linear model and the nonlinear model of the Van der Pol Oscillator.

翻译：本文针对数据驱动下控制器计算的问题展开研究，此类控制器需满足安全关键系统的正确设计原则，并能可证明地满足（复杂）功能需求。聚焦于连续状态不确定系统，我们提出两阶段方法，将问题分解为学习阶段与鲁棒形式化控制器综合阶段。第一阶段利用现有贝叶斯回归结果计算系统真实参数的鲁棒可信集。第二阶段则引入同时存在随机不确定性与参数不确定性的系统处理方法。我们首次提出基于子概率度量的耦合随机系统不确定性的模拟关系，以实现正确设计控制精化。所提出的关系对于构建不仅关联单一模型、而是关联一组参数化模型的抽象模型具有关键作用。研究结果在线性模型及范德波尔振荡器非线性模型上得到验证。