轨迹与路径语义

路径先于轨迹 ​

给定标号转移系统公理库标号转移系统Labeled transition system · Labelled transition system · LTS在状态转移上标记动作，明确路径、可达性、使能动作以及终止与死锁的行为模型。 $\mathcal{L}=(S,I,A,\to )$，一条路径是

$$\pi =s_0{a}_0{s}_1{a}_1{s}_2\cdots ,s_0\in I,s_i\stackrel{a_i}{\to }{s}_{i+1}.$$

路径保留内部状态和每一步的动作标签。有限路径有最后状态；无限路径包含可数无限多步；若一条有限路径的末状态无后继，它是最大路径。分析持续服务时通常关心无限路径，分析会终止的程序时则不能把有限最大路径丢掉。

动作轨迹是路径的动作投影

$$\mathrm{tr}(\pi )=a_0{a}_1{a}_2\cdots .$$

若存在不可观察动作 $\tau$，可见轨迹还会删除所有 $\tau$。因此轨迹是观察接口选择后的结果，不是路径的另一个拼写。

执行历史公理库执行历史Execution history · History区分并发对象接口历史与分布式系统完整执行的总览。常记录并发操作的调用、返回和事件偏序；LTS 路径则由局部转移关系生成一个线性化步骤序列。二者可以互相编码某些观察，却不应默认每份并发历史都已经选择了唯一全序路径。

行为集合与前缀 ​

系统的路径语义和轨迹语义分别是它允许的路径集合与轨迹集合：

$$\mathrm{Paths}(\mathcal{L})=\{\pi :\pi \text{ 是从 }I\text{ 出发的路径}\},$$$$\mathrm{Traces}(\mathcal{L})=\{\mathrm{tr}(\pi ):\pi \in \mathrm{Paths}(\mathcal{L})\}.$$

若只收集有限前缀，则每条轨迹的每个有限前缀也在集合中，形成 prefix-closed 语义。这非常适合安全性：一旦坏事发生，某个有限前缀已经足以见证违反。活性通常需要完整无限行为，因为任意有限前缀仍可能在未来兑现承诺。

有限轨迹集合是否包含非最大前缀必须明确。把“用户发出请求”这一半截执行算作系统完成行为，和仅把它算作可继续前缀，会得到不同的 refinement 与测试结论。

隐藏内部步骤的例子 ​

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

$$s_0\stackrel{request}{\to }{s}_1\stackrel{{\tau }_{cache}}{\to }{s}_2\stackrel{reply}{\to }{s}_3$$

或

$$s_0\stackrel{request}{\to }{s}_1\stackrel{{\tau }_{db}}{\to }{s}_4\stackrel{reply}{\to }{s}_5.$$

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

更强的例子是两个系统拥有完全相同的可见轨迹集合，却在每一步的分支时机不同。环境若能在分支之后选择交互动作，就可能分辨它们。互模拟保留逐步分支结构，通常比单纯 trace equivalence 更强。

投影、隐藏与重命名 ​

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

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

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

状态轨迹与停顿 ​

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

$$L(s_0)L(s_1)L(s_2)\cdots .$$

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

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

语义边界与使用方式 ​

轨迹等价只比较所选观察接口下的行为集合。接口变粗，更多实现会变得等价；接口变细，原先隐藏的状态、时间或失败原因会重新可见。因此任何“两个系统行为相同”的陈述都要同时给出动作字母表、隐藏集合和有限/无限语义。

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

参考资料

• C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985, Chs. 1–3。
• Robin Milner, Communication and Concurrency, Prentice Hall, 1989, Chs. 2–5。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, §§2.1–2.3, 3.2。