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

摘要：

概率程序将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面,它有助于定性和定量地分析仿射概率程序的终止性,可以验证该概率程序是否以概率1终止,估计期望终止时间的上限,并计算步数N,使得N步后给定程序的终止概率呈指数下降;另一方面,它可以估计一个断言成立的概率区间,这有助于分析变量不确定性对概率程序结果的影响.通过实验表明,PROPER对分析各种仿射概率程序是有效的.

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

所属期刊栏目：33

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金;国家自然科学基金;国家自然科学基金

在线出版日期：2022-12-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：4464-4475