Skip to main content
Top

2018 | OriginalPaper | Chapter

Accelerated Model Checking of Parametric Markov Chains

Authors : Paul Gainer, Ernst Moritz Hahn, Sven Schewe

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal settings for a parameter; they can be used to visualise the influence of system parameters; and they can be used to make it easy to adjust the analysis for the case that parameters change. Unfortunately, these advancements come at a cost: parametric model checking is—or rather was—often slow. To make the analysis of parametric Markov models scale, we need three ingredients: clever algorithms, the right data structure, and good engineering. Clever algorithms are often the main (or sole) selling point; and we face the trouble that this paper focuses on – the latter ingredients to efficient model checking. Consequently, our easiest claim to fame is in the speed-up we have often realised when comparing to the state of the art.

To get access to this content you need the following product:

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!

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!

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!

Footnotes
4
We obtain the probablities and expected rewards as functions of the parameters. This can be visualised, just as we have visualised this in Sect. 5.
 
Literature
3.
go back to reference Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. CACM 55(9), 69–77 (2012)CrossRef Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. CACM 55(9), 69–77 (2012)CrossRef
4.
go back to reference Cox, D.R.: Renewal Theory. Methuen & Co., Ltd, London (1967) Cox, D.R.: Renewal Theory. Methuen & Co., Ltd, London (1967)
9.
go back to reference DeMillo, R.A., Lipton, R.J.: A probabilistic remark on algebraic program testing. Inf. Process. Lett. 7, 193–195 (1978)CrossRef DeMillo, R.A., Lipton, R.J.: A probabilistic remark on algebraic program testing. Inf. Process. Lett. 7, 193–195 (1978)CrossRef
10.
go back to reference von Essen, C., Jobstmann, B.: Synthesizing systems with optimal average-case behavior for ratio objectives. In: iWIGP, pp. 17–32 (2011) von Essen, C., Jobstmann, B.: Synthesizing systems with optimal average-case behavior for ratio objectives. In: iWIGP, pp. 17–32 (2011)
11.
go back to reference Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: ICSE, pp. 341–350. ACM (2011) Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: ICSE, pp. 341–350. ACM (2011)
12.
13.
go back to reference Gainer, P., Linker, S., Dixon, C., Hustadt, U., Fisher, M.: The power of synchronisation: formal analysis of power consumption in networks of pulse-coupled oscillators. arXiv preprint arXiv:1709.04385 (2017) Gainer, P., Linker, S., Dixon, C., Hustadt, U., Fisher, M.: The power of synchronisation: formal analysis of power consumption in networks of pulse-coupled oscillators. arXiv preprint arXiv:​1709.​04385 (2017)
16.
go back to reference Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3–19 (2011)CrossRef Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3–19 (2011)CrossRef
18.
go back to reference Han, Y.S.: State elimination heuristics for short regular expressions. FI 128(4), 445–462 (2013) Han, Y.S.: State elimination heuristics for short regular expressions. FI 128(4), 445–462 (2013)
19.
go back to reference Han, Y.S., Wood, D.: Obtaining shorter regular expressions from finite-state automata. TCS 370(1–3), 110–120 (2007)MathSciNetCrossRef Han, Y.S., Wood, D.: Obtaining shorter regular expressions from finite-state automata. TCS 370(1–3), 110–120 (2007)MathSciNetCrossRef
20.
go back to reference Harbron, C.: Heuristic algorithms for finding inexpensive elimination schemes. SC 5(4), 275–287 (1995)CrossRef Harbron, C.: Heuristic algorithms for finding inexpensive elimination schemes. SC 5(4), 275–287 (1995)CrossRef
21.
go back to reference Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: TYPES, pp. 127–165. Springer, Berlin (1993) Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: TYPES, pp. 127–165. Springer, Berlin (1993)
22.
go back to reference Hopcroft, J.E.: Introduction to Automata Theory, Languages, and Computation. Pearson Education India (2008) Hopcroft, J.E.: Introduction to Automata Theory, Languages, and Computation. Pearson Education India (2008)
23.
go back to reference Ibe, O.C., Trivedi, K.S.: Stochastic Petri net models of polling systems. J-SAC 8(9), 1649–1657 (1990) Ibe, O.C., Trivedi, K.S.: Stochastic Petri net models of polling systems. J-SAC 8(9), 1649–1657 (1990)
24.
go back to reference Knuth, D., Yao, A.: The complexity of nonuniform random number generation. Algorithms and Complexity: New Directions and Recent Results. Academic Press, Orlando (1976) Knuth, D., Yao, A.: The complexity of nonuniform random number generation. Algorithms and Complexity: New Directions and Recent Results. Academic Press, Orlando (1976)
28.
go back to reference Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. TISSEC 1(1), 66–92 (1998)CrossRef Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. TISSEC 1(1), 66–92 (1998)CrossRef
29.
go back to reference Schwartz, J.T.: Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27(4), 701–717 (1980)MathSciNetCrossRef Schwartz, J.T.: Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27(4), 701–717 (1980)MathSciNetCrossRef
Metadata
Title
Accelerated Model Checking of Parametric Markov Chains
Authors
Paul Gainer
Ernst Moritz Hahn
Sven Schewe
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_18

Premium Partner