Compositional and symbolic synthesis of reactive controllers for multi-agent systems

• Published in: Information and computation 2018-08, Vol.261, p.616-633
• Main Authors: Alur, Rajeev, Moarref, Salar, Topcu, Ufuk
• Format: Article
• Language: English
• Subjects: Compositional synthesis; Formal methods; Multi-agent systems; Reactive synthesis
• ISSN: 0890-5401; 1090-2651
• DOI: 10.1016/j.ic.2018.02.021

We consider the controller synthesis problem for multi-agent systems that consist of a set of controlled and uncontrolled agents. Controlled agents may need to cooperate with each other and react to actions of uncontrolled agents in order to fulfill their objectives. Moreover, agents may be imperfect, i.e., only partially observe their environment. We propose a framework for controller synthesis based on compositional reactive synthesis. We implement the algorithms symbolically and apply them to a robot motion planning case study where multiple robots are placed on a grid-world with static obstacles and other dynamic, uncontrolled and potentially adversarial robots. We consider different objectives such as collision avoidance, keeping a formation and bounded reachability. We show that by taking advantage of the structure of the system, compositional synthesis algorithm can significantly outperform centralized alternative, both from time and memory perspective, and can solve problems where the centralized algorithm is infeasible.