本文主要研究命題投影時序邏輯（Propositional Projection Temporal Logic, PPTL）的可判定性問題。文中簡要地介紹了PPTL公式的語法、語義及邏輯規(guī)則,定義了PPTL公式的正則形（Normal Form）和完備正則形（Complete Normal Form）。在正則形的基礎上,給出PPTL公式正則圖（Normal Form Graph）的歸納定義和可執(zhí)行的算法,證明了該算法的可終止性�；谡齽t圖,PPTL公式在無窮區(qū)間范圍的可判定性問題得到解決。另外,本文也給出了命題區(qū)間時序邏輯（Propositional Interval Temporal Logic, PITL）在無窮區(qū)間范圍的判定過程。邏輯的可判定性是基于該邏輯的模型檢測方法的基礎,本文給出的判定算法證實了基于PPTL的模型檢測方法的可行性。文章最后回顧了模型檢測工具的發(fā)展現(xiàn)狀,分析了以PPTL為邏輯基礎的模型檢測工具的優(yōu)越性,闡明了開發(fā)基于PPTL的模型檢測器的必要性,且給出了基于PPTL的模型檢測器的概要設計。 

【文章來源】：西安電子科技大學陜西省 211工程院校 教育部直屬院校

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

【學位級別】：碩士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 形式化驗證
    1.2 模型檢測
        1.2.1 模型檢測簡介
        1.2.2 模型驗證方法
        1.2.3 模型檢測的發(fā)展
    1.3 時序邏輯
    1.4 區(qū)間時序邏輯的研究現(xiàn)狀
    1.5 論文組織結構
第二章 命題投影時序邏輯
    2.1 命題投影時序邏輯
        2.1.1 PPTL 的語法
        2.1.2 PPTL 的語義
        2.1.3 可滿足性與有效性
        2.1.4 優(yōu)先級
        2.1.5 邏輯規(guī)則
    2.2 PPTL 與PITL 的比較
        2.2.1 chop 操作符的區(qū)別
        2.2.2 時序操作符prj 與proj
        2.2.3 投影應用實例
第三章 PPTL 公式的可判定性
    3.1 PPTL 公式的正則形
    3.2 PPTL 公式的正則圖
        3.2.1 NFG 的定義
        3.2.2 NFG 的分類
        3.2.3 NFG 的構造算法
        3.2.4 NFG 的有窮性證明
    3.3 PPTL 公式可滿足性的判定過程
        3.3.1 路徑與模型
        3.3.2 PPTL 公式可滿足性的判定過程
        3.3.3 應用實例
第四章 PITL 可滿足性的判定過程
    4.1 命題區(qū)間時序邏輯(PITL)
    4.2 PITL 公式可滿足性的判定過程
第五章 模型檢測
    5.1 模型檢測工具的研究現(xiàn)狀
    5.2 基于PPTL 的模型檢測工具
總結與展望
致謝
參考文獻
研究成果


【參考文獻】：
期刊論文
[1]基于PVS的UML類圖和序列圖的一致性檢驗[J]. 劉曉健,陳平.  系統(tǒng)工程與電子技術. 2004(10)
[2]基于PVS的飛機訂票系統(tǒng)的形式化描述與驗證[J]. 楊紅麗,劉建元,韓俊剛.  西安郵電學院學報. 2001(03)

博士論文
[1]LTLC：面向實時與混成系統(tǒng)的連續(xù)時序邏輯[D]. 李廣元.中國科學院軟件研究所 2001



本文編號：3608832