摘要:假设一保证推理是标记迁移系统组合验证的有效手段,近期,假设-保证推理在概率系统的验证中也得到了应用。在推理中,假设的学习是通过Lstar算法来完成的。针对概率系统的假设一保证推理,提出了一种新的方法:首先直接对组合系统的一个组件进行抽取,得到一个初步的假设;通过与假设一保证规则进行多次交互,不断精化该假设;最后,要么得到一个适当的假设以证明结论的正确性,要么得到一个反例来证明结论不成立。
关键词:抽取精化 概率自动机 概率时间自动机 组合验证
单位:宁波大学职业技术教育学院 浙江宁波315100 南京航空航天大学计算机科学与技术学院 江苏南京210016 广西财经学院信息与统计学院 广西南宁530003
注:因版权方要求,不能公开全文,如需全文,请咨询杂志社