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

TL;DR

This work tackles controller synthesis for large-scale multi-agent systems under Signal Temporal Logic (STL) specifications by introducing a continuous-time assume-guarantee contract (AGC) framework. STL tasks are recast into prescribed performance control (PPC) problems and embedded into local AGCs, enabling distributed synthesis and compositional guarantees. The paper develops two main compositionality results for acyclic and cyclic interconnections, along with a uniform strong satisfaction concept to handle general networks. A closed-form, PPC-based distributed controller is derived to enforce local contracts, which guarantees global STL satisfaction through the AGC-based composition, and its effectiveness is demonstrated on room-temperature regulation and mobile-robot experiments. The approach provides scalable, provably correct control for collaborative STL tasks with low computational overhead, suitable for large multi-agent deployments.

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.

Figures (11)

• Figure 1: A multi-agent system with two clusters $I_1 = \{1,2\}$ and $I_2 = \{3\}$.The solid lines indicate the communication links between agents, and the dotted lines with arrows indicate the dynamical couplings between clusters.
• Figure 2: An illustration of weak and strong satisfaction of a contract. Top: trajectories of the internal inputs $w_i$. Bottom: trajectories of the state $x_i$. Intuitively, the weak (or strong) satisfaction states that if the assumptions $A_i^a$ are satisfied up to time $t \in \mathbb{R}_{\geq 0}$, the system's state belongs to $G_i$ at least until time $t$ ($t+\delta_i$ with $\delta_i >0$ in the case of strong satisfaction).
• Figure 3: An illustration of a multi-agent system with acyclic or cyclic cluster interconnection graphs. The solid lines indicate the communication links between agents, and the dotted lines with arrows indicate the dynamical couplings between clusters.
• Figure 4: Prescribed regions for STL formulae.
• Figure 5: Trajectories of the temperature (a) and control input (b) of the closed-loop agents $\Sigma_1$, $\Sigma_2$, $\Sigma_{N-1}$ and $\Sigma_{N}$, where $N=1000$, under control policy in \ref{['controller']}.

Theorems & Definitions (19)

• Remark 2
• Definition 3
• Example 7
• Definition 8
• Definition 9
• Proposition 10
• Theorem 11
• Theorem 12
• Remark 13
• Definition 14