PROPER:一个概率程序终止性与正确性分析工具  

PROPER:Tool for Analyzing Termination and Correctness of Probabilistic Programs

作　　者：赵旭慧 邓玉欣 符鸿飞 ZHAO Xu-Hui;DENG Yu-Xin;FU Hong-Fei(Shanghai Key Laboratory of Trustworthy Computing,East China Normal University,Shanghai 200062,China;Shanghai Jiao Tong University,Shanghai 200240,China)

机构地区：[1]华东师范大学上海市高可信计算重点实验室,上海200062 [2]上海交通大学,上海200240

出　　处：《软件学报》2022年第12期4464-4475,共12页Journal of Software

基　　金：国家自然科学基金(62072176,61832015,61802254)。

摘　　要：概率程序将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面,它有助于定性和定量地分析仿射概率程序的终止性,可以验证该概率程序是否以概率1终止,估计期望终止时间的上限,并计算步数N,使得N步后给定程序的终止概率呈指数下降;另一方面,它可以估计一个断言成立的概率区间,这有助于分析变量不确定性对概率程序结果的影响.通过实验表明,PROPER对分析各种仿射概率程序是有效的.Probabilistic programs combine probabilistic reasoning models with Turing complete programming languages,unify formal descriptions of calculation and uncertain knowledge,and can effectively deal with complex relational models and uncertain problems.This study provides a tool for analyzing termination and assertions for affine probabilistic programs,namely,PROPER.On one hand,it can help to analyze the termination property of affine probabilistic programs both qualitatively and quantitatively.It can check whether a probabilistic program terminates with probability 1,estimate the upper bound of expected termination time,and calculate the number of steps after which the termination probability of the given probabilistic program decreases exponentially.On the other hand,it can estimate the correct probability interval for a given assertion to hold,which helps to analyze the influence of uncertainty of variables on the results of probabilistic programs.The experiments show that PROPER is effective for analyzing various affine probabilistic programs.

关 键 词：概率编程 终止性 断言分析 程序验证 

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