We present DeepDECS, a new method for the synthesis of correct-by-construction discrete-event controllers for autonomous systems that use deep neural network (DNN) classifiers for the perception step of their decision-making processes. Despite major advances in deep learning in recent years, providing safety guarantees for these systems remains very challenging. Our controller synthesis method addresses this challenge by integrating DNN verification with the synthesis of verified Markov models. The synthesised models correspond to discrete-event controllers guaranteed to satisfy the safety, dependability and performance requirements of the autonomous system, and to be Pareto optimal with respect to a set of optimisation objectives. We use the method in simulation to synthesise controllers for mobile-robot collision mitigation and for maintaining driver attentiveness in shared-control autonomous driving.

翻译：我们提出DeepDECS方法，用于合成自主系统中基于离散事件"正确性由构造保证"的控制器。这类系统在决策过程的感知环节采用深度神经网络(DNN)分类器。尽管近年来深度学习取得重大进展，但为这些系统提供安全保障仍极具挑战性。我们的控制器合成方法通过将DNN验证与已验证马尔可夫模型合成进行集成来应对这一挑战。合成的模型对应离散事件控制器，可保证满足自主系统的安全性、可靠性和性能要求，并在优化目标集合上达到帕累托最优。我们通过仿真方法将该方法应用于移动机器人碰撞缓解控制器合成，以及共享控制自动驾驶中驾驶员注意力维持控制器合成。