Automated synthesis of correct-by-construction controllers for autonomous systems is crucial for their deployment in safety-critical scenarios. Such autonomous systems are naturally modeled as stochastic dynamical models. The general problem is to compute a controller that provably satisfies a given task, represented as a probabilistic temporal logic specification. However, factors such as stochastic uncertainty, imprecisely known parameters, and hybrid features make this problem challenging. We have developed an abstraction framework that can be used to solve this problem under various modeling assumptions. Our approach is based on a robust finite-state abstraction of the stochastic dynamical model in the form of a Markov decision process with intervals of probabilities (iMDP). We use state-of-the-art verification techniques to compute an optimal policy on the iMDP with guarantees for satisfying the given specification. We then show that, by construction, we can refine this policy into a feedback controller for which these guarantees carry over to the dynamical model. In this short paper, we survey our recent research in this area and highlight two challenges (related to scalability and dealing with nonlinear dynamics) that we aim to address with our ongoing research.

翻译：自动化合成安全关键场景中自主系统所需的正确性保证控制器至关重要。此类自主系统自然被建模为随机动力学模型。核心问题在于计算一个控制器，使其能以概率时态逻辑规范的形式，可证明地满足给定任务要求。然而，随机不确定性、参数不完全已知以及混合特征等因素使该问题极具挑战性。我们开发了一种抽象框架，可在多种建模假设下解决该问题。该框架基于将随机动力学模型鲁棒地抽象为带概率区间的马尔可夫决策过程（iMDP）。我们采用最先进的验证技术，在保证满足给定规范的前提下计算iMDP上的最优策略。随后证明，通过构造方法可将该策略精化为反馈控制器，且相关保证可传递至原动力学模型。本文简要综述了我们近期在该领域的研究成果，并着重指出当前研究正在攻克的两个挑战（可扩展性与非线性动力学处理）。