Synchronous and asynchronous multi-agent coordination with cLTL+ constraints
Yunus Emre Sahin, Petter Nilsson, Necmiye Özay · 2017
Planning trajectories for multiple agents in a way to guarantee that their collective behavior satisfies a certain high-level specification is crucial in many application domains. Motivated by this problem, we introduce a new logic called counting linear temporal logic plus (cLTL+). This logic enables specifying multi-agent tasks over possibly infinite horizons in a compact manner. We then propose an optimization-based method that generates trajectories for individual agents that, when implemented together, guarantee the satisfaction of a given cLTL+ formula. In the second part of the paper, we discuss how these results can be extended to generate trajectories that can be asynchronously implemented by the agents while preserving the satisfaction of the desired cLTL+ specification. In particular, we show that when the asynchrony between agent trajectories is bounded, it is possible to generate trajectories robust against such asynchrony with an appropriate modification of the optimization problem. Finally, we demonstrate these ideas on selected examples.