時(shí)態(tài)描述邏輯DL-CTL的模型檢測(cè)技術(shù)研究.pdf

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

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

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

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