Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Extending Parikh’s Theorem to Weighted and Probabilistic Context-Free Grammars Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking

verfasst von : Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher

Erschienen in: Quantitative Evaluation of Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes
Nächstes Kapitel Statistical Abstraction for Multi-scale Spatio-Temporal Systems
Fußnoten
1
The model generation script and the results presented in this paper can be found at https://​github.​com/​PaulGainer/​mc-bio-synch.
 
Literatur
1.
2.
Amin, S., Elahi, A., Saghar, K., Mehmood, F.: Formal modelling and verification approach for improving probabilistic behaviour of robot swarms. In: Proceedings of IBCAST 2017, pp. 392–400. IEEE (2017)
3.
Bartocci, E., Corradini, F., Merelli, E., Tesei, L.: Detecting synchronisation of biological oscillators by model checking. TCS 411(20), 1999–2018 (2010)MathSciNetCrossRefMATH
4.
Bojic, I., Podobnik, V., Ljubi, I., Jezic, G., Kusek, M.: A self-optimizing mobile network: auto-tuning the network with firefly-synchronized agents. Inf. Sci. 182(1), 77–92 (2012)CrossRef
5.
Breza, M.: Bio-inspired tools for a distributed wireless sensor network operating system. Ph.D. thesis, Imperial College London, March 2013
6.
Buck, J.: Synchronous rhythmic flashing of fireflies. II. Q. Rev. Biol. 63(3), 265–289 (1988)CrossRef
7.
Bucur, D., Kwiatkowska, M.: On software verification for sensor nodes. J. Syst. Softw. 84(10), 1693–1707 (2011)CrossRef
8.
Christensen, A.L., Grady, R.O., Dorigo, M.: From fireflies to fault-tolerant swarms of robots. IEEE Trans. Evol. Comput. 13(4), 754–766 (2009)CrossRef
9.
Degesys, J., Basu, P., Redi, J.: Synchronization of strongly pulse-coupled oscillators with refractory periods and random medium access. In: Proceedings of SAC 2008, pp. 1976–1980. ACM (2008)
10.
11.
Gainer, P., Dixon, C., Hustadt, U.: Probabilistic model checking of ant-based positionless swarming. In: Alboul, L., Damian, D., Aitken, J.M.M. (eds.) TAROS 2016. LNCS (LNAI), vol. 9716, pp. 127–138. Springer, Cham (2016). doi:10.​1007/​978-3-319-40379-3_​13
12.
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. FAC 6(5), 512–535 (1994)MATH
13.
Heidarian, F., Schmaltz, J., Vaandrager, F.: Analysis of a clock synchronization protocol for wireless sensor networks. TCS 413(1), 87–105 (2012)MathSciNetCrossRefMATH
14.
Konur, S., Dixon, C., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robot. Auton. Syst. 60(2), 199–213 (2012)CrossRef
15.
Kuramoto, Y.: Collective synchronization of pulse-coupled oscillators and excitable units. Physica D: Nonlin. Phenom. 50(1), 15–30 (1991)CrossRefMATH
16.
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​47 CrossRef
17.
Mirollo, R.E., Strogatz, S.H.: Synchronization of pulse-coupled biological oscillators. SIAM J. App. Math. 50(6), 1645–1662 (1990)MathSciNetCrossRefMATH
18.
Perez-Diaz, F., Trenkwalder, S., Zillmer, R., Gross, R.: Emergence and inhibition of synchronization in robot swarms. In: DARS 2016. Springer Tracts in Advanced Robotics. Springer, Cham (in press)
19.
Werner-Allen, G., Tewari, G., Patel, A., Welsh, M., Nagpal, R.: Firefly-inspired sensor network synchronicity with realistic radio effects. In: Proceedings of SenSys 2005, pp. 142–153. ACM (2005)
Metadaten
Titel
Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking
verfasst von
Paul Gainer
Sven Linker
Clare Dixon
Ullrich Hustadt
Michael Fisher
Copyright-Jahr
2017
Buch
Quantitative Evaluation of Systems

Print ISBN: 978-3-319-66334-0

Electronic ISBN: 978-3-319-66335-7

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66335-7_14