有界模型检测的优化

作     者：杨晋吉 苏开乐 骆翔宇 林瀚 肖茵茵 

作者机构：华南师范大学计算机学院广东广州510631 中山大学信息科学与技术学院广东广州510275 北京大学信息科学技术学院北京100871 桂林电子科技大学计算机与控制学院广西桂林541004 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2009年第20卷第8期

页      面：2005-2014页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：国家杰出青年基金No.60725207 国家自然科学基金Nos.60473004 60763004 广东省自然科学基金No.06023195 广东省科技攻关项目No.2007B010400068~~ 

主　　题：模型检测 有界模型检测 可满足性问题 模态算子 递推公式 

摘      要：G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-time temporal logic,简称LTL)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成SAT(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值.