eprintid: 10089705
rev_number: 18
eprint_status: archive
userid: 608
dir: disk0/10/08/97/05
datestamp: 2020-01-29 16:41:59
lastmod: 2021-10-19 22:21:42
status_changed: 2020-01-29 16:41:59
type: proceedings_section
metadata_visibility: show
creators_name: McIver, A
creators_name: Morgan, C
creators_name: Kaminski, BL
creators_name: Katoen, J-P
title: A New Proof Rule for Almost-Sure Termination
ispublished: pub
divisions: UCL
divisions: B04
divisions: C05
divisions: F48
keywords: cs.PL, cs.PL, cs.LO
note: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
abstract: 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 is expressed in a program logic, and so applies directly to source code. The programs may contain both probabilistic- and demonic choice, and the probabilistic choices may depend on the current state. As do other researchers, we use variant functions (a.k.a. "super-martingales") that are real-valued and probabilistically might decrease 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.
date: 2018-01
publisher: ACM
official_url: https://doi.org/10.1145/3158121
oa_status: green
full_text_type: other
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_id: 1741702
doi: 10.1145/3158121
lyricists_name: Kaminski, Benjamin
lyricists_id: BKAMI07
actors_name: Kaminski, Benjamin
actors_id: BKAMI07
actors_role: owner
full_text_status: public
volume: 2
place_of_pub: Los Angeles, California, USA
pagerange: 33
event_title: 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018)
book_title: Proceedings of the ACM on Programming Languages
citation:        McIver, A;    Morgan, C;    Kaminski, BL;    Katoen, J-P;      (2018)    A New Proof Rule for Almost-Sure Termination.                     In:  Proceedings of the ACM on Programming Languages.  (pp. p. 33).  ACM: Los Angeles, California, USA.       Green open access   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/10089705/1/1711.03588v2.pdf