Formal Safety Net Control Using Backward Reachability Analysis

Ensuring safety is crucial for the successful deployment of autonomous systems, such as self-driving vehicles, unmanned aerial vehicles, and robots acting close to humans. While there exist many controllers that optimize certain criteria, such as energy consumption, comfort, or low wear, they are usually not able to guarantee safety at all times for constrained nonlinear systems affected by disturbances. Many controllers providing safety guarantees, however, have no optimal performance. The idea of this article is, therefore, to synthesize a formally correct controller that serves as a safety net for an unverified, optimal controller. This way, most of the time, the optimal controller is in charge and leads to a desired, optimal control performance. The safety controller constantly monitors the actions of the optimal controller and takes over if the system would become unsafe. The safety controller utilizes a novel concept of backward reachable set computation, where we avoid the need of computing underapproximations of reachable sets. We have further developed a new approach that analytically describes reachable sets, making it possible to efficiently maximize the size of the backward reachable set. We demonstrate our approach by a numerical example from autonomous driving.