Property-Directed Reachability / IC3

形式陈述

Frame 序列不变量

作为一种模型检查算法，PDR 对有限布尔转移系统 $I(x),T(x,x')$ 和安全性质 $P(x)$ ，先检查 $I\land\neg P$ 与 $I\land T\land\neg P'$ ，分别排除零步和一步反例。两者均不可满足后，可取 $F_0=I,F_1=P$ 开始维护公式序列

F_0,F_1,\ldots,F_k

满足

F_0=I,\qquad F_i\Rightarrow P,\qquad F_i\Rightarrow F_{i+1},\qquad F_i(x)\land T(x,x')\Rightarrow F_{i+1}(x').

$F_i$ 过近似至多 $i$ 步可达状态。序列随下标变弱，允许状态增加；每个 frame 内不断学习子句，公式则变强。

若某相邻层语义相等 $F_i=F_{i+1}$ ，相对归纳条件给出

F_i\land T\Rightarrow F_i',

加上 $I\Rightarrow F_i$ 与 $F_i\Rightarrow P$ ，得到归纳不变式，证明安全。

直觉

从坏状态建立 obligation

算法先询问可满足性

F_k(x)\land T(x,x')\land\neg P(x').

若 SAT，得到一个可能一步进入坏状态的 predecessor cube $c$ ，形成层 $k$ 的 proof obligation $(c,k)$ 。算法递归检查 $c$ 是否从 $F_{k-1}$ 有前驱。

对每个 obligation $(c,i)$ ，即使 $i>0$ ，也先检查 $I\land c$ 。若可满足，取这个初态并接上义务中保存的后继链，就已经得到真实反例路径；它可以短于当前层号所允许的长度，不必继续追到第零层。若某层前驱查询 UNSAT，则当前 cube 在该层不可到达，可以学习阻塞子句。

这不是普通反向 BFS：frame 是可达集的逻辑外包络，本页为便于直接重放，把 obligation 保留为完整状态赋值的 cube，SAT 求解器则隐式搜索大量状态；学习的阻塞子句可以概括多个状态。使用部分 cube 作为路径义务的优化，还须另证前后模型可以一致拼接。

PDR IC3 frame 阶梯、反向 proof obligations、UNSAT 学习与固定点 — PDR / IC3 的 frames 与 obligations

例子与边界

子句泛化与阻塞

设当前待阻塞义务为 $(c,i)$ ，其中 $c(x)$ 是一个完整状态 cube，并附有通向坏状态的已保存后继链。先按上节检查 $I\land c$ ；若 SAT 就报告该初态接续后继链的反例。只有确认不与初态相交、且 $i>0$ 时，才查询

F_{i-1}(x)\land T(x,x')\land c(x')

若查询 SAT，模型在当前状态变量 $x$ 上给出前驱 cube $p(x)$ ；算法先递归阻塞 $(p,i-1)$ ，成功后再处理原义务 $(c,i)$ 。若查询 UNSAT，则 $c$ 没有来自 $F_{i-1}$ 的前驱。此时可把 $c$ 泛化为文字更少的 cube $g\subseteq c$ ；这里的包含关系针对文字集合，因此满足 $g$ 的状态反而更多。每次泛化都必须重新验证初态保持与一步排除两项条件

I(x)\Rightarrow\neg g(x),\qquad F_{i-1}(x)\land T(x,x')\Rightarrow\neg g(x').

第一项等价于 $I\land g$ 不可满足，不能由第二项代替；初态可能没有任何前驱。两项验证通过后，把子句 $\neg g$ 加入 $F_1,\ldots,F_i$ ；这既阻塞当前后继 cube，也保持 $F_j\Rightarrow F_{j+1}$ 的层间关系。全文中 $c$ 始终表示当前待阻塞的后继， $p$ 只表示 SAT 查询返回的前驱。

SAT 求解器的 unsat core 可帮助删除 cube 中不必要的文字，得到更一般的阻塞子句，一次排除更多状态。泛化必须同时检查初态和相对一步保持；凭启发式删文字可能连真实可达状态一起排除。

例如初态为 $(x,y)=(0,0)$ ，转移为 $00\to01,01\to01,10\to11,11\to11$ ，性质只禁止 $11$ 。不可达的 $c=x\land\neg y$ 可以一步到坏状态，而从 $F_0=I$ 没有前驱进入它。若把它泛化成 $g=\neg y$ ， $I\land T\land g'$ 仍不可满足，因为初态的唯一后继是 $01$ ；但 $I\land g$ 可满足。贸然学到 $\neg g=y$ 就会排除真正的初态 $00$ ，破坏 $F_0\Rightarrow F_1$ 。因此“没有前驱”与“不是初态”必须分别证明。

例如 cube 指定十个变量，core 只依赖锁位和两个程序计数器，学到的子句便覆盖所有其他变量赋值。这是 PDR 不逐状态枚举的关键来源。

推送与收敛

若子句 $c\in F_i$ 满足

F_i(x)\land T(x,x')\Rightarrow c(x'),

它可推送到 $F_{i+1}$ 。算法周期性尝试推送全部子句；当一层所有约束都能推到下一层且两层相同，获得固定点。

有限布尔状态系统上，理想化 IC3 过程完备：最终找到反例或归纳不变式。实际性能高度依赖 obligation 顺序、generalization、clause subsumption 与 SAT 增量接口。

“frame 数不再增加”不等于收敛；必须检查某对相邻 frame 公式语义等价或子句集合在规范管理下相同。

推论与应用

与 BMC 的差别

BMC 前向展开固定长度路径，UNSAT 通常只有边界意义。PDR 的查询围绕归纳阻塞，目标是主动合成一个全局不变式；它也会生成反例，但不是“更快的 BMC”同义词。

PDR 对 safety/reachability 最自然。一般 LTL 需先做监控器或自动机产品转成安全/接受问题，公平 liveness 不能直接套原始 frame 不变量。

无限状态 SMT-PDR 可能不终止，量词和理论泛化也可能不完备。有限布尔模型上的保证不能无条件推广到软件整数与堆。

一个阻塞子句例子

设安全性质禁止 $pc=C\land lock=0$ 。SAT 查询发现抽象 cube 还包含无关数据位 $d_1,d_2$ 。检查前驱后，unsat core 表明只需 $pc=C\land lock=0$ 就不可从上一 frame 到达，于是学习

pc\ne C\lor lock=1.

这条子句同时阻塞所有数据位组合，比逐一排除完整 cube 更强。若 core 还依赖上一层特有子句，它只相对于该 frame 归纳，不能直接提升到所有层。

子句管理还要做 subsumption：强子句可删除被其蕴含的弱子句，但反向删除会扩大 frame 并可能重新引入坏状态。语法文字数少不自动代表逻辑更强。

参考资料

Aaron R. Bradley, “SAT-Based Model Checking without Unrolling,” VMCAI, 2011, pp. 70–87，作者版 §§3–4、PDF pp.3–5：initiation 与 consecution、初始零／一步检查及 frame 不变量。
Niklas Eén, Alan Mishchenko, and Robert Brayton, “Efficient Implementation of Property Directed Reachability,” FMCAD, 2011, pp. 125–134。
Aaron R. Bradley and Zohar Manna, The Calculus of Computation, Springer, 2007, Chs. 12–14。

形式陈述 ​

Frame 序列不变量 ​

从坏状态建立 obligation ​

子句泛化与阻塞 ​

推送与收敛 ​

与 BMC 的差别 ​

一个阻塞子句例子 ​

反向链接