一句话：为带离散概率选择与有界恶魔非确定性的命令式程序，给出算术断言语言中可靠且相对完备的定性/定量概率终止证明规则。
判定概率命令式程序的终止性是基本问题。本文针对带离散概率选择和有界恶魔非确定性的命令式模型，研究定性与定量概率终止：前者要求无论非确定性如何消解，程序几乎必然终止；后者要求终止概率的界。尽管已有大量工作，此前尚无可靠且相对完备的证明系统。作者在算术断言语言中提出可靠且相对完备的证明规则，用 variant 函数度量到终止的距离，并以上鞅限制其几乎必然增长。完备性结果表明，可从几乎必然终止的程序构造合适的上鞅与 variant 函数。作者还说明现有若干证明系统中的终止证明可转换为本文证明，并给出二维随机游走几乎必然终止的显式证明。该工作填补了概率终止证明系统长期缺失的空白。
Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems for an imperative programming model with discrete probabilistic choice and demonic bounded nondeterminism. The qualitative question asks if the program terminates almost-surely, no matter how nondeterminism is resolved. The quantitative question asks for a bound on the probability of termination. Despite a long and rich literature on the topic, no sound and relatively complete proof systems were known for these problems. In this paper, we provide sound and relatively complete proof rules for proving qualitative and quantitative termination in the assertion language of arithmetic. Our rules use variant functions as measures of distances to termination as well as supermartingales that restrain the growth of these variants almost-surely. Our completeness result shows how to construct suitable supermartingale and variant functions from an almost-surely terminating program. We also show that proofs of termination in many existing proof systems can be transformed to proofs in our system, pointing to its applicability in practice. As an application of our proof rule, we show an explicit proof of almost-sure termination for the two-dimensional random walker.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MajumdarS25,
title = {Sound and Complete Proof Rules for Probabilistic Termination},
author = {Rupak Majumdar and V.R. Sathiyanarayana},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704899}
}