Termination Analysis of Probabilistic Programs with Martingales
Chatterjee K, Fu H, Novotný P. 2020.Termination Analysis of Probabilistic Programs with Martingales. In: Foundations of Probabilistic Programming. , 221–258.
Download
Book Chapter
| Published
| English
Corresponding author has ISTA affiliation
Department
Grant
Abstract
For non-probabilistic programs, a key question in static analysis is termination, which asks whether a given program terminates under a given initial condition. In the presence of probabilistic behaviour, there are two fundamental extensions of the termination question: (a) the almost-sure termination question, which asks whether the termination probability is 1; and (b) the bounded-time termination question, which asks whether the expected termination time is bounded. There are many active research directions to address these two questions; one important such direction is the use of martingale theory for termination analysis. In this chapter, we survey the main techniques of the martingale-based approach to the termination analysis of probabilistic programs.
Publishing Year
Date Published
2020-11-18
Book Title
Foundations of Probabilistic Programming
Publisher
Cambridge University Press
Acknowledgement
Krishnendu Chatterjee is supported by the Austrian Science Fund (FWF) NFN
Grant No. S11407-N23 (RiSE/SHiNE), and COST Action GAMENET. Hongfei Fu
is supported by the National Natural Science Foundation of China (NSFC) Grant
No. 61802254. Petr Novotný is supported by the Czech Science Foundation grant
No. GJ19-15134Y.
Page
221-258
ISBN
IST-REx-ID
Cite this
Chatterjee K, Fu H, Novotný P. Termination Analysis of Probabilistic Programs with Martingales. In: Foundations of Probabilistic Programming. Cambridge University Press; 2020:221-258. doi:10.1017/9781108770750.008
Chatterjee, K., Fu, H., & Novotný, P. (2020). Termination Analysis of Probabilistic Programs with Martingales. In Foundations of Probabilistic Programming (pp. 221–258). Cambridge University Press. https://doi.org/10.1017/9781108770750.008
Chatterjee, Krishnendu, Hongfei Fu, and Petr Novotný. “Termination Analysis of Probabilistic Programs with Martingales.” In Foundations of Probabilistic Programming, 221–58. Cambridge University Press, 2020. https://doi.org/10.1017/9781108770750.008.
K. Chatterjee, H. Fu, and P. Novotný, “Termination Analysis of Probabilistic Programs with Martingales,” in Foundations of Probabilistic Programming, Cambridge University Press, 2020, pp. 221–258.
Chatterjee K, Fu H, Novotný P. 2020.Termination Analysis of Probabilistic Programs with Martingales. In: Foundations of Probabilistic Programming. , 221–258.
Chatterjee, Krishnendu, et al. “Termination Analysis of Probabilistic Programs with Martingales.” Foundations of Probabilistic Programming, Cambridge University Press, 2020, pp. 221–58, doi:10.1017/9781108770750.008.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
2020_ProbProgramming_Chatterjee.pdf
316.68 KB
Access Level

Date Uploaded
2025-09-23
MD5 Checksum
28ece115e8d2d9263e253a598e7caef2