Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard
Benjamin Lucien Kaminski, Joost-Pieter Katoen · arXiv (Cornell University) · 2014
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 $Π^0_2$-complete. Computing lower and upper bounds on the expected outcome is shown to be recursively enumerable and $Σ^0_2$-complete, respectively.