Affordable Access

Publisher Website

Model Checking Biological Oscillators

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
229
Issue
1
Identifiers
DOI: 10.1016/j.entcs.2009.02.004
Keywords
  • Spontaneous Synchronization
  • Kuramoto Model
  • Oscillator Timed Automata
  • Ksl
  • Model Checking
Disciplines
  • Biology
  • Computer Science
  • Linguistics

Abstract

Abstract We define a subclass of timed automata, called oscillator timed automata, suitable to model biological oscillators. The semantics of their interactions, parametric w.r.t. a model of synchronization, is introduced. We apply it to the Kuramoto model. Then, we introduce a logic, Kuramoto Synchronization Logic (KSL), and a model checking algorithm in order to verify collective synchronization properties of a population of coupled oscillators.

There are no comments yet on this publication. Be the first to share your thoughts.