Changeset 89 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Apr 6, 2012, 4:44:06 PM (13 years ago)

Author:

cecile

Message:

corrections typos and co

File:

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

papers/FDL2012/abstraction_refinement.tex

@@ -14 +14 @@
 $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_{i}$.
 \item The spurious counterexample in $\widehat{M}_i$ is  removed from
-$\widehat{M_{i+1}}$.
+$\widehat{M}_{i+1}$.
 \end{enumerate}
 \label{def:goodrefinement}
 \end{definition}
-Moreover, the refinement steps should be easy to compute and ensure a fast
+Furthermore, the refinement steps should be easy to compute and ensure a fast
 convergence by minimizing the number of iterations of the CEGAR loop.
 
@@ -32 +32 @@
 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 counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
+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 @@
 The spurious counterexample $\sigma$ is defined such that :
 \begin{definition}
-Let $\sigma$ be a \emph{spurious counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
+Let $\sigma$ be a \emph{spurious counterexample} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
 \widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
 \rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
@@ -56 +56 @@
 \end{definition}
 The construction of the AKS representing all executions except the one
-described by the spurious counter-example is done in two steps.
+described by the spurious counterexample is done in two steps.
 
 \subsubsection{Step 1~:~Build the structure of the AKS.}
@@ -62 +62 @@
 
 \begin{definition}
-Let $\sigma$ be a spurious counter-example of  length $|\sigma| = n$, the \emph{ AKS of the
-counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
+Let $\sigma$ be a spurious counterexample of  length $|\sigma| = n$, the \emph{ AKS of the
+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 :
@@ -101 +101 @@
 \emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ the configuration associated with $s_0$ assigns false to each variable. The negation of this configuration represents a set of seven concrete configurations which are covered by three (abstract) configurations: $\{\{\mathbf{t},\top,\top\},\{\mathbf{f},\mathbf{t},\top\},\{\mathbf{f},\mathbf{f},\mathbf{t}\}\}$.
 
-To build the final AKS representing all sequences but spurious counter-example
+To build the final AKS representing all sequences but spurious counterexample
 $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by
 $k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$
 and assigns to each of them a label of $k$ variables $\{v_0, \ldots,
-v_{k-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1],
+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
 state $\bar{s_i^j}$ is connected to the same predecessor and successor states
 as state $\bar{s_i}$.
 
-This final AKS presents a number of states in $\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each refinement step, the spurious counter-example {\em only} induces a low convergence. Moreover, in some cases, this strategy may not converge: suppose that all sequences of the form $a.b^*.c$ are spurious counter-examples (here $a$, $b$ and $c$ represent concrete state configurations). At a given refinement step $i$, a particular counter example $\sigma_i = s_0 \rightarrow s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) = b, L(s_n) = c$. Removing this counter-example does not prevent from a new spurious counter-example at step $i+1$ :  $\sigma_{i+1} = s_0 \rightarrow s_1 \rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) = b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious counter-example {\em one by one} diverges in this case. However, we cannot eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step since we do not a priors know if at least one of these sequence is executable in the concrete model.
+This final AKS presents a number of states in
+$\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each
+refinement step, the spurious counterexample {\em only} induces a low
+convergence. Moreover, in some cases, this strategy may not converge: suppose
+that all sequences of the form $a.b^*.c$ are spurious counterexamples (here
+$a$, $b$ and $c$ represent concrete state configurations). Assume, at a given
+refinement step $i$, a particular counterexample $\sigma_i = s_0 \rightarrow
+s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) =
+b, L(s_n) = c$. Removing this counterexample does not prevent from a new
+spurious counterexample at step $i+1$ :  $\sigma_{i+1} = s_0 \rightarrow s_1
+\rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) =
+b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious
+counterexample {\em one by one} diverges in this case. However, we cannot
+eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step
+since we do not {\it a priori} know if at least one of these sequences is executable in the concrete model.
 
 From these considerations, we are interested in removing {\em sets of
-behaviors encompassing the spurious counter-example} but still guaranteeing an
+behaviors encompassing the spurious counterexample} but still guaranteeing an
 over-approximation of the set of tree-organized behaviors of the concrete
 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
-\ref{prop:concrete_compose}) but does not guarantee the elimination of the counter example. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counter example.
+\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.