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

• 作者: 张君华 肖芳雄 黄志球
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 假设-保证验证 抽取精化 概率自动机 概率时间自动机 组合验证
• 年，卷（期）: 2013,（3）
• 所属期刊栏目: 软件工程
• 页码范围: 128-133
• 页数: 6页
• 分类号: TP306
• 字数: 6059字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2013.03.021

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术学院	183	1755	20.0	33.0
2	肖芳雄	广西财经学院信息与统计学院	19	99	5.0	9.0
3	张君华	宁波大学职业技术教育学院	2	1	1.0	1.0