Princeton University

School of Engineering & Applied Science

Synthesis for Autonomy: Connecting the Physical, the Logical and the Human

Vasumathi Raman, United Technologies Research Center
E-Quad, B205
Thursday, March 24, 2016 - 4:30pm

Autonomous cyber-physical systems like unmanned aircraft 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 an optimization-based controller-synthesis framework for high-dimensional systems operating in uncertain environments, bypassing the need for discretizing the state space and admitting specifications that govern not only 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 Senior Scientist at the United Technologies Research Center in Berkeley, CA. 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 in 2013, and was a postdoctoral scholar in the Department of Computing and Mathematical Sciences and the Department of Control and Dynamical Systems at the California Institute of Technology from 2013-2015. She has contributed extensively to the LTLMoP toolkit for robot mission planning and the slugs reactive synthesis tool, and developed BluSTL, a toolbox for automatically generating controllers from timed temporal logic specifications. Vasu also holds a BA in Computer Science and Mathematics from Wellesley College.