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），并利用所谓“情景方法”中的采样技术计算其转移概率区间，从而得到概率上可靠的近似。我们将该方法应用于多个现实基准问题，特别是温度控制与空中飞行器投递问题。