On the Hardness of Almost-Sure Termination

Abstract

This paper considers the computational hardness of computing expected outcomes and deciding (universal) (positive) almost-sure termination of probabilistic programs. It is shown that computing lower and upper bounds of expected outcomes is ${\Sigma }_1^0$- and ${\Sigma }_2^0$-complete, respectively. Deciding (universal) almost-sure termination as well as deciding whether the expected outcome of a program equals a given rational value is shown to be ${\Pi }_2^0$-complete. Finally, it is shown that deciding (universal) positive almost-sure termination is ${\Sigma }_2^0$-complete (${\Pi }_3^0$-complete).

MFCS 2015. arXiv admin note: text overlap with arXiv:1410.7225