Changeset 93 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Apr 10, 2012, 4:30:02 PM (13 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

• papers/FDL2012/abstraction_refinement.tex (modified) (3 diffs)

papers/FDL2012/abstraction_refinement.tex

@@ -24 +24 @@
 
 Refinements based on the concretization of selected abstract variables in
-$\widehat{M}_i$ ensure item 2. Concretization can be performed either in
-modifying the AKS of $\widehat{M}_i$, by changing some abstract value to
-concrete ones, but this approach is rude : in order to ensure item 1,
-concretization needs to be consistent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value.
+$\widehat{M}_i$ ensure item 2. Concretization can be performed by
+modifying the AKS of $\widehat{M}_i$ by changing some abstract value to
+concrete ones. However, this approach is rude : in order to ensure item 1,
+the concretization needs to be consistent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value.
 %Another way to concretize some variables at selected instants is to compose
 %(by a synchronous product) the AKS  of $\widehat{M}_i$ with a new AKS, provided this latest represents over-approximations of the set of behaviors of $M$. By construction, this product satisfies items 1 and 2. We now have to compute an AKS eliminating the spurious counterexample, being easily computable and ensuring a quick convergence of the CEGAR loop.
@@ -96 +96 @@
 \end{itemize}
 \end{definition}
-The labeling function fo $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
+The labeling function of $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
 configurations {\it but} the one of $s_i$. This last set may not be representable by
 the labeling function defined in def \ref{def-aks}. State labeling is treated
@@ -114 +114 @@
 and assigns to each of them a label of $k$ variables $\{v_0, \ldots,
 v_{k-1}\}$ defined such that : $\widehat{L}(\bar{s_i^j}) = \{\forall l \in [0..k-1],
-v_l = \neg  {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each
+v_l = \neg  {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. Each
 state $\bar{s_i^j}$ is connected to the same predecessor and successor states
 as state $\bar{s_i}$.