A Control Architecture for Provably-Correct Autonomous Driving
This work addresses the challenge of provably correct and real-time control for autonomous driving, representing an incremental advance by combining existing methods like MPC and STL with a novel hierarchical structure.
The paper tackles the problem of autonomous vehicle control by introducing a two-level architecture that integrates traffic rules as Signal Temporal Logic constraints into a linear Model Predictive Control framework, achieving substantial improvements in runtime performance validated in the CARLA simulator.
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.