  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. Moreover, the safe controller
remains more human-like than existing cruise controllers.
