Research Training Group SCARE

Investigating Parametric Influence for Discrete Synchronisation Protocols using Quantitative Model Checking

Dr. Sven Linker


Synchronisation is an emergent phenomenon observable throughout nature. The canonical example is that of thousands of fireflies synchronising their flashes to improve their chances of attracting a mate. The flashing of fireflies, and other natural synchronising systems, has inspired the development of protocols for achieving synchrony in a diverse range of artificial systems. These spontaneously synchronising systems can be mathematically modelled as coupled oscillators. Many formal studies have been conducted to analyse the emergence of synchrony in networks of coupled oscillators, and to identify sufficient conditions under which synchrony occurs. Nearly all of these studies use a continuous model of time, a continuous oscillation cycle, or both. In this talk we present a general, formal and discrete oscillator model. That is, we reason about synchrony in oscillators that interact at discrete moments time and whose cycles are defined as a sequence of discrete states. Our aim is to derive sensible parameters for achieving synchronisation of instantiations of our model. To that end, we employ the probabilistic model checker Prism to analyse reachability, and other quantitative properties. To alleviate state space explosion we use a population based model.