Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking.

Synchronisation is an emergent phenomenon observable in nature. Natural synchronising systems have inspired the development of protocols for achieving coordination in a diverse range of distributed dynamic systems. Spontaneously synchronising systems can be mathematically modelled as coupled oscillators. In this paper we present a novel approach using model checking to reason about achieving synchrony for different models of synchronisation. We describe a general, formal population model where oscillators interact at discrete moments in time, and whose cycles are sequences of discrete states. Using the probabilistic model checker Prism, we investigate the influence of various parameters of the model on the likelihood of, and time required for, achieving synchronisation.