J Shanghai Jiaotong Univ Sci ›› 2023, Vol. 28 ›› Issue (6): 772-782.doi: 10.1007/s12204-022-2456-z

• • 上一篇    下一篇



  1. (上海交通大学 电子信息与电气工程学院,上海200240)
  • 接受日期:2021-01-12 出版日期:2023-11-28 发布日期:2023-12-04

Tail-Bound Cost Analysis over Nondeterministic Probabilistic Programs

WANG Peeixin(王培新)   

  1. (School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Shanghai 200240, China)
  • Accepted:2021-01-12 Online:2023-11-28 Published:2023-12-04

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

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

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