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

A decision algorithm for iteration-free CPDL based on OBDD

作　　者：覃凤萍[1] 古天龙[1] 常亮[1] 

机构地区：[1]桂林电子科技大学计算机科学与工程学院,广西桂林541004

出　　处：《桂林电子科技大学学报》2011年第3期221-225,共5页Journal of Guilin University of Electronic Technology

基　　金：国家自然科学基金(60963010)

摘　　要：命题动态逻辑是一种应用模态逻辑,用于程序行为的推理。Iteration-free CPDL是一种无迭代算子而含有逆算子的命题动态逻辑。对于给定的Iteration-free CPDL公式集,方法是应用NCNF变换和FLAT规则对其进行预处理,并对公式集重构模型,然后将其转化为布尔函数,并利用OBDD来表示,从而调用已有的OBDD软件包进行可满足性判定。最终结合实例验证了算法的可行性及正确性。Propositional dynamic logic is one of the simplest applied modal logics designed for reasoning the behavior of programs.Iteration-free CPDL is an iteration-free fragment of propositional dynamic logic with converse of programs.Starting from a CPDL formulas,the NCNF transformation rule and the FLAT rule are used to do some preprocessing in the algorithm,then the model of set of the formulas is reconstructed and transformed into the boolean formulas,finally these boolean formulas are represented as OBDDs,the satisfiability-checking of set of the formulas is done based on the existing OBDD software package that can be called.The algorithm of iteration-free CPDL is verified feasible and accurate.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]