Lower Bounds for Possibly Divergent Probabilistic Programs

TL;DR

This paper introduces a novel proof rule for establishing lower bounds on probabilistic programs, including those that may not terminate, enabling analysis of complex stochastic processes like random walks.

Contribution

It extends existing verification methods to handle non-terminating probabilistic programs, providing tools for lower bound analysis beyond almost-sure termination.

Findings

New proof rule applicable to divergent probabilistic loops

Enables lower bound analysis of termination probabilities

Applicable to complex stochastic processes like 3D random walks

Abstract

We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice.