本文關(guān)鍵詞：模態(tài)邏輯的計(jì)量化研究及其在模型檢驗(yàn)中的應(yīng)用

  更多相關(guān)文章： 計(jì)量邏輯學(xué) 模態(tài)邏輯 時(shí)態(tài)邏輯 模型檢驗(yàn) 遷移系統(tǒng) 局部化真度 全局真度 滿(mǎn)足度 極大縮減

【摘要】：本文的目的在于建立模態(tài)邏輯的計(jì)量化理論,并將其基本方法用于解決模型檢驗(yàn)的計(jì)量化問(wèn)題以及簡(jiǎn)化模型檢驗(yàn)的過(guò)程. 計(jì)量邏輯學(xué)的提出旨在將基于概率、積分等工具的數(shù)值計(jì)算方法引入到以形式推理為特色的數(shù)理邏輯中,使原本符號(hào)化的推理具備某種靈活性從而擴(kuò)展其應(yīng)用范圍.這種思想的雛形最初見(jiàn)于從邏輯語(yǔ)義基本概念的程度化入手而在若干命題邏輯系統(tǒng)中所建立的公式真度理論.此后引發(fā)了大量的后續(xù)研究,包括對(duì)邏輯度量空間的拓?fù)湫再|(zhì)與內(nèi)蘊(yùn)結(jié)構(gòu)的研究、對(duì)邏輯理論的發(fā)散度與相容度的研究以及在命題邏輯中建立近似推理的研究等,至今已形成了較為完善和成熟的計(jì)量邏輯學(xué)理論.如今計(jì)量邏輯學(xué)的研究對(duì)象已從命題邏輯的范圍擴(kuò)展到了表達(dá)力更強(qiáng)的模態(tài)邏輯、時(shí)態(tài)邏輯與謂詞邏輯的理論之中.若干將計(jì)量邏輯學(xué)與其他領(lǐng)域相結(jié)合的創(chuàng)新性研究也不斷涌現(xiàn),顯示出了計(jì)量邏輯學(xué)的旺盛生命力與廣闊的應(yīng)用前景.本文的研究目的在于探索計(jì)量邏輯學(xué)與理論計(jì)算機(jī)科學(xué)的新的結(jié)合點(diǎn),將原本在命題邏輯中行之有效的計(jì)量化方法向表達(dá)力更強(qiáng)的模態(tài)邏輯與時(shí)態(tài)邏輯中推廣,并嘗試將其應(yīng)用于以時(shí)態(tài)邏輯為邏輯背景的模型檢驗(yàn)理論之中. 模態(tài)邏輯是非經(jīng)典數(shù)理邏輯與人工智能理論相結(jié)合的一個(gè)重要方面.它不僅是時(shí)態(tài)邏輯、知識(shí)推理的理論基礎(chǔ),又常在應(yīng)用中作為程序語(yǔ)義描述的工具.作為命題邏輯的模式擴(kuò)張,模態(tài)邏輯具有命題邏輯所不具備的特點(diǎn).例如模態(tài)邏輯中有若干可以表達(dá)“可能”、“必然”以及“將來(lái)”、“過(guò)去”等不同類(lèi)型概念的模態(tài)詞,隨著模態(tài)詞的增多,模態(tài)邏輯的表達(dá)能力也隨之增強(qiáng),此外局部概念的引入以及可能世界之間關(guān)系的論述等也使得模態(tài)邏輯具有比命題邏輯強(qiáng)得多的表達(dá)能力.正是由于這些特點(diǎn),使得將原本在命題邏輯中行之有效的計(jì)量化方法向更為廣泛的模態(tài)邏輯中推廣成為了近幾年計(jì)量邏輯學(xué)的基本研究任務(wù)之一.本文將從模態(tài)邏輯Kripke語(yǔ)義的局部化特點(diǎn)出發(fā),建立模態(tài)公式的局部化真度,繼而再利用某種聚合的方法將其推廣為模態(tài)公式的全局真度,從而在模態(tài)邏輯中建立起較為廣泛的計(jì)量邏輯理論. 另一方面,模型檢驗(yàn)是一種形式化的認(rèn)證方法,可以用來(lái)自動(dòng)地檢驗(yàn)?zāi)诚到y(tǒng)的模型是否滿(mǎn)足為該系統(tǒng)設(shè)定的規(guī)范.這一理論已經(jīng)經(jīng)歷了迅速發(fā)展的三十年,受到了人工智能學(xué)界的廣泛關(guān)注,如今已被成功地應(yīng)用于包括工業(yè)、金融、醫(yī)療乃至航空航天等重要領(lǐng)域.注意到模型檢驗(yàn)理論的邏輯背景是某類(lèi)特殊的時(shí)態(tài)邏輯,它們可以看作是模態(tài)邏輯的模式擴(kuò)張.基于這些考慮,本文將進(jìn)一步把針對(duì)模態(tài)邏輯的計(jì)量化理論向這類(lèi)時(shí)態(tài)邏輯中推廣,從一個(gè)全新的角度建立模型檢驗(yàn)中的計(jì)量化理論,并討論如何針對(duì)特殊類(lèi)型的公式來(lái)簡(jiǎn)化模型檢驗(yàn)的過(guò)程. 全文共分為五章： 第一章首先簡(jiǎn)要介紹有關(guān)命題邏輯的若干預(yù)備知識(shí),包括語(yǔ)構(gòu)理論、語(yǔ)義理論和完備性問(wèn)題,并介紹幾種常用的命題邏輯系統(tǒng)；然后從分析將基本邏輯概念進(jìn)行程度化的必要性入手,簡(jiǎn)要介紹計(jì)量邏輯學(xué)的基本理論,包括公式的真度、公式之間的相似度、公式集上的偽距離以及邏輯度量空間等理論. 第二章首先簡(jiǎn)要回顧基本模態(tài)邏輯的語(yǔ)義理論、語(yǔ)構(gòu)理論以及完備性問(wèn)題；其次對(duì)基本模態(tài)邏輯的Kripke語(yǔ)義進(jìn)行推廣,將基本模型中的賦值域擴(kuò)充為完備格,從而建立格值模態(tài)邏輯的Kripke語(yǔ)義,并證明該語(yǔ)義也將模糊模態(tài)邏輯的Kripke語(yǔ)義納入其框架之下；然后以Boole代數(shù)為背景建立Boole型格值模態(tài)邏輯系統(tǒng)B,討論系統(tǒng)B的語(yǔ)義理論與語(yǔ)構(gòu)理論,并證明完備性定理的成立,即,任一模態(tài)公式是系統(tǒng)召中的定理當(dāng)且僅當(dāng)它是有效公式,同時(shí)指出基本模態(tài)邏輯的Kripke模型實(shí)際上是本文所提出的Boole型模態(tài)模型的特例；最后提出QMR0代數(shù)的概念,并以QMR0代數(shù)為背景構(gòu)建QMR0型格值模態(tài)邏輯系統(tǒng)QML*討論系統(tǒng)QML*的語(yǔ)義理論與語(yǔ)構(gòu)理論,并證明完備性定理的成立,同時(shí)指出模糊模態(tài)邏輯的Kripke模型實(shí)際上是本文提出的QMRo型模態(tài)模型的特例. 第三章首先以單位區(qū)間[0,1]的有限子集作為賦值域,建立多值模態(tài)邏輯的Kripke模型以及相應(yīng)的語(yǔ)義理論,并指出這種模型一方面是第二章提出的格值模態(tài)模型的特例,同時(shí)其Kripke語(yǔ)義又將基本模態(tài)邏輯的Kripke語(yǔ)義納入其框架之下;其次采用固定可能世界集W與二元關(guān)系R而讓賦值映射自由變動(dòng)的方法建立W，R。型框架,并在該框架下用歸納的思想構(gòu)建模態(tài)公式關(guān)于某個(gè)可能世界誘導(dǎo)的局部化映射,從而引入模態(tài)公式的局部化真度概念,證明了這種局部化真度滿(mǎn)足約簡(jiǎn)定理,即,任一模態(tài)公式的局部化真度均可以轉(zhuǎn)化為另一個(gè)不含模態(tài)詞的公式在同一可能世界處的局部化真度,從而達(dá)到簡(jiǎn)化真度計(jì)算的目的;然后進(jìn)一步利用聚合的方法將這種局部化真度推廣為模態(tài)公式的全局真度,并證明全局真度滿(mǎn)足一致性定理,即,當(dāng)某模態(tài)公式不含模態(tài)詞時(shí),其全局真度與其在命題邏輯中的真度一致：同時(shí)證明了模態(tài)公式的局部化真度值與可能世界集的勢(shì)并無(wú)關(guān)系,且其全局真度能夠較好地反應(yīng)時(shí)態(tài)邏輯的語(yǔ)義特點(diǎn)；最后引入模態(tài)公式之間的相似度與偽距離.從而建立起多值模態(tài)邏輯度量空間,并證明基于命題邏輯的度量空間是多值模態(tài)邏輯度量空間的子空間. 第四章首先簡(jiǎn)要回顧模型檢驗(yàn)理論中有關(guān)遷移系統(tǒng)以及線(xiàn)性時(shí)態(tài)邏輯LTL的基本概念；其次在有限遷移系統(tǒng)的全體無(wú)窮初始路徑之集上引入某種適當(dāng)?shù)木鶆蚋怕蕼y(cè)度.并基于該測(cè)度考慮遷移系統(tǒng)TS中滿(mǎn)足某個(gè)LTL公式φ的路徑占總路徑的比例,從而定義遷移系統(tǒng)TS對(duì)于公式φ的滿(mǎn)足度,即TS滿(mǎn)足φ的程度,同時(shí)在此基礎(chǔ)上引入LTL公式之間的相似度與偽距離,并構(gòu)建線(xiàn)性時(shí)態(tài)邏輯中的度量空間,即LTL邏輯度量空間；然后將以上建立的滿(mǎn)足度理論進(jìn)一步推廣至遷移系統(tǒng)的隨機(jī)化模型,即離散時(shí)間馬爾可夫鏈模型,并類(lèi)似地引入LTL公式的滿(mǎn)足度、相似度與偽距離等概念.此時(shí)不再要求各個(gè)狀態(tài)之間相互遷移的概率是等值分布的.從而全體無(wú)窮初始路徑之集上的概率測(cè)度也不是均勻分布的；最后引入線(xiàn)性時(shí)態(tài)邏輯中公式的特征與時(shí)態(tài)范式等概念,指出存在特征的LTL公式在模型檢驗(yàn)中總可以在有限步內(nèi)判斷其有效性,即使相應(yīng)的遷移系統(tǒng)含有無(wú)限多個(gè)狀態(tài)時(shí)也是如此,并證明了LTL公式有與其等價(jià)的時(shí)態(tài)范式當(dāng)且僅當(dāng)其存在特征,從而一類(lèi)特殊的LTL公式可以用線(xiàn)性時(shí)態(tài)邏輯的有界情形LTLn來(lái)刻畫(huà). 第五章首先在一般Boole代數(shù)中引入推演元的概念,并針對(duì)Boole代數(shù)建立相應(yīng)的協(xié)調(diào)集理論;其次在一般Boole代數(shù)中引入反駁、極大縮減、極小減集等概念,并分別給出Boole代數(shù)中求某個(gè)有限不協(xié)調(diào)集的全體極小不協(xié)調(diào)子集以及求有限個(gè)集合的全體極小選擇的算法原理,從而給出求全體極大縮減的方法,同時(shí)指出在一階語(yǔ)言范圍內(nèi)求全體R-縮減的問(wèn)題可以轉(zhuǎn)化至Boole代數(shù)的范圍內(nèi)求解;最后在Boole代數(shù)中引入基本元的概念,并將子句及Horn子句等概念移植到一類(lèi)由基本元生成的特殊Boole代數(shù)中,從而在這類(lèi)特殊Boole代數(shù)中給出求子句集的全體極大縮減的算法原理,同時(shí)指出經(jīng)典二值命題邏輯中求子句集(特別是Horn子句集)的全體R-縮減的問(wèn)題可以轉(zhuǎn)化至由基本元生成的Boole代數(shù)范圍內(nèi)求解.
【關(guān)鍵詞】：計(jì)量邏輯學(xué) 模態(tài)邏輯 時(shí)態(tài)邏輯 模型檢驗(yàn) 遷移系統(tǒng) 局部化真度 全局真度 滿(mǎn)足度 極大縮減
【學(xué)位授予單位】：陜西師范大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2013
【分類(lèi)號(hào)】：O141.1
【目錄】：

• 摘要3-6
• Abstract6-12
• 前言12-16
• 第1章 命題邏輯與計(jì)量邏輯學(xué)簡(jiǎn)介16-28
• 1.1 命題邏輯系統(tǒng)及其完備性16-23
• 1.1.1 命題邏輯系統(tǒng)16-17
• 1.1.2 邏輯系統(tǒng)的完備性17-18
• 1.1.3 若干常用的命題邏輯系統(tǒng)18-23
• 1.2 計(jì)量邏輯學(xué)基本理論簡(jiǎn)介23-28
• 1.2.1 經(jīng)典二值命題邏輯系統(tǒng)L中的計(jì)量邏輯理論23-25
• 1.2.2 Lukasiewicz命題邏輯系統(tǒng)Luk與L_n中的計(jì)量邏輯理論25-27
• 1.2.3 R_0型命題邏輯系統(tǒng)L~*與L_n~*中的計(jì)量邏輯理論27-28
• 第2章 格值模態(tài)邏輯及其完備性28-46
• 2.1 基本模態(tài)邏輯28-31
• 2.1.1 基本模態(tài)邏輯的Kripke模型29-30
• 2.1.2 基本模態(tài)邏輯系統(tǒng)K的完備性30-31
• 2.2 格值模態(tài)邏輯的Kripke語(yǔ)義31-34
• 2.3 Boole型格值模態(tài)邏輯系統(tǒng)B及其完備性34-37
• 2.3.1 系統(tǒng)B的語(yǔ)義理論34-35
• 2.3.2 系統(tǒng)B的語(yǔ)構(gòu)理論及完備性35-37
• 2.4 QMR_0型格值模態(tài)邏輯系統(tǒng)QML~*及其完備性37-46
• 2.4.1 系統(tǒng)QML~*的語(yǔ)義理論38-40
• 2.4.2 系統(tǒng)QML~*的語(yǔ)構(gòu)理論40-42
• 2.4.3 系統(tǒng)QML~*的完備性42-46
• 第3章 多值模態(tài)邏輯的計(jì)量化方法46-74
• 3.1 多值模態(tài)邏輯的Kripke語(yǔ)義47-51
• 3.2 多值模態(tài)邏輯中模態(tài)公式的局部化真度51-59
• 3.2.1 模態(tài)公式誘導(dǎo)的局部化映射51-54
• 3.2.2 模態(tài)公式的局部化真度54-57
• 3.2.3 局部化真度的約簡(jiǎn)定理57-59
• 3.3 多值模態(tài)邏輯中模態(tài)公式的全局真度59-67
• 3.3.1 模態(tài)公式的全局真度59-60
• 3.3.2 全局真度的一致性定理60-62
• 3.3.3 永真公式62-66
• 3.3.4 全局真度在時(shí)態(tài)邏輯中的應(yīng)用66-67
• 3.4 多值模態(tài)邏輯度量空間67-74
• 3.4.1 模態(tài)公式間的局部化相似度與偽距離67-70
• 3.4.2 k模態(tài)度量空間70-74
• 第4章 模型檢驗(yàn)中的計(jì)量化方法74-106
• 4.1 遷移系統(tǒng)與線(xiàn)性時(shí)態(tài)邏輯75-79
• 4.1.1 遷移系統(tǒng)75-76
• 4.1.2 線(xiàn)性時(shí)態(tài)邏輯LTL76-79
• 4.2 LTL中基于遷移系統(tǒng)的計(jì)量化方法79-90
• 4.2.1 單初始有限遷移系統(tǒng)中的概率測(cè)度79-82
• 4.2.2 基于單初始有限遷移系統(tǒng)的LTL公式的滿(mǎn)足度82-86
• 4.2.3 基于多初始有限遷移系統(tǒng)的LTL公式的滿(mǎn)足度86-88
• 4.2.4 基于有限遷移系統(tǒng)的LTL邏輯度量空間88-90
• 4.3 LTL中基于離散時(shí)間馬爾可夫鏈的計(jì)量化方法90-98
• 4.3.1 離散時(shí)間馬爾可夫鏈DTMC90-92
• 4.3.2 DTMC中的概率測(cè)度92-93
• 4.3.3 基于有限D(zhuǎn)TMC的LTL公式的滿(mǎn)足度93-96
• 4.3.4 基于有限D(zhuǎn)TMC的LTL邏輯度量空間96-98
• 4.4 線(xiàn)性時(shí)態(tài)邏輯中的時(shí)態(tài)范式98-106
• 4.4.1 LTL公式的特征98-101
• 4.4.2 LTL公式的時(shí)態(tài)范式101-106
• 第5章 Boole代數(shù)中的極大縮減106-120
• 5.1 Boole代數(shù)中的協(xié)調(diào)集106-109
• 5.2 Boole代數(shù)中的極大縮減109-117
• 5.2.1 極大縮減與極小減集109-113
• 5.2.2 求解極大縮減的算法原理113-117
• 5.3 由基本元生成的Boole代數(shù)及其極大縮減117-120
• 總結(jié)120-122
• 參考文獻(xiàn)122-132
• 致謝132-134
• 攻讀學(xué)位期間的科研成果與獲獎(jiǎng)情況134-135

【相似文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前10條

1 王浦;;中國(guó)住宅房地產(chǎn)價(jià)格影響因素實(shí)證分析[J];中國(guó)集體經(jīng)濟(jì);2008年Z1期

2 陳娟;內(nèi)蒙古包頭市昆都侖河降雨徑流的模擬[J];四川大學(xué)學(xué)報(bào)(工程科學(xué)版);2003年01期

3 顏小飛;黃嵐;王忠義;王成;;植物葉肉細(xì)胞電信號(hào)模型與仿真研究[J];計(jì)算機(jī)仿真;2008年11期

4 陳子俠;李棟;;基于改進(jìn)灰色理論的城市物流量預(yù)測(cè)——以浙江龍泉為例[J];中國(guó)管理信息化;2009年08期

5 徐鳳麗;;對(duì)中國(guó)城鎮(zhèn)居民消費(fèi)函數(shù)的探討[J];經(jīng)營(yíng)管理者;2009年17期

6 時(shí)麗娜;黃漢明;李小勇;唐賢健;潘士虎;;基于等維灰數(shù)遞補(bǔ)動(dòng)態(tài)模型的人口老齡化趨勢(shì)預(yù)測(cè)[J];魯東大學(xué)學(xué)報(bào)(自然科學(xué)版);2009年04期

7 龔亮;陳懷錄;張淑娟;;灰色模型在甘肅省人口預(yù)測(cè)中的應(yīng)用[J];甘肅科技;2010年16期

8 王士鐵;模態(tài)邏輯與程序驗(yàn)證[J];廈門(mén)大學(xué)學(xué)報(bào)(自然科學(xué)版);1985年03期

9 肖慶憲;匯率機(jī)制與匯率模型[J];數(shù)量經(jīng)濟(jì)技術(shù)經(jīng)濟(jì)研究;2002年08期

10 何劍;;IPOs價(jià)格影響因素:一個(gè)定價(jià)模型檢驗(yàn)[J];商場(chǎng)現(xiàn)代化;2006年11期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù) 前10條

1 李文江;陳圖云;;基于模糊測(cè)度的模態(tài)邏輯[A];模糊集理論與應(yīng)用——98年中國(guó)模糊數(shù)學(xué)與模糊系統(tǒng)委員會(huì)第九屆年會(huì)論文選集[C];1998年

2 楚白;;有窮深度的模態(tài)邏輯[A];2005年邏輯研究專(zhuān)輯[C];2005年

3 陳國(guó)勛;閆家杰;;Fuzzy模態(tài)公式的歸約[A];中國(guó)系統(tǒng)工程學(xué)會(huì)模糊數(shù)學(xué)與模糊系統(tǒng)委員會(huì)第五屆年會(huì)論文選集[C];1990年

4 宗群;竇立謙;孫連坤;劉文靜;;基于殘差分析方法的模型檢驗(yàn)[A];第二十七屆中國(guó)控制會(huì)議論文集[C];2008年

5 張丁煜;;門(mén)戶(hù)網(wǎng)站新聞使用比較研究——以中韓兩國(guó)大學(xué)生為例[A];中國(guó)傳媒大學(xué)第五屆全國(guó)新聞學(xué)與傳播學(xué)博士生學(xué)術(shù)研討會(huì)論文集[C];2011年

6 孫希文;;模態(tài)邏輯模型的嵌入定理[A];1994年邏輯研究專(zhuān)輯[C];1994年

7 潘天群;;建立在“笛卡爾公理”上的一個(gè)懷疑邏輯系統(tǒng)[A];邏輯與認(rèn)知學(xué)術(shù)研討會(huì)會(huì)議論文集[C];2004年

8 高思存;;一個(gè)刻畫(huà)n叉有限樹(shù)的模態(tài)系統(tǒng)及其應(yīng)用[A];2005年邏輯研究專(zhuān)輯[C];2005年

9 羅文英;;上海居民年齡與收入滿(mǎn)足度關(guān)系的實(shí)證分析[A];2008年度上海市社會(huì)科學(xué)界第六屆學(xué)術(shù)年會(huì)文集（政治·法律·社會(huì)學(xué)科卷）[C];2008年

10 陳星;陳樹(shù)國(guó);;如何評(píng)價(jià)內(nèi)燃平衡重式叉車(chē)[A];中國(guó)機(jī)械工程學(xué)會(huì)物料搬運(yùn)專(zhuān)業(yè)學(xué)會(huì)第三屆年會(huì)論文集[C];1988年

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前10條

1 記者 任靜波 賈曉靜;我國(guó)將大力推進(jìn)重大技術(shù)裝備國(guó)產(chǎn)化[N];中國(guó)冶金報(bào);2008年

2 白水;演繹“美麗謀略”[N];上海金融報(bào);2006年

3 楊濤 （四川文軒鎖公司策劃中心）;大書(shū)城連鎖中的品牌弱化[N];中國(guó)圖書(shū)商報(bào);2005年

4 《男人裝》主編 瘦馬;誰(shuí)在看你的雜志[N];中國(guó)新聞出版報(bào);2004年

5 陳岸瑛;文字和數(shù)字創(chuàng)造的世界[N];中華讀書(shū)報(bào);2003年

6 記者 杜梅;淮南礦業(yè)集團(tuán)：物資采購(gòu)“能招盡招”[N];現(xiàn)代物流報(bào);2008年

7 本版編輯 余建斌 陳建才 諶文衛(wèi) 杜文娟　楊健　本報(bào)記者　 蔣建科　許健民;科技：讓百姓生活富裕又便捷[N];人民日?qǐng)?bào);2006年

8 張建軍 尤成勇;五大支柱產(chǎn)業(yè)貸走五百億元[N];溫州日?qǐng)?bào);2009年

9 張?jiān)讫?陳芳;經(jīng)濟(jì)發(fā)展與鐵路運(yùn)力的矛盾[N];國(guó)際商報(bào);2004年

10 喻國(guó)明（中國(guó)人民大學(xué)新聞學(xué)院）;一個(gè)主流媒體的百年文本[N];中國(guó)圖書(shū)商報(bào);2002年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 時(shí)慧嫻;模態(tài)邏輯的計(jì)量化研究及其在模型檢驗(yàn)中的應(yīng)用[D];陜西師范大學(xué);2013年

2 胡明娣;邏輯度量空間的內(nèi)蘊(yùn)結(jié)構(gòu)的研究[D];陜西師范大學(xué);2011年

3 王慶平;邏輯度量空間中的仿射變換和幾類(lèi)特殊公式的性態(tài)研究及其應(yīng)用[D];陜西師范大學(xué);2012年

4 董威;面向UML的模型檢驗(yàn)研究[D];中國(guó)人民解放軍國(guó)防科學(xué)技術(shù)大學(xué);2002年

5 李文江;基于格蘊(yùn)涵代數(shù)的廣義格值模態(tài)邏輯及其歸結(jié)自動(dòng)推理的研究[D];西南交通大學(xué);2002年

6 史t，

本文編號(hào)：872793