經(jīng)典的模型檢測由于其自動化的特點被廣泛用于系統(tǒng)的功能正確性和可靠性驗證,其強(qiáng)調(diào)系統(tǒng)功能的絕對正確,是一種定性的驗證方法.隨著系統(tǒng)日益復(fù)雜,系統(tǒng)中不可避免地會出現(xiàn)一些不確定的信息,這就要求驗證過程中不僅要考慮系統(tǒng)的功能需求,還要考慮系統(tǒng)滿足該功能的可能性或精確度.為了有效的處理、刻畫信息系統(tǒng)存在的不確定性,人們對這些不確定性信息進(jìn)行定量分析,研究了定量的模型檢測.廣義可能性模型檢測作為定量模型檢測主要形式之一,在經(jīng)典的時序邏輯上引入了可能性測度,不僅可以處理不滿足測度可加性的模糊不確定現(xiàn)象,而且使時態(tài)性質(zhì)可度量化,可以更加完整地驗證系統(tǒng)的性質(zhì).廣義可能性模型檢測的研究目前處于發(fā)展階段,還有很多工作亟待解決.本文首先利用經(jīng)典模型的驗證方法解決廣義可能性模型檢測問題,其結(jié)果豐富了廣義可能性模型檢測的研究方法,并有助于彌補(bǔ)其在模型檢測工具方面的不足.其次,為了限制時序邏輯中不合理的屬性發(fā)生,進(jìn)而研究具有公平性約束的廣義可能性時序邏輯.由于廣義可能性時序邏輯只是對邏輯聯(lián)結(jié)詞和命題的模糊化,不能表示具有模糊時間特點的時序性質(zhì),引入能表示模糊時間的模糊時態(tài)詞,從而研究能表示模糊時間性質(zhì)的廣義可能性時... 

【文章來源】：陜西師范大學(xué)陜西省211工程院校教育部直屬院校

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

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

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景與意義
    1.2 模型檢測研究現(xiàn)狀
    1.3 本文的主要工作
第二章 預(yù)備知識
    2.1 時序邏輯
        2.1.1 Kripke結(jié)構(gòu)
        2.1.2 線性時序邏輯
        2.1.3 計算樹邏輯
    2.2 廣義可能性時序邏輯
        2.2.1 可能性測度理論
        2.2.2 廣義可能性Kripke結(jié)構(gòu)
        2.2.3 廣義可能性線性時序邏輯
        2.2.4 廣義可能計算樹邏輯
第三章 廣義可能性計算樹邏輯的定量模型檢測
    3.1 廣義可能性計算樹邏輯的模型檢測
        3.1.1 Po(Φ∪Ψ)和Po(□Φ)的等價形式
        3.1.2 計算‖Po(Φ∪Ψ)‖(s)問題歸約
        3.1.3 GPoCTL模型檢測問題歸約
    3.2 具有公平性約束的GPoCTL模型檢測
    3.3 本章小結(jié)
第四章 廣義可能性線性時序邏輯的定量模型檢測
    4.1 廣義可能性線性時序邏輯的模型檢測
        4.1.1 路徑公式的基本性質(zhì)
        4.1.2 GPoLTL模型檢測
        4.1.3 兩類模糊線性時序?qū)傩缘哪Ｐ蜋z測
    4.2 具有公平性約束的GPoLTL模型檢測
    4.3 本章小結(jié)
第五章 具有模糊時態(tài)的GPoLTL模型檢測
    5.1 具有模糊時態(tài)的GPoLTL語構(gòu)和語義
    5.2 幾類具有模糊時間的線性時序?qū)傩?br>    5.3 GPoFLTL的必要性閾值模型檢測
    5.4 本章小結(jié)
第六章 具有模糊時態(tài)的GPoCTL模型檢測
    6.1 具有模糊時態(tài)的GPoCTL語構(gòu)和語義
    6.2 幾類GPoFCTL公式的模型檢測問題
    6.3 本章小結(jié)
第七章 總結(jié)與展望
    7.1 研究內(nèi)容的總結(jié)
    7.2 研究展望
參考文獻(xiàn)
致謝
攻讀博士學(xué)位期間的研究成果


【參考文獻(xiàn)】：
期刊論文
[1]模糊線性時序邏輯的可實現(xiàn)性[J]. 范艷煥,李永明.  電子學(xué)報. 2018(02)
[2]不確定型模糊Kripke結(jié)構(gòu)的計算樹邏輯模型檢測[J]. 范艷煥,李永明,潘海玉.  電子學(xué)報. 2018(01)
[3]具有模糊時態(tài)的廣義可能性線性時序邏輯的模型檢測[J]. 梁常建,李永明.  電子學(xué)報. 2017(12)
[4]廣義可能性計算樹邏輯的模型檢測問題[J]. 梁常建,李永明.  電子學(xué)報. 2017(11)
[5]基于決策過程的廣義可能性計算樹邏輯模型檢測[J]. 馬占有,李永明.  中國科學(xué):信息科學(xué). 2016(11)
[6]廣義可能性計算樹邏輯和計算樹邏輯的關(guān)系[J]. 李丹,李永明.  計算機(jī)科學(xué)與探索. 2017(10)
[7]廣義可能性決策過程的計算樹邏輯模型檢測[J]. 馬占有,李永明.  計算機(jī)工程與科學(xué). 2015(11)
[8]隨機(jī)模型檢驗研究[J]. 劉陽,李宣東,馬艷,王林章.  計算機(jī)學(xué)報. 2015(11)
[9]廣義可能性計算樹邏輯的不動點語義[J]. 鄧楠軼,張興興,李永明.  陜西師范大學(xué)學(xué)報(自然科學(xué)版). 2015(04)
[10]廣義可能性互模擬及其邏輯刻畫[J]. 張興興,鄧楠軼,馬占有,李永明.  計算機(jī)工程與科學(xué). 2015(05)

博士論文
[1]格值交替自動機(jī)的若干問題研究[D]. 魏秀娟.陜西師范大學(xué) 2018
[2]基于決策過程的廣義可能性時態(tài)邏輯模型檢測[D]. 馬占有.陜西師范大學(xué) 2017



本文編號：3639806