k 归纳

一步屏障不够时，多看一段历史 ​

普通归纳假设当前一个状态安全，便要求下一状态安全。$k$ 归纳要求连续 $k$ 个前态都安全，再证明下一状态安全。有些不可达状态虽然自己安全，却根本没有足够长的安全前缀；扩大窗口会把这些干扰排除。

窗口不能代替入口检查。一个系统可能从一开始就坏，此时“连续若干步安全”永远不成立，归纳步空真。base 的任务是把实际初始执行接进这个归纳规则。

一步失败，两步成功 ​

取 $S=\{0,1,2,3\}$，$I=\{0\}$，全部转移为

$k=1$ 时，$B_1$ UNSAT，因为初态0安全；$D_1$ SAT，见证为 $(2,3)$。这不是实际错误轨迹，因从0只能到1，再停在1。

$k=2$ 时，$B_2$ 同时检查深度0和1，只有初态0及其后继1，都安全。若 $D_2$ SAT，需要两个连续安全状态 $u,v$ 再到3。能到3的安全 $v$ 只能是2，但图中没有进入2的边，所以这样的窗口不存在，$D_2$ UNSAT。二式一起证明全局安全。

如果仅报告“BMC查了两步没错”，还没有这个全局结论；证书中必须另交任意起点的 $D_2$ 排除理由。

不可达安全环使所有k都失败 ​

在同一图添加 $2\to 2$。实际可达集仍为 $\{0,1\}$，性质仍真，但对每个 $k\ge 1$ 都有

满足 $D_k$。因此只是不停加大 $k$，不保证有限状态安全系统最终得到证明。下载脚本复算 $k=1,\dots ,8$；上面的任意 $k$ 构造才证明全部深度都会失败。

可加入已独立验证的辅助不变式 $Q(s)\equiv s\le 1$，用 $P\wedge Q$ 做一步归纳。初态0满足，边 $0\to 1,1\to 1$ 保持，故可直接证明并推出 $P$。若 $Q$ 只是未经验证的猜测，不能悄悄用它排除状态2；可先通过Houdini理路Houdini 不变式推断Houdini invariant inference · Houdini algorithm从有限谓词候选中反复剔除初始化或保持失败项，输出可独立复核的归纳合取，并证明候选语言内的最大性。或人工归纳检查建立证书。

别把不可延长短路径丢掉 ​

设系统只有初态0，0已经坏且没有出边。$B_3$ 的 $j=0$ 支仍可满足，准确报告错误。若误把 base 写成必须先走满两条转移再问此前是否坏，整个公式不可满足，会漏掉这个短反例。本页逐个前缀的析取避免依赖停顿补边。

另取一个坏初态自环系统。$D_1$ 由于要求安全源状态而 UNSAT，$B_1$ 却 SAT。这个例子说明归纳步通过并不足够，甚至不能证明初始执行的第一瞬间安全。

证书、成本和增强版本 ​

一个可检查报告应包括 $k$、状态编码、$I,T,P$、各 base 深度的结果、归纳步查询及其证据。真实反例要给从初态开始的逐步路径；归纳失败要明确标记为可能不可达的窗口；unknown 和超时均不给安全结论。

按时间帧共享前缀的布尔电路表示，base 的各前缀可以逐层增量建立，$k$ 个深度总构造规模为 $O(|I|+k(|T|+|P|+1))$；step 同样复制 $k$ 帧。若不共享而把每个前缀完整复制，base 大小可能增至二次量级。公式规模线性不表示 SAT/SMT 求解时间线性，显式枚举长度 $k$ 的路径也可能指数增长。

有限状态系统可进一步在归纳窗口加入“两两状态不同”的简单路径条件。其可靠性需回到最短坏路径：最短路径不会重复状态，否则删去环可得到更短坏路径。因此，当 base 覆盖相应短长度时，排除所有简单安全窗口已足够；有限状态也限制了这种窗口的最大长度。原文[1]讨论该增强及增量求解。本页脚本没有加入唯一状态条件，上面不可达自环反例正用于说明基础版本的边界。

PDR/IC3理路Property-Directed Reachability / IC3Property-directed reachability · PDR · IC3以 SAT 查询阻塞坏状态前驱、学习逐层归纳子句，最终得到反例或安全归纳不变式。通过学习阻塞子句得到归纳屏障，k归纳通过展开窗口寻找证明；二者可配合辅助不变式，但不是同一个算法的不同名字。

迁移练习：将原四状态图的初态改成2。$k=1$ 的 base 仍通过而 step 失败；$k=2$ 的 base 在深度1发现真实路径 $(2,3)$，应报告不安全，不能因原来的 $D_2$ UNSAT 就重用安全结论。初始化也是证书的一部分。