轨迹与路径语义

隐藏内部步骤的例子 ​

设服务收到 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 拥有相同动作种类，却显然不是同一轨迹。

投影也不总与最大性相容。比较两条完整行为：一条在 request reply 后正常结束，另一条在同样两个可见动作后无限执行 $\tau$。删除内部步骤后，两者都是有限词 request reply，但后一条路径从未终止。这种无限内部执行称为发散；若语义需要区分它与正常终止，就必须额外记录完成或发散信息。

状态轨迹与停顿 ​

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

连续若干状态可能拥有同一可观察标记。停顿等价允许把每个相同标记块作有限次重复，同时保持块的次序。比如 $\varnothing ,\{p\},\{p\},\dots$ 与 $\varnothing ,\varnothing ,\{p\},\{p\},\dots$ 只差初始空标记多停一步：两者都满足 $Fp$，但只有前者在位置零满足 $Xp$。

这里不能把“有限次重复”扩展成无限等待。${\varnothing }^{\omega }$ 永远不到达 $p$，与上述两个词都不等价；否则连最终到达这种活性也会丢失。含 next 的公式会观察一步粒度，不含 next 的 LTL 则保持这种通常的停顿等价。

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

语义边界与使用方式 ​

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

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

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

若要求同一公开输入的不同运行给出相同公开输出，检查对象就是两条轨迹之间的相容关系。这属于超性质公理库超性质Hyperproperty · Hyperproperties从确定性自组合进入有限非确定程序，以全称运行、存在匹配运行刻画输出集合相等，并构造完整匹配证书。：它直接约束整套轨迹集合，不能当作一个逐轨迹解释的 LTL 公式来检查。

当合同允许非确定输出、只要求不同秘密输入具有相同的可能输出集合时，公开投影可能过早遗忘所需的信息。有限运行匹配例子公理库超性质Hyperproperty · Hyperproperties从确定性自组合进入有限非确定程序，以全称运行、存在匹配运行刻画输出集合相等，并构造完整匹配证书。保留每条完整运行的秘密输入标签，然后在相同公开输入下要求每次运行都存在一个输出相同的匹配运行。两个程序可以拥有相同的公开轨迹并集，却有不同的按秘密索引的输出集合；观察投影和规格量词的解释域必须分别写清。