Assume-guarantee cooperative satisfaction of multi-agent systems

This paper aims to investigate the task decomposition problem of multi-agent systems. Task decomposition among agents refers to a process to decompose a given global task into subtasks for individual agents. The decomposition is not arbitrary and should be done in such a way that the satisfaction of the sub-tasks by all agents individually would imply the accomplishment of the global task collectively. In this paper, it is assumed that agents are modeled by labeled transition systems, and the global specification is given as a subclass of Computation Tree Logic (CTL) formulas. It is also assumed that the global CTL specification is broadcasted to and known by all agents. Agents could be heterogeneous and have different capabilities. In order to obtain subtasks for each agent with a maximum potential for fault tolerance, our basic idea is to let each agent contribute to their maximum capabilities in the sense of satisfying a maximum number of sub-formulas of the global specification. The maximum satisfaction set is achieved through a modified CTL model checking algorithm. These maximum satisfiable sub-formulas can be used as the subtask for the corresponding agent. Furthermore, based on assume-guarantee reasoning, sufficient conditions are derived to guarantee the satisfaction of the global CTL specification provided that each agent fullfill its own subtasks. A two-robot cooperative motion planning example is given to illustrate the results.