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:
Analysis of Markov Decision Processes Under Parameter Uncertainty Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Analysis of Timed Properties Using the Jump-Diffusion Approximation

verfasst von : Paolo Ballarini, Marco Beccuti, Enrico Bibbona, Andras Horvath, Roberta Sirovich, Jeremy Sproston

Erschienen in: Computer Performance Engineering

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Density dependent Markov chains (DDMCs) describe the interaction of groups of identical objects. In case of large numbers of objects a DDMC can be approximated efficiently by means of either a set of ordinary differential equations (ODEs) or by a set of stochastic differential equations (SDEs). While with the ODE approximation the chain stochasticity is not maintained, the SDE approximation, also known as the diffusion approximation, can capture specific stochastic phenomena (e.g., bi-modality) and has also better convergence characteristics. In this paper we introduce a method for assessing temporal properties, specified in terms of a timed automaton, of a DDMC through a jump diffusion approximation. The added value is in terms of runtime: the costly simulation of a very large DDMC model can be replaced through much faster simulation of the corresponding jump diffusion model. We show the efficacy of the framework through the analysis of a biological oscillator.

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 Delay Analysis of Resequencing Buffer in Markov Environment with HOQ-FIFO-LIFO Policy
Nächstes Kapitel Stability Analysis of a Multiclass Retrial System with Coupled Orbit Queues
Fußnoten
1
I.e., for \(N=1\) we assumed the discrete initial populations and reaction intensities being equal to the continuous ones as given in [15], note that this is in agreement with a cell volume \(V=10^9/n_A\) where \(n_A\) is the Avogadro number given that species concentrations and kinetic rate constants of the ODE model are expressed in nM.
 
2
Notice that zero-order and second-order reactions’ rates are dependent on N because for these conversion from continuous to discrete rates depends on cell’s volume.
 
3
\(\mathbf {L}\) and \(\mathbf {H}\), where \(\mathbf {L}\!<\!\mathbf {H}\), are two thresholds chosen so that the minimal, resp. maximal, peaks of oscillation are most likely to fall below \(\mathbf {L}\), resp. above \(\mathbf {H}\).
 
4
I.e., we use the DTA in Fig. 3 but without the \(T_ min \le x \le T_ max \) conjunct on the edge from low \(_3\)-mid \(_{\text {end}}\), which allows us to obtain the value of the clock x at the moment of reaching the final location of this modified DTA: this value gives the length of the first non-spurious oscillation period.
 
5
Observe that the dimension of integration step is dynamically computed through a heuristic function which provides a good trade-off between speed-up and precision of the solution.
 
Literatur
1.
2.
3.
Angius, A., Balbo, G., Beccuti, M., Bibbona, E., Horvath, A., Sirovich, R.: Approximate analysis of biological systems by hybrid switching jump diffusion. Theor. Comput. Sci. 587, 49–72 (2015)MathSciNetCrossRefMATH
4.
Ballarini, P.: Analysing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking. STTT 17(4), 505–526 (2015)CrossRef
5.
Ballarini, P., Barbot, B., Duflot, M., Haddad, S., Pekergin, N.: HASL: a new approach for performance evaluation and model checking from concepts to experimentation. Perform. Eval. 90, 53–77 (2015)CrossRef
6.
Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: Proceedings of the QEST 2011, pp. 143–144. IEEE Computer Society (2011)
7.
Beccuti, M., Bibbona, E., Horvath, A., Sirovich, R., Angius, A., Balbo, G.: Analysis of petri net models through stochastic differential equations. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 273–293. Springer, Cham (2014). doi:10.​1007/​978-3-319-07734-5_​15 CrossRef
8.
Bibbona, E., Sirovich, R.: Strong approximation of density dependent Markov chains on bounded domains by jump diffusion processes. Technical report, Università di Torino (2017)
9.
Bortolussi, L., Hillston, J.: Model checking single agent behaviours by fluid approximation. Inf. Comput. 242, 183–226 (2015)MathSciNetCrossRefMATH
10.
Bortolussi, L., Lanciani, R.: Model checking markov population models by central limit approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123–138. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40196-1_​9 CrossRef
11.
12.
Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Log. Meth. Comput. Sci. 7(1), 1–34 (2011)MathSciNetCrossRefMATH
13.
Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL\({^{\rm TA}}\). IEEE T. Software Eng. 35(2), 224–240 (2009)CrossRef
14.
Gressens, P., Steenwinckel, J.V., Schang, A., Sigaut, S., Degos, V., Lebon, S., Schwendimann, L., Le Charpentier, T., Hagberg, H., Soussi, N., Fleiss, B.: Microglial Wnt signaling inhibition promotes microglia activation and oligodendrocyte maturation blockade. J. Neurochem. 134, 122 (2015)
15.
Jensen, P.B., Pedersen, L., Krishna, S., Jensen, M.H.: A Wnt oscillator model for somitogenesis. Biophys. J. 98(6), 943–950 (2010)CrossRef
16.
Kolesnichenko, A., de Boer, P., Remke, A., Haverkort B.R.: A logic for model-checking mean-field models. In: Proceedings of the DSN 2013, pp. 1–12. IEEE Computer Society (2013)
17.
Kurtz, T.G.: Solutions of ordinary differential equations as limits of pure jump Markov processes. J. Appl. Probab. 1(7), 49–58 (1970)MathSciNetCrossRefMATH
18.
Kurtz, T.G.: Limit theorems and diffusion approximations for density dependent Markov chains. In: Wets, R.J.B. (ed.) Stochastic Systems: Modeling, Identification and Optimization, I, pp. 67–78. Springer, Heidelberg (1976)CrossRef
19.
20.
Mikeev, L., Neuhäußer, M.R., Spieler, D., Wolf, V.: On-the-fly verification and optimization of DTA-properties for large Markov chains. Form. Method. Syst. Des. 43(2), 313–337 (2013)CrossRefMATH
Metadaten
Titel
Analysis of Timed Properties Using the Jump-Diffusion Approximation
verfasst von
Paolo Ballarini
Marco Beccuti
Enrico Bibbona
Andras Horvath
Roberta Sirovich
Jeremy Sproston
Copyright-Jahr
2017
Buch
Computer Performance Engineering

Print ISBN: 978-3-319-66582-5

Electronic ISBN: 978-3-319-66583-2

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66583-2_5

Neuer Inhalt

    Bildnachweise