時態(tài)描述邏輯ALC-LTL的模型檢測及應(yīng)用研究.pdf

1、模型檢測是一種被廣泛應(yīng)用的驗證有限狀態(tài)系統(tǒng)性質(zhì)的自動化驗證技術(shù)。經(jīng)過三十多年的研究發(fā)展,時態(tài)邏輯LTL和CTL的模型檢測問題已經(jīng)得到了很好的解決。不僅提出了各種高效的實現(xiàn)算法,而且開發(fā)了SPIN、SMV等多種驗證工具予以支撐,使得該技術(shù)在通訊協(xié)議驗證、計算機系統(tǒng)驗證等多領(lǐng)域得到了廣泛的應(yīng)用。
　　傳統(tǒng)的模型檢測技術(shù)都是基于命題邏輯對系統(tǒng)模型及其性質(zhì)進行刻畫的,然而命題邏輯的描述能力有限,這使得模型檢測的應(yīng)用范圍受到限制。時態(tài)描述邏

2、輯將描述邏輯的刻畫能力引入到命題時態(tài)邏輯中,增強了時態(tài)邏輯的刻畫能力,尤為適用于在語義 Web環(huán)境下對考察對象的時態(tài)性質(zhì)進行刻畫。時態(tài)描述邏輯的模型檢測具有重要的研究意義。
　　本文以Franz Baader等給出的時態(tài)描述邏輯ALC-LTL為基礎(chǔ),對時態(tài)描述邏輯的模型檢測問題進行了研究。完成的研究工作主要有:
　　?定義了時態(tài)描述邏輯ALC-LTL的模型檢測問題,相應(yīng)地給出了兩個模型檢測算法。一方面,在傳統(tǒng)的用來構(gòu)建模型的

3、狀態(tài)遷移系統(tǒng)中引入了描述邏輯ALC知識庫,從而可以對所考察的系統(tǒng)的領(lǐng)域知識進行表示;另一方面,使用時態(tài)描述邏輯 ALC-LTL的公式來描述待驗證的時態(tài)規(guī)范。在此基礎(chǔ)上,給出了時態(tài)描述邏輯 ALC-LTL模型檢測問題的形式化定義。針對該模型檢測問題,分別給出了兩個模型檢測算法:算法1將時態(tài)描述邏輯的模型檢測問題轉(zhuǎn)換成命題時態(tài)邏輯模型檢測問題來解決;算法2借助標記büchi自動機進行檢測。
　　?在時態(tài)描述邏輯ALC-LTL中引入合取

4、查詢,增強對時態(tài)規(guī)范的刻畫能力;相應(yīng)地為擴展后的模型檢測問題給出了模型檢測算法。模型檢測算法由三個步驟組成:首先,根據(jù)時態(tài)規(guī)范中涉及的合取查詢從描述邏輯的角度在系統(tǒng)狀態(tài)中進行推理和檢索,求出所有滿足合取查詢的實例;其次,將這些實例映射為命題并帶入時態(tài)規(guī)范中,將 ALC-LTL的模型檢測問題轉(zhuǎn)換為命題 LTL的模型檢測問題;最后調(diào)用LTL的模型檢測算法完成規(guī)范驗證。
　　?對含有合取查詢的時態(tài)描述邏輯ALC-LTL模型檢測算法進行優(yōu)

5、化,給出基于自動機的模型檢測算法。算法首先將時態(tài)規(guī)范的否定形式和系統(tǒng)模型分別構(gòu)造成標記büchi自動機;然后構(gòu)造這兩個自動機的乘積自動機。與通常的乘積自動機構(gòu)造方式不同,這里的乘積自動機構(gòu)造是以系統(tǒng)模型狀態(tài)轉(zhuǎn)移為軸逐步生成乘積自動機的各狀態(tài),構(gòu)造過程中采取措施及時終止不必要的狀態(tài)生成以降低時間開支。
　　?初步研究了時態(tài)描述邏輯模型檢測問題在語義Web服務(wù)驗證中的應(yīng)用。與傳統(tǒng)時態(tài)邏輯LTL的模型檢測相比,時態(tài)描述邏輯ALC-LTL