Symoblic CTL Model Checking

Ordered Binary Decision Diagram

Boolean formulas are represented in diagrams. OBDD has the following property, $$\phi \leftrightarrow \psi \Rightarrow OBDD(\phi) = OBDD(\psi)$$

Symbolic Denotation $\xi$

$\xi : S \rightarrow $boolean formulas (OBDDs). By definition, $$\xi([\phi]) := \xi(\{ s | M,s \models \phi \})$$

A list of some symbolic encodings,

• $\xi([\mathbf{EX}\phi]) = \exists V' . (\xi ([\phi])[V'] \wedge \xi (R)[V,V'])$
• $\xi([\mathbf{EG}\phi]) = \nu Z . (\xi([\phi]) \wedge \xi([\mathbf{EX}Z]))$
• $\xi([\mathbf{E}(\phi\mathbf{U}\psi)]) = \mu Z . (\xi([\psi]) \vee (\xi([\phi]) \wedge \xi([\mathbf{EX}Z])))$

The above exactly parallels the classical fixed-points techniques. See a previous post (link).

Fixed-point Algorithms

The following shows the symbolic counterpart for the classical fixed points algorithms (denotational, based on states). Recall their inductive version,

• $[\mathbf{EG}\phi]$: $X_{j+1} = X_j \cap \mathsf{PreImage}(X_j)$
• $[\mathbf{E}(\phi\mathbf{U}\psi)]$: $X_{j+1} = X_j \cup ([\phi] \cap \mathsf{PreImage}(X_j))$

PreImage

OBDD PreImage(OBDD X){
  return ∃V'. (X[V'] ∧ ξ(R)[V,V']);
}

Check_EG

OBDD Check_EG(OBDD X) {
    Y′ := X;
    repeat
        Y := Y′;
        Y′ := Y ∧ PreImage(Y);
    until (Y′ ↔ Y);
    return Y;
}

Check_EU

OBDD Check_EU(OBDD X1 ,X2) {
    Y′ := X2;
    repeat
        Y := Y′;
        Y′ := Y ∨ (X1 ∧ PreImage(Y));
    until (Y′ ↔ Y);
    return Y;
}

Check_FairEG

Here we need to refer Emerson Lei algorithm which specifies the fair CTL version. $$ [\mathbf{E}_f \mathbf{G} \phi ] = \nu Z .([\phi] \cap \bigcap_{F_i \in FT} [\mathbf{EX}[\mathbf{E}(Z \mathbf{U}(Z \wedge F_i ))])$$

The can be interpreted as $Z$ keeps being true until all fair conditions are met when $Z$ is still true at each step of iteration.

OBDD Check_FairEG(OBDD X) {
    Z’ := X;
    repeat
        Z := Z’;
        for each Fi in FT
            Y := Check_EU(Z, Fi ∧ Z);
            Z’:= Z’ ∧ PreImage(Y);
        end for;
    until (Z’ ↔ Z);
    return Z;
}

Check Invariants

Invariants are specified as $\mathbf{AG}\phi$. Its negation is $\neg \mathbf{EF} \neg \phi$, which is a reachability issue: are there such states which can be reached from the initial states? We show the forward checking technique.

OBDD Compute_reachable() {
    Y′ := I;
    Y := ⊥;
    while ¬(Y′ ↔ Y) {
        Y := Y′;
        Y′ := Y ∨ Image(Y);
    }
    return Y;
}

Note backward checking iteratively calculates the preimage of $\phi$ until a fixed-point is reached or the preimage intersects with $I$. An advanced version with the so-called frontier (F) is presented below.

OBDD Compute_reachable() {
    Y := I;
    F := I;
    while ¬(F ↔ ⊥) {
        F := Image(F) ∧ ¬Y;
        Y := F ∨ Y;
    }
    return Y;
}

If we explain it in the set flavor, it could be at each time we only calculate the image of new states (frontier). The set of reachable states is saturated when the image of the frontier can't bring in more new states.

Forward_Check_EF

Based on the discussion above, we now can check invariants (often feature as bad behaviors).

bool Forward_Check_EF(OBDD BAD) {
    Y := F := I;
    while ¬(F ↔ ⊥) and (F ∧ BAD) ↔ ⊥ {
        F := Image(F ) ∧ ¬Y ;
        Y := Y ∨ F ;
    }
    if F = ⊥
        return false
    else
        return true
}

The above utilizes the frontier technique. It looks for all reachable states and verifies whether there are some bad states within them.

References & Readings

1. R. Sebastiani, Symbolic CTL Model Checking, slides on Formal Methods, 2012
2. McMillan, Symbolic Model Checking, a Carnegie-Mellon PhD dissertation, 1993
3. Wikipedia, Fair Computational Tree Logic, http://en.wikipedia.org/wiki/Fair_computational_tree_logic

Appendix

The most of this post is heavily extracted from the RS's teaching slides, hence I don't claim the copyright. The character of this post is intended to be a note, with marginal and personal remarks. For those who need to respect the source, please read the following copy of the original copyright notice.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.