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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 2/2018

06.05.2017 | TACAS 2016

Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata

verfasst von: Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker, David Müller

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2018

Einloggen

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

search-config
loading …

Abstract

The popular model checker PRISM has been successfully used for the modeling and analysis of complex probabilistic systems. As one way to tackle the challenging state explosion problem, PRISM supports symbolic storage and manipulation using multi-terminal binary decision diagrams for representing the models and in the computations. However, it lacks automated heuristics for variable reordering, even though it is well known that the order of BDD variables plays a crucial role for compact representations and efficient computations. In this article, we present a collection of extensions to PRISM. First, we provide support for automatic variable reordering within the symbolic engines of PRISM and allow users to manually control the variable ordering at a fine-grained level. Second, we provide extensions in the realm of reward-bounded properties, namely symbolic computations of quantiles in Markov decision processes and, for both the explicit and symbolic engines, the approximative computation of quantiles for continuous-time Markov chains as well as support for multi-reward-bounded properties. Finally, we provide an implementation for obtaining minimal weak deterministic Büchi automata for the obligation fragment of linear temporal logic (LTL), with applications for expected accumulated reward computations with a finite horizon given by a co-safe LTL formula.
Vorheriger Artikel Multi-core symbolic bisimulation minimisation
Nächster Artikel PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives

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
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
This article is an extended version of the TACAS’16 paper [31].
 
2
The depicted scheme corresponds to the default ordering for the Hybrid and Sparse engines. There are subtle differences when using the Mtbdd engine, discussed in Appendix A in supplementary material. Additionally, standard PRISM preallocates only extra state variables, mainly for the product with deterministic automata. To support generic symbolic model transformations, we also preallocate choice variables, i.e., for fresh actions in the transformed MDP.
 
3
The benchmarks for reordering were carried out on a machine with two Intel Xeon L5630 4-core CPUs at 2.13GHz and 192GB RAM, with a timeout of 1 h and a CUDD memory limit of 10GB. The max-growth factor of CUDD was set to 2, i.e., allowing a doubling in MTBDD size before sifting is abandoned.
 
4
As the quantile algorithm for reward-bounded path formulas in the symbolic engines is currently only implemented for MDPs, reward-bounded reachability computations for DTMCs convert all reward bounds into counters in the state space.
 
5
As demonstrated in [26], the termination criterion for detecting convergence in the iterative numerical computations used by all engines of PRISM and by other probabilistic model checkers can lead to imprecise results for certain models. This is due to the convergence check succeeding before the overall result has converged with a sufficient precision. In the quantile calculations, we currently follow the standard PRISM approach. In separate work, we are currently working on an implementation of the fix proposed in [26]. As the relevant parts of the quantile computations are similar, those can then be adapted easily as well.
 
6
The benchmarks for the quantile computations were carried out on a machine with two Intel E5-2680 8-core CPUs at 2.70 GHz with 384GB of RAM running Linux.
 
7
Comparing with the experiments for eServer presented in [31], our Mtbdd implementation for quantile computations features an improved handling of the zero-reward fragment of the MDP, which more than halved the query times.
 
Literatur
1.
Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Proceedings of Formal Modeling and Analysis of Timed Systems (FORMATS’03), volume 2791 of LNCS, pp. 88–104. Springer, (2003)
2.
Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Form. Methods Syst. Des. 10(2/3), 171–206 (1997)CrossRef
3.
Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: Proceedings of International Colloquium on Automata, Languages and Programming (ICALP’97), volume 1256 of LNCS, pp. 430–440, (1997)
4.
Baier, C., Daum, M., Dubslaff, C., Klein, J., Klüppelholz, S.: Energy-utility quantiles. In: Proceedings of NASA Formal Methods (NFM’14), Volume 8430 of LNCS, pp. 285–299. Springer (2014)
5.
Baier, C., Dubslaff, C., Klein, J., Klüppelholz, S., Wunderlich, S.: Probabilistic model checking for energy-utility analysis. In: Horizons of the Mind. A Tribute to Prakash Panangaden-Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, Volume 8464 of LNCS, pp. 96–123. Springer (2014)
6.
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the logical characterisation of performability properties. In: Proceedings of International Colloquium on Automata, Languages and Programming (ICALP’00), Volume 1853 of LNCS, pp. 780–792. Springer, (2000)
7.
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)CrossRefMATH
8.
Baier, C., Kiefer, S., Klein, J., Klüppelholz, S., Müller, D., Worrell, J.: Markov chains and unambiguous Büchi automata. In: Proceedings of Computer Aided Verification (CAV’16), Part I, volume 9779 of LNCS, pp. 23–42. Springer, (2016)
9.
Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. Math. Theory Autom. 12, 529–561 (1963)MathSciNetMATH
10.
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10\(^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)MathSciNetCrossRefMATH
11.
Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: Family-based modeling and analysis for probabilistic systems-featuring ProFeat. In: Proceedings of Fundamental Approaches to Software Engineering (FASE’16), Volume 9633 of LNCS, pp. 287–304. Springer, (2016)
12.
Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. SIGMETRICS Perform. Eval. Rev. 36(4), 58–63 (2009)CrossRef
13.
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Proceedings of Computer Aided Verification (CAV’02), Volume 2404 of LNCS, pp. 359–364. Springer, (2002)
14.
Dax, C., Eisinger, J., Klaedtke, F.: Mechanizing the powerset construction for restricted classes of \(\omega \)-automata. In: Proceedings of Automated Technology for Verification and Analysis (ATVA’07), Volume 4762 of LNCS, pp. 223–236. Springer, (2007)
15.
Donaldson, A.F., Miller, A., Parker, D.: Language-level symmetry reduction for probabilistic model checking. In: Proceedings of Quantitative Evaluation of Systems (QEST’09), pp. 289–298. IEEE, (2009)
16.
Dubslaff, C., Baier, C., Klüppelholz, S.: Probabilistic model checking for feature-oriented systems. Trans. Aspect-Oriented Softw. Dev. 12, 180–220 (2015)
17.
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0—a framework for LTL and \(\omega \)-automata manipulation. In: Proceedings of Automated Technology for Verification and Analysis (ATVA’16), Volume 9938 of LNCS, pp. 122–129. Springer, (2016)
18.
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of International Conference on Software Engineering (ICSE’99), pp. 411–420. ACM, (1999)
19.
Esparza, J., Kretínský, J.: From LTL to deterministic automata: a Safraless compositional approach. In: Proceedings of Computer Aided Verification (CAV’14), Volume 8559 of LNCS, pp. 192–208. Springer, (2014)
20.
Etessami, K., Holzmann, G.: Optimizing Büchi automata. In: Proceedings of International Conference on Concurrency Theory (CONCUR’00), Volume 1877 of Lecture Notes in Computer Science, pp. 153–167, (2000)
21.
Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Proceedings of School on Formal Methods for the Design of Computer, Communication and Software Systems, Formal Methods for Eternal Networked Software Systems (SFM’11), Volume 6659 of LNCS, pp. 53–113. Springer, (2011)
22.
Fujita, M., McGeer, P.C., Yang, J.C.-Y.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form. Methods Syst. Des. 10(2/3), 149–169 (1997)CrossRef
23.
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, Volume of 2500 of LNCS. Springer, Berlin (2002)
24.
Haase, C., Kiefer, S.: The odds of staying on budget. In: Proceedings of Automata, Languages, and Programming (ICALP’15), Volume 9135 of LNCS, pp. 234–246. Springer, (2015)
25.
Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Markovian analysis of large finite state machines. IEEE Trans. CAD Integr. Circuits Syst. 15(12), 1479–1493 (1996)CrossRef
26.
Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: Proceedings of International Workshop on Reachability Problems (RP’14), Volume 8762 of LNCS, pp. 125–137. Springer, (2014)
27.
Hartonas-Garmhausen, V., Campos, S.V.A., Clarke, E.M.: ProbVerus: probabilistic symbolic model checking. In: Proceedings of Formal Methods for Real-Time and Probabilistic Systems (ARTS’99), Volume 1601 of LNCS, pp. 96–110, (1999)
28.
Heiner, M., Rohr, C., Schwarick, M., Tovchigrechko, A.A.: MARCIE’s secrets of efficient model checking. Trans. Petri Nets Other Models Concurr. 11, 286–296 (2016)MathSciNet
29.
Hermanns, H., Kwiatkowska, M.Z., Norman, G., Parker, D., Siegle, M.: On the use of MTBDDs for performability analysis and verification of stochastic systems. J. Log. Algebraic Program 56(1–2), 23–67 (2003)MathSciNetCrossRefMATH
30.
Klein, J., Baier, C.: Experiments with deterministic \(\omega \)-automata for formulas of linear temporal logic. Theoret. Comput. Sci. 363(2), 182–195 (2006)MathSciNetCrossRefMATH
31.
Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Klüppelholz, S., Märcker, S., Müller, D.: Advances in symbolic probabilistic model checking with PRISM. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16), Volume 9636 of LNCS, pp. 349–366. Springer, (2016)
32.
Komárková, Z., Kretínský, J.: Rabinizer 3: Safraless translation of LTL to small deterministic automata. In: Proceedings of Automated Technology for Verification and Analysis (ATVA’14), Volume 8837 of LNCS, pp. 235–241. Springer, (2014)
33.
Kuntz, M., Siegle, M.: CASPA: symbolic model checking of stochastic systems. In: Proceedings of Measuring, Modelling and Evaluation of Computer and Communication Systems (MMB’06), pp. 465–468. VDE Verlag, (2006)
34.
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19(3), 291–314 (2001)CrossRefMATH
35.
Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. Softw. Tools Technol. Transf. 6(2), 128–142 (2004)CrossRefMATH
36.
Kwiatkowska, M.Z., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Proceedings of Computer Aided Verification (CAV’06), Volume 4144 of LNCS, pp. 234–248. Springer, (2006)
37.
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Proceedings of Computer Aided Verification (CAV’11), Volume 6806 of LNCS, pp. 585–591. Springer, (2011)
38.
39.
Lacerda, B., Parker, D., Hawes, N.: Optimal and dynamic planning for Markov decision processes with co-safe LTL specifications. In: Proceedings of Conference on Intelligent Robots and Systems (IROS’14), pp. 1511–1516. IEEE, (2014)
40.
Lampka, K.: A symbolic approach to the state graph based analysis of high-level Markov reward models. PhD thesis, Universität Erlangen-Nürnberg, (2007)
41.
Löding, C.: Efficient minimization of deterministic weak omega-automata. Inf. Process. Lett. 79(3), 105–109 (2001)CrossRefMATH
42.
43.
McMillan, K.L., Symbolic Model Checking. Kluwer Academic Publishers, Boston, USA (1993)
44.
Meijer, J., van de Pol, J.: Bandwidth and wavefront reduction for static variable ordering in symbolic reachability analysis. In: Proceedings of NASA Formal Methods (NFM’16), Volume 9690 of LNCS, pp. 255–271. Springer, (2016)
45.
Miner, A.S., Parker, D.: Symbolic representations and analysis of large probabilistic systems. In: Validation of Stochastic Systems-A Guide to Current Research, Volume 2925 of LNCS, pp. 296–338, (2004)
46.
Panda, S., Somenzi, F.: Who are the variables in your neighborhood. In: Proceedings of Computer-Aided Design (ICCAD’95), pp. 74–77. IEEE, (1995)
47.
Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham, (2002)
48.
49.
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of Computer-Aided Design (ICCAD’93), pp. 42–47. IEEE, (1993)
50.
Schwarick, M., Heiner, M.: CSL model checking of biochemical networks with interval decision diagrams. In: Proceedings of Computational Methods in Systems Biology (CMSB’09), Volume 5688 of LNCS, pp. 296–312. Springer, (2009)
51.
Sickert, S., Esparza, J., Jaax, S., Kretínský, J.: Limit-deterministic Büchi automata for linear temporal logic. In: Proceedings of Computer Aided Verification (CAV’16), Part II, Volume 9780 of LNCS, pp. 312–332. Springer, (2016)
52.
53.
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Proceedings of Computer Aided Verification (CAV’00), Volume 1855 of Lecture Notes in Computer Science, pp. 248–263. Springer, (2000)
54.
Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6:1–6:45 (2014)CrossRef
55.
Ummels, M., Baier, C.: Computing quantiles in Markov reward models. In: Proceedings of Foundations of Software Science and Computation Structures (FOSSACS’13), Volume 7794 of LNCS, pp. 353–368. Springer, (2013)
56.
Vardi, M.Y.: Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In: Proceedings of AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems (ARTS’99), Volume 1601 of LNCS, pp. 265–276. Springer, (1999)
Metadaten
Titel
Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata
verfasst von
Joachim Klein
Christel Baier
Philipp Chrszon
Marcus Daum
Clemens Dubslaff
Sascha Klüppelholz
Steffen Märcker
David Müller
Publikationsdatum
06.05.2017
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 2/2018
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-017-0456-3

Weitere Artikel der Ausgabe 2/2018

International Journal on Software Tools for Technology Transfer 2/2018 Zur Ausgabe

Regular Paper

Automated translation of VDM to JML-annotated Java

TACAS 2016

PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives

TACAS 2016

Multi-core symbolic bisimulation minimisation

TACAS 2016

Coqoon

TACAS 2016

The Tinker tool for graphical tactic development

Introduction

Recent advances in interactive and automated analysis

Premium Partner

    Bildnachweise