Discrete-Event Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Autonomous DrivingDecision MakingSimilar Papers 제목 키워드 기반
Technical Report: Directed Controller Synthesis of Discrete Event Systems
This paper presents a Directed Controller Synthesis (DCS) technique for discrete event systems. The DCS method explores the solution space for reactive controllers guided by a domain-independent heuristic. The heuristic …
Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges
In recent years, formal methods have been extensively used in the design of autonomous systems. By employing mathematically rigorous techniques, formal methods can provide fully automated reasoning processes with provabl…
Bounded Synthesis and Reinforcement Learning of Supervisors for Stochastic Discrete Event Systems with LTL Specifications
In this paper, we consider supervisory control of stochastic discrete event systems (SDESs) under linear temporal logic specifications. Applying the bounded synthesis, we reduce the supervisor synthesis into a problem of…
A Parametric Model for Near-Optimal Online Synthesis with Robust Reach-Avoid Guarantees
Objective: To obtain explainable guarantees in the online synthesis of optimal controllers for high-integrity cyber-physical systems, we re-investigate the use of exhaustive search as an alternative to reinforcement lear…
Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller
Controller synthesis, including reset controller, feedback controller, and switching logic controller, provides an essential mechanism to guarantee the correctness and reliability of hybrid systems in a correct-by-constr…