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

• 作者: 古天龙 常亮 韦林
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: 动态命题逻辑 模型检测 规划
• 年，卷（期）: 2010,（2）
• 页码范围: 150-153
• 分类号: TP301
• 字数: 3601字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-808X.2010.02.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	古天龙	桂林电子科技大学计算机与控制学院	207	1546	18.0	30.0
2	常亮	桂林电子科技大学计算机与控制学院	77	450	12.0	17.0
3	韦林	桂林电子科技大学计算机与控制学院	3	20	2.0	3.0