本文關鍵詞：模態(tài)邏輯的計量化研究及其在模型檢驗中的應用

  更多相關文章： 計量邏輯學 模態(tài)邏輯 時態(tài)邏輯 模型檢驗 遷移系統(tǒng) 局部化真度 全局真度 滿足度 極大縮減

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

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

【相似文獻】

中國期刊全文數據庫 前10條

1 王浦;;中國住宅房地產價格影響因素實證分析[J];中國集體經濟;2008年Z1期

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

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

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

5 徐鳳麗;;對中國城鎮(zhèn)居民消費函數的探討[J];經營管理者;2009年17期

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

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

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

9 肖慶憲;匯率機制與匯率模型[J];數量經濟技術經濟研究;2002年08期

10 何劍;;IPOs價格影響因素:一個定價模型檢驗[J];商場現代化;2006年11期

中國重要會議論文全文數據庫 前10條

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

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

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

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

5 張丁煜;;門戶網站新聞使用比較研究——以中韓兩國大學生為例[A];中國傳媒大學第五屆全國新聞學與傳播學博士生學術研討會論文集[C];2011年

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

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

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

9 羅文英;;上海居民年齡與收入滿足度關系的實證分析[A];2008年度上海市社會科學界第六屆學術年會文集（政治·法律·社會學科卷）[C];2008年

10 陳星;陳樹國;;如何評價內燃平衡重式叉車[A];中國機械工程學會物料搬運專業(yè)學會第三屆年會論文集[C];1988年

中國重要報紙全文數據庫 前10條

1 記者 任靜波 賈曉靜;我國將大力推進重大技術裝備國產化[N];中國冶金報;2008年

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

3 楊濤 （四川文軒鎖公司策劃中心）;大書城連鎖中的品牌弱化[N];中國圖書商報;2005年

4 《男人裝》主編 瘦馬;誰在看你的雜志[N];中國新聞出版報;2004年

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

6 記者 杜梅;淮南礦業(yè)集團：物資采購“能招盡招”[N];現代物流報;2008年

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

8 張建軍 尤成勇;五大支柱產業(yè)貸走五百億元[N];溫州日報;2009年

9 張云龍 陳芳;經濟發(fā)展與鐵路運力的矛盾[N];國際商報;2004年

10 喻國明（中國人民大學新聞學院）;一個主流媒體的百年文本[N];中國圖書商報;2002年

中國博士學位論文全文數據庫 前10條

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

2 胡明娣;邏輯度量空間的內蘊結構的研究[D];陜西師范大學;2011年

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

4 董威;面向UML的模型檢驗研究[D];中國人民解放軍國防科學技術大學;2002年

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

6 史t，

本文編號：872793