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）公式提供保证。我们基于多个通用基准问题展开实验，并对比了近期验证upMDPs的相关研究成果。