Aditi Kabra

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 ω). 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.

This thesis starts by designing, as a target for automation, the first verified train control envelope that accounts for all the forces in a realistic train kinematics model, demonstrating the feasibility and potential benefits of applying verified control envelopes to a realistic industrial-scale system. The thesis then automates the process of designing such a control envelope 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. It then 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 (gamse 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 (two-player, zero-sum games). It introduces a specialized algorithm, CESAR, to solve for an important class of control problems (time-triggered control, where the controller repeatedly polls to provide control decisions with some maximum time latency). By strategically using AI along with verification, it provides a general framework that leverages large language models for sound, scalable synthesis.