中文摘要：

模型检验的智能规划方法具有较高的求解效率,是当今通用智能规划研究的热点。由于模型检验的命题动态逻辑规划方法无法从拆卸角度求解规划问题,给出了含逆反动作的命题动态逻辑的符号模型检验算法,开发了CPDL符号化模型检验工具;针对一般智能规划问题中的机械装配序列规划问题,从装配体的拆卸出发,给出了基于CPDL模型检验技术的装配序列求解方法,并结合实例验证了该方法的可行性。

英文摘要：

The artificial intelligence planning by model checking has become a hot spot in AI planning because of its higher efficiency.Propositional dynamic logic planning based on model checking can not solve planning problem with disassembly.A symbolic model checking algorithm for proposition dynamic logic with converse is presented in this paper.The CPDL symbolic model checker is implemented.We give the solution of CPDL symbolic model checking for assembly sequence planning which is one of AI planning.The feasibility of this method is verified by an example.