命题动态逻辑(PDL)是一种应用模态逻辑,用于程序行为的推理。Iteration-free CPDL是一种无迭代算子而含有逆算子的命题动态逻辑。包括Iteration-free CPDL在内的各种命题动态逻辑在程序性质的分析以及动作的刻画和推理等方面具有重要的应用价值。　　命题动态逻辑中一个基本的推理问题是检查公式的可满足性,别的推理问题通常可规约到这一问题。现有的可满足性算法是通常是基于Tableau来实现的。有序二叉决策图(OBDD)是一种有效地表示和处理大规模问题的数据结构,在大规模模型检测和验证等领域已经得到成功应用,在逻辑公式的可满足判定方面也具有巨大的应用潜力。为了使OBDD符号化技术应用于命题动态逻辑可满足性判定,提高PDL算法的效率,本文对OBDD的Iteration-free CPDL可满足性判定算法进行了研究。在此基础上,应用Iteration-free CPDL去描述Web服务组合问题。本文的具体研究成果如下:　　(1)给出了基于OBDD的Iteration-free CPDL判定算法。在分析其他逻辑可满足性判定算法的基础上,重构了公式集模型,给出了基于OBDD的Iteration-free CPDL判定算法;证明和实例验证该算法是正确可行的。　　(2)设计并实现了Iteration-free CPDL可满足性判定系统。借鉴描述逻辑概念可满足性判定推理机的实现方法,设计并实现了Iteration-free CPDL可满足性判定系统,能够对Iteration-free CPDL公式集进行可满足性判定;并将其和Pdlprover进行了比较。　　(3)应用Iteration-free CPDL去描述Web服务组合问题,并对服务组合方法进行了研究,将服务组合规约到Iteration-free CPDL推理问题中,最终利用Iteration-free CPDL公式集的可满足性判定算法进行服务组合。