Petri 网

生产者—消费者轨迹 ​

容量一缓冲区可用库所 empty、full 表示，初态在 empty 有一个 token。变迁 produce 消耗 empty 并产生 full；consume 反向移动 token。

状态轨迹为

在 (0,1) 中 produce 不使能，因此容量一约束由 token 守恒直接表达。若错误地让 produce 不消耗 empty，连续触发会在 full 累积多个 token，模型已不再表示单槽缓冲区。

多个生产者可共享 empty token，竞争同一资源；谁先触发由非确定性选择，不隐含概率或公平调度。

若要允许容量 $k$，可让 empty 初始有 $k$ 个 token。每次 produce 消耗一个空槽 token、consume 归还一个，守恒式变为 $M(empty)+M(full)=k$。这与把 full 库所弧权重改成 $k$ 不同；后者要求一次变迁成批消费或产生 $k$ 个 token，改变了单次操作语义。

带身份的数据不能由普通无色 token 区分。若需要知道哪个消息或进程持有资源，应扩展为 colored Petri net，或把有限身份展开成多个库所；前一种扩展的高层语法最终仍需给出精确 firing semantics。

并发、冲突与 step ​

若两个变迁的输入资源互不冲突，它们可以独立触发；在合适 marking 下，先 $t_1$ 后 $t_2$ 与反向顺序到达同一 marking。Petri 网可把二者视为一个并发 step，而不仅是两条交错路径。

若 $t_1,t_2$ 竞争同一个单 token 库所，则只能选一个，形成 conflict。结构上的共享输入提示冲突，但若库所有两个 token，两者仍可同时使能；判断要结合 marking 和弧权重。

并发不等于“图上没有路径相连”。两个变迁可能通过其他库所间接共享守恒资源，局部外观独立却无法同时发生。

place invariant 与 token 守恒 ​

令 incidence matrix $C=Post-Pre$。列向量 $y\in {\mathbb{Z}}^{|P|}$ 若满足

则任意触发保持 $y^{T}M$。对缓冲区，$M(empty)+M(full)=1$ 是 place invariant，证明任意可达 marking 都恰有一个容量 token。

这类线性不变量给出不可达性的充分证据，却通常不能刻画全部可达 marking。满足所有已知守恒方程的 marking 仍可能因触发顺序约束而不可达。

transition invariant $Cx=0$ 则描述一组变迁计数净效应为零；它表示潜在循环的代数必要条件，不自动保证这些变迁可按某顺序从给定初态触发。

对任意触发序列 $\sigma =t_1\cdots t_n$，令 Parikh 向量 $\overrightarrow{\sigma }(t)$ 统计每个变迁出现次数，则状态方程

成立。它遗忘顺序，适合快速排除目标：若不存在非负整数向量解，目标必不可达；有解却可能因中间 token 不足而无法排成合法 firing sequence。

例如两个变迁的净效应相互抵消，状态方程允许各触发一次，但第一个所需 token 只有第二个先产生，而第二个又依赖第一个，初态下二者均未使能。线性方程没有捕捉这个循环依赖。

可达、有界与活性边界 ​

reachability 问是否存在触发序列从 $M_0$ 到目标 $M$。boundedness 问每个库所 token 是否在全部可达 marking 上有有限上界；safe net 是每库所至多一个 token 的特例。

dead marking 没有使能变迁。它可能是正常完成，也可能是死锁，取决于规格。liveness 的多种定义还会要求某变迁从任意可达 marking 未来仍可能触发，不能从“当前使能”直接推出。

普通 P/T 网没有 inhibitor arcs、优先级、时间或概率。加入这些扩展会改变使能规则和可判定性，不能把彩色、时间或随机 Petri 网的结论无条件搬回基础模型。

覆盖性（coverability）问是否能到达某个 $M^{\prime }\ge M$，比精确可达性更适合表达“某库所至少积累若干 token”。Karp–Miller tree 用 $\omega$ 概括无界增长，但它证明覆盖和有界性，不直接给任意目标 marking 的精确可达序列。把 coverable 误写成 reachable 会把“至少这些资源”与“恰好这个全局配置”混为一谈。

给定初始标识的有界性要求存在有限 $K$，使从这个 $M_0$ 可达的每个 $M$、每个库所 $p$ 都满足 $M(p)\le K$。结构有界性则要求对每个有限初始标识 $M_0$ 都有这样的界 $K_{M_0}$；界可随初始标识变化。例如单库所变迁消费一个 token、产生两个，从零初始标识出发没有动作且有界，从一个 token 出发则可无限增长，所以该网不是结构有界的。仅检查弧权重有限不能推出任何这类全运行上界。

逐坐标比较 token 向量时，Dickson 引理理路Dickson 引理Dickson lemma自然数向量的逐坐标序为良拟序；用逐坐标抽取证明，并手算二维最小基和维数变化的边界。保证这个顺序是良拟序；普通变迁的使能和更新公式又保证增加资源不会阻止同一变迁。两项合起来使网成为良结构转移系统理路良结构迁移系统Well structured transition system · WSTS把良拟序与迁移兼容性分开验证，以普通 Petri 网和零测试说明何时能安全地用大状态模拟小状态。。添加零测试可能破坏后一项，即使自然数向量的良拟序性质仍未改变。