A Temporal Logic-Based Hierarchical Network Connectivity Controller

TL;DR

This paper introduces a hierarchical LTL-based method for designing scalable, correct-by-construction communication schedules in sensor networks, ensuring information propagation while avoiding interference and congestion.

Contribution

It presents a novel hierarchical LTL-based algorithm that improves scalability and efficiency over existing centralized approaches for network communication scheduling.

Findings

The hierarchical algorithm is complete and scalable.

It effectively manages communication to prevent collisions and congestion.

Numerical experiments demonstrate improved efficiency and scalability.

Abstract

In this paper, we consider networks of static sensors with integrated sensing and communication capabilities. The goal of the sensors is to propagate their collected information to every other agent in the network and possibly a human operator. Such a task requires constant communication among all agents which may result in collisions and congestion in wireless communication. To mitigate this issue, we impose locally non-interfering connectivity constraints that must be respected by every agent. We show that these constraints along with the requirement of propagating information in the network can be captured by a Linear Temporal Logic (LTL) framework. Existing temporal logic control synthesis algorithms can be used to design correct-by-construction communication schedules that satisfy the considered LTL formula. Nevertheless, such approaches are centralized and scale poorly with the size of the network. We propose a hierarchical LTL-based algorithm that designs communication schedules that determine which agents should communicate while maximizing network usage. We show that the proposed algorithm is complete and demonstrate its efficiency and scalability through analysis and numerical experiments.