The local plan of robot \(i\) , denoted by \(\tau _{i,\mathcal {R}}\) , is an infinite path of \(\mathcal {R}_i\)  whose trace satisfies its local task \(\varphi _i\) .
We rely on the automaton-based model checking algorithm [1]}, [2]} to synthesize \(\tau _{i,\mathcal {R}}\) , whose description we omit here due to limited space.
Particularly, the local plan \(\tau _{i,\mathcal {R}}\)  has the prefix-suffix structure below and the minimum total cost as the summation of prefix and suffix costs:
\(\tau _{i,\mathcal {R}} = \pi _{i,\mathcal {R}}^0\,\pi _{i,\mathcal {R}}^1 \cdots \pi _{i,\mathcal {R}}^{k_i-1}\, (\pi _{i,\mathcal {R}}^{k_i}\,\pi _{i,\mathcal {R}}^{k_i+1}\cdots \pi _{i,\mathcal {R}}^{K_i})^\omega ,\) 
