| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 422276 | Electronic Notes in Theoretical Computer Science | 2009 | 18 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
