Autonomous systems in the intersection of controls, learning theory and formal methods
University of Texas at Austin
Autonomous systems are emerging as a driving technology for countlessly many applications. Numerous disciplines tackle the challenges toward making these systems agile, adaptable, reliable, user friendly and economical. On the other hand, the existing disciplinary boundaries delay and possibly even obstruct progress. I argue that the non-conventional problems that arise in the design and verification of autonomous systems require hybrid solutions at the intersection of learning, formal methods and controls.
I will present our recent results in two problems. The first one is on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for dynamics that are subject to rich temporal logic specifications, heterogenous uncertainties and possibly adversarial environments. They combine ideas from control theory with those from formal methods, and exploit underlying system-theoretic interpretations to suppress the inherent computational complexity. My studies of the second problem have resulted in a series of new reinforcement learning algorithms that build on both learning theory and formal methods. A common feature in these algorithms is the guarantees they provide during both training and execution with respect to given formal specifications expressed in variants of temporal logic. Throughout the talk, I will place the results in the context of aerospace applications with concrete examples.
Ufuk Topcu joined the Department of Aerospace Engineering at the University of Texas at Austin as an assistant professor in Fall 2015.
He received his Ph.D. degree from the University of California at Berkeley in 2008. He held research positions at the University of Pennsylvania and California Institute of Technology. His research focuses on the theoretical, algorithmic and computational aspects of design and verification of autonomous systems through novel connections between formal methods, learning theory and controls. He has received the NSF CAREER and AFOSR YIP awards.