数理逻辑之 时态逻辑

前面说了谓词逻辑。实际上谓词逻辑还需要了解的有谓词逻辑的语义推导和谓词逻辑的完备性。不过这一块的概念和思想都很复杂和繁冗，本系列略去。

基于模型是和基于证明相对的。前面我们一直在使用证明，好像看起来还不错。不过在基于证明的处理中，系统描述是一组（适当的逻辑中的）公式Γ，而规范是另一个公式φ。验证方法是试图找到Γ├φ的证明。这需要指导和专业知识。

在基于模型的处理中，系统由适当逻辑的模型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，也可能是p₁,p₂,p₃等。每个原子代表一个可能成立的原子事实。

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={s₀,s₁,s₂}

→={s₀ → s₁, s₀ → s_{2 ,} s₁→s₀, s₁→s₂,s₂ → s₂}

L(s₀)={p,q},L(s₁)={q,r},L(s₂)={r}

 模型M = (S, →,L)的一条路径是S中状态的无限序列s₁,s₂,s₃,…,对于每个i ≥1，有s_i →s_i+1。该路径记为s₁ → s₂ →…。路径π¹= s₁ → s₂ →…表示一个可能的未来。π 的上标表示起点的下标。

将迁移系统展开为一个无限计算树很有用。这样，模型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 ╞ φ。