Abstract
Hoare logic can be used to verify properties of deterministic programs by deriving correctness formulae, also called Hoare triples. The goal of this paper is to extend the Hoare logic to be able to deal with probabilistic programs. To this end a generic non-uniform language Lpw with a probabilistic choice operator is introduced and a denotational semantics D is given for the language. A notion of probabilistic predicate is defined to express claims about the state of a probabilistic program. To reason about the probabilistic predicates a derivation system pH, similar to that of standard Hoare logic, is given. The derivation system is shown to be correct with respect to the semantics D. Some basic examples illustrate the use of the system.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997.
S. Andova. Probabilistic process algebra. In Proceedings of ARTS’99, Bamberg, Germany, 1999.
K.R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer-Verlag, 1991.
C. Baier, M. Kwiatkowska, and G. Norman. Computing probabilistic lower and upper bounds for ltl formulae over sequential and concurrent markov chains. Technical Report CSR-98-4, University of Birmingham, June 1998.
J.W. de Bakker. Mathematical Theory of Program Correctness. Series in Computer Science. Prentice-Hall Internationall, 1980.
P.R. D’Argenio, J.-P. Katoen, and E. Brinksma. A stochastic process algebra for discrete event simulation. Technical report, University of Twente, 1998.
N. Francez. Program Verification. International Computer Science Series. Addison-Wesley, 1992.
J.I. den Hartog. Comparative semantics for a process language with probabilistic choice and non-determinism. Technical Report IR-445, Vrije Universiteit, Ams-terdam, February 1998.
J.I. den Hartog and E.P. de Vink. Mixing up nondeterminism and probability: A preliminary report. ENTCS, 1999. to appear.
J.I. den Hartog and E.P. de Vink. Taking chances on merge and fail: Extending strong and probabilistic bisimulation. Technical Report IR-454, Vrije Universiteit, Amsterdam, March 1999.
H. Hermanns. Interactive Markov Chains. PhD thesis, University of Erlangen-Nurnberg, July 1998.
J. Hooman. Program design in PVS. In Proceedings Workshop on Tool Support for System Development and Verification, June 1996.
D. Kozen. A probabilistic PDL. Journal of Computer and System Sciences, 30:162–178, 1985.
K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1–28, 1991.
N. Lynch. Distributed Algorithms. The Morgan Kaufmann series in data manage-ment systems. Kaufmann, 1996.
C. Morgan and A. McIver. pGCL: formal reasoning for random algorithms. South African Computer Journal, 1999. to appear.
C. Morgan, A. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325–353, May 1996.
R. Motwani and P. Raghavan. Randomized Algorithms. Cambridge University Press, 1995.
R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, June 1995.
S.-H. Wu, S.A. Smolka, and E.W. Stark. Composition and behavior of probabilistic I/O automata. Theoretical Computer Science, 176:1–38, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
den Hartog, J.I. (1999). Verifying Probabilistic Programs Using a Hoare like Logic. In: Thiagarajan, P.S., Yap, R. (eds) Advances in Computing Science — ASIAN’99. ASIAN 1999. Lecture Notes in Computer Science, vol 1742. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46674-6_11
Download citation
DOI: https://doi.org/10.1007/3-540-46674-6_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66856-5
Online ISBN: 978-3-540-46674-1
eBook Packages: Springer Book Archive