Fast Decomposition of Temporal Logic Specifications for Heterogeneous
  Teams
  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.
