基于模型检测的命题动态逻辑规划

摘要：

命题动态逻辑是对动作进行刻画和推理,并在此基础上进行规划求解的一种有效工具.PDL规划问题一般通过逻辑推演进行求解,其本质是将规划问题转化为PDL公式的可满足性问题,相应的推理复杂度为EXP-完全.与可满足性推理相对应,PDL模型检测问题具有多项式级别的时间复杂度.鉴于PDL模型检测的高效,对基于模型检测的PDL规划求解进行研究,从PDL规划语义的角度证明了PDL规划可以通过模型检测的方法求解,在这基础上给出基于模型检测的PDL规划算法,结合实例验证了算法的正确性.

关键词：动态命题逻辑、模型检测、规划

所属期刊栏目：30

分类号：TP301(计算技术、计算机技术)

资助基金：广西自然科学基金0832006Z

在线出版日期：2010-06-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：150-153