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

命题动态逻辑是一种应用模态逻辑,用于程序行为的推理。Iteration—free CPDL是一种无迭代算子而含有逆算子的命题动态逻辑。PDL不但用于程序形式化描述和推理。而且还能够提供合适的形式框架对动作进行刻画和推理,可用其进行web服务组合。