Automated synthesis of provably correct controllers for cyber-physical systems is crucial for deployment in safety-critical scenarios. However, hybrid features and stochastic or unknown behaviours make this problem challenging. We propose a method for synthesising controllers for Markov jump linear systems (MJLSs), a class of discrete-time models for cyber-physical systems, so that they certifiably satisfy probabilistic computation tree logic (PCTL) formulae. An MJLS consists of a finite set of stochastic linear dynamics and discrete jumps between these dynamics that are governed by a Markov decision process (MDP). We consider the cases where the transition probabilities of this MDP are either known up to an interval or completely unknown. Our approach is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We formalise this abstraction as an interval MDP (iMDP) for which we compute intervals of transition probabilities using sampling techniques from the so-called 'scenario approach', resulting in a probabilistically sound approximation. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.

翻译：在安全关键场景中部署时，自动化合成可证明正确的信息物理系统控制器至关重要。然而，混合特性与随机或未知行为使这一问题充满挑战。本文提出一种针对马尔可夫跳变线性系统（MJLS）——信息物理系统的一类离散时间模型——的控制器合成方法，使其能够可验证地满足概率计算树逻辑（PCTL）公式。MJLS由一组有限随机线性动力学及其之间的离散跳变构成，这些跳变受马尔可夫决策过程（MDP）支配。我们考虑该MDP的转移概率在区间内已知或完全未知两种情况。该方法基于有限状态抽象，该抽象同时捕捉MJLS的离散（模态跳变）和连续（随机线性）行为。我们将该抽象形式化为区间MDP（iMDP），并利用所谓的"场景方法"中的采样技术计算其转移概率区间，从而得到概率意义上可靠的近似。我们将此方法应用于多个现实基准问题，特别是温度控制与飞行器配送问题。