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

作者简介:

赵旭慧(1996-),女,硕士,主要研究领域为形式化方法;符鸿飞(1984-),男,博士,副教授,博士生导师,CCF专业会员,主要研究领域为形式化方法;邓玉欣(1978-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法.

通讯作者:

邓玉欣,E-mail:yxdeng@sei.ecnu.edu.cn

中图分类号:

TP311

基金项目:

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


PROPER: Tool for Analyzing Termination and Correctness of Probabilistic Programs
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

赵旭慧,邓玉欣,符鸿飞. PROPER:一个概率程序终止性与正确性分析工具.软件学报,2022,33(12):4464-4475

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-01-28
  • 最后修改日期:2021-02-27
  • 录用日期:
  • 在线发布日期: 2022-12-03
  • 出版日期: 2022-12-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号