重新开始学数学 • 数理逻辑（4）

时序逻辑

在逻辑中，术语时间逻辑被用来描述为表现和推理关于时间限定的命题的规则和符号化的任何系统。 —— Wikipedia

基于模型的程序正确性验证，比如现在常用的 TLA+，背后的原理就是时序逻辑。

线性时间时序逻辑（LTL, Linear-time Temporal Logic）

In logic, linear temporal logic or linear-time temporal logic(LTL) is a modal temporal logic with modalities referring to time. —— Wikipedia

Linear-time temporal logic, or LTL for short, is a temporal logic, with connectives that allow us to refer to the future. —— Logic in Computer Science

简单来说就是提供了描述时间的工具的时间逻辑系统。

这种逻辑系统将时间建模为一系列（不分支的）无限向未来延伸的状态。

形式化表述

$$\displaylines { Formula ::= \\ \top | \bot | p | \neg Formula | Formula \wedge Formula | Formula \vee Formula | Formula \rightarrow Formula \\ | X\ Formula | F\ Formula | G\ Formula | Formula\ U\ Formula | Formula\ W\ Formula | Formula\ R\ Formula } $$

其中 $p$ 是一个原子命题。

语意

除了喜闻乐见的 $\wedge$、$\vee$ 等，时序逻辑还添加了一些别的，用来描述状态之间关系的谓词符号¹：

• $X$ 代表 neXt state，比如 $X\ p$ 就是 $p$ 在下一个状态成立。
• $F$ 代表 some Future state，比如 $F\ p$ 就是 $p$ 一定在某个未来²状态成立，常写作 $\diamond$。
• $G$ 代表 all future states (Globally)，比如 $G\ p$ 就是 $p$ 在所有未来状态成立，常写作 $\square$。
• $U$ 代表 Until，比如 $p\ U\ q$ 就是 $p$ 一直成立，“直到”³有一天 $q$ 成立，而且也 imply 了 $q$ 真的总有一天会成立。
• $W$ 代表 Weak until，比如 $p\ W\ q$ 就是 $p$ 一直成立，直到有一天 $q$ 成立，但并不 imply $q$ 真的总有一天会成立。
• $R$ 代表 Release，$p\ R\ q$ 等价于 $\neg (\neg p\ U \neg q)$，也就是说，$p$ 的成立 释放了 $q$，使得 $q$ 可以不再成立。

分支时序逻辑（CTL，Computation Tree Logic）

Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. —— Wikipedia & Logic in Computer Science

简单来说就是可以描述整个执行树的逻辑系统。

相比 LTL，CTL 多出了“分支”，使得原本在 LTL 里无法表达的 “存在” 可以表达了。

形式化表述

$$\displaylines { Formula ::= \\ \top | \bot | p | \neg Formula | Formula \wedge Formula | Formula \vee Formula | Formula \rightarrow Formula \\ | AX\ Formula | EX\ Formula | AF\ Formula | EF\ Formula | AG\ Formula | EG\ Formula | A[Formula\ U\ Formula] | E[Formula\ U\ Formula] } $$

其中 $p$ 是一个原子命题。

CTL 一般不包含 $W$ 和 $R$。

需要注意的是，CTL 不包括“连用” LTL 新引入的连接词 的句子，比如 LTL $FG\ p$ 是合法的 LTL，但 $A(FG\ p)$ 却不是合法的 CTL。

语意

A 是 along All paths（但我更倾向于继续使用 Always）, 即后面的 LTL 在所有路径上成立。 E 是 there Exists one path，即后面的 LTL-like 的公式在某条路径上成立。

CTL*

CTL* 可以看作是 LTL 和 CTL “取长补短” 得到的结果，它也是 LTL 和 CTL 的超集。

在 CTL* 中，可以自由地使用 $A$/$E$ 和 $X$/$F$/$G$/$U$ 来连结命题。