不变式与归纳不变式

形式陈述 ​

两个容易混淆的量词 ​

设状态机公理库状态机State machine · Transition system用状态集合、初始状态和转移关系描述系统可能执行轨迹的模型。 $M=(S,I,\to )$，可达集合公理库集合Set由成员完全决定的数学对象；成员关系给出集合的内容，额外结构须另行指定。 $\mathrm{Reach}(M)$ 包含所有从某个初始状态经有限步到达的状态。谓词 $P:S\to \{\mathsf{true},\mathsf{false}\}$ 是不变式，若

$$\mathrm{\forall }s\in \mathrm{Reach}(M),P(s).$$

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

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

$$\mathrm{\forall }s\in I,P(s),$$$$\mathrm{\forall }s,s^{\prime }\in S,P(s)\wedge s\to s^{\prime }⟹P(s^{\prime }).$$

第二个量词覆盖所有满足 $P$ 的状态，包括不可达状态。这个额外强度使归纳不变式可以直接用数学归纳法公理库数学归纳法Mathematical induction · Weak induction由基例和从 n 到 n+1 的归纳步推出性质对全部自然数成立。证明所有有限执行都留在 $P$ 内。

从归纳条件到安全性 ​

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

$$s_0\to s_1\to \cdots \to s_n,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,\mathrm{post}(P)\subseteq P,P\cap B=\varnothing ,$$

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

若部分转移由控制器选择，安全博弈公理库安全博弈与反应式综合Safety game · Reactive synthesis · 安全游戏 · 获胜区域 · Controllable predecessor从安全闭包进入有限Büchi博弈，用嵌套吸引域计算反复到达目标的获胜区域，并构造双方位置策略。中的可控不变集只要求每个控制器顶点存在一个留在集合内的后继，而每个环境顶点的所有后继都留在集合内。固定这样的控制策略、保留全部环境选择后，集合才对所得转移系统满足通常的一步闭包；未被选择的控制器边不属于这个闭包义务。

直觉

真不变式为何可能不归纳 ​

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

$$0\to 0,1\to 2,2\to 2.$$

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

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

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

例子与边界

计数器协议的辅助事实 ​

设两个计数器 $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$ 不再保持；辅助不变式是证明手段，不必是系统允许行为的最宽描述。

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

推论与应用

与循环和模型检查的接口 ​

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

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

不变式也不等于任意时序性质。“请求最终得到响应”允许中间状态反复变化，不能表示成某个状态集合永远封闭；它是活性条件，需要时序逻辑公理库时序逻辑Temporal logic · Temporal modal logic在执行序列上解释下一步、最终、始终与直到，并区分线性时间和分支时间的统一规格层。和公平性假设。

Petri 网中有一类可直接从结构读出的布尔不变量：虹吸一旦为空便保持空，陷阱一旦被标记便保持被标记公理库Petri 网的虹吸与陷阱Petri net siphon · Petri net trap从库所集合的入出变迁关系定义虹吸与陷阱，证明空集保持和有标记保持，并用资源流动反例区分线性不变量。。它们跟踪资源集合的空与非空，不要求 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。