Petri 网覆盖性的复杂度

“存在有限覆盖树”只说明可判定。为了给复杂度上界，必须进一步控制最短成功执行有多长、过程中数值有多大、存储这些数值要多少位。

反过来，一个小例子很快收敛，也不能反驳最坏情况困难性。复杂度下界是在整个输入家族上说，某些系统能利用资源增长和控制结构模拟非常昂贵的计算。

路径极长，存储可以少得多 ​

设某证明给出成功执行长度不超过

的界。若每步计数增量的绝对值不超过输入给定的 $W$，沿这样的路径各坐标最多增长到 $\Vert M_0{\Vert }_{\mathrm{\infty }}+LW$。保存一个坐标所需位数为

逐步猜测变迁只需保存当前向量和长度计数器，无需存储整条路径。Rackoff 型短见证定理由此给出非确定指数空间上界；用Savitch 空间确定化公理库Savitch 定理Savitch's theorem通过配置可达性的中点递归与工作区复用，把非确定空间 s 确定化为平方空间。，平方空间仍为指数空间。[1] 双指数步数与指数空间并不冲突。

这段计算是从见证长度界推出空间界的机制，不是独立证明那个深刻的长度定理。长度界本身通过分层控制小计数器、把足够大的计数器暂时当作可供资源，再归纳修补执行来建立。

数字编码会改变输入长度 ​

一个无输入弧、每次只产生一个 token 的变迁，要覆盖目标 $2^k$，需要 $2^k$ 次触发。若目标二进编码，目标只占 $k+1$ 位；一元编码则已占 $2^k$ 个符号。这个例子说明测量路径长度必须先写清编码。

但它本身没有证明 EXPSPACE 困难：保存当前计数只需 $O(k)$ 位，问题答案也显而易见。长执行、难决定与大空间三者不能靠同一个例子自动等同。

Karp–Miller 树公理库Karp–Miller 覆盖树Karp-Miller tree用沿祖先的增长比较将 Petri 网无界计数加速为 omega，手算树并以奇偶约束区分覆盖与精确可达。给结构清晰的终止算法，但其朴素构造的最坏复杂度不能直接等同于覆盖问题的最优 EXPSPACE 上界。问题复杂度与某个算法的开销必须分开评价。

后向基搜索公理库覆盖性的后向基算法Backward coverability algorithm从向上闭坏状态反向扩展有限基，给出 Petri 网前驱公式、完整小例运行与终止和安全不动点证明。在许多小模型中有用，不过其有限基也可能迅速变大。实践上可以先用守恒不变量、支配删除和结构约束排除目标，仍需如实报告未解决实例，不能把超时当成安全结论。

精确可达性问 $M=b$，而覆盖性只问 $M\ge b$；二者有不同的复杂度理论。引用覆盖性的 EXPSPACE 完全性不能替精确可达性定级，也不能给其他扩展网模型贴同一个标签。