nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

01.08.2015 | SMC

Analysing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking

verfasst von: Paolo Ballarini

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 4/2015

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

The application of formal methods to the analysis of stochastic oscillators has been at the focus of several research works in recent times. In this paper, we provide insights on the application of an expressive temporal logic formalism, namely the hybrid automata stochastic logic (HASL), to that issue. We show how one can take advantage of the expressive power of the HASL logic to define and assess relevant characteristics of (stochastic) oscillators.

Vorheriger Artikel Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains

Nächster Artikel Statistical model checking for biological applications

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

Nur mit Berechtigung zugänglich

As opposed to numerical stochastic model checking which requires the complete construction of a model’s state-space to assess the exact value of the target measure.

Hence, in essence, a DESP corresponds to a generalised semi-Markov processes [2, 14].

GSPN with timed transitions associated to generic probability distributions, that is, not necessarily Negative Exponential as with the standard GSPN definition [1].

Notice that because of the “initial-nondeterminism” of LHA there can be at most one initial state for the product process.

Notice that because of the determinism constraints of the LHA edges (conditions c2 and c3) at most only one autonomous or synchronised edge can ever be enabled in any location of the LHA.

Otherwise PDF/CDF measures can be encoded explicitly in an LHA but such encoding would usually result in a rather complex LHA.

Cosmos is an acronym of the French sentence “Concept et Outils Statistiques pour le MOdèles Stochastiques” whose English translation would sound like: “Tools and Concepts for Statistical analysis of stochastic models”.

Note that the duration of the \(k\)th period of a trace is, in turn, dependent on the random variables \(x_{j \downarrow }\), \(x_{j \uparrow }\) corresponding to the entering of the \(low\), \(high\) regions.

Although the LHA in Fig. 4 is designed so that periods detection starts from \(low\) it can be easily adapted so that the identification starts from any location.

with a slight abuse of notation we refer to \(Lmin[]\) and \(Lmax[]\) as arrays whereas in reality within COSMOS/HASL they correspond to a set of variables \(Lmin_i\), \(Lmax_j\), each of which is associated to a given level of the observed population, thus \(Lmin_1\) counts the frequency of observed minimum at value 1, \(Lmin_2\) the observed minima at value 2 and so on. The number of required \(Lmin_i\), \(Lmax_j\) variables, which is potentially infinite, can be actually bounded without loss of precision to a sufficiently large value \(Lmin_m\) (resp. \(Lmax_m\)) which must be established manually beforehand, for example by observing few previously generated traces.

Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley, London (1995)MATH

Alur, R., Courcoubetis, C., Dill, D.: Model-checking for probabilistic real-time systems. In: ICALP’91, LNCS 510 (1991)

Andrei, O., Calder, M.: Trend-based analysis of a population model of the akap scaffold protein. Trans. Compt. Syst. Biol. 14, 1–25 (2012)CrossRef

Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for CTMCs. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)

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 8th international conference on quantitative evaluation of systems (QEST’11), pp. 143–144. IEEE Computer Society Press (2011)

Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: an expressive language for statistical verification of stochastic models. In: Proceedings of Valuetools (2011)

Ballarini, P., Guerriero, M.: Query-based verification of qualitative trends and oscillations in biochemical systems. Theor. Comput. Sci. 411(20), 2019–2036 (2010)MathSciNetCrossRef

Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: Uppaal-SMC: statistical model checking for priced timed automata. In: Proceedings 10th workshop on quantitative aspects of programming languages and systems, volume 85 of EPTCS, pp. 1–16 (2012)

Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of CTMC against timed automata specifications. In: Proceedings of LICS’09 (2009)

10.

CosyVerif home page. http://www.cosyverif.org

11.

Cosmos home page. http://www.lsv.ens-cachan.fr/software/cosmos/

12.

David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Runtime verification of biological systems. ISoLA 1, 388–404 (2012)

13.

Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with \(CSL^{TA}\). IEEE Trans. Softw. Eng., 35, 224–240 (2009)

14.

Glynn, P.W.: On the role of generalized semi-Markov processes in simulation output analysis. In: Proceedings of conference winter simulation (1983)

15.

Herault, T., Lassaigne, R., Peyronnet, S.: APMC 3.0: Approximate verification of discrete and continuous time Markov chains. In: Proceedings of QEST’06 (2006)

16.

Ihekwaba, A., Sedwards, S.: Communicating oscillatory networks: frequency domain analysis. BMC Syst. Biol. 5(1), 203 (2011)CrossRef

17.

Jégourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking-plasma. In: TACAS, Volume 7214 of Lecture Notes in Computer Science, pp. 498–503 (2012)

18.

Júlvez, J., Kwiatkowska, M., Norman, G., Parker, D.: Evaluation of sustained stochastic oscillations by means of a system of differential equations. Int. J. Comput Appl. (IJCA) 19(2), 101–111 (2012)

19.

Katoen, J.P., Zapreev, I.S.: Simulation-based CTMC model checking: an empirical evaluation. In: Proceedings of QEST’09 (2009)

20.

Knuth, D.E.: The Art of Computer Programming, Volume 2 (3rd Ed.): Seminumerical Algorithms. Addison-Wesley Longman Publishing Co., Inc, Boston (1997)

21.

Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation, volume 4486 of LNCS, pp. 220–270, Springer, Berlin (2007)

22.

Prism home page. http://www.prismmodelchecker.org

23.

Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: Proceedings of QEST’05 (2005)

24.

Spieler, D. : Model checking of oscillatory and noisy periodic behavior in markovian population models. Master’s thesis, Saarland University (2009)

25.

Spieler, D.: Characterizing oscillatory and noisy periodic behavior in markov population models. In: Proceedings of QEST’13 (2013)

26.

Vilar, J., Kueh, H.-Y., Barkai, N., Leibler, S.: Mechanisms of noise-resistance in genetic oscillators. Proc. Natl. Acad. Sci. USA 99(9), 5988–5992 (2002)CrossRef

27.

Ymer, H.L. Younes.: A statistical model checker. In: Computer Aided Verification, pp. 429–433, Springer, Berlin (2005)

Titel: Analysing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking
verfasst von: Paolo Ballarini
Publikationsdatum: 01.08.2015
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 4/2015
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-015-0370-5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 4/2015

Modelling and statistical model checking of a microgrid

Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains

Statistical model checking: challenges and perspectives

Smart sampling for lightweight verification of Markov decision processes

Statistical model checking for biological applications

Approximate planning and verification for large Markov decision processes