Tail-Bound Cost Analysis over Nondeterministic Probabilistic Programs  

作　　者：王培新 WANG Peixin(School of Electronic Information and Electrical Engineering,Shanghai Jiao Tong University,Shanghai 200240,China)

机构地区：[1]School of Electronic Information and Electrical Engineering,Shanghai Jiao Tong University,Shanghai 200240,China

出　　处：《Journal of Shanghai Jiaotong university(Science)》2023年第6期772-782,共11页上海交通大学学报（英文版）

基　　金：the National Natural Science Foundation of China(Nos.61802254,62072299,and 61772336)。

摘　　要：For probabilistic programs,there is some work for qualitative and quantitative analysis about expec-tation 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 proba-bilistic 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.

关 键 词：program cost analysis probabilistic programs tail bound MARTINGALES 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]