Sciweavers

Share
TCS
2010

Detecting synchronisation of biological oscillators by model checking

9 years 2 months ago
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...
Ezio Bartocci, Flavio Corradini, Emanuela Merelli,
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where TCS
Authors Ezio Bartocci, Flavio Corradini, Emanuela Merelli, Luca Tesei
Comments (0)
books