  We propose a formal design framework for synthesizing coordination and
control policies for cooperative multi-agent systems to accomplish a global
mission. The global performance requirements are specified as regular languages
while dynamics of each agent as well as the shared environment are
characterized by finite automata, upon on which a formal design approach is
carried out via divide-and-conquer. Specifically, the global mission is
decomposed into local tasks; and local mission supervisors are designed to
accomplish these local tasks while maintaining the multi-agent performance by
integrating supervisor synthesis with compositional verification techniques;
finally, motion plans are automatically synthesized based on the obtained
mission plans. We present three modifications of the L* learning algorithm such
that they are adapted for the synthesis of the local mission supervisors, the
compositional verification and the synthesis of local motion plans, to
guarantee that the collective behavior of the agents will ensure the
satisfaction of the global specification. Furthermore, the effectiveness of the
proposed framework is demonstrated by a detailed experimental study based on
the implementation of a multi-robot coordination scenario. The proposed
hardware-software architecture, with each robot's communication and
localization capabilities, is exploited to examine the automatic supervisor
synthesis with inter-robot communication.
