Dissertation Talk: Constructive Formal Control Synthesis through Abstraction and Decomposition

Presentation | May 9 | 11 a.m.-12 p.m. | 531 Cory Hall

 Electrical Engineering and Computer Sciences (EECS)

It is often easier to describe what we want an autonomous system to do rather than how to do it. A control synthesizer bridges that gap by automatically constructing control software so the closed loop dynamics enforce a desired behavior such as safety or reachability. While many specific instances of control synthesis have elegant mathematical solutions, designing tractable algorithms to compute solutions for general systems and specifications remains elusive.

This talk will present a modular and constructive theoretical framework to express computational pipelines for robust control synthesis. I apply this framework to a dynamic programming pipeline and show how systematically modifying it allows one to exploit structural properties in the dynamics and specification. Finite abstractions enable one to explore tradeoffs between tractability and completeness by coarsening and refining the dynamics. The traditional robust controlled predecessor operator can also be decomposed into a more efficient, iterative counterpart. Each of these modifications recovers the true solution to the original problem or yields a sound under-approximation. I will showcase some robotics and traffic benchmarks and, if time permits, will also present techniques to interconnect distributed control systems while safely preserving guarantees about the global behavior.

 eskim@berkeley.edu