一句话：提出不依赖几乎必然终止的新证明规则，为可能发散的概率程序建立终止概率与期望值的非平凡下界。
概率程序的定量验证通常需要程序几乎必然终止，才能对终止概率、期望值等量给出下界；但许多实际概率程序（如格点上的随机游走）可能发散，现有规则因而失效。本文提出一种新的证明规则，用于验证可能发散的概率程序的下界，突破了现有规则对几乎必然终止性的限制。该规则能够为非平凡的终止概率与期望值建立下界。作者以三维格点随机游走等经典的可能发散概率循环说明方法的适用性。该工作为可能发散的概率循环的定量推理提供了通用而有效的验证手段。
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.
@article{paperbot2044,
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 = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586051}
}