Feng, Shenghua;
Chen, Mingshuai;
Su, Han;
Kaminski, Benjamin Lucien;
Katoen, Joost-Pieter;
Zhan, Naijun;
(2023)
Lower Bounds for Possibly Divergent Probabilistic Programs.
Proceedings of the ACM on Programming Languages
, 7
(OOPSLA1)
pp. 696-726.
10.1145/3586051.
Preview |
PDF
3586051.pdf - Published Version Download (448kB) | Preview |
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.
| Type: | Article |
|---|---|
| Title: | Lower Bounds for Possibly Divergent Probabilistic Programs |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3586051 |
| Publisher version: | https://doi.org/10.1145/3586051 |
| Language: | English |
| Additional information: | © 2023 Copyright held by the owner/author(s). This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery-pp.ucl.ac.uk/id/eprint/10168175 |
Archive Staff Only
 |
View Item |
