Petri 网展开与有限完备前缀

状态图把“先做甲后做乙”与“先做乙后做甲”画成两条路径；若二者使用独立资源，这只是同一次并发活动的两种排队方式。展开保留甲、乙没有因果先后的事实，用一个配置代表这些交错。

另一方面，共享输入资源的两项选择不能一起进入配置。因果无先后不自动等于可并发，还必须排除冲突。

两个独立任务只需两个事件 ​

初态在 $p,q$ 各有一个 token。变迁 $a:p\to p^{\prime }$，$b:q\to q^{\prime }$。展开含初始条件 $p_0,q_0$，事件 $a_0,b_0$ 以及输出条件 $p_0^{\prime },q_0^{\prime }$。

$a_0$ 与 $b_0$ 没有因果关系，也不冲突。配置有 $\varnothing$、$\{a_0\}$、$\{b_0\}$、$\{a_0,b_0\}$。最后一个配置同时代表执行 $ab$ 和 $ba$，终态都在 $p^{\prime },q^{\prime }$ 各有一个 token。

若再加入 $c:p\to r$，展开中的 $c_0$ 与 $a_0$ 消耗同一个条件 $p_0$，因此冲突；$\{a_0,c_0\}$ 不是配置，即使两事件之间没有有向路径。

循环为什么复制 token 实例 ​

若网只有 $t:p\to p$，初态一个 $p$ token，那么展开为

每个 $p_i$ 标签都是同一个原库所 $p$，每个 $t_i$ 标签都是 $t$，但实例不同。直接把 $p_1$ 与 $p_0$ 合并会重新制造环，并丢失“第几次发生”的因果信息。

有限完整前缀凭什么截断 ​

有界网虽然展开可无限，但能构造保留全部可达 marking 所需信息的有限完整前缀。典型规则将某事件的局部配置与一个更早配置比较：若到达相同 marking，且后者在合适的 adequate order 中更小，就把该事件标为 cutoff，不继续扩展其后代。这里的顺序须良基、与有限扩展相容，并细化配置的严格包含关系，即 $C⊊C^{\prime }$ 蕴含 $C\prec C^{\prime }$。[1]

上面的单循环中，发生一次 $t$ 后又回到同一个 marking，可由较早的空配置代表未来，因此很早就能截断。一般并发网中，任意遇到相同标签就合并不够；比较的是配置到达的完整 marking，并须使用保证完整性的顺序条件。

展开适合分析可达 marking、死锁及因果冲突。其优势取决于并发结构：$n$ 个互不依赖的一次性事件有 $n!$ 种全序交错，却可由 $n$ 个事件的一份偏序表示。若模型主要是冲突选择，展开仍可能指数大。

偏序约简公理库偏序约简Partial-order reduction · POR · Ample-set reduction利用独立并发动作的可交换性只探索等价交错代表，并以 proviso 保存死锁与时序性质。通常从状态探索中删去冗余交错；展开则显式构造事件及 token 的因果结构。二者目标相近，保存的数据对象和正确性证明不同。Mazurkiewicz 迹公理库Mazurkiewicz traceMazurkiewicz trace · Trace monoid · Partially commutative word以独立动作的相邻交换对执行词取商，使一个 trace 表示同一因果偏序的全部交错。把独立动作交换归为同类，可帮助理解交错如何对应同一个配置。

本页没有声称任意无界网都能靠同样规则得到有限完整前缀。离开 1-safe 或有界范围时，需要额外的多重 token 处理和明确的终止条件。