Karp–Miller 覆盖树

若同一条执行路径从 $x$ 走到 $y\ge x$，原来的操作可以在更多资源下再做一遍。每次都能增加同样的非负资源差，于是那些真正增长的坐标可以泵到任意大。

祖先关系提供可重复的具体路径；单纯数值比较没有这条路径作证。加速把重复执行的无限家族压成一个符号，而不会告诉我们所有中间整数都可精确达到。

一棵可以完整手算的小树 ​

两库所 $p,q$，初态 $(1,0)$。变迁 $a:p\to 3p$ 增加两个 $p$，变迁 $b:p\to q$ 把一个 $p$ 移到 $q$。

根经 $a$ 得 $(3,0)$，覆盖祖先 $(1,0)$，第一坐标严格增长，加速成 $(\omega ,0)$。根经 $b$ 得 $(0,1)$，两变迁均不使能，成为叶子。

在 $(\omega ,0)$ 上，$a$ 给相同标签，关闭；$b$ 给 $(\omega ,1)$，与祖先 $(\omega ,0)$ 比较后把第二坐标加速，得 $(\omega ,\omega )$。这里再触发 $a$ 或 $b$ 都保持相同标签，分别关闭。

这说明任意有限 $(r,s)$ 都可覆盖：先反复 $a$ 得到足够多的 $p$，再把其中 $s$ 个经 $b$ 移到 $q$，剩余 $p$ 仍可不少于 $r$。

覆盖成功不意味着精确到达 ​

该网每次 $a$ 使 token 总数加二，每次 $b$ 保持总数，所以所有可达 marking 总数为奇数。目标 $(0,2)$ 被树中 $(\omega ,\omega )$ 覆盖，也确实被可达的 $(1,2)$ 覆盖；但 $(0,2)$ 本身总数为偶数，永远不可达。

因此不能把一个 $\omega$ 随意换成目标数字，然后当成已经找到精确执行。线性同余、触发顺序等信息会被覆盖抽象抹去。

终止机制与模型边界 ​

每条分支上，一个坐标至多从有限值升级为 $\omega$ 一次。在最后一次升级之后，剩余有限坐标若产生无限分支，Dickson 引理公理库Dickson 引理Dickson lemma自然数向量的逐坐标序为良拟序；用逐坐标抽取证明，并手算二维最小基和维数变化的边界。会给出祖先可比对；严格增长应触发新的升级，无增长则遇到相同标签并关闭，矛盾。有限分支度再保证整树有限。

这个论证不包含有用的小运行时间界。添加 inhibitor arc、零测试或任意其他扩展后，“增加资源仍可重复原路径”可能失败，本算法的正确性不能沿用。

树中没有 $\omega$ 当且仅当这个给定初态的网有界；有限标签最大值可给各库所上界。若有 $\omega$，相应库所无界，但不是说单条有限执行拥有无限资源。

与后向有限基算法公理库覆盖性的后向基算法Backward coverability algorithm从向上闭坏状态反向扩展有限基，给出 Petri 网前驱公式、完整小例运行与终止和安全不动点证明。相比，Karp–Miller 从一个初态概括所有可覆盖阈值；后向算法从一个坏阈值集概括所有危险初态。二者共享单调性，保存的方向和摘要却不同。