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

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

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

• 摘要3-6
• Abstract6-12
• 前言12-16
• 第1章 命題邏輯與計量邏輯學(xué)簡介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 計量邏輯學(xué)基本理論簡介23-28
• 1.2.1 經(jīng)典二值命題邏輯系統(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的語構(gòu)理論及完備性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~*的語構(gòu)理論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)公式誘導(dǎo)的局部化映射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)邏輯中的應(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章 模型檢驗中的計量化方法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 基于有限D(zhuǎn)TMC的LTL公式的滿足度93-96
• 4.3.4 基于有限D(zhuǎn)TMC的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代數(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é)位期間的科研成果與獲獎情況134-135

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

中國重要報紙全文數(shù)據(jù)庫 前10條

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

6 史t，

本文編號：872793