Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Coordination and Synchronization of Multi-Robot Systems Under Recurring Linear Temporal Logic

Davide Peron, Victor Nan Fernandez-Ayala, Eleftherios E. Vlahakis, Dimos V. Dimarogonas

TL;DR

The paper presents a scalable, bottom-up framework for coordinating and synchronizing multi-robot teams under recurring LTL tasks by combining offline plan synthesis with online collaboration and synchronization. It introduces ROI-based motion-transition representations and a dedicated recurring-LTL task specification to reduce state-space size and avoid heavy PBA constructions, while implementing a robust RRC (request-reply-confirmation) cycle and time synchronization within ROS2. The methodology is validated on nine real robots and demonstrated at scale in simulations with up to ninety agents, showing substantial complexity reductions, improved adaptability, and successful coordination despite action delays. The approach enables practical large-scale deployment by leveraging ROI, FTS, MIP filtering, and robust synchronization, with open avenues for richer actions and human-in-the-loop extensions.

Abstract

We consider multi-robot systems under recurring tasks formalized as linear temporal logic (LTL) specifications. To solve the planning problem efficiently, we propose a bottom-up approach combining offline plan synthesis with online coordination, dynamically adjusting plans via real-time communication. To address action delays, we introduce a synchronization mechanism ensuring coordinated task execution, leading to a multi-agent coordination and synchronization framework that is adaptable to a wide range of multi-robot applications. The software package is developed in Python and ROS2 for broad deployment. We validate our findings through lab experiments involving nine robots showing enhanced adaptability compared to previous methods. Additionally, we conduct simulations with up to ninety agents to demonstrate the reduced computational complexity and the scalability features of our work.

Efficient Coordination and Synchronization of Multi-Robot Systems Under Recurring Linear Temporal Logic

TL;DR

The paper presents a scalable, bottom-up framework for coordinating and synchronizing multi-robot teams under recurring LTL tasks by combining offline plan synthesis with online collaboration and synchronization. It introduces ROI-based motion-transition representations and a dedicated recurring-LTL task specification to reduce state-space size and avoid heavy PBA constructions, while implementing a robust RRC (request-reply-confirmation) cycle and time synchronization within ROS2. The methodology is validated on nine real robots and demonstrated at scale in simulations with up to ninety agents, showing substantial complexity reductions, improved adaptability, and successful coordination despite action delays. The approach enables practical large-scale deployment by leveraging ROI, FTS, MIP filtering, and robust synchronization, with open avenues for richer actions and human-in-the-loop extensions.

Abstract

We consider multi-robot systems under recurring tasks formalized as linear temporal logic (LTL) specifications. To solve the planning problem efficiently, we propose a bottom-up approach combining offline plan synthesis with online coordination, dynamically adjusting plans via real-time communication. To address action delays, we introduce a synchronization mechanism ensuring coordinated task execution, leading to a multi-agent coordination and synchronization framework that is adaptable to a wide range of multi-robot applications. The software package is developed in Python and ROS2 for broad deployment. We validate our findings through lab experiments involving nine robots showing enhanced adaptability compared to previous methods. Additionally, we conduct simulations with up to ninety agents to demonstrate the reduced computational complexity and the scalability features of our work.

Paper Structure

This paper contains 31 sections, 3 theorems, 9 equations, 5 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. LTL and Büchi Automaton
  4. LTL Planning
  5. System Setup
  6. System description
  7. Motion Transition System
  8. Action Model
  9. Agent Transition System
  10. Task Specification
  11. Main Results
  12. Offline Initial Planning
  13. Collaboration Request
  14. Reply
  15. Confirmation
  16. ...and 16 more sections

Key Result

Theorem 1

Consider the set of agents $\mathcal{N}$ and the $M$ actions in $\mathbf{Req}^{a_i}$. Let $\mathcal{N}_F$ be the set of filtered agents given by Proc. proc:filtering. Assume that the MIP in eq:MIP for $\mathcal{R}=\mathcal{N}$ is feasible. Then, the MIP in eq:MIP for $\mathcal{R}=\mathcal{N}$ and fo

Figures (5)

  • Figure 1: T. Turtlebot, B. Rosie
  • Figure 2: Workspace abstraction
  • Figure 4: Effects of agents filtering
  • Figure 5: Agents actions in the experimental settings
  • Figure 6: 90 agents actions in the scalability simulation

Theorems & Definitions (9)

  • Definition 1
  • Definition 2
  • Remark 1
  • Theorem 1
  • proof
  • Lemma 1
  • proof
  • Theorem 2
  • proof