Doctoral Thesis Proposal - Aditi Kabra

— 1:00pm

Location:
In Person - Gordon Bell Conference Room, Gates Hillman 5117

Speaker:
ADITI KABRA, Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://aditink.github.io/

Verified Control Envelope Synthesis for Hybrid Systems

Many cyber-physical systems, such as trains, planes, and self-driving cars, are safety-critical but difficult to reason about. Formal verification can provide strong safety guarantees, but most industrial controllers are too complex to formally verify. Safe control envelopes characterize families of safe controllers and are used to monitor untrusted controllers on verifiable abstractions of control systems that isolate the parts relevant to safety without the full complexity of a specific control implementation, at runtime. They can put complex controllers, even when machine learning based, within the reach of formal guarantees. But correct control envelopes are still hard to design because the control engineer needs to identify correct control conditions that tell the controller what to do right now to stay safe at all times in the future by anticipating the behavior of the system over complex dynamics and an uncountably infinite state space. 

This thesis proposes to provide synthesis techniques to automatically synthesize provably correct control conditions, greatly reducing the manual effort required for control envelope design. It aims to scale synthesis to complexity of real-world systems. The input of the synthesis tool is a sketch of the control envelope in a hybrid system showing what kind of control behavior is physically possible. The tool fills in the blanks of the sketch by synthesizing control conditions using hybrid system game theory. The output is a provably correct symbolic control envelope. Existing controller synthesis techniques do not solve control envelope synthesis because control envelopes have the higher-order constraint of permitting as many valid control solutions as possible. 

Completed work provides the algorithm CESAR (Control Envelope Synthesis via Angelic Refinement) which solves a class of problems where a set of systematic game refinements allows automatic control envelope synthesis. Proposed work generalizes synthesis to a broad class of systems (characterized by admitting a natural representation in differential game logic) and develops a system that allows users to provide the human intuition based insights that, together with automated reasoning, can complete the control envelope synthesis process in more complex cases. 

Thesis Committee

André Platzer (Co-chair, Carnegie Mellon University/Karlsruhe Institute of Technology)
Stefan Mitsch (Co-chair, Carnegie Mellon University/DePaul University)
Eunsuk Kang
Armando Solar-Lezama (Massachusetts Institute of Technology)
 

Additional Information

Event Website:
https://csd.cmu.edu/calendar/doctoral-thesis-proposal-aditi-kabra