良结构迁移系统

$s⪯t$ 表示 $t$ 拥有足够多的资源，至少可以模仿 $s$ 的一次行为。若系统增加资源反而禁用操作，就可能破坏这种关系。良拟序保证状态摘要不能无限变新，兼容性保证这些摘要确实尊重程序行为。

这是一种单向模拟：大状态可以跟随小状态，不表示小状态也能重现大状态的所有行为。覆盖性只问能否达到“不少于目标”的状态，正好利用这一方向。

普通 Petri 网逐式核验 ​

对 Petri 网公理库Petri 网Petri net · Place-transition net · P/T net以库所、变迁和 token 多重集建模资源、同步与真正并发，并研究可达标识。，状态为自然数向量 $M$，顺序逐坐标。Dickson 引理公理库Dickson 引理Dickson lemma自然数向量的逐坐标序为良拟序；用逐坐标抽取证明，并手算二维最小基和维数变化的边界。给出 wqo。若变迁 $t$ 在 $M$ 使能，即 $M\ge {\mathrm{Pre}}_t$，且 $N\ge M$，则 $N$ 也使能同一变迁，并且

例如变迁消耗 $(1,2)$、产生 $(0,1)$：从 $(2,3)$ 到 $(1,2)$，从更大的 $(4,3)$ 到 $(3,2)$，顺序仍保持。条件与结论都可直接检查，没有依赖抽象的“资源越多越好”口号。

零测试破坏的不是良拟序 ​

考虑控制状态 $q$ 和计数器 $n$，允许仅在 $n=0$ 时转到终态 $r$。虽然 $(q,0)⪯(q,1)$，小状态可以转移，大状态却没有对应操作；若没有其他降到零的路径，连多步兼容也失败。

状态空间仍是有限控制乘以 $\mathbb{N}$，依然 wqo。失败发生在迁移与顺序的接口，因此不能用“计数器是自然数”就证明整个系统 WSTS。Petri 网的 inhibitor arc 正会引入这类零测试。

结构良好仍需可计算接口 ​

即使某个向上闭集合数学上有有限基，也未必能从所给程序描述中求出它。后向算法需要：给目标基点 $b$，计算能一步到达 $\uparrow b$ 的状态集合的有限基；在一般多步兼容版本中，文献采用 $\uparrow \mathrm{Pre}(\uparrow b)$ 的有效基接口。[1, §3]

强兼容保证 $\mathrm{Pre}(U)$ 对每个向上闭 $U$ 仍向上闭。于是 后向覆盖算法公理库覆盖性的后向基算法Backward coverability algorithm从向上闭坏状态反向扩展有限基，给出 Petri 网前驱公式、完整小例运行与终止和安全不动点证明。可以反复计算有限前驱基，wqo 则保证增长链最终稳定。

兼容性不能把覆盖性偷换成精确可达性。即使 $s^{\prime }$ 被某可达状态覆盖，额外 token 或消息未必能随意删除；要到达恰好 $s^{\prime }$，仍可能有不同障碍。

也不能从“覆盖性可判定”推广到任意时序逻辑、互模拟或终止问题。不同问题可能需要有限分支、严格兼容、公平性约束或其他独立条件。