nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Bounded Model Checking for Probabilistic Programs

verfasst von : Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

In this paper we investigate the applicability of standard model checking approaches to verifying properties in probabilistic programming. As the operational model for a standard probabilistic program is a potentially infinite parametric Markov decision process, no direct adaption of existing techniques is possible. Therefore, we propose an on–the–fly approach where the operational model is successively created and verified via a step–wise execution of the program. This approach enables to take key features of many probabilistic programs into account: nondeterminism and conditioning. We discuss the restrictions and demonstrate the scalability on several benchmarks.

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 Parameter Synthesis for Markov Models: Faster Than Ever

Nächstes Kapitel How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?

Also referred to as adversaries, strategies, or policies.

We have tacitly overloaded the variable name x to an expectation here for readability. More formally, by the “expectation x” we actually mean the expectation \(\lambda \sigma . \sigma (x)\).

All input programs and log files of the experiments can be downloaded at moves.rwth-aachen.de/wp-content/uploads/conference_material/pgcl_atva16.tar.gz.

https://en.wikipedia.org/wiki/Coupon_collector%27s_problem.

Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE, pp. 167–181. ACM Press (2014)

Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI, pp. 447–458. ACM (2013)

Claret, G., Rajamani, S.K., Nori, A.V., Gordon, A.D., Borgström, J.: Bayesian inference using data flow analysis. In: ESEC/SIGSOFT FSE, pp. 92–102. ACM Press (2013)

Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110–132 (2014)CrossRef

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

Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Heidelberg (2014). doi:10.1007/978-3-319-06410-9_22 CrossRef

Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90–104 (2011)CrossRef

Kattenbelt, M.: Automated quantitative software verification. Ph.D. thesis, Oxford University (2011)

Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM J. Comput. 13(2), 292–314 (1984)MathSciNetCrossRefMATH

10.

Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338. IEEE Computer Society (1985)

11.

Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)MATH

12.

Baier, C., Klein, J., Klüppelholz, S., Märcker, S.: Computing conditional probabilities in Markovian models efficiently. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 515–530. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_43 CrossRef

13.

Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J., Ábrahám, E.: PROPhESY: a probabilistic parameter synthesis tool. In: Kroening, D., Pâsâreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214–231. Springer, Berlin (2015)CrossRef

14.

Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.: Parameter synthesis for Markov models: faster than ever. In: Nelson, S.P., Meyer, V. (eds.) ATVA 2016. LNCS, vol. 9938, pp. xx–yy. Springer, Heidelberg (2016). CoRR abs/1602.05113

15.

Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)MATH

16.

McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Berlin (2004)MATH

17.

Jansen, N., Kaminski, B.L., Katoen, J., Olmedo, F., Gretz, F., McIver, A.: Conditioning in probabilistic programming. Electr. Notes Theoret. Comput. Sci. 319, 199–216 (2015)MathSciNetCrossRef

18.

Kaminski, B.L., Katoen, J.-P.: On the hardness of almost–sure termination. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 307–318. Springer, Heidelberg (2015)CrossRef

19.

Dehnert, C., Jansen, N., Wimmer, R., Ábrahám, E., Katoen, J.-P.: Fast debugging of PRISM models. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 146–162. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11936-6_11

20.

Jansen, N., Dehnert, C., Kaminski, B.L., Katoen, J., Westhofen, L.: Bounded model checking for probabilistic programs. In: Nelson, S.P., Meyer, V. (eds.) ATVA 2016. LNCS, vol. 9938, pp. xx–yy. Springer, Heidelberg (2016). CoRR abs/1605.04477

21.

Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. ACM Trans. Inf. Syst. Secur. 1(1), 66–92 (1998)CrossRef

22.

Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63–67 (1990)MathSciNetCrossRefMATH

23.

Brauer, F., Castillo-Chavez, C.: Mathematical Models in Population Biology and Epidemiology. Texts in Applied Mathematics. Springer, New York (2001)CrossRefMATH

24.

Erds, P., Rnyi, A.: On a classical problem of probability theory. Publ. Math. Inst. Hung. Acad. Sci. Ser. A 6, 215–220 (1961)MathSciNet

25.

Olmedo, F., Kaminski, B., Katoen, J.P., Matheja, C.: Reasoning about recursive probabilistic programs. In: LICS (2016, to appear)

26.

Gretz, F., Katoen, J.-P., McIver, A.: Prinsys—on a quest for probabilistic loop invariants. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 193–208. Springer, Heidelberg (2013)CrossRef

27.

Kaminski, B.L., Katoen, J.-P., Matheja, C.: Inferring covariances for probabilistic programs. In: Agha, G., Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 191–206. Springer, Heidelberg (2016). doi:10.1007/978-3-319-43425-4_14 CrossRef

28.

Ábrahám, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.-P., Wimmer, R.: Counterexample generation for discrete-time Markov models: an introductory survey. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 65–121. Springer, Heidelberg (2014). doi:10.1007/978-3-319-07317-0_3 CrossRef

29.

Wimmer, R., Jansen, N., Abraham, E., Katoen, J.P.: High-level counterexamples for probabilistic automata. Log. Methods Comput. Sci. 11, 1–15 (2015)MathSciNetCrossRefMATH

30.

Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326–340. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_30 CrossRef

31.

Pathak, S., Ábrahám, E., Jansen, N., Tacchella, A., Katoen, J.-P.: A greedy approach for the efficient repair of stochastic models. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 295–309. Springer, Heidelberg (2015). doi:10.1007/978-3-319-17524-9_21

Titel: Bounded Model Checking for Probabilistic Programs
verfasst von: Nils Jansen
Christian Dehnert
Benjamin Lucien Kaminski
Joost-Pieter Katoen
Lukas Westhofen
Verlag: Springer International Publishing
Buch: Automated Technology for Verification and Analysis
Print ISBN: 978-3-319-46519-7

Electronic ISBN: 978-3-319-46520-3

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-46520-3_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"