Counterexample-guided Abstraction Refinement Algorithm

The main idea of the CEGAR algorithm is:

• Initially, build an approximate model of the original model with a smaller state space
• Run the verification algorithm on the model. If verification fails, the model checker provides a counterexample
  • This counterexample might be due to execution paths introduced during the approximation process that don't exist in the original model In this case, we need to refine the approximate model and re-run the verification
• Use symbolic methods like BDD to efficiently implement the above process

Building the Approximate Model

We group ACTL*¹ formulas that share variables into equivalence classes. That is, if:

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

then $\phi_1$ and $\phi_2$ belong to the same equivalence class.

We denote the equivalence class of a formula as $[\phi]_f$, called a formula cluster.

Correspondingly, the set of all variables in formulas from the same formula cluster is called a variable cluster.

If all formulas in the same formula cluster evaluate to the same value in two different states (represented by variable values), then these two states can be mapped to the same abstract state.

Refinement

Identifying Spurious Counterexamples

SplitPATH

Suppose the model checker finds a counterexample path:

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

We denote the set of original states corresponding to abstract state $\hat s_i$ as $\gamma(\hat s)$.

To identify spurious counterexamples, we define a sequence of symbolic sets:

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

where:

• $R_0 = \gamma(\hat s_0) \cap I$, where I is the set of initial states in the original state sequence
• $R_i = \text{Post}(R_{i-1} \cap \gamma(\hat s_i))$

Essentially, we follow the abstract path in the actual model to see if it's feasible.

If all $R_i$ are non-empty, then the path is feasible and represents a real counterexample in the original model. Otherwise, it's a spurious counterexample, and we need to refine the abstract model.

SplitLOOP

A loop in the abstract model might correspond to multiple loops in the actual model.

We can identify this by unrolling the abstract loop several times and then using SplitPATH.

The upper bound for unrolling is the maximum number of concrete states corresponding to any state in the abstract loop.

Refinement

After identifying a spurious counterexample, we need to refine the abstract model to eliminate it.

PolyRefine

We divide the concrete state set $S = \gamma(\hat s_i)$ into three categories:

• $S_{i,0}$: States reachable from the initial state in the concrete model This is $R_i$.

• $S_{i,1}$: States not in $S_{i,0}$ but can reach $\hat s_{i+1}$ in the abstract model.

• Other states (which we don't care about)

To break the conditions that produce spurious counterexamples, we need to split the $\hat s_i$ where we found $R_i$ to be empty, making the corresponding $S_{i,0}$ and $S_{i,1}$ belong to different new states.

Each abstract state corresponds to original states in the form:

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

For example, if $X_j = \{mode, valid\}$, where $mode \in \{IDLE, RUN, ERR\}$ and $valid \in \{true, false\}$, a possible partition might be:

$$ 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\} $$

The goal of refinement is to split this $E_j$ into smaller parts.

The core of the algorithm is:

For each pair of equivalence classes $a$ and $b$ in $E_j$: If there exist two states $s_1$ and $s_2$ that differ only in the j-th variable, where one belongs to $a$ and the other to $b$, then we can determine that $a$ and $b$ are not equivalent, and thus split $E_j$ into smaller parts.

Pseudocode:

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);
        }
    }
}

where $proj(S, j, a)$ represents $\{s.remove(j) | s \in S, s.j = a\}$.