The above framework has also been applied to multi-robot systems either in a top-down approach where a global LTL task formula is assigned to the whole team of robots [1]}, [2]}, [3]}, [4]}, or in a bottom-up manner where an individual LTL task formula is assigned locally to each robot [5]}, [6]}.
Here, we favor the latter formalism as it provides a more natural framework to model independent temporal tasks within large teams of robots that have heterogeneous capabilities.
Specifically, we consider two types of robots: source robots that are assigned local tasks to gather different types of data in different regions in the workspace, and relay robots that receive data from source robots and upload them directly to a data center.
All robots have a limited buffer to store the data. Thus the data gathered by source robots should be transferred to relay robots before the buffers overflow.
Moreover, all robots have a limited communication range, so that they can only communicate when they are sufficiently close to each other.
