基于OBDD的Iteration-free CPDL判定算法

摘要：

命题动态逻辑是一种应用模态逻辑,用于程序行为的推理.Iteration-free CPDL是一种无迭代算子而含有逆算子的命题动态逻辑.对于给定的Iteration-free CPDL公式集,方法是应用NCNF变换和FLAT规则对其进行预处理,并对公式集重构模型,然后将其转化为布尔函数,并利用OBDD来表示,从而调用已有的OBDD软件包进行可满足性判定.最终结合实例验证了算法的可行性及正确性.

关键词：命题动态逻辑、可满足性判定、有序二叉决策图

所属期刊栏目：31

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

资助基金：国家自然科学基金60963010

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

页数：共5页

页码：221-225