First, the correctness of the local plan for each source robot is guaranteed by the model-checking algorithm, see [1]}, [2]}.
Moreover, since all local tasks are independent, these local plans can be executed independently. Thus we need to show that the plan can be executed successfully by each source robot, i.e., the data-gathering actions can be performed and the data buffer never overflows.
Initially, each source robot is confirmed to meet with one relay robot by (REF ).
When the two robots meet, the stored data can be transferred and uploaded, before the source robot's buffer overflows due to the formulation of (REF ).
Then execution of the meeting events above ensures that every source robot always waits to meet a relay robot and transfer the stored data before performing the next gathering action that leads to buffer overflow.
Similarly, the spontaneous meeting events described in Section REF  ensure that all data-gathering actions up to the next meeting time can be performed and the data buffer never overflows. The same procedure repeats itself and holds for all source robots.
