CESAR: Control Envelope Synthesis via Angelic Refinements

TL;DR

CESAR is a novel method for synthesizing provably correct control envelopes for hybrid systems, enabling safe runtime monitoring and flexible control strategies through angelic refinement and game-theoretic techniques.

Contribution

The paper introduces CESAR, an algorithm that synthesizes optimal control envelopes for hybrid systems using angelic refinements and hybrid game theory, enhancing safety and flexibility.

Findings

Successfully applied to various safe control synthesis examples

Maximized control envelope permissiveness while ensuring safety

Demonstrated effectiveness in complex hybrid system scenarios

Abstract

This paper presents an approach for synthesizing provably correct control envelopes for hybrid systems. Control envelopes characterize families of safe controllers and are used to monitor untrusted controllers at runtime. Our algorithm fills in the blanks of a hybrid system's sketch specifying the desired shape of the control envelope, the possible control actions, and the system's differential equations. In order to maximize the flexibility of the control envelope, the synthesized conditions saying which control action can be chosen when should be as permissive as possible while establishing a desired safety condition from the available assumptions, which are augmented if needed. An implicit, optimal solution to this synthesis problem is characterized using hybrid systems game theory, from which explicit solutions can be derived via symbolic execution and sound, systematic game refinements. Optimality can be recovered in the face of approximation via a dual game characterization. The resulting algorithm, Control Envelope Synthesis via Angelic Refinements (CESAR), is demonstrated in a range of safe control synthesis examples with different control challenges.