Fast Decomposition of Temporal Logic Specifications for Heterogeneous Teams

TL;DR

This paper presents a method to efficiently decompose large multi-agent path planning problems with temporal logic goals into smaller, manageable sub-problems, enabling faster planning while ensuring the overall mission is satisfied.

Contribution

We introduce a novel SMT-based approach to jointly decompose temporal logic specifications and agent teams for scalable multi-agent planning.

Findings

Significant speed-up in planning time using the decomposition method.

Trade-offs between computational efficiency and conservativeness of the SMT encoding.

Effective handling of complex temporal logic specifications over heterogeneous agents.

Abstract

In this work, we focus on decomposing large multi-agent path planning problems with global temporal logic goals (common to all agents) into smaller sub-problems that can be solved and executed independently. Crucially, the sub-problems' solutions must jointly satisfy the common global mission specification. The agents' missions are given as Capability Temporal Logic (CaTL) formulas, a fragment of signal temporal logic, that can express properties over tasks involving multiple agent capabilities (sensors, e.g., camera, IR, and effectors, e.g., wheeled, flying, manipulators) under strict timing constraints. The approach we take is to decompose both the temporal logic specification and the team of agents. We jointly reason about the assignment of agents to subteams and the decomposition of formulas using a satisfiability modulo theories (SMT) approach. The output of the SMT is then distributed to subteams and leads to a significant speed up in planning time. We include computational results to evaluate the efficiency of our solution, as well as the trade-offs introduced by the conservative nature of the SMT encoding.