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）的控制器综合方法——MJLS是一类离散时间信息物理系统模型——使得系统可被证明满足概率计算树逻辑（PCTL）公式。MJLS由有限随机线性动态集及控制这些动态间离散跳变的马尔可夫决策过程（MDP）构成。我们考虑两种情形：该MDP的转移概率已知区间范围或完全未知。该方法基于有限状态抽象，该抽象同时捕捉MJLS的离散（模态跳变）与连续（随机线性）行为。我们将此抽象形式化为区间MDP（iMDP），并采用所谓"场景方法"的采样技术计算其转移概率区间，从而得到具有概率保证的近似结果。我们将该方法应用于多个实际基准问题，特别是温度控制与空中飞行器投递问题。