命题动态逻辑(propositional dynamic logic.简称PDL)最初是由Fischer和Ladner在上世纪70年代末引入的,已成为计算机科学中一种有价值的理论工具。PDL不但用于程序形式化描述和推理,而且还能够提供合适的形式框架对动作进行刻画和推理,是在此基础上进行规划求解的一种有效工具。PDL模型检测是对程序或动作进行形式化规约和验证的有效方式,现有的模型检测算法是基于关系矩阵表示和实现。基于 OBDD的符号技术极大的提高了模型检测的效率,在时态逻辑模型检测中取得了成功的应用。为了使符号技术应用于命题动态逻辑模型检测,提高PDL模型检测的效率,本文对PDL符号模型检测技术进行了研究。在此基础上,针对PDL规划问题,本文研究了符号模型检测技术在PDL规划求解中的应用。本文的具体研究成果如下:　　(1)给出了基于OBDD的PDL模型检测算法。在分析其他逻辑符号模型检测方法的基础上,建立了基于OBDD的PDL符号模型;给出了基于OBDD的PDL模型检测算法;证明和实例验证该算法是正确可行的;实验说明,PDL规范可以采用符号技术进行有效的验证。　　(2)设计并实现了PDL符号模型检测工具。借鉴时态逻辑模型检测工具的实现方法,设计并实现了PDL符号模型检测工具,能够对正则PDL公式进行模型检测;实验表明,PDL符号模型检测工具的效率优于现有的PDL模型检测工具。　　(3)提出了基于模型检测求解PDL规划算法。应用PDL去描述规划问题,论证了PDL规划可以通过模型检测的方法求解;给出基于模型检测的PDL规划符号算法;结合实例验证算法的正确性。