A Control Architecture for Provably-Correct Autonomous Driving

TL;DR

This paper introduces a two-level control architecture for autonomous vehicles that ensures safety and rule compliance using formal logic, real-time optimization, and runtime monitoring, validated in a simulator.

Contribution

A novel hierarchical control framework combining linear MPC with STL-based constraints and runtime monitoring for provably-correct autonomous driving.

Findings

Significant runtime performance improvements over existing methods

Effective enforcement of traffic rules and safety constraints

Validated control approach in CARLA simulator

Abstract

This paper presents a novel two-level control architecture for a fully autonomous vehicle in a deterministic environment, which can handle traffic rules as specifications and low-level vehicle control with real-time performance. At the top level, we use a simple representation of the environment and vehicle dynamics to formulate a linear Model Predictive Control (MPC) problem. We describe the traffic rules and safety constraints using Signal Temporal Logic (STL) formulas, which are mapped to mixed integer-linear constraints in the optimization problem. The solution obtained at the top level is used at the bottom-level to determine the best control command for satisfying the constraints in a more detailed framework. At the bottom-level, specification-based runtime monitoring techniques, together with detailed representations of the environment and vehicle dynamics, are used to compensate for the mismatch between the simple models used in the MPC and the real complex models. We obtain substantial improvements over existing approaches in the literature in the sense of runtime performance and we validate the effectiveness of our proposed control approach in the simulator CARLA.