Changeset 101 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Jul 19, 2012, 11:44:48 AM (12 years ago)

Author:

syed

Message:

final

File:

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

papers/FDL2012/abstraction_refinement.tex

@@ -26 +26 @@
 $\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,
+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
@@ -32 +32 @@
 
 We propose to compose the abstraction with another AKS to build a good refinement
-according to definition \ref{def:goodrefinement}.
-We have  several options. The most straightforward consists in building
-an AKS representing all possible executions except the  spurious counterexample ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counterexample are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
+according to Definition \ref{def:goodrefinement}.
+We have several options. The most straightforward method consists in building
+an AKS representing all possible executions except the  spurious counterexample; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones: first local CTL properties eliminating the spurious counterexample are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
 
 
@@ -43 +43 @@
 counterexample given by the model-checker, the variable configuration in each
 state is Boolean. We name $\widehat{L_i}$ this new labeling.
-The spurious counterexample $\sigma$ is defined such that :
+The spurious counterexample $\sigma$ is defined such that:
 \begin{definition}
 Let $\sigma$ be a \emph{spurious counterexample} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
@@ -70 +70 @@
 counterexample negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
 \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
-\widehat{F}_{\overline{\sigma}} \rangle$ is such that :
+\widehat{F}_{\overline{\sigma}} \rangle$ is such that:
 \vspace*{-2mm}
 \begin{itemize}
@@ -98 +98 @@
 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
+the labeling function defined in Definition \ref{def-aks}. State labeling is treated
 in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}.
 %The size of this structure is linear with the size of the counter-example.
@@ -139 +139 @@
 model. The strengthening of the abstraction $\widehat{M}_i$ with the
 addition of AKS of already verified local CTL properties eliminates sets of
-behaviors and guarantees the over-approximation (property
+behaviors and guarantees the over-approximation (Property
 \ref{prop:concrete_compose}) but does not guarantee the elimination of the counterexample. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counterexample.