  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.
