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

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

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

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

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

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