时序逻辑

性质随执行位置解释 ​

命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。在一个状态赋值上判断 $p\wedge q$、$p\to q$ 等公式。时序逻辑把满足关系扩展到执行路径公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。的位置：给定无限状态词

$$\pi =s_0{s}_1{s}_2\cdots ,$$

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

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

$$\pi ,i\models X\phi ⟺\pi ,i+1\models \phi ,$$$$\pi ,i\models F\phi ⟺\mathrm{\exists }j\ge i,\pi ,j\models \phi ,$$$$\pi ,i\models G\phi ⟺\mathrm{\forall }j\ge i,\pi ,j\models \phi .$$

直到公式 $\phi U\psi$ 要求存在 $j\ge i$ 使 $\psi$ 在 $j$ 成立，并且每个 $i\le k<j$ 都满足 $\phi$。经典 strong until 因而保证 $\psi$ 最终出现；只要求 $\phi$ 一直成立而允许 $\psi$ 永不出现的是 weak until，必须另用符号或定义声明。

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

$G\mathrm{\neg }bad$ 的意思是沿所量化执行的每个未来位置都没有坏状态；它不是在状态里新增一个名为 time 的整数再写普通一阶公式。时间来自转移序列的位置次序，状态可以完全不含物理时钟。

同样，$Fdone$ 只表达某个有限位置最终出现 done，没有给出多久之内。若规格要求“5 秒内响应”，需要离散计步界、实时逻辑或时间自动机，不能把定量上界藏在 eventually 的自然语言翻译里。

$X\phi$ 对一步粒度敏感。把一条实现动作细化成两个内部步骤后，原来下一状态成立的 $\phi$ 可能移到下下状态。$F,G,U$ 在适当标记下通常对有限停顿更稳健，这也是规格是否允许 stuttering 的重要分界。

三类典型规格 ​

互斥安全性可写成

$$G\mathrm{\neg }(c_1\wedge c_2),$$

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

请求—响应性质可写成

$$G(request\to Fgrant).$$

它要求每次请求后都存在未来授权，而不是只要求系统历史上曾出现过一次授权。公式若改成 $Fgrant$，一个早期 grant 就足以满足，无法约束后来的请求。

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

$$availableUmaintenance.$$

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

线性与分支时间 ​

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

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

$$EFsuccess\text{与}AFsuccess,$$

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

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

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

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

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

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

从规格到验证算法 ​

时序逻辑定义性质语言，不规定如何求值。模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。把系统模型与公式组合成判定问题；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。