论文部分内容阅读
装配序列规划作为制造领域的研究热点之一,其好坏直接影响产品的可装配性、装配成本以及装配质量。自上世纪八十年代以来,国内外专家提出了各种各样的装配序列规划求解方法,但到目前为止装配序列规划问题仍然没有得到很好的解决。模型检验集成规划系统(MIPS),以较高的求解效率在国际规划大赛中取得了优良成绩,体现了模型检验技术在智能规划领域中的优势。命题动态逻辑(PDL)具有对动作进行形式化描述和推理的特点,使得PDL模型检验技术能够对系统中动作引起的状态变化进行有效验证。模型检验技术主要通过对状态空间的搜索来验证系统的性质,但是随着状态数目的增加,状态爆炸问题无法避免,有序二叉决策图(OBDD)符号化技术具有对信息进行高效压缩的特点,能够有效地解决状态空间爆炸问题。 本文借助于OBDD符号化技术,对含逆反动作的命题动态逻辑(CPDL)的符号模型检测技术进行了研究。在此基础上,针对装配序列规划,研究了CPDL模型检验技术在装配序列规划问题中的应用。做了如下工作: (1)提出了CPDL的符号化模型检验算法。首先通过对OBDD符号化模型检验技术进行分析,给出了基于OBDD符号化的CPDL模型系统;然后在此模型基础上给出了CPDL符号化模型检验算法;最后对该算法进行了证明并通过实例验证了算法是正确可行的。 (2)设计并实现了CPDL模型检验工具。首先借鉴时态逻辑模型检验技术原理,给出了CPDL模型检验系统框架;然后借助于BuDDy BDD库开发了CPDL模型检验软件;最后通过实例验证了软件的正确性,并通过实验数据对软件进行了分析。 (3)提出了利用CPDL模型检验求解装配序列可行规划解的方法。首先对模型检验求解智能规划问题的一般性原理进行分析,给出了装配模型的构建方法;其次考虑实际的装配过程利用领域的装配知识对模型进行优化;然后利用CPDL语言中的逆反动作算子对拆卸动作进行描述,最后从拆卸角度出发给出了利用CPDL模型检验技术求解装配序列规划可行解的算法。