欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
G（p）和Gp→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中求解这些模态算子的现有的两种重要方法从BMC和Timo_BMC．所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值．
英文摘要：
This paper optimizes the encoding of verifying G（p） and G（p→F（q）） which are two important and frequently used modal operators in optimization of encoding for bounded model checking （BMC）. Through analysis of the properties of finite state machine （FSM） and LTL （linear-time temporal logic） when verifying these modal operators, it presents a concise recursive formula, which can efficiently translate BMC instances into SAT （satisfiability） instances. The logical properties of these recursion formulas are verified. The experimental comparison between the optimization of BMC and the other two important methods AA_BMC and Timo_BMC for solving these modal operators in BMC shows that the former is superior to the latter in both the scale of instances and the difficulty to solve the problem. Research of this paper is also beneficial to encoding optimization of verifying other modal operators in BMC.
同期刊论文项目
同项目期刊论文
期刊信息
位置：