Detecting synchronisation of biological oscillators by model checking

We define a subclass of timed automata, called oscillator timed automata, suitable to model biological oscillators. Coupled biological oscillators may synchronise, as emerging behaviour, after a period of time in which they interact through physical or chemical means. We introduce a parametric semantics for their interaction that is general enough to capture the behaviour of different types of oscillators. We instantiate it both to the Kuramoto model, a model of synchronisation based on smooth interaction, and to the Peskin model of pacemaker cells in the heart, a model of synchronisation based on pulse interaction. We also introduce a logic, Biological Oscillators Synchronisation Logic (BOSL), that is able to describe collective synchronisation properties of a population of coupled oscillators. A model checking algorithm is proposed for the defined logic and it is implemented in a model checker. The model checker can be used to detect synchronisation properties of a given populati...

• Type: Journal
• Year: 2010
• Where: TCS
• Authors: Ezio Bartocci, Flavio Corradini, Emanuela Merelli, Luca Tesei
• Keywords: Biological Oscillators, Model, Oscillators, TCS 2010, Theoretical Computer Science