## Saturday, June 1, 2013

### 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.