Provably-correct coordination of large collections of agents with counting temporal logic constraints

In this paper, we consider the problem of coordinating a large collection of homogeneous agents subject to a novel class of constraints: counting temporal logic constraints. Counting constraints arise naturally in many multi-agent planning problems where the identity of the agents is not important for the task to be completed. We introduce a formal language to capture such tasks and present an optimization-based technique to synthesize plans for large collections of agents in a way to guarantee the satisfaction of tasks specified in this formalism.