Olmedo, F;
Kaminski, BL;
Katoen, J-P;
Matheja, C;
(2016)
Reasoning about Recursive Probabilistic Programs.
In:
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS).
(pp. pp. 672-681).
ACM: New York, NY, USA.
Preview |
Text
main.pdf - Accepted Version Download (647kB) | Preview |
Abstract
This paper presents a wp--style calculus for obtaining expectations on the outcomes of (mutually) recursive probabilistic programs. We provide several proof rules to derive one-- and two--sided bounds for such expectations, and show the soundness of our wp--calculus with respect to a probabilistic pushdown automaton semantics. We also give a wp--style calculus for obtaining bounds on the expected runtime of recursive programs that can be used to determine the (possibly infinite) time until termination of such programs.
| Type: | Proceedings paper |
|---|---|
| Title: | Reasoning about Recursive Probabilistic Programs |
| Event: | 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS) |
| Location: | New York City, NY |
| Dates: | 05 July 2016 - 08 July 2016 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/2933575.2935317 |
| Publisher version: | https://doi.org/10.1145/2933575.2935317 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Science & Technology, Technology, Computer Science, Theory & Methods, Logic, Computer Science, Science & Technology - Other Topics, recursion, probabilisitic programming, program verification, weakest pre-condition calculus, expected runtime, SEMANTICS, CALCULUS |
| 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.ucl.ac.uk/id/eprint/10089694 |
Archive Staff Only
 |
View Item |
