High-level verifiable robotics

The recent DARPA Robotics Challenge has demonstrated that while robots have advanced significantly in the past few decades in terms of both hardware and software, even the best of them take almost an hour to perform tasks a person can do in 5 minutes. This is mostly due to the human-in-the-loop; Instead of providing high-level instructions such as "turn the valve", most teams had expert operators looking through the robot's "eyes" and controlling most of the robot's actions. Furthermore, some of the falls during the challenge are attributed to operator error. For such challenges, and for robots to be integrated into society in general, autonomy, and more specifically, verifiable autonomy, is a key factor for success.

To achieve autonomy and true human robot collaboration, 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; the use of language, abstractions and temporal logic to capture high-level task specifications, and the development of formal methods that automatically either transform task specifications into correct robot behavior, if such behavior exists, or provide explanations to the user of why a robot might fail