Changeset 69 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Mar 15, 2012, 2:27:06 PM (13 years ago)

Author:

cecile

Message:

partie raffinement avec liste des propriétés mis à jour

File:

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

papers/FDL2012/abstraction_refinement.tex

@@ -12 +12 @@
 \item The new refinement is more concrete than the previous one:
 $\widehat{M}_{i} \sqsubseteq \widehat{M}_{i+1}$.
-\item The spurious counter-example in $\widehat{M}_i$ is  removed from
+\item The spurious counterexample in $\widehat{M}_i$ is  removed from
 $\widehat{M_{i+1}}$.
 \end{enumerate}
@@ -22 +22 @@
 
 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 coherent 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 counter-example, being easily computable and ensuring a quick convergence of the CEGAR loop.
+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.
 
-Several proposals can be made. The most straightforward consists in building the AKS representing all possible executions except the  spurious counter-example ; 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$.
+Several proposals can be made. The most straightforward consists in building the 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$.
 
 
@@ -31 +31 @@
 The counterexample at a refinement step $i$, $\sigma$ is a path in the
 abstract model $\widehat{M}_i$ which dissatisfy $\Phi$.  In the counterexample given by the model-checker, the variables value in each states are boolean.
-The spurious counter-example $\sigma$ is defined such that :
+The spurious counterexample $\sigma$ is defined such that :
 \begin{definition}
-\textbf{\emph{The counterexample $\sigma$ :}} \\
-\\
-Let $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
-\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ and let the length of the
-counterexample, $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
-s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
+Let $\sigma$ be a \emph{counter-example} 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]$.
 \begin{itemize}
 \item All its variables are concrete: $\forall s_i$ and $\forall p\in
 \widehat{AP}_i$, $p$ is either true or false
 (not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$
-\item  $\sigma$ is a counter-example in  $\widehat{M}_i$: $s_0\not\models \Phi$.
+\item  $\sigma$ is a counterexample in  $\widehat{M}_i$: $s_0\not\models \Phi$.
 \item  $\sigma$ is not a path of the concrete system $M$: $\exists k \in [1..n-1]$ such
 that $\forall j < k, (s_j,s_{j+1}) \in R$ and $(s_{k}, s_{k+1}) \not\in R$.