Formal Methods for Building a Multi-Robot Task Server

ABSTRACT: In this talk, I will talk about synthesis challenges that arose in our attempts to build Antlab, an end-to-end system that takes streams of user task requests and executes them using collections of robots. In Antlab, each request is specified declaratively in linear temporal logic extended with quantifiers over robots. The user does not program robots individually, nor know how many robots are available at any time or the precise state of the robots. The Antlab runtime system manages the set of robots, schedules robots to perform tasks, automatically synthesizes robot motion plans from the task specification, and manages the co-ordinated execution of the plan.

We are using Antlab as an end-to-end application of formal methods in cyber-physical systems.I will describe techniques to bridge the gap between continuous and discrete worlds,and hierarchical synthesis tools based on repeated re-planning and dynamic conflict resolution. On the theoretical side, I will describe compositional synthesis for continuous systems and some new classesof synthesis problems.On the practical side, I will describe ongoing work in using natural language for declarative specifications of tasks.

This talk represents joint work with Brendon Boldt, Eva Darulova, Rayna Dimitrova, Ivan Gavran, Kaushik Mallik, Vinayak Prabhu, Indranil Saha, Anne-Kathrin Schmuck, Sadegh Soudjani, and Damien Zufferey.

BIO: Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems. Previously, he was a faculty member at the University of California, Los Angeles. His research interests are in the verification and control of reactive, real-time, hybrid, and probabilistic systems, software verification and programming languages, logic, and automata theory. He received the President’s Gold Medal from IIT, Kanpur, the Leon O. Chua award from UC Berkeley, an NSF CAREER award, a Sloan Foundation Fellowship, an ERC Synergy award, and “Most Influential Paper” awards from PLDI and POPL.

Hosted by: Paul Bogdan