本文的目的在于建立模态逻辑的计量化理论,并将其基本方法用于解决模型检验的计量化问题以及简化模型检验的过程.计量逻辑学的提出旨在将基于概率、积分等工具的数值计算方法引入到以形式推理为特色的数理逻辑中,使原本符号化的推理具备某种灵活性从而扩展其应用范围.这种思想的雏形最初见于从逻辑语义基本概念的程度化入手而在若干命题逻辑系统中所建立的公式真度理论.此后引发了大量的后续研究,包括对逻辑度量空间的拓扑性质与内蕴结构的研究、对逻辑理论的发散度与相容度的研究以及在命题逻辑中建立近似推理的研究等,至今已形成了较为完善和成熟的计量逻辑学理论.如今计量逻辑学的研究对象已从命题逻辑的范围扩展到了表达力更强的模态逻辑、时态逻辑与谓词逻辑的理论之中.若干将计量逻辑学与其他领域相结合的创新性研究也不断涌现,显示出了计量逻辑学的旺盛生命力与广阔的应用前景.本文的研究目的在于探索计量逻辑学与理论计算机科学的新的结合点,将原本在命题逻辑中行之有效的计量化方法向表达力更强的模态逻辑与时态逻辑中推广,并尝试将其应用于以时态逻辑为逻辑背景的模型检验理论之中.模态逻辑是非经典数理逻辑与人工智能理论相结合的一个重要方面.它不仅是时态逻辑、知识推理的理论基础,又常在应用中作为程序语义描述的工具.作为命题逻辑的模式扩张,模态逻辑具有命题逻辑所不具备的特点.例如模态逻辑中有若干可以表达“可能”、“必然”以及“将来”、“过去”等不同类型概念的模态词,随着模态词的增多,模态逻辑的表达能力也随之增强,此外局部概念的引入以及可能世界之间关系的论述等也使得模态逻辑具有比命题逻辑强得多的表达能力.正是由于这些特点,使得将原本在命题逻辑中行之有效的计量化方法向更为广泛的模态逻辑中推广成为了近几年计量逻辑学的基本研究任务之一.本文将从模态逻辑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代数范围内求解.