Control of Swarm Robotic Systems from High-Level Temporal Logic Specifications


Swarm robotics is the study of robotic systems consisting of large numbers of robots whose local interactions with each other and with their environment lead to a collectively intelligent behavior. Swarm robotic systems have many potential applications such as exploration, surveillance, search and rescue, intrusion detection, inspection, construction and cleaning. Thus, it is not surprising that swarm robotics have been a very active research area. However, the intuition of the human designer is still the main ingredient in the development of swarm robotic systems, and a trial and error process based on iterative design and testing is an essential part of many existing design methods.


Advancements in technology are enabling mass production of cheap and capable robots, and there will be an indispensable need for scientific and engineering methods for formal mission specification and automated design techniques that result in swarm robotic systems with provably-correct collective behavior. To this end, in this project we considered the problem of automated synthesis of controllers from high-level temporal logic specifications for safe navigation of robotic swarms. The proposed framework facilitates the design and deployment process for swarm robotic systems, while providing formal guarantees on fulfillment of the collective objective.  

Relevant publications: 

  • Salar Moarref and Hadas Kress-Gazit, “Reactive Synthesis for Robotic Swarms”, To appear in 16th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2018

  • Ji Chen, Salar Moarref, and Hadas Kress-Gazit, “Verifiable Control of Robotic Swarm  from High-level Specifications", 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2018

  • Salar Moarref and Hadas Kress-Gazit, “Decentralized Control of Robotic Swarms from High-Level Temporal Logic Specification”, IEEE International Symposium on Multi-Robot and Multi-Agent Systems (MRS),  2017

Check out the video for our AAMAS 2018 paper: 

Compositional Reactive Synthesis for Multi-Agent Systems


Complex systems often consist of multiple agents (or components) interacting with each other and their environment to perform certain tasks and achieve specified objectives. For example, teams of robots are employed to perform tasks such as monitoring, surveillance, and disaster response in different domains including assembly planning, evacuation, search and rescue, localization, object transportation, and formation control. With growing complexity of systems and guarantees they are required to provide, the need for automated and reliable design and analysis methods and tools is increasing.  The necessity becomes more evident considering the safety-critical nature of some of these systems, e.g., medical devices, where the consequences of errors can be too catastrophic and even life threatening. An appealing approach to address these challenges is to automate the design process, i.e., to systematically build the system where the correctness follows from construction. To this end, reactive synthesis with the ambitious goal of automatically synthesizing correct-by-construction controllers from high-level specifications, has recently attracted significant attention in system design and control.


The goal of this project was to investigate and develop the necessary tools and methods for automated synthesis of controllers from high-level specifications for multi-agent systems. We studied how the existing structure in such problems can be exploited to achieve more efficient synthesis algorithms, e.g., through compositional synthesis techniques that can be applied to more realistic systems than the ones considered in the related literature. We proposed different frameworks for compositional synthesis of controllers for multi-agent systems. The overall theme of the solution approaches is to take advantage of the existing structure in multi-agent systems in order to decompose the synthesis problem into smaller and more manageable sub-problems, solving the sub-problems, and merging the results to obtain a solution to the main problem.  

Relevant publications: 

  • Rajeev Alur, Salar Moarref, Ufuk Topcu, “Pattern-Based Refinement of Interface Specifications in Reactive Synthesis”, In Tools and Algorithms for the Construction and Analysis of Systems, pp. 501-516. Springer Berlin Heidelberg, 2015 

  • Rajeev Alur, Salar Moarref, Ufuk Topcu, “Compositional Synthesis with Parametric Reactive Controllers”, Hybrid Systems: Computation and Control, 2016

  • Rajeev Alur, Salar Moarref, Ufuk Topcu, “Compositional Synthesis of Reactive Controllers for Multi-Agent Systems”, Computer Aided Verification, 2016

  • Salar Moarref, “Compositional Reactive Synthesis for Multi-Agent Systems”, Ph.D. Dissertation, 2016

  • Rajeev Alur, Salar Moarref, and Ufuk Topcu, “Compositional and Symbolic Synthesis of Reactive Controllers for Multi-Agent Systems”, Information and Computation, 2018

Automatic Refinement of Temporal Logic Specifications


Automatically constructing a provably-correct system from a high-level specification is an ambitious goal in system design and control. Such methods can facilitate the design of systems by focusing on what a system must achieve instead how it should be implemented. As a result, automated synthesis from high-level logical specifications has attracted significant attention in computer science and also control communities. However, in practice, writing a correct and complete formal specification which conforms to the (informal) design intent is a hard and tedious task and initial specifications are often incomplete and unrealizable, i.e. there is no system that can implement the specification. Furthermore, an unrealizable specification cannot be executed or simulated which makes its debugging a challenging and frustrating task.


In this project we developed debugging algorithms that automatically correct a specification by refining it through adding more logical formulas. The computed refinement can be considered as a feedback to the user (the one who wrote the initial specification) that explains in an understandable way what the problem is with the initial specification and how it can be fixed. The suggested refinement found by our algorithms can be validated by the user to ensure compatibility with her design intent and can be added to the specification to make it realizable.

Relevant publications: 

  • Rajeev Alur, Salar Moarref, and Ufuk Topcu, “Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications”, Formal Methods in Computer-Aided Design (FMCAD), 2013

Safe Schedulability of Bounded-Rate Multi-Mode Systems


Cyber Physical Systems (CPSs) are engineered systems which integrate the computational and communication capabilities with physical processes. These systems are usually composed of a set of controllers monitoring and controlling physical environment via a set of actuators, sensors and communication devices. Examples of such systems include medical devices, autonomous vehicles, power plants, and robots. Complex cyber-physical systems typically have several modes of operation where the goal of the system is to switch properly between these modes in order to satisfy a higher-level requirement or control objective. For example, the air-conditioning unit in each room of a building can be in different operational mode (heating, cooling, etc.). The goal is then to keep the temperature of each room in a comfort zone while keeping the peak energy consumption under a given budget (e.g., by avoiding turning all the units in all the rooms on at the same time). As peak power prices are 200-400 times that of the nominal rate, an uncoordinated activity is both expensive and operationally inefficient, and hence must be avoided.


In this project we studied an important scheduling problem for a special class of hybrid-systems (systems with both continuous and discrete behavior) that creates a recipe on when the system should switch to a different mode of operation and how long it should stay in that mode. For example, how the heating or cooling subsystems of each room must perform to keep the temperatures of the rooms in a given comfort zone while avoiding the pricey peak energy consumption for the whole building. On the theoretical side, we established the complexity results for solving such scheduling problems.

Relevant publications: 

  • Rajeev Alur, Vojtech Forejt, Salar Moarref, Ashutosh Trivedi, “Safe Schedulability of Bounded-Rate Multi-Mode Systems”, Hybrid Systems Computation and Control (HSCC), 2013

  • Rajeev Alur, Vojtech Forejt, Salar Moarref, Ashutosh Trivedi, “Schedulability of Bounded-Rate Multi-Mode Systems”, Journal of ACM Transactions on Embedded Computing Systems, 2016