基于cpdl符号化模型检验的装配序列规划研究

《基于cpdl符号化模型检验的装配序列规划研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、独创性（或创新性）声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中不包含其他人已经发表或撰写过的研究成果；也不包含为获得桂林电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。申请学位论文与资料若有不实之处，本人承担一切相关责任。本人签名：日期：关于论文使用授权的说明本人完全了解桂林电子科技大学有关保留和使用学位论文的规定，即：研究生在校攻读学位期间论文工作的知识产权单位属桂林

2、电子科技大学。本人保证毕业离校后，发表论文或使用论文工作成果时署名单位仍然为桂林电子科技大学。学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内容，可以允许采用影印、缩印或其它复制手段保存论文。（保密的论文在解密后遵守此规定）本学位论文属于保密在____年解密后适用本授权书。本人签名：日期：导师签名：日期：万方数据摘要摘要装配序列规划作为制造领域的研究热点之一，其好坏直接影响产品的可装配性、装配成本以及装配质量。自上世纪八十年代以来，国内外专家提出了各种各样的装配序列规划求解方法，但到目前为止装配序列规划问题仍然没有

3、得到很好的解决。模型检验集成规划系统(MIPS)，以较高的求解效率在国际规划大赛中取得了优良成绩，体现了模型检验技术在智能规划领域中的优势。命题动态逻辑(PDL)具有对动作进行形式化描述和推理的特点，使得PDL模型检验技术能够对系统中动作引起的状态变化进行有效验证。模型检验技术主要通过对状态空间的搜索来验证系统的性质，但是随着状态数目的增加，状态爆炸问题无法避免，有序二叉决策图(OBDD)符号化技术具有对信息进行高效压缩的特点，能够有效地解决状态空间爆炸问题。本文借助于OBDD符号化技术，对含逆反动作的命题动态逻辑(CPDL)的符号模型检测技术进

4、行了研究。在此基础上，针对装配序列规划，研究了CPDL模型检验技术在装配序列规划问题中的应用。做了如下工作：(1)提出了CPDL的符号化模型检验算法。首先通过对OBDD符号化模型检验技术进行分析，给出了基于OBDD符号化的CPDL模型系统；然后在此模型基础上给出了CPDL符号化模型检验算法；最后对该算法进行了证明并通过实例验证了算法是正确可行的。(2)设计并实现了CPDL模型检验工具。首先借鉴时态逻辑模型检验技术原理，给出了CPDL模型检验系统框架；然后借助于BuDDyBDD库开发了CPDL模型检验软件；最后通过实例验证了软件的正确性，并通过实验

5、数据对软件进行了分析。(3)提出了利用CPDL模型检验求解装配序列可行规划解的方法。首先对模型检验求解智能规划问题的一般性原理进行分析，给出了装配模型的构建方法；其次考虑实际的装配过程利用领域的装配知识对模型进行优化；然后利用CPDL语言中的逆反动作算子对拆卸动作进行描述，最后从拆卸角度出发给出了利用CPDL模型检验技术求解装配序列规划可行解的算法。关键字：装配序列规划；CPDL；OBDD；模型检验；拆卸I万方数据AbstractAbstractAssemblysequenceplanning(ASP)isoneofhotspotsinthema

6、nufacturing;it’sdirectlyimpactoftheproductassembly,thecostsandthequality.Fromtheeightiesoflastcenturytonow,allkindsofASPmethodhavebeenprovidedbyexpertsfromhomeandabroad,buteachofthemisfarfromperfect.TheModelCheckingIntegratedPlanningSystem(MIPS)gotabrilliantsuccessinInternati

7、onalPlanningCompetitionbecauseofitshighamplificationefficiency,andshowitsadvantagesinAI.Propositionaldynamiclogic(PDL)isaneffectivewaytoformallydescriptandreasonforact,andPDLmodelcheckingcanverifystatesofsystemwhichchangedbyaction.Modelcheckingtechnologymainlyverifythepropert

8、iesoverthesystemthroughexhaustiveenumerationofallstatesreachable.Wit