Fast Decomposition of Temporal Logic Specifications for Heterogeneous Teams

Abstract

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