Cooperative Planning for Coupled Multi-Agent Systems under Timed Temporal Specifications

TL;DR

This paper introduces an automated method for synthesizing controllers for multi-agent systems with coupled constraints, ensuring each agent satisfies high-level temporal specifications using formal verification techniques.

Contribution

It presents a novel decentralized abstraction and an algorithm for controller synthesis that guarantees high-level temporal logic specifications are met in coupled multi-agent systems.

Findings

Successfully synthesized controllers satisfying specifications in simulation.

Decentralized abstraction enables scalable formal verification.

Method ensures provable satisfaction of high-level tasks.

Abstract

This paper presents a fully automated procedure for controller synthesis for multi-agent systems under coupled constraints. Each agent has dynamics consisting of two terms: the first one models the coupled constraints and the other one is an additional control input. We aim to design these inputs so that each agent meets an individual high-level specification given as a Metric Interval Temporal Logic (MITL). First, a decentralized abstraction that provides a time and space discretization of the multi-agent system is designed. Second, by utilizing this abstraction and techniques from formal veri- fication, we provide an algorithm that computes the individual runs which provably satisfy the high-level tasks. The overall approach is demonstrated in a simulation example.