# Multirobot Coordination with Counting Temporal Logics

arXiv: https://arxiv.org/abs/1810.13087 · HTML: https://mlsanity.com/paper/1810.13087/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 Oct 2018.

## Built on by (most cited first, 7 of 7)

- [Conformal Temporal Logic Planning using Large Language Models](https://mlsanity.com/paper/2309.10092/) (2023)
- [Decomposition-based Hierarchical Task Allocation and Planning for Multi-Robots under Hierarchical Temporal Logic Specifications](https://mlsanity.com/paper/2308.10393/) (2023)
- [Neural Network-based Control for Multi-Agent Systems from Spatio-Temporal Specifications](https://mlsanity.com/paper/2104.02737/) (2021)
- [Simultaneous Task Allocation and Planning for Multi-Robots under Hierarchical Temporal Logic Specifications](https://mlsanity.com/paper/2401.04003/) (2024)
- [Safety-Critical Learning of Robot Control with Temporal Logic Specifications](https://mlsanity.com/paper/2109.02791/) (2021)
- [CatlNet: Learning Communication and Coordination Policies from CaTL+ Specifications](https://mlsanity.com/paper/2212.11792/) (2022)
- [CoFineLLM: Conformal Finetuning of LLMs for Language-Instructed Robot Planning](https://mlsanity.com/paper/2511.06575/) (2025)

## Abstract (arXiv)

In many multirobot applications, planning trajectories in a way to guarantee that the collective behavior of the robots satisfies a certain high-level specification is crucial. Motivated by this problem, we introduce counting temporal logics---formal languages that enable concise expression of multirobot task specifications over possibly infinite horizons. We first introduce a general logic called counting linear temporal logic plus (cLTL+), and propose an optimization-based method that generates individual trajectories such that satisfaction of a given cLTL+ formula is guaranteed when these trajectories are synchronously executed. We then introduce a fragment of cLTL+, called counting linear temporal logic (cLTL), and show that a solution to planning problem with cLTL constraints can be obtained more efficiently if all robots have identical dynamics. In the second part of the paper, we relax the synchrony assumption and discuss how to generate trajectories that can be asynchronously executed, while preserving the satisfaction of the desired cLTL+ specification. In particular, we show that when the asynchrony between robots is bounded, the method presented in this paper can be modified to generate robust trajectories. We demonstrate these ideas with an experiment and provide numerical results that showcase the scalability of the method.