Doctoral Thesis Oral Defense - Aditi Nandkishor Kabra
April 21, 2026 1:00PM—2:30PM
Location:
In Person and Virtual - ET
-
Reddy Conference Room, Gates Hillman 4405 and Zoom
Speaker:
ADITI NANDKISHOR KABRA,
Ph.D. Candidate
Computer Science Department
Carnegie Mellon University
https://aditink.github.io/
Many cyber-physical systems, such as trains, planes, and self-driving cars, are safety-critical but difficult to reason about. The task of designing controllers for such systems is complex (the subject of an entire field, control theory), made even more challenging by the need to ensure correctness over all of the infinitely many possible scenarios that the system may face. This thesis develops techniques that let computers automatically synthesize the conditions that define correct control solutions, with mathematical guarantees that these conditions are correct.
Symbolic control envelopes are our representation of the control conditions that characterize sets of safe control solutions. They are represented parametrically in symbols that can be instantiated with any real-valued input (e.g., for a train control envelope, train weight w). Control envelopes provide a path to designing complex controllers that still have mathematical correctness guarantees by allowing separation of concerns during controller design. A verified (i.e., mathematically correct) safe control envelope can first identify the set of control solutions that ensure the safety-critical control objectives, and then non-formal techniques, e.g., machine learning, can optimize within that envelope for secondary objectives.
The thesis automates the process of designing symbolic control envelopes by creating the first framework for symbolic control envelope synthesis. The framework takes as input the shape of a control system, which indicates what control and environment behaviors are physically possible and what the desired control behavior is, making the synthesis question well-defined. The framework automatically identifies the symbolic control conditions indicating when a given control action is correct, which is shown to correspond to the nondeterministic control policies of players in hybrid games (games with both continuous and discrete dynamics).
This thesis tackles the hybrid game control envelope synthesis problem in its full generality, developing the theory to solve for all of differential game logic. It introduces a specialized procedure for an interesting subset of problems (time-triggered, where the controller loops with some maximum time latency) that is total computable under some reasonable assumptions. By strategically using large language models along with verification, it provides a general approach to sound, scalable synthesis.
Thesis Committee
André Platzer (Co-Chair)
Stefan Mitsch (Co-Chair)
Eunsuk Kang
Armando Solar-Lezama (Massachusetts Institute of Technology)
In Person and Zoom Participation. See announcement.
For More Information:
matthewstewart@cmu.edu