Autonomous cyber-physical systems like robots and self-driving cars stretch the limits of engineering, and reasoning precisely about their behavior is increasingly difficult. Moreover, a correct implementation is often elusive even when the desired outcome is obvious. Algorithmic synthesis makes the formal specification of desired behavior an integral part of the controller design process -- the resulting controllers are correct by construction. Synthesis enables non-expert human users to provide complex system specifications, and be assured of their fulfillment. However, this goal of automatically generating autonomous control from user-defined specifications poses a host of unprecedented challenges.
In this talk, I will present two frameworks for automated synthesis from high-level specifications. I will first describe a system for generating, troubleshooting, and executing controllers for autonomous robots from natural language specifications, including analytical tools for automatically determining causes of failure to synthesize. I will then introduce a novel approach to synthesis for high-dimensional systems operating in uncertain environments, bypassing the need for discretizing the state space and admitting specifications that govern not just the order of events, but also their timing. Finally, I will present new research directions that push the envelope of synthesis for autonomous systems.
Vasu Raman is a postdoctoral scholar in the Department of Computing and Mathematical Sciences at the California Institute of Technology. Her research explores algorithmic methods for designing and controlling autonomous cyber-physical systems, guaranteeing correctness with respect to user-defined specifications. She earned a PhD in Computer Science from Cornell University and a BA in Computer Science and Mathematics from Wellesley College.