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 such sound and relatively complete proof rules for proving qualitative and quantitative termination in the assertion language of arithmetic. Our rules use supermartingales as estimates of the likelihood of a program's evolution and variants as measures of distances to termination. Our key insight is our completeness result, which shows how to construct a suitable supermartingales 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.

翻译：判定终止性是分析概率性命令式程序的基本问题。我们考虑一个包含离散概率选择与恶魔式有界非确定性的命令式编程模型的定性与定量概率终止问题。定性问题询问程序是否几乎必然终止，无论非确定性如何被消解。定量问题则要求给出终止概率的上界。尽管该主题已有长期且丰富的文献，但此前尚未存在针对这些问题的可靠且相对完备的证明系统。本文在算术断言语言中，为证明定性与定量终止性提供了此类可靠且相对完备的证明规则。我们的规则使用上鞅作为程序演化可能性的估计，并使用变式作为衡量距离终止状态的尺度。我们的核心洞见体现在完备性结果中，该结果展示了如何从几乎必然终止的程序构造合适的上鞅。我们还证明，许多现有证明系统中的终止性证明均可转化为我们系统中的证明，这表明了其实际适用性。作为我们证明规则的应用，我们展示了二维随机游走程序几乎必然终止性的显式证明。