Fu, Hongfei ; Chatterjee, KrishnenduIST Austria
Enea, Constantin ; Piskac, Ruzica
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.
Verification, Model Checking, and Abstract Interpretation, VMCAI
2019-01-13 – 2019-01-15
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.