Current browse context:
eess.SY
Change to browse by:
References & Citations
Electrical Engineering and Systems Science > Systems and Control
Title: CESAR: Control Envelope Synthesis via Angelic Refinements
(Submitted on 6 Nov 2023 (v1), last revised 4 Apr 2024 (this version, v2))
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.
Submission history
From: Aditi Kabra [view email][v1] Mon, 6 Nov 2023 02:41:41 GMT (146kb,D)
[v2] Thu, 4 Apr 2024 20:05:39 GMT (149kb,D)
Link back to: arXiv, form interface, contact.