覆盖性的后向基算法

前向搜索问“还能走到哪里”，可能不断生产更大的资源。后向搜索改问“至少需要哪些资源才能出事”。某个阈值一旦被更小的阈值替代，原先表示的所有大状态自动保留，无需逐个存储。

不变量是：第 $n$ 轮的 $U_n$ 恰为至多 $n$ 步能进入坏状态集的状态。最终不动点因此收集了所有能出事的起点；它的补集是不会一步进入该集合的安全区域。

Petri 网的前驱公式 ​

对目标阈值向量 $b$ 和变迁 $t$，使能且覆盖 $b$ 的最小前驱是

最大值逐坐标取。它同时保证输入 token 足够、扣除输入再加输出后不少于目标。只倒减净变化可能给出负数或不使能的伪前驱。

从三个 token 的坏状态倒推 ​

两库所 $p,q$，变迁 $a:p\to 2q$，$b:q\to p$；初态 $(1,0)$，坏条件是 $q\ge 3$。初始基 $B_0=\{(0,3)\}$。

第一轮由 $a$ 得 $(1,1)$，由 $b$ 得 $(0,4)$，后者已被 $(0,3)$ 支配，故

再算 $(1,1)$ 的前驱：$a$ 给 $(2,0)$，$b$ 给 $(0,2)$。删去被 $(0,2)$ 支配的 $(0,3)$，得

第三轮，$(0,2)$ 经 $a$ 的前驱是 $(1,0)$，它支配后两个旧基点；于是 $B_3=\{(0,2),(1,0)\}$。初态已在其中，所以坏状态可达。对应见证为

若继续，$(1,0)$ 经 $b$ 的前驱是 $(0,1)$，最终基为 $\{(1,0),(0,1)\}$ 并稳定：恰好所有非空 marking 都能覆盖坏阈值，空 marking 永远不能。

为什么会停，为什么可能很慢 ​

$U_n$ 是向上闭增长链。若它无限严格增长，每轮挑一个新点，就得到良拟序公理库良拟序Well quasi order · WQO用每条无限序列中的顺向可比对定义良拟序，证明向上闭集有限基和增长链终止，并辨别良基与良拟序。禁止的无限坏序列。因此算法最终停止。

但基的大小、每轮前驱的数值和轮数均可能很大。对 $r$ 个 $d$ 维候选做朴素最小化需 $O(r^{2}d)$ 次坐标比较；这只是单轮局部开销，不能据此宣布整个算法多项式。

若稳定基 $B$ 没有覆盖初态，则 $s_0\notin \uparrow B$，且安全区域 $S\setminus \uparrow B$ 对迁移封闭。这同时给出否定答案和一个可复核的归纳安全证明。

坏集合必须向上闭，或先证明所作向上闭包是允许的抽象。若规格是“恰好两个 token”，直接替换为“至少两个”可能产生额外反例；此算法回答的是覆盖，不是任意精确可达性。