Distributed Communication-aware Motion Planning for Networked Mobile Robots under Formal Specifications

TL;DR

This paper introduces a novel distributed control framework for networked mobile robots that integrates motion planning with communication quality optimization using formal logic specifications, ensuring high-level objectives are met while maintaining communication performance.

Contribution

It is the first to synthesize controllers for STREL specifications, combining STL and STREL in a hierarchical MPC approach for robot networks.

Findings

Validated through simulation examples demonstrating effectiveness.

First to address controller synthesis for STREL specifications.

Ensures soundness and completeness of the hierarchical MPC approach.

Abstract

Control and communication are often tightly coupled in motion planning of networked mobile robots, due to the fact that robotic motions will affect the overall communication quality, and the quality of service (QoS) of the communication among the robots will in turn affect their coordination performance. In this paper, we propose a control theoretical motion planning framework for a team of networked mobile robots in order to accomplish high-level spatial and temporal motion objectives while optimizing communication QoS. Desired motion specifications are formulated as Signal Temporal Logic (STL), whereas the communication performances to be optimized are captured by recently proposed Spatial Temporal Reach and Escape Logic (STREL) formulas. Both the STL and STREL specifications are encoded as mixed integer linear constraints posed on the system and/or environment state variables of the mobile robot network, where satisfactory control strategies can be computed by exploiting a distributed model predictive control (MPC) approach. To the best of the authors' knowledge, we are the first to study controller synthesis for STREL specifications. A two-layer hierarchical MPC procedure is proposed to efficiently solve the problem, whose soundness and completeness are formally ensured. The effectiveness of the proposed framework is validated by simulation examples.