Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs

K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming Languages and Systems 40 (2018) 7.


Journal Article | Published | English
Department
Abstract
In this article, we consider the termination problem of probabilistic programs with real-valued variables. Thequestions 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); andquantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) tocompute a boundBsuch that the probability not to terminate afterBsteps decreases exponentially (con-centration problem). To solve these questions, we utilize the notion of ranking supermartingales, which isa powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmicsynthesis of linear ranking-supermartingales over affine probabilistic programs (Apps) with both angelic anddemonic non-determinism. An important subclass of Apps is LRApp which is defined as the class of all Appsover which a linear ranking-supermartingale exists.Our main contributions are as follows. Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor Apps with angelic non-determinism. Moreover, theNP-hardness result holds already for Appswithout probability and demonic non-determinism. Secondly, we show that the concentration problem overLRApp can be solved in the same complexity as for the membership problem of LRApp. Finally, we show thatthe expectation problem over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate theeffectiveness of our approach to answer the qualitative and quantitative questions over Apps with at mostdemonic non-determinism.
Publishing Year
Date Published
2018-06-01
Journal Title
ACM Transactions on Programming Languages and Systems
Volume
40
Issue
2
Article Number
7
ISSN
IST-REx-ID

Cite this

Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. ACM Transactions on Programming Languages and Systems. 2018;40(2):7. doi:10.1145/3174800
Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2018). Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. ACM Transactions on Programming Languages and Systems, 40(2), 7. https://doi.org/10.1145/3174800
Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” ACM Transactions on Programming Languages and Systems 40, no. 2 (2018): 7. https://doi.org/10.1145/3174800.
K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs,” ACM Transactions on Programming Languages and Systems, vol. 40, no. 2, p. 7, 2018.
Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2018. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. ACM Transactions on Programming Languages and Systems. 40(2), 7.
Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” ACM Transactions on Programming Languages and Systems, vol. 40, no. 2, Association for Computing Machinery (ACM), 2018, p. 7, doi:10.1145/3174800.

Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data IST Research Explorer

Sources

arXiv 1510.08517

Search this title in

Google Scholar