前面说了谓词逻辑。实际上谓词逻辑还需要了解的有谓词逻辑的语义推导和谓词逻辑的完备性。不过这一块的概念和思想都很复杂和繁冗,本系列略去。
基于模型是和基于证明相对的。前面我们一直在使用证明,好像看起来还不错。不过在基于证明的处理中,系统描述是一组(适当的逻辑中的)公式Γ,而规范是另一个公式φ。验证方法是试图找到Γ├φ的证明。这需要指导和专业知识。
在基于模型的处理中,系统由适当逻辑的模型M表示。规范仍然由φ表示。验证方法是计算M是否满足φ,即M ╞ φ。这是自动的。所以基于模型的方法更简单。
模型检测基于时态逻辑 temporal logic。命题逻辑和谓词逻辑中的公式真假是固定的,但是时态逻辑模型包含若干状态,具有动态真的性质,即公式可以随系统的状态演化而改变其真值。
模型检测中,模型M是迁移系统(下面会解释这个概念),性质φ是时态逻辑公式。这样验证过程是:
1.使用模型检测器的描述语言建模,得到模型M;
2.用模型检测器的规范语言对性质编码,得到时态逻辑公式φ;
3.输入M和φ,运行模型检测器。
如果M ╞ φ,机器回答yes,否则no并输出行为轨迹。
时态逻辑主要有两类:线性时间逻辑LTL把时间看成是路径的集合,路径即时间瞬时的一个序列;分支时间逻辑CTL把时间表示为树,以当前时间为根向未来分叉,使得未来的不确定性变得明确。
时态逻辑公式的真值依赖于模型内部的时间点。
现在说一下迁移系统的概念。迁移系统M = (S, →,L)是一个状态集合S,带有迁移关系→(S上的二元关系),使得每个s ∈S有某个s’ ∈S,满足s →s’,以及一个标记函数L:S →P(Atoms)。迁移系统简称模型。P(Atoms)表示Atoms的幂集,即原子描述集。L可以看作是对所有原子命题的一个真值赋值。由于不止一个状态,这种赋值依赖于系统所处的状态s:L(s)包含了状态s下为真的所有原子。
说了这么多,模型检测要干嘛呢?模型检测就是对问题M ,s╞ φ是否成立进行计算的过程,其中:M 是所考虑系统的一个适当模型;s 是该模型的一个状态;╞是满足关系; φ是一个LTL或CTL公式。
这里的研究工具是线性时态逻辑LTL。LTL带有允许我们指示未来的连接词。它将时间建模成状态的序列,无限延伸到未来。该序列称为计算路径(或路径)。由于未来的不确定性,我们要考虑若干可能的路径。
设立一个原子公式的集合Atoms。原子公式可能形如p,q,r,也可能是p1,p2,p3等。每个原子代表一个可能成立的原子事实。
LTL公式表达为 φ :: =┬|┴|p|(┐φ)|(φ∧φ)|(φ∨φ)|(φ→φ)|(Xφ)|(Fφ)|(Gφ)|(φUφ)|(φWφ)|(φRφ)
上面,p是Atoms中的原子;┬和┴是LTL公式,也是Atoms原子。φ 是LTL公式,所以┐φ也是。X是下一个状态neXt; F是某未来状态Future; G是所有未来状态Globally; U是直到Until;R是释放Rlease;W是弱直到Weak-until。
这就是线性时态逻辑语法。下面都是LTL实例:(((Fp) ∧(Gp)) →(pWr)), (F(p →(Gr)) ∨((┐q)Up)), (pW(qWr)), ((G(Fp)) →(F(q ∨s)))。LTL也有语法树,下面是(F(p →(Gr)) ∨((┐q)Up))的语法树:
一元连接词┐和时态连接词X,F,G具有最高优先级,然后是U,R,W;接下来是∨和∧,最低的是→。这样,上面几个例子可以化简为:Fp ∧Gp →pWr,F(p →Gr) ∨┐qUp,pW(qWr),GFp →F(q ∨s)。
可以用有向图来表示一个迁移系统:
S={s0,s1,s2}
→={s0 → s1, s0 → s2 , s1→s0, s1→s2,s2 → s2}
L(s0)={p,q},L(s1)={q,r},L(s2)={r}
模型M = (S, →,L)的一条路径是S中状态的无限序列s1,s2,s3,…,对于每个i ≥1,有si →si+1。该路径记为s1 → s2 →…。路径π1= s1 → s2 →…表示一个可能的未来。π 的上标表示起点的下标。
将迁移系统展开为一个无限计算树很有用。这样,模型M的执行路径被明确表示出来:
设M = (S, →,L)是一个模型,π 是其中的一条路径。π 是否满足一个LTL公式,由满足关系╞定义如下(里面涉及到不能推导的符号,所以我只能在PPT中做好截图过来了)
通过这个满足关系表可以立即明白XGFUWR各字母的意思了吧。
φUψ表示φ一直成立直到ψ成立。ψ成立后φ怎么样了?这里体现不出来的。例如:
s代表“我吸烟”,t代表“我22岁”。则sUt:我吸烟一直到了22岁。不能表示22岁以后不吸烟。如果要这样需要这样表示sU(t ∧ G ┐ s)。
W和U类似。不过φWψ不要求ψ在某处会成立,而是φ可以一直成立下去。
φRψ等价于┐(┐φU┐ψ),约等价于ψWφ,不过R可以取到i。
设M = (S, →,L)是一个模型,s∈S,且φ是一个LTL公式。如果对M 的每条始于s的执行路径π,都有π╞ φ,则记为M,s ╞ φ。
相关推荐
高级数理逻辑的焦点包括命题逻辑和谓词逻辑的形式化描述,形式化系统的语义结构,自动化推理技术,以及模态逻辑、时态逻辑和非单调逻辑系统等扩展领域。 **数理逻辑的发展历程**从亚里士多德的逻辑思想开始,到...
高级数理逻辑第六章:时态逻辑的发展历史及详细内容
此外,PPT学习教案还讨论了数理逻辑在计算机科学、控制论和人工智能等领域的应用,包括模糊逻辑、概率逻辑、归纳逻辑、时态逻辑等热门研究领域。 本PPT学习教案旨在帮助学生掌握离散数学的基本概念和理论,为进一步...
2. TLA+之“道”——时态逻辑 时态逻辑是TLA+的核心,它允许我们将系统的状态和行为建模为随时间变化的过程。正确性证明的关键在于,通过将系统的状态转换抽象为时态逻辑,我们可以分析这些状态序列来确定系统是否...
数理逻辑是计算机科学的基石,它包括命题逻辑、一阶逻辑和更高阶的逻辑系统。Pnueli的工作不仅将时态逻辑引入到这一领域,还探讨了如何将其应用于实际的计算问题。他的研究成果使得逻辑工具能够处理更复杂的系统模型...
### 数理逻辑在计算机科学中的应用 #### 一、引言 《数学逻辑与计算机科学》(第三版)由Mordechai Ben-Ari教授撰写,是面向计算机科学领域的一本经典教材。本书深入探讨了数学逻辑的基础理论及其在计算机科学中的...
模态逻辑是数理逻辑的一个分支,主要研究包含模态词(如必然性、可能性等)的命题或陈述的逻辑性质。模态逻辑在哲学、计算机科学、数学等多个领域都有广泛的应用。Kripke 结构是一种用于描述模态逻辑语义的重要工具...
首先,演绎推理是一种基于已知事实和规则推导出新结论的方法,通常在形式逻辑中得到应用,包括经典的数理逻辑和非经典逻辑如模态逻辑、时态逻辑等。演绎推理具有保真性,即如果前提正确,那么结论也是正确的。在机器...
关键词部分提供了文章研究的几个核心概念,即“多值模态逻辑”、“〈W,R〉n-型框架”、“n-值模态模型”、“局部化真度”、“全局真度”和“时态逻辑”。这些关键词为文章的研究范围和深度提供了明确的指示,涉及到...
首先,本卷给出了离散数学的基本介绍,包括数、集合、笛卡尔、类型、函数、λ-演算、代数和数理逻辑,然后讲授基本的面向属性与面向模型的规约的基本原理和技术。一些其他的规约语言,比如B、VDM-SL和Z都具有面向...
2. **语法**:理解并掌握英语语法规则是提高语言运用能力的关键,包括时态(一般现在时、过去时、将来时等)、语态(主动语态与被动语态)、虚拟语气、条件句等。 3. **阅读理解**:阅读各种类型的文本,如新闻、...
考生需要熟练掌握大纲规定的词汇,了解各种时态、语态、句型结构,并能阅读理解不同类型的文章。同时,写作部分需要考生具备清晰的逻辑思维和良好的表达能力,能够写出符合规范的议论文或应用文。 2. **高等数学**...
- 概率论与数理统计:随机变量、概率分布、期望、方差、协方差、大数定律和中心极限定理。 2. **英语**: - 词汇与语法:要求考生掌握大量词汇,熟悉各种时态、语态、句型结构。 - 阅读理解:训练快速阅读能力,...
数据挖掘技术的对象也非常多样,包括了媒体数据库、遗产数据库、空间数据库、文本数据库、异质数据库和时态数据库等。每种数据库都蕴含了不同类型的数据信息,需要不同的挖掘策略来应对。 在实际应用中,数据挖掘...
高等数学是理工科专业的重要基础课程,涵盖了微积分、线性代数、概率论与数理统计等多个领域。在成都理工大学的历年高数真题中,可能会涉及以下核心知识点: 1. **极限与连续**:理解函数的极限概念,掌握极限的四...