Note that the above solution has two serious drawbacks: first, it is computationally intractable for systems with large numbers of robots and complex tasks, due to the combinatorial size of composed system and the double-exponential complexity of the model-checking process [1]}. Second, the derived plan needs to be executed in a fully-synchronized way, meaning that the next transition can be taken only if all robots have completed their current transition. Not only does this introduce heavy communication overhead for synchronization but also this all-time synchronization may be infeasible due to limited communication range considered here. More numerical analyses can be found in Section .
