停顿等价

把状态词分成常值块 ​

设路径经命题标记后形成无限状态词

$$w=A_0{A}_1{A}_2\cdots ,A_i\subseteq AP.$$

把连续相同的标记合并成最大常值块，可写为

$$w=B_0^{k_0}{B}_1^{k_1}{B}_2^{k_2}\cdots ,B_i\ne B_{i+1},k_i\ge 1.$$

两个状态词停顿等价，若它们的块标记序列 $B_0{B}_1{B}_2\cdots$ 相同，而每块重复次数可以不同。该关系在固定原子命题观察下是等价关系公理库等价关系Equivalence relation满足自反、对称和传递性的关系。。

对有限词还要处理最后一块；对无限停留在同一标记的 suffix，不能简单“压成一个有限符号”后忘记路径仍然无限。定义应保留无限尾块或采用明确约定。

实现微步的例子 ​

抽象规格用一次动作把标记从 idle 变为 done：

$$\{idle\},\{done\},\{done\},\dots$$

实现先经过三个对外仍标记为 idle 的内部阶段，再提交结果：

$$\{idle\},\{idle\},\{idle\},\{done\},\{done\},\dots$$

两条状态词压缩后都是 $\{idle\}\{done{\}}^{\omega }$，因此停顿等价。实现可以多做有限内部工作，只要外部命题不变、可观察阶段顺序不变。

若第二条路径在中途标记 error，压缩序列会多出一块，等价立即失败。停顿不等于“删除任意不喜欢的状态”，它只能改变同一观察值连续出现的次数。

为什么 next 会破坏等价 ​

在第一条路径初始位置，$Xdone$ 为真，因为下一状态已经标记 done；在细化路径初始位置，它为假，因为下一状态仍是 idle。两条路径停顿等价，含 next 的公式却能数出一步差异。

不含 $X$ 的经典 LTL 公式对 stuttering 不变：若两条无限状态词停顿等价，它们满足相同的 LTL$\setminus X$ 公式。这一结论依赖公式只观察标记变化顺序，而不观察块长度。

“不含 next”是充分的语法边界，不应推广成所有时序语言都自动保持停顿。带计步界、实时约束或定量奖励的逻辑同样可能观察重复次数。

状态关系版本 ​

系统级停顿关系把一个系统的一步匹配为另一个系统的有限多步，其中中间状态与起点或终点具有相同观察。证明时需给出 relation 和 well-founded rank，避免一边永远做内部停顿而不完成匹配。

若允许任意无限停顿，系统可能把规格的可见动作永久推迟，却仍声称每个有限阶段可匹配。divergence-sensitive stuttering equivalence 会区分这种发散与真正的有限细化。

并发精化中，新增局部赋值步骤常不改变规格变量标记，停顿等价因此能连接不同原子性粒度。但若环境可在内部阶段读到共享状态，这些步骤已不再不可观察，标记接口必须扩大。

观察接口决定结果 ​

状态 $s,t$ 是否“相同”取决于标记 $L(s),L(t)$。只观察 done 时，两个内部缓冲状态可以同块；加入命题 buffer-full 后，它们可能分属不同块。

因此停顿等价不是状态图本身的绝对属性，而是相对于原子命题集合和标记函数。删掉关键命题可以制造过粗等价，保留实现私有变量又会阻止合理抽象。

轨迹投影公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。删除不可见动作，停顿压缩重复状态标记；二者作用对象不同。一个内部动作即使隐藏，若改变了可观察命题，状态词仍会多出新块。

检查等价时不能只比较压缩后的若干有限样本。两个系统可能在任意给定深度内都只重复 idle，一个最终转到 done，另一个存在永久 idle 路径；完整无限行为集合仍不同。有限状态算法需要同时处理可达块变化和保持同标记的循环，才能识别发散尾部。

若路径含有限终止，还要区分“最后状态永久停顿”的无限化与真正没有后继。补自环后它们产生相同状态词，适合不观察终止事件的逻辑；若正常退出与死锁必须区分，就应加入不同命题或显式结束标签，否则停顿商会把关键结果合并。

参考资料

• Leslie Lamport, “What Good Is Temporal Logic?” in Information Processing 83, North-Holland, 1983, pp. 657–668。
• Doron Peled and Thomas Wilke, “Stutter-Invariant Temporal Properties are Expressible without the Next-Time Operator,” Information Processing Letters 63(5), 1997, pp. 243–246。
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999, §§2.3, 10.4。