时序逻辑 | Codeboy's Blog

形式陈述

性质随执行位置解释

命题逻辑在一个状态赋值上判断 $p\land q$ 、 $p\to q$ 等公式。时序逻辑把满足关系扩展到执行路径的位置：给定无限状态词

\pi=s_0s_1s_2\cdots,

公式 $\varphi$ 是否在位置 $i$ 成立写作 $\pi,i\models\varphi$ 。原子命题仍由当前状态 $s_i$ 决定，时间算子则量化后继位置。

常用算子包括 next、eventually、always 和 until，分别记作 $X,F,G,U$ 。在线性路径语义下，核心量词为

\pi,i\models X\varphi \Longleftrightarrow \pi,i+1\models\varphi,

\pi,i\models F\varphi \Longleftrightarrow \exists j\ge i, \pi,j\models\varphi,

\pi,i\models G\varphi \Longleftrightarrow \forall j\ge i, \pi,j\models\varphi.

直到公式 $\varphi U\psi$ 的精确量词是

\pi,i\models\varphi U\psi \Longleftrightarrow \exists j\ge i: \pi,j\models\psi\ \land\ \forall k\in[i,j),\ \pi,k\models\varphi.

这是 strong until，因而强制 $\psi$ 最终出现。允许 $\psi$ 永不出现的 weak until 为

\varphi W\psi\equiv(\varphi U\psi)\lor G\varphi.

until 的对偶 release 可定义为 $\varphi R\psi\equiv\neg(\neg\varphi U\neg\psi)$ 。自然语言中的“直到”常没有说明强弱，形式规格不能省略这一选择。

直觉

不是给状态加一个时间变量

时间算子读取的是转移序列的位置次序，不是在状态中偷偷增加一个 time 整数。 $G\neg bad$ 检查所量化执行的每个未来位置； $F done$ 只要求某个有限位置出现 done，没有给出等待上界。若需求是“5 秒内响应”，必须加入计步界、实时逻辑或带时钟模型。

$X\varphi$ 尤其依赖一步粒度：把一个实现动作细化成两个内部步骤，会把原本下一状态的 $\varphi$ 推到下下状态。不含 $X$ 的定性 $F,G,U$ 公式在适当标记下通常对有限停顿更稳健，因此状态抽象是否保留 next 性质必须单独证明。

请求响应时间线上第零位置的请求被后续授权满足，而第四位置的请求没有后续授权并违反全局响应公式 — 时序逻辑：每个请求都产生未来授权义务

例子与边界

三类典型规格

互斥安全性可写成

G\neg(c_1\land c_2),

表示任何时刻两个进程都不同时处在临界区。一次有限前缀到达 $c_1\land c_2$ 就构成反例，后续行为无法修复这次违反。

请求—响应性质可写成

G(request\to F\,grant).

令位置 $0$ 与 $4$ 各出现一次 request，位置 $2$ 出现 grant，而位置 $5$ 以后再无授权。位置 $0$ 的义务由 $j=2$ 见证，位置 $4$ 的义务却没有任何 $j\ge4$ 可见证，所以整条执行违反公式。改写成 $F\,grant$ 时，位置 $2$ 的一次授权就足够，后来的请求完全不受约束。

“服务保持可用直到维护窗口开始”可写成

available\ U\ maintenance.

strong until 还要求维护最终开始；若维护可能永不到来、但服务应永远可用，则需要 weak until 或等价组合。自然语言中的“直到”常对这点含混，形式规格必须选定。

线性与分支时间

线性时间把每条执行看作一条完整未来，公式在路径上解释。LTL 使用这种语义，系统满足 LTL 公式通常意味着所有初始路径都满足它。

分支时间在当前状态同时保留多种未来，并显式使用路径量词。CTL 可区分

EF\,success \qquad\text{与}\qquad AF\,success,

前者说存在一条未来成功，后者说每条未来都成功。只画一条时间线无法表达分支选择是在当前发生还是以后发生。

线性与分支语义不是谁“更真实”的二选一。LTL 很自然地描述每次执行上的响应、公平与持续行为；CTL 很自然地描述从状态出发是否存在恢复路径或所有分支都安全。选择取决于规格想保留的观察结构。

有限行为、公平性与假设

经典 LTL 默认无限路径。终止程序可给终止状态补自环，或改用有限轨迹语义；不同选择会改变 $X$ 和某些 until 公式。页面、工具或论文若未说明 LTLf、三值监控语义等变体，就不应把有限日志直接代入经典定义。

公式 $G(request\to F\,grant)$ 在一个永远不调度服务器的路径上失败。若系统模型允许这种路径，但环境承诺持续使能的进程终会运行，就要用公平性约束限制被量化的路径。公平性是模型假设或规格的一部分，不会因写了活性公式而自动成立。

assume–guarantee 写法还要区分环境假设和系统保证。把“不发生断电”与“协议最终响应”合成一个无条件公式，会让验证失败时无法判断是环境超出假设还是实现违背承诺。

推论与应用

从规格到验证算法

时序逻辑定义性质语言，不规定如何求值。模型检查把系统模型与公式组合成判定问题；LTL 可经自动机转换检查接受环，CTL 常以状态集合不动点计算。

公式成立也只相对于给定模型及其原子命题标记。若实现错误被建模阶段遗漏，或 bad 标记没有覆盖真实危险条件，逻辑证明不会自动修复模型—实现差距。

参考资料

Amir Pnueli, “The Temporal Logic of Programs,” FOCS, 1977, pp. 46–57。
E. Allen Emerson, “Temporal and Modal Logic,” in Handbook of Theoretical Computer Science, Vol. B, Elsevier, 1990, Ch. 16。
Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Chs. 3, 5–6。
Zohar Manna and Amir Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer, 1992, Chs. 1–3。

形式陈述 ​

性质随执行位置解释 ​

不是给状态加一个时间变量 ​

三类典型规格 ​

线性与分支时间 ​

有限行为、公平性与假设 ​

从规格到验证算法 ​