Tata Institute of Fundamental Research
Formal Methods for Building a Multi-Robot Task Server
STCS Seminar
Speaker:
Rupak Majumdar (Max Planck Institute for Software Systems
Paul-Ehrlich Strasse G 26
67663 Kaiserslautern
Germany)
Organiser:
Paritosh K Pandya
Date:
Monday, 17 Dec 2018, 16:00 to 17:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
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.
| Speaker: | Rupak Majumdar (Max Planck Institute for Software Systems Paul-Ehrlich Strasse G 26 67663 Kaiserslautern Germany) |
| Organiser: | Paritosh K Pandya |
| Date: | Monday, 17 Dec 2018, 16:00 to 17:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
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.
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.