不变式与归纳不变式

形式陈述

设状态机 $M=(S,I,\to)$ ，可达集合 $\operatorname{Reach}(M)$ 包含所有从某个初始状态经有限步到达的状态。谓词 $P:S\to\{\mathsf{true},\mathsf{false}\}$ 是不变式，若

\forall s\in\operatorname{Reach}(M),\qquad P(s).

它陈述的是语义事实：真实可达的状态全都满足 $P$ 。

$P$ 是归纳不变式，若同时满足初始性与一步保持性：

\forall s\in I, P(s),

\forall s,s'\in S,\qquad P(s)\land s\to s'\Longrightarrow P(s').

第二个量词覆盖所有满足 $P$ 的状态，包括不可达状态。这个额外强度使归纳不变式可以直接用数学归纳法证明所有有限执行都留在 $P$ 内。

取任意长度为 $n$ 的执行

s_0\to s_1\to\cdots\to s_n,\qquad s_0\in I.

基例由初始性得到 $P(s_0)$ 。若 $P(s_k)$ 已成立，一步保持性与 $s_k\to s_{k+1}$ 推出 $P(s_{k+1})$ 。因此对每个 $n$ 与每条长度为 $n$ 的执行都有 $P(s_n)$ ，即归纳不变式一定是不变式。

若坏状态集合为 $B\subseteq S$ ，找到归纳不变式 $P$ 满足

I\subseteq P,\qquad \operatorname{post}(P)\subseteq P,\qquad P\cap B=\varnothing,

便证明坏状态不可达。 $P$ 在这里充当把初始区域与坏区域分开的归纳屏障，而不是对若干测试执行的经验总结。

若部分转移由控制器选择，安全博弈中的可控不变集只要求每个控制器顶点存在一个留在集合内的后继，而每个环境顶点的所有后继都留在集合内。固定这样的控制策略、保留全部环境选择后，集合才对所得转移系统满足通常的一步闭包；未被选择的控制器边不属于这个闭包义务。

直觉

考虑状态集 $S=\{0,1,2\}$ ，初始集合 $I=\{0\}$ ，转移只有

0\to0,\qquad 1\to2,\qquad 2\to2.

从初始状态只能到达 $0$ 。谓词 $P(s)\equiv(s\ne2)$ 在全部可达状态上为真，所以它是不变式；但 $P(1)$ 为真且 $1\to2$ ，而 $P(2)$ 为假，因此一步保持性失败。

问题出在不可达的状态 $1$ 被 $P$ 纳入了证明范围。更强的谓词 $Q(s)\equiv(s=0)$ 排除这个干扰状态，既包含所有初始状态又对转移闭合，于是成为归纳不变式。所谓归纳加强，是给目标安全性质增加辅助约束，使它足够强到能自己维持。

“加强”指允许状态集合变小：若用集合表示谓词， $Q\Rightarrow P$ 等价于 $\{s:Q(s)\}\subseteq\{s:P(s)\}$ 。增加合取条件在逻辑上更强，在集合包含次序上却更小，方向不能混淆。

Houdini候选筛选把这一次序区别用于可执行算法：删掉候选会扩大归纳源状态集，可能触发下一轮失败；返回候选最多的有效子集，所定义允许状态集合反而最小于该候选合取族。k归纳另以安全窗口排除部分不可达干扰，但仍需从初态开始的base证书。

例子与边界

设两个计数器 $x,y\in\mathbb N$ ，初始为 $(0,0)$ ，每一步要么同时令二者加一，要么保持不变。目标是证明 $x\le y$ 。它确实归纳，但只验证这个目标会隐藏系统更精确的结构。

谓词

Q(x,y)\equiv x=y

在初始状态成立，同时加一和停顿都保持相等，因此 $Q$ 是归纳不变式，并由 $x=y\Rightarrow x\le y$ 推出目标。若实现新增一步只增加 $y$ ， $x\le y$ 仍可能保持，而 $x=y$ 不再保持；辅助不变式是证明手段，不必是系统允许行为的最宽描述。

在并发协议中，常需把互斥目标与控制位置、所有权、消息计数或任期单调性一起加强。随意堆叠“看起来合理”的断言不够，每个合取项都必须在所有转移下闭合。

推论与应用

循环不变式是程序控制流上的特例：初始化对应进入循环头，一步保持对应执行一次循环体，退出条件与不变式共同推出后置条件。循环终止还需变元或良基关系，归纳不变式本身只证明安全，不保证最终离开循环。

显式模型检查可以先计算精确可达集合，它本身是最小的归纳闭集；无限状态系统通常无法枚举该集合，便用可表达的较大集合 $P$ 包住它。PDR/IC3 通过 SAT 查询逐层学习子句，目标正是得到足以排除坏状态的归纳不变式。

不变式也不等于任意时序性质。“请求最终得到响应”允许中间状态反复变化，不能表示成某个状态集合永远封闭；它是活性条件，需要时序逻辑和公平性假设。

Petri 网中有一类可直接从结构读出的布尔不变量：虹吸一旦为空便保持空，陷阱一旦被标记便保持被标记。它们跟踪资源集合的空与非空，不要求 token 数精确守恒，因此与线性 place invariant 提供不同的安全证据。

参考资料

Amir Pnueli, “The Temporal Logic of Programs,” FOCS, 1977, pp. 46–57。
Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999, Chs. 1–2。
Aaron R. Bradley and Zohar Manna, The Calculus of Computation, Springer, 2007, Chs. 12–14。
Robert W. Floyd, “Assigning Meanings to Programs,” in Mathematical Aspects of Computer Science, AMS, 1967, pp. 19–32。