Synthesising verifiably correct controllers for dynamical systems is crucial for safety-critical problems. To achieve this, it is important to account for uncertainty in a robust manner, while at the same time it is often of interest to avoid being overly conservative with the view of achieving a better cost. We propose a method for verifiably safe policy synthesis for a class of finite state models, under the presence of structural uncertainty. In particular, we consider uncertain parametric Markov decision processes (upMDPs), a special class of Markov decision processes, with parameterised transition functions, where such parameters are drawn from a (potentially) unknown distribution. Our framework leverages recent advancements in the so-called scenario approach theory, where we represent the uncertainty by means of scenarios, and provide guarantees on synthesised policies satisfying probabilistic computation tree logic (PCTL) formulae. We consider several common benchmarks/problems and compare our work to recent developments for verifying upMDPs.

翻译：为动态系统综合可验证的正确控制器对于安全关键问题至关重要。为实现这一目标，需以鲁棒方式处理不确定性，同时避免因过度保守而损失性能指标。本文提出一种在结构不确定性条件下，针对有限状态模型的可验证安全策略综合方法。具体而言，我们考虑不确定性参数马尔可夫决策过程（upMDPs）——一类具有参数化转移函数的特殊马尔可夫决策过程，其参数服从（可能未知的）分布。本框架利用近期发展的情景方法理论，通过情景表示不确定性，并为综合策略满足概率计算树逻辑（PCTL）公式提供保障。我们基于多个标准基准问题开展实验，并将研究成果与近期upMDP验证方法进行对比。