线性时序逻辑 LTL

语法与无限词语义 ​

给定原子命题集合 $AP$，LTL 公式由

$$\phi ::=p\mid \mathrm{\neg }\phi \mid (\phi \wedge \phi )\mid X\phi \mid (\phi U\phi )$$

生成，其中 $p\in AP$。布尔析取、蕴含以及 $F,G$ 都可作为派生符号。模型是一条无限序列公理库序列Sequence以自然数为定义域的函数。

$$w=w_0{w}_1{w}_2\cdots \in (2^{AP}{)}^{\omega }.$$

满足关系在位置 $i$ 递归定义。原子命题满足 $w,i\models p⟺p\in w_i$；next 满足 $w,i\models X\phi ⟺w,i+1\models \phi$；until 满足

$$w,i\models \phi U\psi ⟺\mathrm{\exists }j\ge i:w,j\models \psi \wedge \mathrm{\forall }k\in [i,j),w,k\models \phi .$$

于是 $F\phi \equiv trueU\phi$，$G\phi \equiv \mathrm{\neg }F\mathrm{\neg }\phi$。经典 until 是 strong until，右侧目标必须最终出现。

系统满足关系的隐藏全称 ​

公式先在单条词上解释。对带状态标记的系统 $M$，通常定义

$$M\models \phi ⟺\mathrm{\forall }\pi \in {\mathrm{Paths}}_I(M),L(\pi )\models \phi .$$

路径全称不写在 LTL 公式内部，而放在系统满足关系外层。把 $E$、$A$ 随意插入 LTL 语法，会混入分支时间逻辑。

若只要求存在一条路径满足 LTL 公式，那是另一个查询，常可通过检查否定或构造 witness 实现；它不能替代系统正确性的默认全路径量词。

请求—授权的逐位置检查 ​

公式

$$G(request\to Fgrant)$$

要求对每个位置 $i$：若 $request$ 在 $i$ 成立，则存在某个 $j\ge i$ 使 $grant$ 成立。两个不同请求可以由同一次稍后授权同时见证，除非规格另外要求一一对应或授权发生在下一个请求之前。

词

$$\{request\},\varnothing ,\{grant\},\varnothing ,\dots$$

满足第一个请求的响应义务。若后续又在位置 $4$ 出现请求却再无授权，整条词违反公式；早期成功不能抵消晚期失败。

若写成 $GFgrant$，意思是授权出现无限多次；$FGstable$ 则表示从某个位置起永远稳定。$GF$ 与 $FG$ 量词顺序不同，不能靠自然语言“最终总会”含混翻译。

常用等价与正常形 ​

对无限词有

$$F\phi \equiv \phi \vee XF\phi ,G\phi \equiv \phi \wedge XG\phi ,$$$$\phi U\psi \equiv \psi \vee (\phi \wedge X(\phi U\psi )).$$

这些展开式揭示公式是不动点方程，但单独的等式可能同时有多个解；strong until 的最小解语义和 globally 的最大解语义还来自无限词定义。

否定可推到原子命题前，但 until 的对偶需要 release 算子 $R$：

$$\mathrm{\neg }(\phi U\psi )\equiv (\mathrm{\neg }\phi )R(\mathrm{\neg }\psi ).$$

模型检查前做正常化时，若错误地把 until 自对偶，会改变活性义务。

有限轨迹与停顿边界 ​

经典 LTL 假设无限行为。对有限日志，$X\phi$ 在最后位置究竟为假、未知还是采用 weak next，取决于 LTLf 或监控语义；必须单独声明。

不含 $X$ 的 LTL 对停顿等价公理库停顿等价Stuttering equivalence · Stutter equivalence · Stutter invariance忽略连续重复的相同可观察状态块，以比较只增加内部停顿步骤的行为。不变，适合忽略实现增加的有限内部微步。含 $X$、有界 eventually 或实时算子的公式可以观察步数，不能套用该结论。

LTL 能描述每条路径上的事件顺序，却不能在一个公式内部比较两条不同未来分支。要表达“存在恢复路径但并非所有路径恢复”，需用分支逻辑。

公式语义还区分命题在当前位置还是严格未来成立。由于 $j\ge i$，$F\phi$ 允许 $\phi$ 当下即真，$\phi U\psi$ 也允许 $\psi$ 当下兑现而无需先满足 $\phi$。若需求写的是“之后某个严格更晚时刻”，需显式加入 $XF\phi$ 或其他适合的事件边界。

参考资料

• Amir Pnueli, “The Temporal Logic of Programs,” FOCS, 1977, pp. 46–57。
• Zohar Manna and Amir Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer, 1992, Chs. 1–4。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Ch. 5。