版權說明:本文檔由用戶提供并上傳,收益歸屬內容提供方,若內容存在侵權,請進行舉報或認領
文檔簡介
1、模型檢測是一種被廣泛應用的驗證有限狀態(tài)系統(tǒng)性質的自動化驗證技術。經(jīng)過三十多年的研究發(fā)展,時態(tài)邏輯LTL和CTL的模型檢測問題已經(jīng)得到了很好的解決。不僅提出了各種高效的實現(xiàn)算法,而且開發(fā)了SPIN、SMV等多種驗證工具予以支撐,使得該技術在通訊協(xié)議驗證、計算機系統(tǒng)驗證等多領域得到了廣泛的應用。
傳統(tǒng)的模型檢測技術都是基于命題邏輯對系統(tǒng)模型及其性質進行刻畫的,然而命題邏輯的描述能力有限,這使得模型檢測的應用范圍受到限制。時態(tài)描述邏
2、輯將描述邏輯的刻畫能力引入到命題時態(tài)邏輯中,增強了時態(tài)邏輯的刻畫能力,尤為適用于在語義 Web環(huán)境下對考察對象的時態(tài)性質進行刻畫。時態(tài)描述邏輯的模型檢測具有重要的研究意義。
本文以Franz Baader等給出的時態(tài)描述邏輯ALC-LTL為基礎,對時態(tài)描述邏輯的模型檢測問題進行了研究。完成的研究工作主要有:
?定義了時態(tài)描述邏輯ALC-LTL的模型檢測問題,相應地給出了兩個模型檢測算法。一方面,在傳統(tǒng)的用來構建模型的
3、狀態(tài)遷移系統(tǒng)中引入了描述邏輯ALC知識庫,從而可以對所考察的系統(tǒng)的領域知識進行表示;另一方面,使用時態(tài)描述邏輯 ALC-LTL的公式來描述待驗證的時態(tài)規(guī)范。在此基礎上,給出了時態(tài)描述邏輯 ALC-LTL模型檢測問題的形式化定義。針對該模型檢測問題,分別給出了兩個模型檢測算法:算法1將時態(tài)描述邏輯的模型檢測問題轉換成命題時態(tài)邏輯模型檢測問題來解決;算法2借助標記büchi自動機進行檢測。
?在時態(tài)描述邏輯ALC-LTL中引入合取
4、查詢,增強對時態(tài)規(guī)范的刻畫能力;相應地為擴展后的模型檢測問題給出了模型檢測算法。模型檢測算法由三個步驟組成:首先,根據(jù)時態(tài)規(guī)范中涉及的合取查詢從描述邏輯的角度在系統(tǒng)狀態(tài)中進行推理和檢索,求出所有滿足合取查詢的實例;其次,將這些實例映射為命題并帶入時態(tài)規(guī)范中,將 ALC-LTL的模型檢測問題轉換為命題 LTL的模型檢測問題;最后調用LTL的模型檢測算法完成規(guī)范驗證。
?對含有合取查詢的時態(tài)描述邏輯ALC-LTL模型檢測算法進行優(yōu)
5、化,給出基于自動機的模型檢測算法。算法首先將時態(tài)規(guī)范的否定形式和系統(tǒng)模型分別構造成標記büchi自動機;然后構造這兩個自動機的乘積自動機。與通常的乘積自動機構造方式不同,這里的乘積自動機構造是以系統(tǒng)模型狀態(tài)轉移為軸逐步生成乘積自動機的各狀態(tài),構造過程中采取措施及時終止不必要的狀態(tài)生成以降低時間開支。
?初步研究了時態(tài)描述邏輯模型檢測問題在語義Web服務驗證中的應用。與傳統(tǒng)時態(tài)邏輯LTL的模型檢測相比,時態(tài)描述邏輯ALC-LTL
溫馨提示
- 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
- 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權益歸上傳用戶所有。
- 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內容里面會有圖紙預覽,若沒有圖紙預覽就沒有圖紙。
- 4. 未經(jīng)權益所有人同意不得將文件中的內容挪作商業(yè)或盈利用途。
- 5. 眾賞文庫僅提供信息存儲空間,僅對用戶上傳內容的表現(xiàn)方式做保護處理,對用戶上傳分享的文檔內容本身不做任何修改或編輯,并不能對任何下載內容負責。
- 6. 下載文件中如有侵權或不適當內容,請與我們聯(lián)系,我們立即糾正。
- 7. 本站不保證下載資源的準確性、安全性和完整性, 同時也不承擔用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。
最新文檔
- 時態(tài)描述邏輯ALC-LTL的推理及應用研究.pdf
- 時態(tài)描述邏輯DL-LiteLTL模型檢測研究.pdf
- 基于描述邏輯的時態(tài)擴充研究及應用.pdf
- 時態(tài)描述邏輯DL-CTL的模型檢測技術研究.pdf
- 模型檢測時態(tài)知識邏輯及其應用.pdf
- 概率時態(tài)知識邏輯的符號模型檢測研究.pdf
- 基于時態(tài)邏輯的UML交互模型檢測研究.pdf
- 命題動態(tài)邏輯模型檢測技術及應用研究.pdf
- 時態(tài)數(shù)據(jù)模型及應用研究.pdf
- 基于時態(tài)認知邏輯的Web服務模型檢測.pdf
- 基于描述邏輯的時態(tài)知識表示與推理研究.pdf
- 時態(tài)認知邏輯的模型檢測與安全協(xié)議驗證.pdf
- 時序動態(tài)描述邏輯TDDLALC的推理機制及應用研究.pdf
- 基于時態(tài)描述邏輯的語義物聯(lián)網(wǎng)服務驗證.pdf
- 基于時態(tài)描述邏輯的語義物聯(lián)網(wǎng)服務驗證
- 命題投影時序邏輯符號模型檢測及其應用研究.pdf
- 基于動作的多智能體系統(tǒng)時態(tài)認知邏輯模型檢測.pdf
- RBAC模型中的時態(tài)研究及應用.pdf
- 基于云計算平臺的時態(tài)邏輯模型檢測算法研究與實現(xiàn).pdf
- 概率和實時時態(tài)認知邏輯模型檢測中的抽象技術.pdf
評論
0/150
提交評論