A formal approach to probabilistic termination. (English) Zbl 1013.68193

Carreño, Victor A. (ed.) et al., Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2410, 230-245 (2002).
Summary: We present a probabilistic version of the while loop, in the context of our mechanised framework for verifying probabilistic programs. The while loop preserves useful program properties of measurability and independence, provided a certain condition is met. This condition is naturally interpreted as “from every starting state, the while loop will terminate with probability 1”, and we compare it to other probabilistic termination conditions in the literature. For illustration, we verify in HOL two example probabilistic algorithms that necessarily rely on probabilistic termination: an algorithm to sample the Bernoulli(\(p\)) distribution using coin-flips; and the symmetric simple random walk.
For the entire collection see [Zbl 0997.00025].


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: Link