Correct-By-Construction Control Synthesis in Model-Based Design of Autonomous Systems
Ufuk Topcu, Department of Electrical and Systems Engineering, University of Pennsylvania
Friday, November 21, 2014
Schwada Classroom Office Building (SCOB) 210, Tempe campus [map]
How can we affordably build trustworthy autonomous, networked systems?
Partly motivated by this question, Ufuk Topcu will describe a shift from the traditional “design+verify” approach to “specify+synthesize” in model-based engineering. He will then discuss our recent results on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for hybrid dynamics that are subject to rich temporal logic specifications and heterogenous uncertainties, and that operate in adversarial environments. They combine ideas from control theory with those from computer science, and exploit underlying system-theoretic interpretations to suppress the inherent computational complexity. The expressivity of the resulting design methodology enables us to formally investigate a number of emerging issues in autonomous, networked systems. The talk will conclude with a brief overview of several such issues from my ongoing projects: (i) compositional synthesis for the so-called fractionated systems; (ii) effects of perception imperfections on protocol synthesis; (iii) interfaces between learning modules and reactive controllers with provable guarantees of correctness; and (iv) human-embedded autonomy.
Ufuk Topcu is a research assistant professor in the Department of Electrical and Systems Engineering at the University of Pennsylvania. He received his Ph.D. from the University of California, Berkeley and was a postdoctoral scholar at the California Institute of Technology until 2012. His research is on the analysis, design, and verification of autonomous, networked systems.