Home > Research > Publications & Outputs > Investigating Parametric Influence on Discrete ...


Text available via DOI:

View graph of relations

Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNChapter (peer-reviewed)peer-review

  • Paul Gainer
  • Sven Linker
  • Clare Dixon
  • Ullrich Hustadt
  • Michael Fisher
Publication date5/09/2017
Host publicationQuantitative Evaluation of Systems: Proceedings of the 14th International Conference on Quantitative Evaluation of Systems, QEST 2017
EditorsNathalie Bertrand, Luca Bortolussi
Place of PublicationCham
Number of pages16
ISBN (Electronic)9783319663357
ISBN (Print)9783319663340
<mark>Original language</mark>English

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Synchronisation is an emergent phenomenon observable in nature. Natural synchronising systems have inspired the development of protocols for achieving coordination in a diverse range of distributed dynamic systems. Spontaneously synchronising systems can be mathematically modelled as coupled oscillators. In this paper we present a novel approach using model checking to reason about achieving synchrony for different models of synchronisation. We describe a general, formal population model where oscillators interact at discrete moments in time, and whose cycles are sequences of discrete states. Using the probabilistic model checker Prism, we investigate the influence of various parameters of the model on the likelihood of, and time required for, achieving synchronisation.