Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components

TY - JOUR

T1 - Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components

AU - Calinescu, Radu

AU - Imrie, Calum Corrie

AU - Mangal, Ravi

AU - Rodrigues, Genaina

AU - S.Păsăreanu, Corina

AU - Alpizar Santana, Misael

AU - Vazquez Flores, Gricel

N1 - © 2024 The Authors

PY - 2024/6/1

Y1 - 2024/6/1

N2 - We present DeepDECS, a new method for the synthesis of correct-by-construction software 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 software 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 evaluate the method in simulation by using it to synthesise controllers for mobile-robot collision limitation, and for maintaining driver attentiveness in shared-control autonomous driving.

AB - We present DeepDECS, a new method for the synthesis of correct-by-construction software 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 software 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 evaluate the method in simulation by using it to synthesise controllers for mobile-robot collision limitation, and for maintaining driver attentiveness in shared-control autonomous driving.

KW - discrete-event controller synthesis

KW - Markov model

KW - deep neural network

KW - uncertainty quantification

KW - neuro-symbolic AI

U2 - 10.1109/TSE.2024.3385378

DO - 10.1109/TSE.2024.3385378

M3 - Article

SN - 0098-5589

VL - 50

SP - 1374

EP - 1395

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

ER -