Controller Synthesis of Collaborative Signal Temporal Logic Tasks for Multi-Agent Systems via Assume-Guarantee Contracts

TL;DR

This paper presents a compositional framework for synthesizing controllers for large multi-agent systems to satisfy collaborative signal temporal logic tasks, ensuring global specifications through local contract enforcement.

Contribution

It introduces a novel assume-guarantee contract-based approach for STL task synthesis in multi-agent systems, enabling scalable and distributed controller design.

Findings

Successfully guarantees global STL task satisfaction through local contracts.

Provides a closed-form distributed feedback controller for agents.

Demonstrates effectiveness with numerical examples.

Abstract

This paper considers the problem of controller synthesis of signal temporal logic (STL) specifications for large-scale multi-agent systems, where the agents are dynamically coupled and subject to collaborative tasks. A compositional framework based on continuous-time assume-guarantee contracts is developed to break the complex and large synthesis problem into subproblems of manageable sizes. We first show how to formulate the collaborative STL tasks as assume-guarantee contracts by leveraging the idea of funnel-based control. The concept of contracts is used to establish our compositionality result, which allows us to guarantee the satisfaction of a global contract by the multi-agent system when all agents satisfy their local contracts. Then, a closed-form continuous-time feedback controller is designed to enforce local contracts over the agents in a distributed manner, which further guarantees the global task satisfaction based on the compositionality result. Finally, the effectiveness of our results is demonstrated by two numerical examples.