Formal methods play an increasingly important role in ensuring the correctness of autonomous systems. In this talk, I will first describe various controller synthesis techniques for systems that are subject to temporal logic specifications. The focus will be on the key assumptions and guarantees of these different techniques, including closed system synthesis, probabilistic synthesis, reactive synthesis, and minimum violation planning, especially in the context of autonomous vehicles. The second part of the talk will focus on a key bottleneck that prevents formal methods from realizing their full potential in the autonomous system domain---the (un)availability of formal specifications, which is a common, fundamental assumption all the temporal logic synthesis techniques rely on. Finally, I will discuss our early effort to partially address this problem and the remaining challenges.
Tichakorn (Nok) Wongpiromsarn received the B.S. degree in mechanical engineering from Cornell University in 2005 and the M.S. and Ph.D. degrees in mechanical engineering from California Institute of Technology in 2006 and 2010, respectively. She is currently an assistant professor in the Department of Computer Science at Iowa State University. Her research spans several areas of computer science, control, and optimization, including formal methods, motion planning, situational reasoning, hybrid systems, and distributed control systems. Most of her work draws inspiration from practical applications, especially in autonomy, robotics, and transportation. A significant portion of her career has been devoted to the development of autonomous vehicles, both in academia and industry settings. In particular, she was a principal research scientist and led the planning team at nuTonomy (now Hyundai-Aptiv Autonomous Driving Joint Venture), where her work focused on planning, decision making, control, behavior specification, and validation of autonomous vehicles. She also led the Systems Team for Team Caltech in the 2007 DARPA Urban Challenge during her Ph.D.