在执行过程中解释命题
时序逻辑（temporal logic）是在普通逻辑基础上加入时间或状态先后关系的形式语言。它不只是断言“资源被占用”，还可以断言占用将持续、最终会解除，或者每次请求之后都能得到响应。在程序验证中，时间常表示执行步骤的次序，不必对应钟表秒数。
本文采用常见的离散、无限状态序列语义。原子命题在每个位置有真假，公式的满足关系还要指定当前所在位置。有限轨迹、连续时间或带数值时限的逻辑需要另外约定，特别是终止位置有没有下一步，不能把一种模型下的公式解释直接套到另一种模型。
几个基本时序算子
在线性时间语义中，X p表示下一位置满足p，F p表示从当前位置起某个位置满足p，G p表示从当前位置起所有位置都满足p。p U q表示q终将出现，而且在它首次选定出现的位置之前，p一直成立。这里采用强直到，包含q最终发生；弱直到则还允许p永远持续而q不出现。
算子的次序会改变要求。G F p表示此后总还能等到p，亦即p反复出现；F G p则表示经过某段有限前缀后，p一直成立。对单条路径写π满足φ，是说该路径符合公式；在常见LTL模型检查中，说整个系统满足φ，通常进一步要求所有初始运行路径都满足它。
安全性与活性
安全性强调坏事不会发生。例如用c1、c2表示两个进程位于临界区，G非(c1且c2)表达互斥：一旦观察到二者同时进入，就能用有限执行前缀说明违规。仅有互斥还不够，系统也可能让所有进程永远等待，从不发生冲突却无法提供服务。
活性强调好事最终发生，例如G(req蕴涵F ack)表示每次请求最终得到确认。等待了很多步仍没有确认，通常还不足以反驳无期限的“最终”，因为下一步仍可能发生；模型检查可用无限运行或循环证据揭示永远不响应的行为。安全和活性因此回答不同问题，不能用其中一种取代全部正确性要求。
参考：[1]
分支未来与模型假设
计算树逻辑CTL显式使用A表示所有路径、E表示存在路径，并将路径量词与时序算子配对。EF ready只要求有一种执行能到达就绪状态，AF ready则要求每种执行最终都到达。一个有机会恢复却也能一直停滞的系统，可能满足前者而不满足后者。
LTL与CTL的表达能力一般不可互相包含，CTL*则允许更自由的状态和路径公式组合。建模还必须明确哪些调度路径被纳入考虑；若证明依赖公平性，就要说明相应限制，而不是静默排除不喜欢的运行。时序公式的价值在于准确表达与检查这些要求，结论仍以转移模型及其假设为边界。