CESAR: Control Envelope Synthesis via Angelic Refinements

TL;DR

This work tackles the problem of automatically synthesizing provably safe control envelopes for hybrid systems, yielding families of safe controllers that maximize permissiveness while guaranteeing safety. It formalizes the optimal envelope through differential game logic (dGL) and characterizes it as an optimal controllable invariant $I^{\mathrm{opt}}$ with guards $G^{\mathrm{opt}}$, then derives explicit, runtime-checkable solutions via symbolic execution and iterative refinements. A reduction oracle is used to translate loop-free subproblems into decidable real-arithmetic formulas, aided by action permanence and, when needed, differential-invariant techniques for non-solvable dynamics. The CESAR algorithm systematically generates a sequence of increasingly capable envelopes (with varying optimality guarantees) and validates them on benchmarks, demonstrating its ability to handle diverse control challenges and to provide formal guarantees of safety and, in many cases, optimality. This approach enables robust runtime monitoring and has potential to integrate with learning-based controllers while preserving formal safety guarantees.

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.

Figures (3)

• Figure 1: Robot navigating a corridor (model:corridor). A 2D robot must navigate safely within a corridor with a dead-end without crashing against a wall. The corridor extends infinitely on the bottom and on the right. The robot can choose between going left and going down with a constant speed $V$. The left diagram shows $I^0$ in gray. The right diagram shows $I^1$ under the additional assumption $VT < 2R$ ($I^1$ and $I^0$ are otherwise equivalent). A darker shade of gray is used for regions of $I^1$ where only one of the two available actions is safe according to $G^1$.
• Figure 2: Definition of ${\normalfont \textsf{reduce}}\xspace$ ( exact elided). Notation $P\{e/x\}$ indicates $P$ with unbound occurrences of $x$ replaced by expression $e$. $\texttt{odereduce}$ isolates the effect of reduce on ODEs. $\triangleright$ simplifies and quantifier eliminates $P$ assuming $A$.
• Figure 3: axiomatization and derived axioms and rules

Theorems & Definitions (8)

• definition thmcounterdefinition
• definition thmcounterdefinition: Controllable Invariant
• definition thmcounterdefinition: Reduction Oracle
• definition thmcounterdefinition: Action Permanence
• definition thmcounterdefinition: Uniform Action Optimality
• definition thmcounterdefinition: ODE reduction
• definition thmcounterdefinition: semantics
• definition thmcounterdefinition: Semantics of hybrid games