Signal Temporal Logic Task Decomposition via Convex Optimization

TL;DR

This paper presents a convex optimization approach for decomposing a global Signal Temporal Logic (STL) formula into local tasks for multi-agent systems, ensuring the global specification is satisfied through local task satisfaction.

Contribution

It introduces a novel convex optimization method for decomposing global STL formulas into local tasks with hypercube predicates, guaranteeing global satisfaction.

Findings

Convex program maximizes the volume of predicate zero level-sets.

Two alternative local STL task definitions are proposed.

Global STL satisfaction is proven when local tasks are satisfied.

Abstract

In this paper we focus on the problem of decomposing a global Signal Temporal Logic formula (STL) assigned to a multi-agent system to local STL tasks when the team of agents is a-priori decomposed to disjoint sub-teams. The predicate functions associated to the local tasks are parameterized as hypercubes depending on the states of the agents in a given sub-team. The parameters of the functions are, then, found as part of the solution of a convex program that aims implicitly at maximizing the volume of the zero level-set of the corresponding predicate function. Two alternative definitions of the local STL tasks are proposed and the satisfaction of the global STL formula is proven when the conjunction of the local STL tasks is satisfied.