Abstract: For probabilistic programs, there is some work for qualitative and quantitative analysis about expectation or mean, such as expected termination time, and expected cost analysis. However, another non-trivial issue is about tail bounds (i.e., upper bounds of tail probabilities), which can provide high-probability guarantees to extreme events. In this work, we focus on the problem of tail-bound cost analysis over nondeterministic probabilistic programs, which aims to automatically obtain the tail bound of resource usages over such programs. To achieve this goal, we present a novel approach, combined with a suitable concentration inequality, to derive the tail bound of accumulated cost until program termination. Our approach can handle both positive and negative costs. Moreover, our approach enables an automated template-based synthesis of supermartingales and leads to an efficient polynomial-time algorithm. To show the effectiveness of our approach, we present experimental results on various programs and make a comparison with state-of-the-art tools.

Key words: program cost analysis, probabilistic programs, tail bound, martingales

摘要： 对于概率程序，已有一些关于期望或均值的定性和定量分析工作，例如期望终止时间和预期消耗分析。然而，另一个非常重要的问题是尾部界限（即尾部概率的上界），可以为极端事件提供高概率保证。在这项工作中，我们关注的问题是对于非确定性概率程序消耗的尾部界限分析，旨在自动获取这些程序的资源使用的尾部界限。为了实现这一目标，提出了一种新颖的方法，结合适当的集中不等式，来推导程序终止之前累积消耗的尾部界限。提出的方法可以处理正、负消耗。此外，这个方法实现了基于模板的排序上鞅的自动合成，并产生了一个高效的多项式时间算法。为了展示提出的方法的有效性，提供了对不同程序的实验结果，并与最先进的工具进行了比较。

关键词: 程序消耗分析，概率程序，尾部界限，鞅