POPL 2019 (series) / VMCAI 2019 (series) / VMCAI 2019 - 20th International Conference on Verification, Model Checking, and Abstract Interpretation /
Termination of Nondeterministic Probabilistic Programs
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.
Mon 14 JanDisplayed time zone: Belfast change
Mon 14 Jan
Displayed time zone: Belfast change
14:00 - 15:30 | |||
14:00 30mTalk | Syntactic Partial Order Compression for Probabilistic Reachability VMCAI | ||
14:30 30mTalk | Termination of Nondeterministic Probabilistic Programs VMCAI | ||
15:00 30mTalk | Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics VMCAI |