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 Σ01– and Σ02–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 Π02 –complete. Finally, it is shown that deciding (universal) positive almost–sure termination is Σ02–complete (Π03–complete).