Extended Abstract: Formal Design of Cooperative Multi-Agent Systems

We propose a formal design framework to automatically synthesize coordination and control schemes for cooperative multi-agent systems by combining a top-down mission planning with a bottom-up motion planning. The multi-agent system is assigned a global mission, specified as regular languages over all the agents’ capabilities, whereas basic motion controllers for each agent shall be designed with respect to given environment description. On one hand, a mission planning layer sits on the top of the proposed framework, decomposing the global mission into local tasks that are in consistency with each agent’s individual capabilities, and compositionally verifying the joint effort of the agents via an assume guarantee paradigm. On the other hand, corresponding to these local missions, motion plans associated with each agent are synthesized by composing basic motion primitives, which are verified safe by differential dynamic logic (dL), through a Satisfiability Modulo Theories (SMT) solver that searches feasible solutions in face of constraints due to local task requirements and the environment description. It is shown that the proposed framework can handle changing environments as the motion primitives are reactive in nature, making the motion planning adaptive to local environmental changes. Furthermore, on-line mission reconfiguration can be triggered by the motion planning layer once no feasible solutions can be found through the SMT solver. The effectiveness of the overall design framework is demonstrated by an automated warehouse case study.