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

摘要

命题动态逻辑是一种应用模态逻辑,用于程序行为的推理.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.