Termination of nondeterministic probabilistic programs
Fu H, Chatterjee K. 2019. Termination of nondeterministic probabilistic programs. International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 11388, 468–490.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Scopus indexed
Author
Fu, Hongfei;
Chatterjee, KrishnenduISTA 
Department
Series Title
LNCS
Abstract
We study the termination problem for nondeterministic probabilistic programs. We consider the bounded termination problem that asks whether the supremum of the expected termination time over all schedulers is bounded. First, we show that ranking supermartingales (RSMs) are both sound and complete for proving bounded termination over nondeterministic probabilistic programs. For nondeterministic probabilistic programs a previous result claimed that RSMs are not complete for bounded termination, whereas our result corrects the previous flaw and establishes completeness with a rigorous proof. Second, we present the first sound approach to establish lower bounds on expected termination time through RSMs.
Publishing Year
Date Published
2019-01-11
Proceedings Title
International Conference on Verification, Model Checking, and Abstract Interpretation
Volume
11388
Page
468-490
Conference
VMCAI: Verification, Model Checking, and Abstract Interpretation
Conference Location
Cascais, Portugal
Conference Date
2019-01-13 – 2019-01-15
IST-REx-ID
Cite this
Fu H, Chatterjee K. Termination of nondeterministic probabilistic programs. In: International Conference on Verification, Model Checking, and Abstract Interpretation. Vol 11388. Springer Nature; 2019:468-490. doi:10.1007/978-3-030-11245-5_22
Fu, H., & Chatterjee, K. (2019). Termination of nondeterministic probabilistic programs. In International Conference on Verification, Model Checking, and Abstract Interpretation (Vol. 11388, pp. 468–490). Cascais, Portugal: Springer Nature. https://doi.org/10.1007/978-3-030-11245-5_22
Fu, Hongfei, and Krishnendu Chatterjee. “Termination of Nondeterministic Probabilistic Programs.” In International Conference on Verification, Model Checking, and Abstract Interpretation, 11388:468–90. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-11245-5_22.
H. Fu and K. Chatterjee, “Termination of nondeterministic probabilistic programs,” in International Conference on Verification, Model Checking, and Abstract Interpretation, Cascais, Portugal, 2019, vol. 11388, pp. 468–490.
Fu H, Chatterjee K. 2019. Termination of nondeterministic probabilistic programs. International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 11388, 468–490.
Fu, Hongfei, and Krishnendu Chatterjee. “Termination of Nondeterministic Probabilistic Programs.” International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 11388, Springer Nature, 2019, pp. 468–90, doi:10.1007/978-3-030-11245-5_22.
Export
Marked PublicationsOpen Data ISTA Research Explorer
Web of Science
View record in Web of Science®Sources
arXiv 1701.02944
Google Scholar