A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles

Title:	A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
Authors:	Albert Rizaldi (albert /dot/ rizaldi /at/ ntu /dot/ edu /dot/ sg) and Fabian Immler
Submission date:	2020-06-01
Abstract:	The Vienna Convention on Road Traffic defines the safe distance traffic rules informally. This could make autonomous vehicle liable for safe-distance-related accidents because there is no clear definition of how large a safe distance is. We provide a formally proven prescriptive definition of a safe distance, and checkers which can decide whether an autonomous vehicle is obeying the safe distance rule. Not only does our work apply to the domain of law, but it also serves as a specification for autonomous vehicle manufacturers and for online verification of path planners.
BibTeX:	@article{Safe_Distance-AFP, author = {Albert Rizaldi and Fabian Immler}, title = {A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles}, journal = {Archive of Formal Proofs}, month = jun, year = 2020, note = {\url{http://isa-afp.org/entries/Safe_Distance.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Sturm_Sequences
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.