Probabilistic Swarm Guidance Subject to Graph Temporal Logic Specifications

As the number of agents comprising a swarm increases, individual-agent-based control techniques for collective task completion become computationally intractable. We study a setting in which the agents move along the nodes of a graph, and the high-level task specifications for the swarm are expressed in a recently proposed language called graph temporal logic (GTL). By constraining the distribution of the swarm over the nodes of the graph, GTL specifies a wide range of properties, including safety, progress, and response. In contrast to the individual-agent-based control techniques, we develop an algorithm to control, in a decentralized and probabilistic manner, a collective property of the swarm: its density distribution. The algorithm, agnostic to the number of agents in the swarm, synthesizes a time-varying Markov chain modeling the time evolution of the density distribution of a swarm subject to GTL. We first formulate the synthesis of such a Markov chain as a mixed-integer nonlinear program (MINLP). Then, to address the intractability of MINLPs, we present an iterative scheme alternating between two relaxations of the MINLP: a linear program and a mixed-integer linear program. We evaluate the algorithm in several scenarios, including a rescue mission in a high-fidelity ROS-Gazebo simulation.