反例引导的抽象精化 CEGAR

闭环的四个阶段

CEGAR 维护具体系统 $C$ 与当前抽象 $A_i$ 。每轮执行：构造或更新抽象；对 $A_i$ 做模型检查；若得到抽象反例则检查具体可行性；若不可行，利用失败原因生成更精细的 $A_{i+1}$ 。

可靠抽象要求

Beh(C)\subseteq\gamma(Beh(A_i)).

因此抽象系统证明安全即可推出具体安全。抽象系统发现反例却只说明“可能违反”，必须经过 concretization feasibility check。

精化应满足行为收缩

\gamma(Beh(A_{i+1})) \subseteq \gamma(Beh(A_i)),

并排除当前伪反例。只增加新术语而不删除该路径，不构成有效精化进展。

考虑程序

text

x := 0
y := 0
while nondet:
    x := x + 1
    y := y + 1
assert x == y

只跟踪 x>=0、y>=0 的非关系抽象会允许某抽象路径到达 $x\ne y$ ，因为它把两个变量的可能值独立组合。模型检查输出一条反例轨迹，但沿具体赋值约束合取可得每轮都保持 $x=y$ ，路径不可行。

加入谓词 $x=y$ 后，抽象状态划分能区分相等与不等，transfer 证明循环体保持该谓词，原伪反例被删除。

把循环常数换成另一个数字不会修复根因；真正新增的是变量关系这一表达能力。

给定抽象动作序列 $e_0,\ldots,e_{k-1}$ ，构造路径公式

I(s_0)\land \bigwedge_{i=0}^{k-1}T_{e_i}(s_i,s_{i+1}) \land Bad(s_k).

SAT 给出具体反例，可直接报告；UNSAT 证明至少有一处抽象连接无法由同一具体状态序列实现。

失败可能来自 guard 互斥、变量相关性或抽象合流。检查器要保留动作与状态帧对应，不能只逐边确认“某些具体状态能走这条边”；不同边的见证状态若无法连接，整条路径仍是伪的。

把不可满足路径公式分成前缀 $A$ 与后缀 $B$ ，Craig interpolant $J$ 满足

A\Rightarrow J,\qquad J\land B\text{ 不可满足},

且只使用两边共享符号。 $J$ 概括前缀到达状态必须具有、而坏后缀无法接受的事实，可抽取为新谓词。

另一策略从 unsat core、weakest precondition 或失败 transition pair 中选谓词。生成谓词要在表达力、数量和求解成本之间权衡；把路径公式所有子式都加入会迅速造成 $2^m$ 个谓词抽象状态。

精化后必须重新证明抽象 transfer 的 soundness。新的状态划分更细不意味着旧的转移边自动准确，需按谓词可满足性重新连接。

有限状态系统若精化策略最终能区分每个必要具体状态，最坏可退化到精确模型并终止。对无限状态软件，CEGAR 不保证找到有限谓词集，也可能不断产生新反例而不收敛。

求解器 unknown 既不是真实反例也不是不可行证明。把超时当 UNSAT 会错误删除可能真实路径，把它当 SAT 又可能报告无法重放的警报；工具应保留 unknown 状态。

精化也可能过拟合一条路径：加入只排除某个具体常数的谓词，下一轮出现同构伪反例。好的概括来自失败原因，而非反例表面数字。

抽象解释提供可靠 over-approximation 的数学基础；CEGAR 是选择和迭代改进抽象的一种控制循环。它不是独立于 soundness 的“反复跑模型检查”技巧。

区间阈值、谓词集合、状态分裂和 transition refinement 都可成为 refinement 维度。每种选择要说明哪部分 concretization 变小以及为何仍覆盖具体行为。

终止时还应区分两种证书：真实反例附具体可行路径；安全结果附最终抽象的可靠性和抽象模型无反例证明。只保存“循环若干轮后工具返回 safe”不足以复核结论。

参考资料

Edmund M. Clarke et al., “Counterexample-Guided Abstraction Refinement,” CAV, Springer, 2000, pp. 154–169。
Thomas A. Henzinger et al., “Lazy Abstraction,” POPL, 2002, pp. 58–70。
Kenneth L. McMillan, “Interpolation and SAT-Based Model Checking,” CAV, Springer, 2003, pp. 1–13。