Lower Bounds for Possibly Divergent Probabilistic Programs
Logic in Computer Science
2023-02-14 v1 Probability
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.
Cite
@article{arxiv.2302.06082,
title = {Lower Bounds for Possibly Divergent Probabilistic Programs},
author = {Shenghua Feng and Mingshuai Chen and Han Su and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Naijun Zhan},
journal= {arXiv preprint arXiv:2302.06082},
year = {2023}
}
Comments
Paper conditionally accepted by OOPSLA 2023