**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!)

**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

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

## No comments:

## Post a Comment