Termination of nondeterministic probabilistic programs

H. Fu, K. Chatterjee, 11388 (2019) 468–490.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published | English
Author
Editor
;
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
Volume
11388
Page
468-490
Conference
Verification, Model Checking, and Abstract Interpretation, VMCAI
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. Enea C, Piskac R, eds. 2019;11388:468-490. doi:10.1007/978-3-030-11245-5_22
Fu, H., & Chatterjee, K. (2019). Termination of nondeterministic probabilistic programs. (C. Enea & R. Piskac, Eds.). Presented at the Verification, Model Checking, and Abstract Interpretation, VMCAI, Cascais, Portugal: Springer. https://doi.org/10.1007/978-3-030-11245-5_22
Fu, Hongfei, and Krishnendu Chatterjee. “Termination of Nondeterministic Probabilistic Programs.” Edited by Constantin Enea and Ruzica Piskac. Lecture Notes in Computer Science. Springer, 2019. https://doi.org/10.1007/978-3-030-11245-5_22.
H. Fu and K. Chatterjee, “Termination of nondeterministic probabilistic programs,” vol. 11388. Springer, pp. 468–490, 2019.
Fu H, Chatterjee K. 2019. Termination of nondeterministic probabilistic programs (eds. C. Enea & R. Piskac). 11388, 468–490.
Fu, Hongfei, and Krishnendu Chatterjee. Termination of Nondeterministic Probabilistic Programs. Edited by Constantin Enea and Ruzica Piskac, vol. 11388, Springer, 2019, pp. 468–90, doi:10.1007/978-3-030-11245-5_22.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar