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

• 作者: 古天龙 常亮 覃凤萍
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: 命题动态逻辑 可满足性判定 有序二叉决策图
• 年，卷（期）: 2011,（3）
• 页码范围: 221-225
• 分类号: TP301
• 字数: 5265字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-808X.2011.03.012

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	古天龙	桂林电子科技大学计算机科学与工程学院	207	1546	18.0	30.0
2	常亮	桂林电子科技大学计算机科学与工程学院	77	450	12.0	17.0
3	覃凤萍	桂林电子科技大学计算机科学与工程学院	1	0	0.0	0.0