| 基于OBDD的Iteration-free CPDL判定算法 |
| |
| 引用本文： | 覃凤萍,古天龙,常亮. 基于OBDD的Iteration-free CPDL判定算法[J]. 桂林电子科技大学学报, 2011, 31(3): 221-225 |
| |
| 作者姓名： | 覃凤萍 古天龙 常亮 |
| |
| 作者单位： | 桂林电子科技大学,计算机科学与工程学院,广西,桂林,541004 |
| |
| 摘 要： | 命题动态逻辑是一种应用模态逻辑,用于程序行为的推理.Iteration-free CPDL是一种无迭代算子而含有逆算子的命题动态逻辑.对于给定的Iteration-free CPDL公式集,方法是应用NCNF变换和FLAT规则对其进行预处理,并对公式集重构模型,然后将其转化为布尔函数,并利用OBDD来表示,从而调用已有...
|
| 关 键 词： | 命题动态逻辑 可满足性判定 有序二叉决策图 |
A decision algorithm for iteration-free CPDL based on OBDD |
| |
| Qin Fengping,Gu Tianlong,Chang Liang. A decision algorithm for iteration-free CPDL based on OBDD[J]. Journal of Guilin University of Electronic Technology, 2011, 31(3): 221-225 |
| |
| Authors: | Qin Fengping Gu Tianlong Chang Liang |
| |
| Affiliation: | Qin Fengping,Gu Tianlong,Chang Liang(School of Computer Science and Engineering,Guilin University of Electronic Technology,Guilin 541004,China) |
| |
| Abstract: | 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 ... |
| |
| Keywords: | propositional dynamic logic satisfiability-checking ordered binary decision diagram |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
