Blog • Counterexample-guided Abstraction Refinement 算法

CEGAR 算法主要的想法是：

最初，建立一个原模型的近似模型，其拥有较小的状态空间
在模型上运行验证算法，如果验证失败，模型检测器会给出反例
- 这个反例可能是由于在对原模型的近似过程中引入了原模型中不存在的执行路径在此情况下需要细化近似模型，并重新进行验证
使用 BDD 等符号方法高效地实现上述过程

构建近似模型

我们将所有使用的变量存在交集的 ACTL*¹ 公式归为一个等价类，即，若：

$$ \text{Var}(\phi_1) \cap \text{Var}(\phi_2) \neq \emptyset $$

则 $\phi_1$ 和 $\phi_2$ 属于同一个等价类。

我们将一个公式的等价类记为 $[\phi]_f$，称为一个公式簇。

相对应的，同一个公式簇中的公式的所有变量集合称为一个变量簇。

如果同一公式簇在两个不同状态（体现为变量的值）下每个公式的取值都相同，则称这两个状态暂且可以被映射到同一个抽象状态。

假设 model checker 找到了一个反例路径：

$$ \hat \pi = \hat s_0 \rightarrow \hat s_1 \rightarrow \cdots \rightarrow \hat s_n $$

我们将抽象状态 $\hat \s_i$ 所对应的原状态集合记为 $\gamma(\hat s)$。

为了识别伪反例，我们定义符号集合序列：

$$ R_0, R_1, \cdots, R_n $$

其中：

基本上就是沿着抽象路径，在实际的模型中走，看能不能走通。

若所有 $R_i$ 都非空，则说明能走通，这确实也是原路径中的一个反例，否则这就是一个伪反例，需要对抽象模型进行细化。

一个抽象模型中的循环可能对应于实际模型中的多次循环。

只需将抽象循环展开数次，然后使用 SplitPATH 进行识别即可。

展开次数的上限就是抽象循环中，每个状态对应的具体状态个数的最大值。

识别出伪反例后，我们需要对抽象模型进行细化，消除找到的伪反例。

我们将具体状态集合 $S = \gamma(\hat s_i)$ 分为三类：

为了破坏伪反例的产生条件，我们需要把之前发现 $R_i$ 为空时对应的 $\hat s_i$ 分开，让此时对应的 $S_{i,0}$ 和 $S_{i,1}$ 分属不同的新状态。

每个抽象状态对应的原状态形式如下：

$$ E = E_1 \times E_2 \times \cdots \times E_n $$

比如 $X_j = \{mode, valid\}$，$mode \in \{IDLE, RUN, ERR\}$，$valid \in \{true, false\}$，一个可能的划分方式是：

$$ C_1 = \{(IDLE, true), (IDLE, false)\} $$

$$ C_2 = \{(RUN, true), (RUN, false)\} $$

$$ C_3 = \{(ERR, true), (ERR, false)\} $$

$$ E_j = \{C_1, C_2, C_3\} $$

细化的目标就是把这个 $E_j$ 拆分成更小的部分。

算法的核心是：

对于 $E_j$ 中的每对等价类 $a$ 和 $b$：如果存在两个状态 $s_1$ 和 $s_2$，两者的差异只在第 j 个变量上，即其中一个为 $a$ 的元素，另一个为 $b$ 的元素，则可以根据这个，判定 $a$ 和 $b$ 不等价，进而将 $E_j$ 拆分成更小的部分。

伪代码如下：

for j in 1 to m {
    for (a, b) in E_j {
        if proj(S_i_0, j, a) != proj(S_i_0, j, b) {
            split(a, b);
        }
    }
}

其中 $proj(S, j, a)$ 表示 $\{s.remove(j) | s \in S, s.j = a\}$。

就是只准 A 不准 E 的 CTL*.