where \(S_{\texttt {a}}=(\Pi _1\times \mathcal {B}_1)\times (\Pi _2\times \mathcal {B}_2)\times \cdots (\Pi _N\times \mathcal {B}_N)\)  is the set of composed states and \(\mathcal {B}_i=\lbrace 0,1,\cdots ,\overline{B}_i\rbrace \) .
Namely, state \(s\in S_{\texttt {a}}\)  indicates the position and buffer size of each robot.
The transition relation \(\rightarrow _{\texttt {a}}\subset S_{\texttt {a}}\times S_{\texttt {a}}\)  is defined by \((s,\,s^{\prime })\in \rightarrow _{\texttt {a}}\)  where \(s=(\pi _1,b_1)\times \cdots (\pi _N,b_N)\)  and \(s^{\prime }=(\pi ^{\prime }_1,b^{\prime }_1)\times \cdots (\pi ^{\prime }_N,b^{\prime }_N)\)  if robot \(i\)  is allowed to transition from \(\pi _i\)  to \(\pi _i^{\prime }\) , and if the change in buffer size from \(b_i\)  to \(b_i^{\prime }\)  satisfies both the communication-range constraints and the buffer dynamics defined in (REF )-(REF ), \(\forall i\in \mathcal {N}\) . The initial state \(S_{\texttt {a},0}\in S_{\texttt {a}}\)  is given by the initial position and buffer size of the robots. The transition cost \(T_{\texttt {a}}:\rightarrow _{\texttt {a}}\rightarrow \mathbb {R}^+\)  measures the time that each transition takes. \(AP=\cup _{i\in \mathcal {N}^f}AP_i\)  is the set of propositions. Lastly, the labeling function \(L_{\texttt {a}}:S_{\texttt {a}} \rightarrow 2^{AP}\)  reflects the data-gathering actions that have been performed by the source robots at the regions of interest.
(ii) The conjunction of all source robots' local tasks is defined as \(\varphi _{\texttt {a}}=\bigwedge _{i\in \mathcal {N}^f} \varphi _i\) , and the corresponding NBA is derived as \(\mathcal {A}_{\varphi _{\texttt {a}}}\) , as described in Section . (iii) Standard model checking algorithms [1]} can be used to search for a lasso-shaped path of \(\mathcal {T}_{\texttt {a}}\)  that satisfies \(\varphi _{\texttt {a}}\) . These involve constructing the product automaton \(\mathcal {P}_{\texttt {a}}\)  between \(\mathcal {T}_{\texttt {a}}\)  and the NBA \(\mathcal {A}_{\varphi _{\texttt {a}}}\) .
To optimize the total plan cost both in the plan prefix and plan suffix, defined as the accumulated travel time, the synthesis algorithm from our earlier work [2]} can be used.
