Reasoning about Recursive Probabilistic Programs
Logic in Computer Science
2016-03-10 v1
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.
Cite
@article{arxiv.1603.02922,
title = {Reasoning about Recursive Probabilistic Programs},
author = {Federico Olmedo and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
journal= {arXiv preprint arXiv:1603.02922},
year = {2016}
}