基于CPDL符號(hào)化模型檢驗(yàn)的裝配序列規(guī)劃研究.pdf

1、裝配序列規(guī)劃作為制造領(lǐng)域的研究熱點(diǎn)之一,其好壞直接影響產(chǎn)品的可裝配性、裝配成本以及裝配質(zhì)量。自上世紀(jì)八十年代以來(lái),國(guó)內(nèi)外專家提出了各種各樣的裝配序列規(guī)劃求解方法,但到目前為止裝配序列規(guī)劃問(wèn)題仍然沒(méi)有得到很好的解決。模型檢驗(yàn)集成規(guī)劃系統(tǒng)(MIPS),以較高的求解效率在國(guó)際規(guī)劃大賽中取得了優(yōu)良成績(jī),體現(xiàn)了模型檢驗(yàn)技術(shù)在智能規(guī)劃領(lǐng)域中的優(yōu)勢(shì)。命題動(dòng)態(tài)邏輯(PDL)具有對(duì)動(dòng)作進(jìn)行形式化描述和推理的特點(diǎn),使得PDL模型檢驗(yàn)技術(shù)能夠?qū)ο到y(tǒng)中動(dòng)作引起

2、的狀態(tài)變化進(jìn)行有效驗(yàn)證。模型檢驗(yàn)技術(shù)主要通過(guò)對(duì)狀態(tài)空間的搜索來(lái)驗(yàn)證系統(tǒng)的性質(zhì),但是隨著狀態(tài)數(shù)目的增加,狀態(tài)爆炸問(wèn)題無(wú)法避免,有序二叉決策圖(OBDD)符號(hào)化技術(shù)具有對(duì)信息進(jìn)行高效壓縮的特點(diǎn),能夠有效地解決狀態(tài)空間爆炸問(wèn)題。
　　本文借助于OBDD符號(hào)化技術(shù),對(duì)含逆反動(dòng)作的命題動(dòng)態(tài)邏輯(CPDL)的符號(hào)模型檢測(cè)技術(shù)進(jìn)行了研究。在此基礎(chǔ)上,針對(duì)裝配序列規(guī)劃,研究了CPDL模型檢驗(yàn)技術(shù)在裝配序列規(guī)劃問(wèn)題中的應(yīng)用。做了如下工作:
　

3、　(1)提出了CPDL的符號(hào)化模型檢驗(yàn)算法。首先通過(guò)對(duì)OBDD符號(hào)化模型檢驗(yàn)技術(shù)進(jìn)行分析,給出了基于OBDD符號(hào)化的CPDL模型系統(tǒng);然后在此模型基礎(chǔ)上給出了CPDL符號(hào)化模型檢驗(yàn)算法;最后對(duì)該算法進(jìn)行了證明并通過(guò)實(shí)例驗(yàn)證了算法是正確可行的。
　　(2)設(shè)計(jì)并實(shí)現(xiàn)了CPDL模型檢驗(yàn)工具。首先借鑒時(shí)態(tài)邏輯模型檢驗(yàn)技術(shù)原理,給出了CPDL模型檢驗(yàn)系統(tǒng)框架;然后借助于BuDDy BDD庫(kù)開(kāi)發(fā)了CPDL模型檢驗(yàn)軟件;最后通過(guò)實(shí)例驗(yàn)證了軟件