Synergy: Verified Control of Cooperative Autonomous Vehicles

Verified control algorithms will be developed for the control of autonomous vehicles. Autonomous vehicles are used to perform increasingly complex tasks, safely and reliably, under changing environmental conditions. They promise to fundamentally transform our society in areas such as transportation, logistics, telecommunications, remote sensing and defense. However, operating in adverse environments requires the ability to perform highly aggressive maneuvers that exploit the complex dynamics of these vehicles. On the other hand, safe and verifiable control restricts us to maneuvers that can be designed based on simplified models of the vehicle dynamics. These problems are further complicated in scenarios that involve multiple cooperating vehicles where vehicles can benefit by knowing the capabilities and maneuver decisions of other vehicles.

In our work, we have combined ideas from dynamical systems, control theory and formal methods to implement verified control algorithms that will perform "aggressive" maneuvers involving multiple vehicles under different driving conditions. A stack of increasingly accurate but more complex models have been used in order to design provably correct controllers at the lowest level of complexity. The stack allows us to "transfer" the controllers and their certificates from simpler to more accurate models. Ideas from control theory have been extended to characterize sets of maneuvers and their corresponding control algorithms, including the automated search for Lyapunov and barrier function certificates. The overall approach has been lifted from the space of maneuvers for a single vehicle to a cooperative setting to characterize maneuvers that can be performed under communication constraints.

Our work has been evaluated experimentally on the Ninja Car testbed at CU-Boulder. The safety and performance of the control algorithms have been applied by simulating real driving conditions in our laboratory and through multi-scale simulation using realistic road models.