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的离散（模态跳变）与连续（随机线性）行为。我们将该抽象形式化为区间马尔可夫决策过程（iMDP），并利用所谓的"场景方法"中的采样技术计算其转移概率区间，从而得到概率意义上的可靠近似。我们将该方法应用于多个实际基准问题，特别地，包括温度控制问题与空中飞行器递送问题。