Abstraction in Model Checking

Finite Transition System $M = (S, I, R, L)$, respectively the set of states, the set of initial states, the set of transition relations, labels. Simply put, a computational model, similar to Finite State Machine.

Which Computation? Well, model checking. $M \models \varphi$

Why abstraction? Too many states to compute and the abstraction reduces the number of states.

Why abstraction works? The existential-quantified properties (ECTL) are preserved after the abstraction ($M$ simulates $M'$, i.e., $M$ has whatever $M'$ has), that is, $M' \models \varphi \rightarrow M \models \varphi$. (But not vice versa!)

Now let's go to terms.

Abstraction function $h: S \rightarrow S'$

Simulation $M$ simulates $M'$ when each transition of $M'$ has a corresponding one in $M$. The simulation is the set of pairs of states $p \subseteq \{ (s,s') | s \in S, s' \in S' \}$ that records such behavior. It is the set denotation of the abstract function $h$.

Bisimulation The simulation applies on both sides. According to property preservation, $M \models \varphi \rightarrow M' \models \varphi$. As a consequence, $M \not \models \varphi \rightarrow M' \not \models \varphi$, otherwise we reach a contradiction.

$M$ simulates $M'$, plainly put, $M$ is an abstraction (simulation) from $M'$.

What about universal-quantified properties? (in LTL or ACTL) They are preserved when $M'$ simulates $M$. That is,

$$M' \models \varphi \rightarrow M \models \varphi$$ Yes, same conclusion but different condition. Still, the reverse doesn't hold.

Exercise

Credit: ~rseba, disi.unitn.it

If we draw a relation $p = \{(S_{ij}, T_i) | \text{for all possible } i,j \}$, we see (with effort) that $p$ is a simulation from $M$ to $M'$ (i.e. $M'$ simulates $M$). Verify it by the rigorous definition, if $(S_{11}, T_1) \in p$, $(S_{11}, S_{12}) \in R_M$, $\exists (T_1, T_1) \in R_{M'}$ s.t. $(S_{12}, T_1) \in p$. So are the rest transition relations of $M$. Hence, the universal-quantified property preservation applies. e.g. if $\varphi$ is pure boolean,

$$M' \models \mathbf{AG} \varphi \rightarrow M \models \mathbf{AG} \varphi$$

To note that the reverse doesn't hold. For instance, $(S_{13}, T_1) \in p$, $(T_1, T_1) \in R_{M'}$, $\forall j. \nexists (S_{13},S_{1j}) \in R_{M}$ s.t. $(S_{1j},T_1) \in p$.