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. In particular, I shall describe the technique of abstraction-based controller synthesis, which applies reactive synthesis techniques to continuous control problems.
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.