Discrete-Event Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components
This addresses safety assurance for autonomous systems using DNNs, but it is incremental as it builds on existing DNN verification and synthesis techniques.
The authors tackled the challenge of providing safety guarantees for autonomous systems with deep-learning perception by developing DeepDECS, a method that synthesizes correct-by-construction discrete-event controllers, achieving Pareto optimality for safety, dependability, and performance requirements in simulations for mobile-robot collision mitigation and driver attentiveness.
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.