%0 Journal Article
%T 有界模型检测的优化
%A 杨晋吉？
%A 苏开乐？
%A 骆翔宇？
%A 林瀚？
%A 肖茵茵？
%J 软件学报
%P 2005-2014
%D 2009
%X 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中验证其他模态算子时的编码优化也有参考价值.
%K 模型检测
%K 有界模型检测
%K 可满足性问题
%K 模态算子
%K 递推公式
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3387&flag=1