In this paper, we consider networks of mobile robots responsible for accomplishing tasks, captured by Linear Temporal Logic (LTL) formulas, while ensuring communication with all other robots in the network. The robots operate in complex environments represented by appropriate transition systems (TS). We propose an intermittent communication framework, which is based on a LTL statement that enforces the robots to meet and communicate at pre-determined points in the environment infinitely often. Our approach combines an existing model checking method with a novel technique that aims to reduce the state-space of the TS satisfying at the same time the LTL statement.
展开▼
