In this article, we consider the termination problem of probabilistic programs with real-valued variables. The questions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); and quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability not to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales, which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (A pps ) with both angelic and demonic non-determinism. An important subclass of A pps is LRA pp which is defined as the class of all A pps over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRA pp (i) can be decided in polynomial time for A pps with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for A pps with angelic non-determinism. Moreover, the NP-hardness result holds already for A pps without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRA pp can be solved in the same complexity as for the membership problem of LRA pp . Finally, we show that the expectation problem over LRA pp can be solved in 2EXPTIME and is PSPACE-hard even for A pps without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over A pps with at most demonic non-determinism.

@article{paperbot321,
  title = {Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs},
  author = {Krishnendu Chatterjee and Hongfei Fu and Petr Novotný and Rouzbeh Hasheminezhad},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {40},
  number = {2},
  year = {2018},
  doi = {10.1145/3174800}
}