返回学习路线

U15 单元验收：有限摘要究竟证明了什么 ​

任务 ​

对两库所网 $p,q$，初态 $(1,0)$，变迁 $a:p\to 3p$、$b:p\to q$，完成：Karp–Miller 加速树；坏条件 $q\ge 2$ 的后向最小基迭代；覆盖与精确可达的区分。再给出状态方程可解却不可达的小网。最后对有损 FIFO 信道分别说明 wqo 与迁移单调性的来源。

完整解答 ​

1. Karp–Miller 的每次加速都有祖先路径 ​

根 $(1,0)$ 经 $a$ 得 $(3,0)$，大于同一路径祖先且 $p$ 增长，故加速为 $(\omega ,0)$。根经 $b$ 得 $(0,1)$，不使能任何变迁，是终叶。

$(\omega ,0)$ 经 $a$ 仍为 $(\omega ,0)$，遇到相同祖先关闭。经 $b$ 得 $(\omega ,1)$，与 $(\omega ,0)$ 比较，$q$ 严格增长，加速为 $(\omega ,\omega )$。其两个后继均保持该标签，关闭。

含有 $(\omega ,\omega )$ 表示任意有限双坐标阈值可被覆盖：先执行足够多的 $a$，再用 $b$ 移动足够多个 token。它不是一条实际具有无穷 token 的执行。

2. 同一网的后向基 ​

每个变迁的最小前驱公式为 ${\mathrm{Pre}}_t+max(0,c-{\mathrm{Post}}_t)$。从 $B_0=\{(0,2)\}$ 开始，逐轮合并前驱并删除被支配的点：

$$B_1=\{(0,2),(1,1)\},$$$$B_2=\{(0,2),(1,1),(2,0)\},$$$$B_3=\{(0,2),(1,0)\}.$$

关键新点依次来自 $b$ 对 $(0,2)$ 的前驱、$b$ 对 $(1,1)$ 的前驱、$a$ 对 $(2,0)$ 的前驱。最后一轮 $(1,0)$ 支配 $(1,1)$、$(2,0)$。再次求前驱只得到已被这两个基点覆盖的点，所以稳定。

最终危险初态恰为“已有至少两个 $q$，或至少一个 $p$”。初态 $(1,0)$ 在其中，见证为

$$(1,0)\stackrel{a}{\to }(3,0)\stackrel{b}{\to }(2,1)\stackrel{b}{\to }(1,2).$$

基的向上闭包随轮次增长，虽然基列表中某些点被删除。删除的是冗余代表，不是已经发现的危险状态。

3. 不能把覆盖答案写成精确可达 ​

每次 $a$ 增加总数二，每次 $b$ 保持总数，所以从初态出发所有 marking 的总数都是奇数。$(0,2)$ 被 $(1,2)$ 覆盖，但自身总数偶数，故不可达。

要反驳“状态方程有解就可达”，另取初态 $(0,0)$，变迁 $t:p\to q$、$u:q\to 2p$，目标 $(1,0)$。发生次数向量 $(t,u)=(1,1)$ 满足

$$(0,0)+(-1,1)+(2,-1)=(1,0).$$

可是初态没有任何 token，两个变迁均不使能，唯一可达状态仍是 $(0,0)$。方程忘记了中间使能顺序。

4. 有损信道有两个独立证明义务 ​

每个配置由有限控制状态与有限字母表上的有限队列字组成。控制相同、各队列按散布子词比较；Higman 引理及有限乘积封闭性给出良拟序。这一步只谈集合与关系。

迁移单调性来自丢失语义：大队列可以先删去额外消息变成小队列，再模仿小队列的一步。可靠队列 ab 不能立刻接收 b，有损队列可先丢掉 a 再接收；这个小例子展示为什么无损系统不能套用同一模拟论证。

后向算法还需要可计算前驱基与可判定顺序。只证明 wqo，没有给有效性接口，不足以声称算法可运行；仅有每个有限基的存在性也不足够。

验收标准 ​

每个 omega 都须指出可比祖先和真正增长坐标；后向迭代须写出新基点来源及删除理由；覆盖结论须给实际有限执行；精确不可达须给独立不变量；状态方程反例须检查全部初态变迁；信道部分须把 Higman、丢失模拟和有效前驱分成三项。只画一个 omega 结点或只说“单调所以可判定”不通过。

依据 ​

Karp–Miller 覆盖树与结构方法见 Esparza《Petri Nets》讲义；有限基与有效前驱见 Finkel–Schnoebelen《Well-Structured Transition Systems Everywhere!》§§2–3；有损信道语义见 Abdulla–Jonsson《Verifying Programs with Unreliable Channels》。