线性时序逻辑 LTL

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

公式

要求对每个位置 $i$：若 $request$ 在 $i$ 成立，则存在某个 $j\ge i$ 使 $grant$ 成立。取无限词

并令 $w_4=\{request\}$、$w_i=\varnothing$ 对所有 $i\ge 5$。位置 $0$ 的请求由 $j=2$ 的授权见证；位置 $4$ 的请求没有见证，所以 $w,0⊭G(request\to Fgrant)$。早期成功不能抵消晚期失败。反过来，两个请求可以由同一次稍后授权同时见证，除非规格另行要求请求—授权一一对应。

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

常用等价与正常形 ​

对无限词有

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

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

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

有限轨迹与停顿边界 ​

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

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

LTL 能描述每条路径上的事件顺序，却不能在公式内部重新量化另一条未来。要表达“存在恢复路径但并非所有路径恢复”，需用CTL公理库计算树逻辑 CTLComputation tree logic · CTL · Branching-time temporal logic将路径量词 A/E 与时间算子成对组合，在 Kripke 状态上表达分支未来性质。；需要在一次路径选择后组合多个线性义务并再次嵌套路径量词，则进入CTL*公理库CTL*CTL* · Computation tree logic star · Full branching-time temporal logic以状态公式和路径公式两层语法自由嵌套路径量词与线性时间算子，统一包含 LTL 与 CTL。。

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

模型检查通常把 $M⊭\phi$ 改写为“存在系统路径满足 $\mathrm{\neg }\phi$”，再经LTL 到 Büchi 转换公理库LTL 到 Büchi 自动机的转换LTL to Büchi translation · LTL-to-automata translation将 LTL 公式构造为接受其模型无限词的 Büchi 自动机，并揭示 closure、承诺跟踪与指数状态增长。寻找接受 lasso。这个算法出口不改变本页的全路径满足定义；它只是用否定把全称失败变成存在见证。