This paper considers the computational hardness of computing expected outcomes and deciding almost-sure termination of probabilistic programs. We show that deciding almost-sure termination and deciding whether the expected outcome of a program equals a given rational value is Π20-complete. Computing lower and upper bounds on the expected outcome is shown to be recursively enumerable and Σ20-complete, respectively.
@article{arxiv.1410.7225,
title = {Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen},
journal= {arXiv preprint arXiv:1410.7225},
year = {2014}
}