Projects per year
Abstract
We present a new proof rule for proving almostsure termination of probabilistic programs, including those that contain demonic nondeterminism.
An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice.
Like others, we use variant functions (a.k.a. "supermartingales") that are realvalued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (nondemonic) Markov chains.
An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice.
Like others, we use variant functions (a.k.a. "supermartingales") that are realvalued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (nondemonic) Markov chains.
Original language  English 

Article number  33 
Pages (fromto)  128 
Number of pages  28 
Journal  Proceedings of the ACM on Programming Languages 
Volume  2 
Issue number  POPL 
DOIs  
Publication status  Published  5 Jan 2018 
Keywords
 Almostsure termination
 demonic nondeterminism
 program logic pGCL
Fingerprint
Dive into the research topics of 'A new proof rule for almostsure termination'. Together they form a unique fingerprint.Projects
 1 Finished

More information for better utility; less information for better privacy
McIver, A., Morgan, C., Teague, V., Schneider, S., MQRES, M. & PhD Contribution (ARC), P. C. (.
26/03/14 → 31/12/20
Project: Research