Automatic synthesis of cooperative multi-agent systems

In this paper, the cooperative tasking and automatic controller synthesis problem for multi-agent systems are investigated. It is assumed that the global specification is given as regular languages while the multi-agent system is modeled as a concurrent discrete-event system defined by a collection of finite automata that interact with each other. A top-down and iterative design approach is pursued and the basic idea is to divide-and-conquer. First, the global specification is decomposed into subtasks with respect to each individual agents event sets. Then, a local supervisor is automatically synthesized for each agent respectively using learning based approaches. Thirdly, we use the assume-guarantee reasoning to check whether the collective behaviors of the local controlled agents can satisfy the global specification. Once the checking fails, a counterexample is generated and used to modify the task decomposition and the automatic synthesis process repeats. It is proved that the iterative process converges and a correctness of the design process is guaranteed. Finally, the design process is illustrated through a robot cooperative tasking example.