模态逻辑的计量化研究及其在模型检验中的应用

发布时间：2017-09-18 02:17

  本文关键词：模态逻辑的计量化研究及其在模型检验中的应用

  更多相关文章： 计量逻辑学 模态逻辑 时态逻辑 模型检验 迁移系统 局部化真度 全局真度 满足度 极大缩减

【摘要】：本文的目的在于建立模态逻辑的计量化理论,并将其基本方法用于解决模型检验的计量化问题以及简化模型检验的过程. 计量逻辑学的提出旨在将基于概率、积分等工具的数值计算方法引入到以形式推理为特色的数理逻辑中,使原本符号化的推理具备某种灵活性从而扩展其应用范围.这种思想的雏形最初见于从逻辑语义基本概念的程度化入手而在若干命题逻辑系统中所建立的公式真度理论.此后引发了大量的后续研究,包括对逻辑度量空间的拓扑性质与内蕴结构的研究、对逻辑理论的发散度与相容度的研究以及在命题逻辑中建立近似推理的研究等,至今已形成了较为完善和成熟的计量逻辑学理论.如今计量逻辑学的研究对象已从命题逻辑的范围扩展到了表达力更强的模态逻辑、时态逻辑与谓词逻辑的理论之中.若干将计量逻辑学与其他领域相结合的创新性研究也不断涌现,显示出了计量逻辑学的旺盛生命力与广阔的应用前景.本文的研究目的在于探索计量逻辑学与理论计算机科学的新的结合点,将原本在命题逻辑中行之有效的计量化方法向表达力更强的模态逻辑与时态逻辑中推广,并尝试将其应用于以时态逻辑为逻辑背景的模型检验理论之中. 模态逻辑是非经典数理逻辑与人工智能理论相结合的一个重要方面.它不仅是时态逻辑、知识推理的理论基础,又常在应用中作为程序语义描述的工具.作为命题逻辑的模式扩张,模态逻辑具有命题逻辑所不具备的特点.例如模态逻辑中有若干可以表达“可能”、“必然”以及“将来”、“过去”等不同类型概念的模态词,随着模态词的增多,模态逻辑的表达能力也随之增强,此外局部概念的引入以及可能世界之间关系的论述等也使得模态逻辑具有比命题逻辑强得多的表达能力.正是由于这些特点,使得将原本在命题逻辑中行之有效的计量化方法向更为广泛的模态逻辑中推广成为了近几年计量逻辑学的基本研究任务之一.本文将从模态逻辑Kripke语义的局部化特点出发,建立模态公式的局部化真度,继而再利用某种聚合的方法将其推广为模态公式的全局真度,从而在模态逻辑中建立起较为广泛的计量逻辑理论. 另一方面,模型检验是一种形式化的认证方法,可以用来自动地检验某系统的模型是否满足为该系统设定的规范.这一理论已经经历了迅速发展的三十年,受到了人工智能学界的广泛关注,如今已被成功地应用于包括工业、金融、医疗乃至航空航天等重要领域.注意到模型检验理论的逻辑背景是某类特殊的时态逻辑,它们可以看作是模态逻辑的模式扩张.基于这些考虑,本文将进一步把针对模态逻辑的计量化理论向这类时态逻辑中推广,从一个全新的角度建立模型检验中的计量化理论,并讨论如何针对特殊类型的公式来简化模型检验的过程. 全文共分为五章： 第一章首先简要介绍有关命题逻辑的若干预备知识,包括语构理论、语义理论和完备性问题,并介绍几种常用的命题逻辑系统；然后从分析将基本逻辑概念进行程度化的必要性入手,简要介绍计量逻辑学的基本理论,包括公式的真度、公式之间的相似度、公式集上的伪距离以及逻辑度量空间等理论. 第二章首先简要回顾基本模态逻辑的语义理论、语构理论以及完备性问题；其次对基本模态逻辑的Kripke语义进行推广,将基本模型中的赋值域扩充为完备格,从而建立格值模态逻辑的Kripke语义,并证明该语义也将模糊模态逻辑的Kripke语义纳入其框架之下；然后以Boole代数为背景建立Boole型格值模态逻辑系统B,讨论系统B的语义理论与语构理论,并证明完备性定理的成立,即,任一模态公式是系统召中的定理当且仅当它是有效公式,同时指出基本模态逻辑的Kripke模型实际上是本文所提出的Boole型模态模型的特例；最后提出QMR0代数的概念,并以QMR0代数为背景构建QMR0型格值模态逻辑系统QML*讨论系统QML*的语义理论与语构理论,并证明完备性定理的成立,同时指出模糊模态逻辑的Kripke模型实际上是本文提出的QMRo型模态模型的特例. 第三章首先以单位区间[0,1]的有限子集作为赋值域,建立多值模态逻辑的Kripke模型以及相应的语义理论,并指出这种模型一方面是第二章提出的格值模态模型的特例,同时其Kripke语义又将基本模态逻辑的Kripke语义纳入其框架之下;其次采用固定可能世界集W与二元关系R而让赋值映射自由变动的方法建立W，R。型框架,并在该框架下用归纳的思想构建模态公式关于某个可能世界诱导的局部化映射,从而引入模态公式的局部化真度概念,证明了这种局部化真度满足约简定理,即,任一模态公式的局部化真度均可以转化为另一个不含模态词的公式在同一可能世界处的局部化真度,从而达到简化真度计算的目的;然后进一步利用聚合的方法将这种局部化真度推广为模态公式的全局真度,并证明全局真度满足一致性定理,即,当某模态公式不含模态词时,其全局真度与其在命题逻辑中的真度一致：同时证明了模态公式的局部化真度值与可能世界集的势并无关系,且其全局真度能够较好地反应时态逻辑的语义特点；最后引入模态公式之间的相似度与伪距离.从而建立起多值模态逻辑度量空间,并证明基于命题逻辑的度量空间是多值模态逻辑度量空间的子空间. 第四章首先简要回顾模型检验理论中有关迁移系统以及线性时态逻辑LTL的基本概念；其次在有限迁移系统的全体无穷初始路径之集上引入某种适当的均匀概率测度.并基于该测度考虑迁移系统TS中满足某个LTL公式φ的路径占总路径的比例,从而定义迁移系统TS对于公式φ的满足度,即TS满足φ的程度,同时在此基础上引入LTL公式之间的相似度与伪距离,并构建线性时态逻辑中的度量空间,即LTL逻辑度量空间；然后将以上建立的满足度理论进一步推广至迁移系统的随机化模型,即离散时间马尔可夫链模型,并类似地引入LTL公式的满足度、相似度与伪距离等概念.此时不再要求各个状态之间相互迁移的概率是等值分布的.从而全体无穷初始路径之集上的概率测度也不是均匀分布的；最后引入线性时态逻辑中公式的特征与时态范式等概念,指出存在特征的LTL公式在模型检验中总可以在有限步内判断其有效性,即使相应的迁移系统含有无限多个状态时也是如此,并证明了LTL公式有与其等价的时态范式当且仅当其存在特征,从而一类特殊的LTL公式可以用线性时态逻辑的有界情形LTLn来刻画. 第五章首先在一般Boole代数中引入推演元的概念,并针对Boole代数建立相应的协调集理论;其次在一般Boole代数中引入反驳、极大缩减、极小减集等概念,并分别给出Boole代数中求某个有限不协调集的全体极小不协调子集以及求有限个集合的全体极小选择的算法原理,从而给出求全体极大缩减的方法,同时指出在一阶语言范围内求全体R-缩减的问题可以转化至Boole代数的范围内求解;最后在Boole代数中引入基本元的概念,并将子句及Horn子句等概念移植到一类由基本元生成的特殊Boole代数中,从而在这类特殊Boole代数中给出求子句集的全体极大缩减的算法原理,同时指出经典二值命题逻辑中求子句集(特别是Horn子句集)的全体R-缩减的问题可以转化至由基本元生成的Boole代数范围内求解.
【关键词】：计量逻辑学 模态逻辑 时态逻辑 模型检验 迁移系统 局部化真度 全局真度 满足度 极大缩减
【学位授予单位】：陕西师范大学
【学位级别】：博士
【学位授予年份】：2013
【分类号】：O141.1
【目录】：

• 摘要3-6
• Abstract6-12
• 前言12-16
• 第1章 命题逻辑与计量逻辑学简介16-28
• 1.1 命题逻辑系统及其完备性16-23
• 1.1.1 命题逻辑系统16-17
• 1.1.2 逻辑系统的完备性17-18
• 1.1.3 若干常用的命题逻辑系统18-23
• 1.2 计量逻辑学基本理论简介23-28
• 1.2.1 经典二值命题逻辑系统L中的计量逻辑理论23-25
• 1.2.2 Lukasiewicz命题逻辑系统Luk与L_n中的计量逻辑理论25-27
• 1.2.3 R_0型命题逻辑系统L~*与L_n~*中的计量逻辑理论27-28
• 第2章 格值模态逻辑及其完备性28-46
• 2.1 基本模态逻辑28-31
• 2.1.1 基本模态逻辑的Kripke模型29-30
• 2.1.2 基本模态逻辑系统K的完备性30-31
• 2.2 格值模态逻辑的Kripke语义31-34
• 2.3 Boole型格值模态逻辑系统B及其完备性34-37
• 2.3.1 系统B的语义理论34-35
• 2.3.2 系统B的语构理论及完备性35-37
• 2.4 QMR_0型格值模态逻辑系统QML~*及其完备性37-46
• 2.4.1 系统QML~*的语义理论38-40
• 2.4.2 系统QML~*的语构理论40-42
• 2.4.3 系统QML~*的完备性42-46
• 第3章 多值模态逻辑的计量化方法46-74
• 3.1 多值模态逻辑的Kripke语义47-51
• 3.2 多值模态逻辑中模态公式的局部化真度51-59
• 3.2.1 模态公式诱导的局部化映射51-54
• 3.2.2 模态公式的局部化真度54-57
• 3.2.3 局部化真度的约简定理57-59
• 3.3 多值模态逻辑中模态公式的全局真度59-67
• 3.3.1 模态公式的全局真度59-60
• 3.3.2 全局真度的一致性定理60-62
• 3.3.3 永真公式62-66
• 3.3.4 全局真度在时态逻辑中的应用66-67
• 3.4 多值模态逻辑度量空间67-74
• 3.4.1 模态公式间的局部化相似度与伪距离67-70
• 3.4.2 k模态度量空间70-74
• 第4章 模型检验中的计量化方法74-106
• 4.1 迁移系统与线性时态逻辑75-79
• 4.1.1 迁移系统75-76
• 4.1.2 线性时态逻辑LTL76-79
• 4.2 LTL中基于迁移系统的计量化方法79-90
• 4.2.1 单初始有限迁移系统中的概率测度79-82
• 4.2.2 基于单初始有限迁移系统的LTL公式的满足度82-86
• 4.2.3 基于多初始有限迁移系统的LTL公式的满足度86-88
• 4.2.4 基于有限迁移系统的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 线性时态逻辑中的时态范式98-106
• 4.4.1 LTL公式的特征98-101
• 4.4.2 LTL公式的时态范式101-106
• 第5章 Boole代数中的极大缩减106-120
• 5.1 Boole代数中的协调集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 徐凤丽;;对中国城镇居民消费函数的探讨[J];经营管理者;2009年17期

6 时丽娜;黄汉明;李小勇;唐贤健;潘士虎;;基于等维灰数递补动态模型的人口老龄化趋势预测[J];鲁东大学学报(自然科学版);2009年04期

7 龚亮;陈怀录;张淑娟;;灰色模型在甘肃省人口预测中的应用[J];甘肃科技;2010年16期

8 王士铁;模态逻辑与程序验证[J];厦门大学学报(自然科学版);1985年03期

9 肖庆宪;汇率机制与汇率模型[J];数量经济技术经济研究;2002年08期

10 何剑;;IPOs价格影响因素:一个定价模型检验[J];商场现代化;2006年11期

中国重要会议论文全文数据库 前10条

1 李文江;陈图云;;基于模糊测度的模态逻辑[A];模糊集理论与应用——98年中国模糊数学与模糊系统委员会第九届年会论文选集[C];1998年

2 楚白;;有穷深度的模态逻辑[A];2005年逻辑研究专辑[C];2005年

3 陈国勋;闫家杰;;Fuzzy模态公式的归约[A];中国系统工程学会模糊数学与模糊系统委员会第五届年会论文选集[C];1990年

4 宗群;窦立谦;孙连坤;刘文静;;基于残差分析方法的模型检验[A];第二十七届中国控制会议论文集[C];2008年

5 张丁煜;;门户网站新闻使用比较研究——以中韩两国大学生为例[A];中国传媒大学第五届全国新闻学与传播学博士生学术研讨会论文集[C];2011年

6 孙希文;;模态逻辑模型的嵌入定理[A];1994年逻辑研究专辑[C];1994年

7 潘天群;;建立在“笛卡尔公理”上的一个怀疑逻辑系统[A];逻辑与认知学术研讨会会议论文集[C];2004年

8 高思存;;一个刻画n叉有限树的模态系统及其应用[A];2005年逻辑研究专辑[C];2005年

9 罗文英;;上海居民年龄与收入满足度关系的实证分析[A];2008年度上海市社会科学界第六届学术年会文集（政治·法律·社会学科卷）[C];2008年

10 陈星;陈树国;;如何评价内燃平衡重式叉车[A];中国机械工程学会物料搬运专业学会第三届年会论文集[C];1988年

中国重要报纸全文数据库 前10条

1 记者 任静波 贾晓静;我国将大力推进重大技术装备国产化[N];中国冶金报;2008年

2 白水;演绎“美丽谋略”[N];上海金融报;2006年

3 杨涛 （四川文轩锁公司策划中心）;大书城连锁中的品牌弱化[N];中国图书商报;2005年

4 《男人装》主编 瘦马;谁在看你的杂志[N];中国新闻出版报;2004年

5 陈岸瑛;文字和数字创造的世界[N];中华读书报;2003年

6 记者 杜梅;淮南矿业集团：物资采购“能招尽招”[N];现代物流报;2008年

7 本版编辑 余建斌 陈建才 谌文卫 杜文娟　杨健　本报记者　 蒋建科　许健民;科技：让百姓生活富裕又便捷[N];人民日报;2006年

8 张建军 尤成勇;五大支柱产业贷走五百亿元[N];温州日报;2009年

9 张云龙 陈芳;经济发展与铁路运力的矛盾[N];国际商报;2004年

10 喻国明（中国人民大学新闻学院）;一个主流媒体的百年文本[N];中国图书商报;2002年

中国博士学位论文全文数据库 前10条

1 时慧娴;模态逻辑的计量化研究及其在模型检验中的应用[D];陕西师范大学;2013年

2 胡明娣;逻辑度量空间的内蕴结构的研究[D];陕西师范大学;2011年

3 王庆平;逻辑度量空间中的仿射变换和几类特殊公式的性态研究及其应用[D];陕西师范大学;2012年

4 董威;面向UML的模型检验研究[D];中国人民解放军国防科学技术大学;2002年

5 李文江;基于格蕴涵代数的广义格值模态逻辑及其归结自动推理的研究[D];西南交通大学;2002年

6 史t，

本文编号：872793