Mechanical and Civil Engineering Seminar

Why don't we have robots fetching us coffee and finding our keys for us? While robots have become more capable and powerful, they are not yet integrated into everyday life. Part of the reason is that robots are difficult to program and even more difficult to verify. Therefore, to achieve the dream of a robot in every home, two key challenges must be addressed; people should be able to easily interact with robots, and robots must always do as they are told.

In this talk I will discuss the work done in my group to address these challenges. Specifically, I will describe the use of language and temporal logic to capture high-level task specifications, the development of formal methods that automatically transform task specifications into correct robot behavior, if such behavior exists, and approaches to dealing with the extra complexities of verifying autonomous robots.