Lower Bounds for Possibly Divergent Probabilistic Programs

Proceedings of the ACM on Programming Languages, vol. 7, pp. 696–726

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.

Authors 5

1. Shenghua Feng

   Chinese Academy of Sciences · Institute of Software · University of Chinese Academy of Sciences

   Affiliation as printed

   Institute of Software at Chinese Academy of Sciences, China / University of Chinese Academy of Sciences, China

2. Mingshuai Chen

   Zhejiang University

   Affiliation as printed

   Zhejiang University, China

3. Benjamin Lucien Kaminski

   University College London · Saarland University

   Affiliation as printed

   Saarland University, Germany / University College London, UK

4. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

5. Naijun Zhan

   Chinese Academy of Sciences · Institute of Software · University of Chinese Academy of Sciences

   Affiliation as printed

   Institute of Software at Chinese Academy of Sciences, China / University of Chinese Academy of Sciences, China