有界模型检测的优化

摘要：

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中验证其他模态算子时的编码优化也有参考价值.

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

所属期刊栏目：20

分类号：TP301(计算技术、计算机技术)

资助基金：the Outstanding Young Research Fund of China under Grant No.60725207;the National Natural Science Foundation of China under Grant Nos.60473004, 60763004;the Guangdong Provincial Natural Science Foundation of China under Grant No.06023195;the Guangdong Provincial Research Foundation of Science and Technology of China under Grant No.2007B010400068

在线出版日期：2009-10-23（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：2005-2014