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

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

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

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