Safety and progress proofs for a reactive planner and controller for autonomous driving

TL;DR

This paper analyzes the safety and performance of a reactive autonomous driving system that navigates race laps using sensor inputs and Voronoi diagrams, providing formal safety proofs and practical validation.

Contribution

It introduces a reactive planning and control approach with formal safety and performance analysis, validated through simulations and real-world experiments.

Findings

The reactive planner is locally consistent with full-map Voronoi plans.

The system successfully completes laps on five different circuits.

Formal safety proofs are established using hybrid automata reachability analysis.

Abstract

In this paper, we perform safety and performance analysis of an autonomous vehicle that implements reactive planner and controller for navigating a race lap. Unlike traditional planning algorithms that have access to a map of the environment, reactive planner generates the plan purely based on the current input from sensors. Our reactive planner selects a waypoint on the local Voronoi diagram and we use a pure-pursuit controller to navigate towards the waypoint. Our safety and performance analysis has two parts. The first part demonstrates that the reactive planner computes a plan that is locally consistent with the Voronoi plan computed with full map. The second part involves modeling of the evolution of vehicle navigating along the Voronoi diagram as a hybrid automata. For proving the safety and performance specification, we compute the reachable set of this hybrid automata and employ some enhancements that make this computation easier. We demonstrate that an autonomous vehicle implementing our reactive planner and controller is safe and successfully completes a lap for five different circuits. In addition, we have implemented our planner and controller in a simulation environment as well as a scaled down autonomous vehicle and demonstrate that our planner works well for a wide variety of circuits.