| 摘要: |
| 概率程序将概率推理模型与图灵完备的编程语言相结合，统一了对计算和不确定性知识的形式化描述，能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面，它有助于定性和定量地分析仿射概率程序的终止性，可以验证该概率程序是否以概率1终止，估计期望终止时间的上限，并计算步数N，使得N步后给定程序的终止概率呈指数下降；另一方面，它可以估计一个断言成立的概率区间，这有助于分析变量不确定性对概率程序结果的影响.通过实验表明，PROPER对分析各种仿射概率程序是有效的. |
| 关键词: 概率编程 终止性 断言分析 程序验证 |
| DOI：10.13328/j.cnki.jos.006341 |
| 分类号:TP311 |
| 基金项目:国家自然科学基金（62072176，61832015，61802254） |
|
| PROPER: Tool for Analyzing Termination and Correctness of Probabilistic Programs |
|
ZHAO Xu-Hui1, DENG Yu-Xin1, FU Hong-Fei2
|
|
1.Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China;2.Shanghai Jiao Tong University, Shanghai 200240, China
|
| Abstract: |
| 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. |
| Key words: probabilistic programming program verification termination assertion estimation |
