有界模型检测的优化

g(p)和g(p→f(q))是有界模型检测(boundedmodelchecking,简称bmc)中的两个重要的常用模态算子.对验证g(p)和g(p→f(q))编码转换公式进行优化.通过分析当验证这些模态算子时fsm(finitestatemachine)的状态转移和线性时序逻辑(linear-timetemporallogic,简称ltl)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成sat(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成sat实例规模和易求解方面都优于bmc中求解这些模态算子的现有的两种重要方法aa_bmc和timo_bmc.所给出的方法和思想对于bmc中验证其他模态算子时的编码优化也有参考价值.