1、模型檢測是一種廣泛應(yīng)用的形式化驗證技術(shù)，它不僅有高效的驗證算法作為理論基礎(chǔ)，而且成熟的驗證工具使其在工業(yè)界得到了廣泛的應(yīng)用。描述邏輯（DL）是一種隨著語義Web的發(fā)展而受到廣泛關(guān)注的邏輯系統(tǒng)。它雖然具有表達能力強且可判定的優(yōu)點，但只能刻畫靜態(tài)領(lǐng)域的知識。因此，研究者分別從時態(tài)和動態(tài)領(lǐng)域?qū)γ枋鲞壿嬤M行擴展，分別得到時態(tài)描述邏輯（TDL）和動態(tài)描述邏輯（DDL）。
　　本文主要將描述邏輯的這些擴展引入到模型檢測技術(shù)中。目前，在該領(lǐng)域已

2、經(jīng)有研究成果中，它們驗證的性質(zhì)大都是線性的，雖然也出現(xiàn)了對分支性質(zhì)驗證的嘗試，但并沒有利用描述邏輯豐富的推理機制；與此同時，在將動作理論引入到模型檢測技術(shù)中的時候，僅考慮了原子動作，并沒有考慮諸如“選擇”、“迭代”等動態(tài)描述邏輯DDL中的復雜動作。
　　本文利用分支時態(tài)描述邏輯DL-CTL和動態(tài)描述邏輯DDL，結(jié)合模型檢測技術(shù)，來解決上述的問題，主要的研究內(nèi)容如下：
　　1.研究時態(tài)描述邏輯DL-CTL的模型檢測問題。一方面

3、，在模型建立時，基于描述邏輯DL的知識庫對背景知識和模型中狀態(tài)的性質(zhì)進行描述；另一方面，采用時態(tài)描述邏輯 DL-CTL公式對待驗證的性質(zhì)進行刻畫。最后，形式化地定義時態(tài)描述邏輯DL-CTL模型檢測問題的，并結(jié)合描述邏輯相關(guān)的推理機制，研究得到其模型檢測算法。
　　2.設(shè)計并開發(fā)時態(tài)描述邏輯DL-CTL的模型檢測工具。以研究得到的時態(tài)描述邏輯DL-CTL模型驗證算法為基礎(chǔ)，設(shè)計并開發(fā)了基于DL-CTL的模型驗證工具。該工具能夠完成知

4、識庫的建立、系統(tǒng)模型的創(chuàng)建、時態(tài)公式輸入、驗證等核心功能。利用這些功能，該工具能夠快速方便地驗證時態(tài)邏輯公式在系統(tǒng)模型中是否成立。
　　3.研究引入動作理論的DL-CTL的模型檢測問題。一方面，在傳統(tǒng)的模型檢測技術(shù)基礎(chǔ)上，將動態(tài)描述邏輯DDL中原子動作的執(zhí)行作為系統(tǒng)模型中狀態(tài)間的遷移原因；另一方面，采用時態(tài)描述邏輯DL-CTL公式描述待驗證的時態(tài)規(guī)范。在此基礎(chǔ)上，形式化定義了引入動作理論之后的模型檢測問題。借助描述邏輯成熟的推理機