会议专题

基于抽取-精化的概率系统假设-保证验证

  假设-保证推理是标记迁移系统组合验证的有效手段。近期,假设-保证推理在概率系统的验证中也得到应用。在推理中,假设的学习是通过L star算法来完成的。本文针对概率系统的假设-保证推理提出了一种新的方法。首先直接对组合系统的一个组件进行抽取,得到一个初步的假设,通过与假设-保证规则进行多次交互,不断精化该假设。最后,要么得到一个适当的假设以证明结论的正确性,要么得到一个反例来证明结论不成立。

假设-保证验证 抽取精化 概率自动机 概率时间自动机 组合验证

张君华 黄志球 肖芳雄

宁波大学职教学院,宁波 中国 315100 南京航空航天大学计算机科学与技术学院,南京 中国 210016 广西财经学院信息与统计学院,南宁 中国 530003

国内会议

第十一届全国软件与应用学术会议(NASAC2012)

南京

中文

1-8

2012-10-20(万方平台首次上网日期,不代表论文的发表时间)