Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking



Gainer, Paul, Linker, Sven ORCID: 0000-0003-2913-7943, Dixon, Clare ORCID: 0000-0002-4610-9533, Hustadt, Ullrich ORCID: 0000-0002-0455-0267 and Fisher, Michael
(2017) Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking. In: 14th International Conference on Quantitative Evaluation of SysTems (QEST), 2017-9-5 - 2017-9-7, Berlin, Germany.

[thumbnail of QEST17.pdf] Text
QEST17.pdf - Author Accepted Manuscript

Download (384kB)

Abstract

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.

Item Type: Conference or Workshop Item (Unspecified)
Uncontrolled Keywords: Probabilistic Model Checker PRISM, Broadcast Failure, Failure Vector, Probabilistic Computation Tree Logic (PCTL), Short Synchronization Time
Depositing User: Symplectic Admin
Date Deposited: 06 Jul 2017 13:09
Last Modified: 19 Jan 2023 07:00
DOI: 10.1007/978-3-319-66335-7_14
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3008343