nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs

verfasst von : Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

This paper presents a wp–style calculus for obtaining bounds on the expected run–time of probabilistic programs. Its application includes determining the (possibly infinite) expected termination time of a probabilistic program and proving positive almost–sure termination—does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the run–time of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson’s approach for reasoning about the run–time of deterministic programs. We analyze the expected run–time of some example programs including a one–dimensional random walk and the coupon collector problem.

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 An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages

Nächstes Kapitel Improving Floating-Point Numbers: A Lazy Approach to Adaptive Accuracy Refinement for Numerical Computations

A Dirac distribution assigns the total probability mass, i.e. 1, to a single point.

If \(H:\mathcal {D} \rightarrow \mathcal {D}\) is a continuous function over an \(\omega \)–cpo \((\mathcal {D},\sqsubseteq )\) with bottom element, then \(H(d) \sqsubseteq d\) implies \( \textsf {lfp} \,H \sqsubseteq d\) for every \(d \in \mathcal {D}\).

Limit \(\lim _{n \rightarrow \infty } I_n\) is to be understood pointwise, on \(\mathbb {R}_{{}\ge 0}^{\infty }\), i.e. \(\lim _{n \rightarrow \infty } I_n = \lambda \sigma . \lim _{n \rightarrow \infty } I_n(\sigma )\) and \(\lim _{n \rightarrow \infty } I_n(\sigma ) = \infty \) is considered a valid value.

If \(\langle a_n \rangle _{n \in \mathbb N}\) is an increasing sequence in \(\mathbb {R}_{{}\ge 0}^{\infty }\), then \(\lim _{n \rightarrow \infty } a_n\) coincides with supremum \(\sup \nolimits _{n}a_n\).

Note that while this program terminates with probability one, the expected run–time to achieve termination is infinite.

The problem formulation presented here is taken from [20].

Arthan, R., Martin, U., Mathiesen, E.A., Oliva, P.: A general framework for sound and complete Floyd-Hoare logics. ACM Trans. Comput. Log. 11(1), 7 (2009)MathSciNetCrossRefMATH

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

Berghammer, R., Müller-Olm, M.: Formal development and verification of approximation algorithms using auxiliary variables. In: Bruynooghe, M. (ed.) LOPSTR 2004. LNCS, vol. 3018, pp. 59–74. Springer, Heidelberg (2004)CrossRef

Brázdil, T., Kiefer, S., Kucera, A., Vareková, I.H.: Runtime analysis of probabilistic programs with unbounded recursion. J. Comput. Syst. Sci. 81(1), 288–310 (2015)MathSciNetCrossRefMATH

Celiku, O., McIver, A.K.: Compositional specification and analysis of cost-based properties in probabilistic programs. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 107–122. Springer, Heidelberg (2005)CrossRef

Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511–526. Springer, Heidelberg (2013)CrossRef

Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Upper Saddle River (1976)MATH

Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: Principles of Programming Languages (POPL), pp. 489–501. ACM (2015)

Frandsen, G.S.: Randomised Algorithms. Lecture Notes. University of Aarhus, Denmark (1998)

10.

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

11.

Hehner, E.C.R.: Formalization of time and space. Formal Aspects Comput. 10(3), 290–306 (1998)CrossRefMATH

12.

Hehner, E.C.R.: A probability perspective. Formal Aspects Comput. 23(4), 391–419 (2011)MathSciNetCrossRefMATH

13.

Hickey, T., Cohen, J.: Automating program analysis. J. ACM 35(1), 185–220 (1988)MathSciNetCrossRefMATH

14.

Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefMATH

15.

Hurd, J.: A formal approach to probabilistic termination. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 230–245. Springer, Heidelberg (2002)CrossRef

16.

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

17.

Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. ArXiv e-prints (2016). http://arxiv.org/abs/1601.01001

18.

Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)MathSciNetCrossRefMATH

19.

McIver, A., Morgan, C.: Abstraction Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, New York (2004)MATH

20.

Mitzenmacher, M., Upfal, E.: Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press, Cambridge (2005)CrossRefMATH

21.

Monniaux, D.: An abstract analysis of the probabilistic termination of programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 111–126. Springer, Heidelberg (2001)CrossRef

22.

Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)CrossRefMATH

23.

Nielson, H.R.: A Hoare-like proof system for analysing the computation time of programs. Sci. Comput. Program. 9(2), 107–136 (1987)MathSciNetCrossRefMATH

24.

Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, London (2007)CrossRefMATH

25.

Wechler, W.: Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science, vol. 25. Springer, Heidelberg (1992)CrossRefMATH

26.

Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)

Titel: Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
verfasst von: Benjamin Lucien Kaminski
Joost-Pieter Katoen
Christoph Matheja
Federico Olmedo
Verlag: Springer Berlin Heidelberg
Buch: Programming Languages and Systems
Print ISBN: 978-3-662-49497-4

Electronic ISBN: 978-3-662-49498-1

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-662-49498-1_15

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"