A new proof rule for almost-sure termination

Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen

Research output: Contribution to journalArticleResearchpeer-review

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.
LanguageEnglish
Article number33
Pages1-28
Number of pages28
JournalProceedings of the ACM on Programming Languages
Volume2
Issue numberPOPL
DOIs
Publication statusPublished - 5 Jan 2018

Fingerprint

Markov processes
Innovation

Cite this

McIver, Annabelle ; Morgan, Carroll ; Kaminski, Benjamin Lucien ; Katoen, Joost-Pieter. / A new proof rule for almost-sure termination. In: Proceedings of the ACM on Programming Languages. 2018 ; Vol. 2, No. POPL. pp. 1-28.
@article{28c65f95fd514b6c9f705dffce8b0175,
title = "A new proof rule for almost-sure termination",
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.",
keywords = "Almost-sure termination, demonic non-determinism, program logic pGCL",
author = "Annabelle McIver and Carroll Morgan and Kaminski, {Benjamin Lucien} and Joost-Pieter Katoen",
year = "2018",
month = "1",
day = "5",
doi = "10.1145/3158121",
language = "English",
volume = "2",
pages = "1--28",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
number = "POPL",

}

A new proof rule for almost-sure termination. / McIver, Annabelle; Morgan, Carroll; Kaminski, Benjamin Lucien; Katoen, Joost-Pieter.

In: Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, 33, 05.01.2018, p. 1-28.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - A new proof rule for almost-sure termination

AU - McIver,Annabelle

AU - Morgan,Carroll

AU - Kaminski,Benjamin Lucien

AU - Katoen,Joost-Pieter

PY - 2018/1/5

Y1 - 2018/1/5

N2 - 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.

AB - 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.

KW - Almost-sure termination

KW - demonic non-determinism

KW - program logic pGCL

U2 - 10.1145/3158121

DO - 10.1145/3158121

M3 - Article

VL - 2

SP - 1

EP - 28

JO - Proceedings of the ACM on Programming Languages

T2 - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - POPL

M1 - 33

ER -