10.3969/j.issn.1673-808X.2011.03.012
基于OBDD的Iteration-free CPDL判定算法
命题动态逻辑是一种应用模态逻辑,用于程序行为的推理.Iteration-free CPDL是一种无迭代算子而含有逆算子的命题动态逻辑.对于给定的Iteration-free CPDL公式集,方法是应用NCNF变换和FLAT规则对其进行预处理,并对公式集重构模型,然后将其转化为布尔函数,并利用OBDD来表示,从而调用已有的OBDD软件包进行可满足性判定.最终结合实例验证了算法的可行性及正确性.
命题动态逻辑、可满足性判定、有序二叉决策图
31
TP301(计算技术、计算机技术)
国家自然科学基金60963010
2011-09-27(万方平台首次上网日期,不代表论文的发表时间)
共5页
221-225