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

【文章來(lái)源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

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

【學(xué)位級(jí)別】：碩士

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


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

博士論文
[1]LTLC：面向?qū)崟r(shí)與混成系統(tǒng)的連續(xù)時(shí)序邏輯[D]. 李廣元.中國(guó)科學(xué)院軟件研究所 2001



本文編號(hào)：3608832