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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
Titolo: | Model Checking Biological Oscillators | |
Autori: | ||
Data di pubblicazione: | 2009 | |
Rivista: | ||
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. | |
Handle: | http://hdl.handle.net/11581/115139 | |
Appare nelle tipologie: | Contributo in atto di convegno su rivista |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.