Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges

We provide a review of recent work on formal methods for autonomous driving. Formal methods have been traditionally used to specify and verify the behavior of computer programs and digital circuits. Enabled by abstraction techniques for dynamical systems and the availability of verification and synthesis tools for finite systems, they have been adopted by the control and robotics communities. In particular, in autonomous driving, recent research proposes formal languages such as temporal logics to specify driving behaviors ranging from safety, such as collision avoidance, to compliance with complex rules of the road. Our review focuses on formal verification, monitoring, and synthesis techniques enabling autonomous vehicles to adhere to such specifications. We only consider works about system-level methods that have an ego-centric perspective, i.e., we focus on the behavior of an autonomous vehicle in its entirety, rather than specific software code within the vehicle or traffic networks consisting of multiple vehicles. This paper also identifies the main remaining challenges.