# Learning-based Formal Synthesis of Cooperative Multi-agent Systems

## TL;DR

This paper introduces a formal, learning-based framework for synthesizing coordination policies in multi-agent systems, ensuring global mission satisfaction through local task decomposition, supervisor synthesis, and motion planning, validated by multi-robot experiments.

## Contribution

It presents a novel divide-and-conquer formal synthesis approach using modified L* algorithms for multi-agent coordination with verified global specifications.

## Key findings

- Effective multi-robot coordination demonstrated
- Automated supervisor synthesis verified in experiments
- Framework guarantees global mission satisfaction

## Abstract

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.