停顿等价

实现微步的例子 ​

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

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

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

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

为什么 next 会破坏等价 ​

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

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

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

状态关系版本 ​

系统级停顿关系把一个系统的一步匹配为另一个系统的有限多步，其中中间状态与起点或终点具有相同观察。精确的状态关系定义还须规定双向匹配及中间状态如何与关系中的端点对应，不能只要求标记相同。若证明用零步匹配隐藏具体内部推进，还要另证不会遗漏相关的发散行为；良基停顿排名是常用的充分工具，并不是所有停顿等价证明都必须采用的唯一证书。

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

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

观察接口决定结果 ​

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

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

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

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

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