We consider termination of probabilistic programs with real-valued variables. The relevant probabilistic termination questions are as follows: (1) qualitative questions that ask whether (a) the program terminates with probability 1 (almost-sure termination), (b) the expected termination time is finite (finite termination); (2) quantitative questions that ask to (a) approximate the expected termination time (expectation problem),
(b) approximate the probability to terminate in a given number of steps (probabilistic problem), (c) compute a bound $B$ such that the probability to terminate after $B$ steps decreases exponentially (concentration problem). The notion of ranking supermartingales is a powerful approach to establish termination for probablistic programs. In this work we consider algorithmic questions related probabilistic termination, and since our focus is algorithms we consider the simplest class of ranking supermartingales, namely linear ranking supermartingales. We consider the class of affine probabilistic programs (APPs) for which linear ranking supermartingales exist and refer the subclass as LRAPPs.

Our main results for LRAPPs are as follows: First, we show that the qualitative problems (i) can be answered for probabilistic programs with demonic nondeterminism in polynomial time, (ii) are NP-hard for programs with angelic nondeterminism, and (iii) can be solved in PSPACE for probabilistic programs with both angelic and demonic nondeterminism. Second, we show that the concentration problem can be solved in the same complexity as for the qualitative problems. Finally, we establish complexity results for the expectation and probabilistic problems. For both the problems we show PSPACE-hardness even for deterministic programs, and that the problems for probabilistic programs with both types of nondeterminism can be solved in 2EXPTIME. We present experimental results to show the effectiveness of our approach to answer the qualitative and quantitative questions on probabilistic programs with demonic nondeterminism.