Synchronization Modulo k in Dynamic Networks

We define the modk -synchronization problem as a weakening of the Firing Squad problem, where all nodes fire not at the same round, but at rounds that are all equal modulo k. We propose an algorithm that achieves modk -synchronization in any dynamic network where there exist – possibly several – fixed spanning stars within each period of Δ consecutive rounds. In other words, we require that there always exists a temporal path of length at most Δ between some fixed node γ and every other node. As opposed to the perfect synchronization achieved in the Firing Squad problem, modk -synchronization thus does not require any strong connectivity property in the network. In our algorithm, all the nodes “know” Δ, but they ignore what nodes are the centers of the spanning stars. We also prove that if the bound Δ for guaranteeing fixed spanning stars exists but is unknown to the agents, then modk -synchronization is impossible. All nodes in our algorithm fire in less that 6 kn+ 4 k rounds after all nodes become active, but unfortunately uses unbounded counters. We then propose a refinement of this algorithm so that it becomes finite state while maintaining the same time complexity. The correctness of our first algorithm has been formally established in the proof assistant Isabelle.