首页 > 技术文献 > PROPER:一个概率程序终止性与正确性分析工具

PROPER:一个概率程序终止性与正确性分析工具
2022-12-06 15:31:51 来源：点击：

文档介绍

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