Learning a Safety Verifiable Adaptive Cruise Controller from Human Driving Data
Qin Lin, Sicco Verwer, John Dolan

TL;DR
This paper presents a method to learn a hybrid automaton-based cruise controller from human data that can be formally verified for safety, ensuring collision avoidance while maintaining human-like driving behavior.
Contribution
The paper introduces a hybrid automaton model for cruise control learned from human data that can be formally verified for safety using the SpaceEx model checker.
Findings
The learned controller can be verified as collision-free.
Adding a safety state based on headway ensures provable safety.
The safe controller remains human-like in behavior.
Abstract
Imitation learning provides a way to automatically construct a controller by mimicking human behavior from data. For safety-critical systems such as autonomous vehicles, it can be problematic to use controllers learned from data because they cannot be guaranteed to be collision-free. Recently, a method has been proposed for learning a multi-mode hybrid automaton cruise controller (MOHA). Besides being accurate, the logical nature of this model makes it suitable for formal verification. In this paper, we demonstrate this capability using the SpaceEx hybrid model checker as follows. After learning, we translate the automaton model into constraints and equations required by SpaceEx. We then verify that a pure MOHA controller is not collision-free. By adding a safety state based on headway in time, a rule that human drivers should follow anyway, we do obtain a provably safe cruise control.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Autonomous Vehicle Technology and Safety
