A new proof rule for almost-sure termination
Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.
Download (ext.)
https://dl.acm.org/doi/10.1145/3158121
[Published Version]
DOI
Journal Article
| Published
| English
Scopus indexed
Author
Mciver, Annabelle;
Morgan, Carroll;
Kaminski, Benjamin Lucien;
Katoen, Joost PISTA
Department
Abstract
We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. 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. "super-martingales") that are real-valued 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 (non-demonic) Markov chains.
Publishing Year
Date Published
2017-12-07
Journal Title
Proceedings of the ACM on Programming Languages
Publisher
Association for Computing Machinery
Acknowledgement
McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics
at McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and
Prakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.
Volume
2
Issue
POPL
Article Number
33
Conference
POPL: Programming Languages
Conference Location
Los Angeles, CA, United States
Conference Date
2018-01-07 – 2018-01-13
eISSN
IST-REx-ID
Cite this
Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158121
Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158121
Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121.
A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.
Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.
Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:10.1145/3158121.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Link(s) to Main File(s)
Access Level
Open Access
Export
Marked PublicationsOpen Data ISTA Research Explorer
Sources
arXiv 1711.03588