隨著計算機軟硬件系統(tǒng)日益復(fù)雜,如何保證其正確性和可靠性,已成為大家廣泛探討的問題.模型檢測由于其借助嚴格的數(shù)學(xué)方法來驗證系統(tǒng)是否滿足性質(zhì)和自動化驗證等特點,深受學(xué)術(shù)界和工業(yè)界的關(guān)注.經(jīng)典的模型檢測是一種定性的驗證方法,其強調(diào)的是系統(tǒng)滿足功能需求性質(zhì)的絕對正確.然而很多實際的系統(tǒng)被賦予量化行為特征,需要定量分析其滿足用戶的功能和非功能需求性質(zhì)的程度.近年來,學(xué)者們開始研究定量的模型檢測.定量的模型檢測不僅能體現(xiàn)系統(tǒng)多大程度滿足其功能需求性質(zhì),還能體現(xiàn)系統(tǒng)的性能指標(biāo)等非功能需求,極大地拓展了模型檢測的應(yīng)用范圍.定量的模型檢測包括概率模型檢測和模糊模型檢測,其中概率模型檢測用于驗證概率系統(tǒng),對具有不確定信息和不相容信息的非概率系統(tǒng),學(xué)者們提出了模糊模型檢測.廣義可能性模型檢測是模糊模型檢測的主要形式之一,由于其考慮了測度信息,它能更完善地驗證模糊系統(tǒng)的性質(zhì).本文主要針對模糊系統(tǒng),引入廣義可能性決策過程（generalized possibilistic decision process,GPDP）模型來描述此類模糊系統(tǒng)的行為.利用可能性測度理論和決策過程的相關(guān)理論,將經(jīng)典的計算樹邏輯（Com... 

【文章頁數(shù)】：117 頁

【學(xué)位級別】：博士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景與意義
    1.2 模型檢測技術(shù)研究現(xiàn)狀
    1.3 本文的主要工作
第二章 預(yù)備知識
    2.1 Kripke結(jié)構(gòu)
    2.2 時態(tài)邏輯
        2.2.1 線性時序邏輯(LTL)
        2.2.2 計算樹邏輯(CTL)
        2.2.3 分支時態(tài)邏輯(CTL~*)
    2.3 模糊集和模糊矩陣的基本概念
    2.4 可能性測度理論
    2.5 廣義可能性Kripke結(jié)構(gòu)及其廣義可能性測度
    2.6 Knaster-Tarski不動點定理
第三章 基于決策過程的廣義可能性CTL模型檢測
    3.1 廣義可能性決策過程
    3.2 廣義可能性計算樹邏輯
    3.3 廣義可能性計算樹模型檢測
    3.4 實例應(yīng)用
    3.5 本章小結(jié)
第四章 基于決策過程的廣義可能性線性時間屬性模型檢測
    4.1 廣義可能性線性時間屬性
    4.2 廣義可能性線性時間屬性的可達可能性
        4.2.1 最終可達事件的可能性
        4.2.2 總是可達事件的可能性
        4.2.3 限制可達事件的可能性
        4.2.4 重復(fù)可達事件的可能性
        4.2.5 持久可達事件的可能性
    4.3 廣義可能性線性時間屬性的可能性測度
        4.3.1 廣義可能性正則安全屬性的可能性測度
        4.3.2 廣義可能性ω-正則屬性的可能性測度
    4.4 本章小結(jié)
第五章 基于決策過程的GPoCTL~*模型檢測和可能性互模擬
    5.1 GPoCTL~*語法和語義
    5.2 GPoLTL模型檢測算法
        5.2.1 GPoLTL PNF語法和語義
        5.2.2 GPoLTL模型檢測算法
    5.3 GPoCTL~*模型檢測算法
    5.4 最大可能性互模擬及其邏輯刻畫
        5.4.1 最大可能性互模擬
        5.4.2 GPoCTL/GPoCTL~*與最大可能性互模擬的等價性
    5.5 本章小結(jié)
第六章 總結(jié)與展望
    6.1 研究內(nèi)容的總結(jié)
    6.2 研究展望
參考文獻
致謝
攻讀博士學(xué)位期間的研究成果


【參考文獻】：
期刊論文
[1]基于決策過程的廣義可能性計算樹邏輯模型檢測[J]. 馬占有,李永明.  中國科學(xué):信息科學(xué). 2016(11)
[2]廣義可能性決策過程的計算樹邏輯模型檢測[J]. 馬占有,李永明.  計算機工程與科學(xué). 2015(11)
[3]隨機模型檢驗研究[J]. 劉陽,李宣東,馬艷,王林章.  計算機學(xué)報. 2015(11)
[4]一個命題投影時序邏輯符號模型檢測器[J]. 逄濤,段振華,劉曉芳.  軟件學(xué)報. 2015(08)
[5]廣義可能性計算樹邏輯的不動點語義[J]. 鄧楠軼,張興興,李永明.  陜西師范大學(xué)學(xué)報(自然科學(xué)版). 2015(04)
[6]廣義可能性互模擬及其邏輯刻畫[J]. 張興興,鄧楠軼,馬占有,李永明.  計算機工程與科學(xué). 2015(05)
[7]基于廣義可能性測度的可達性問題的模型檢測[J]. 馬占有,李永明.  模糊系統(tǒng)與數(shù)學(xué). 2014(06)
[8]可能LTL模型檢測的兩種方法[J]. 李永明.  陜西師范大學(xué)學(xué)報(自然科學(xué)版). 2014(06)
[9]基于可能性測度的工程管理決策的研究[J]. 李召妮,馬占有,李永明.  計算機科學(xué). 2014(08)
[10]馬爾可夫決策過程的限界模型檢測[J]. 周從華,邢支虎,劉志鋒,王昌達.  計算機學(xué)報. 2013(12)

博士論文
[1]命題投影時序邏輯的完備公理系統(tǒng)與形式驗證[D]. 張南.西安電子科技大學(xué) 2012
[2]狀態(tài)轉(zhuǎn)換系統(tǒng)的格值量化驗證方法研究[D]. 潘海玉.華東師范大學(xué) 2012
[3]多智能體系統(tǒng)的符號模型檢測[D]. 駱翔宇.中山大學(xué) 2006



本文編號：3656031