轨迹与路径语义

隐藏内部步骤的例子 ​

设服务收到 request 后有两条内部路径：缓存命中时执行 ${\tau }_{cache}$，缓存未命中时执行 ${\tau }_{db}$；两者最后都发出 reply。完整路径可以是

或

删除内部标签后，两条路径都有可见轨迹 request reply。若 $s_3$ 以后允许 fast-renew，而 $s_5$ 只允许 slow-renew，当前短轨迹仍看不出这项分支差异；观察更长轨迹才可能区分。

相同轨迹也可能掩盖分支时机。系统 $P$ 先唯一执行 $a$ 到状态 $p$，再由 $p$ 选择 $b$ 或 $c$；系统 $Q$ 在初态就有两条同标号 $a$ 边，分别到只允许 $b$ 与只允许 $c$ 的状态。二者有限可见轨迹同为

但 $P$ 在 $a$ 后仍同时提供 $b,c$，$Q$ 的某次 $a$ 已经承诺其中一个。环境若能在 $a$ 后选择交互动作，就可能分辨它们。trace equality 看不见这项差别；逐步互模拟或 ready semantics 保留了更多分支信息。

投影、隐藏与重命名 ​

给定可观察动作集 $O\subseteq A$，投影 ${\pi }_O$ 删除不在 $O$ 中的动作。组件组合后，可用投影只观察某个接口；隐藏则把选定动作改成 $\tau$。重命名函数 $r:A\to B$ 可以把实现级事件归并到规格级事件。

这些操作必须作用于整条行为并尊重顺序。仅比较“出现过哪些动作”的集合会丢失先后与重复次数，例如 open close 和 close open 拥有相同动作种类，却显然不是同一轨迹。

投影也不总与最大性相容。一条包含无限多个内部步骤、但只有有限多个可见动作的路径，投影后可能成为有限轨迹；这就是 divergence。若语义把它与正常终止视为相同，就会掩盖系统永远在内部忙等的事实，因此有些模型另外记录发散标记。

状态轨迹与停顿 ​

若状态带原子命题标记 $L:S\to 2^{AP}$，路径还可投影为状态词

连续若干状态可能拥有同一可观察标记。把有限次重复压缩后比较得到停顿等价；它适合把实现内部微步视作不可见，但含 next 运算子的时序公式一般能数出这些重复，因而不保持该等价。

路径语义不会自动规定公平性。一个始终使能却永不执行的动作，仍可能出现在系统允许的无限路径中；要排除这种调度，需要另加公平性约束。把期望的公平路径直接从例子中挑出来，会把规格假设伪装成模型事实。

语义边界与使用方式 ​

轨迹等价只比较所选观察接口下的行为集合。接口变粗，更多实现会变得等价；接口变细，原先隐藏的状态、时间或失败原因会重新可见。行为精化常写成

表示实现没有产生规格禁止的可见序列。任何这类结论都要同时给出动作字母表、隐藏集合和有限/无限语义；轨迹包含不会自动保持死锁自由、发散敏感性或分支结构。若这些也属于合同，应改用带 failures/divergence 的语义或更强的模拟关系。

时序逻辑公理库时序逻辑Temporal logic · Temporal modal logic在执行序列上解释下一步、最终、始终与直到，并区分线性时间和分支时间的统一规格层。在这些执行序列上解释“最终”“始终”“直到”；反例与见证轨迹把逻辑失败还原成一条可读行为。逻辑是对行为集合提出性质，不替代本页对行为本身的定义。