Changeset 68 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Mar 15, 2012, 1:43:45 PM (13 years ago)

Author:

ema

Message:

 

File:

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

papers/FDL2012/abstraction_refinement.tex

@@ -7 +7 @@
 %\medskip
 
-\begin{definition} An efficient \emph{refinement} verified the following properties:
+\begin{definition} An efficient \emph{refinement} verifies the following properties:
 \begin{enumerate}
 \item The new refinement is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$.
@@ -29 +29 @@
 \subsection{Refinement by negation of the counterexample}
 
-\TODO{Mettre la def avant ?}
-\TODO{Rafinement par négation du contre-exemple}
 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.
@@ -51 +49 @@
 \end{definition}
 
-2. Negation of states in an AKS
+The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps.
+\subsubsection{step 1 : Build the structure of the AKS.}
+Let us denote $AKS(\overline{\sigma})$ this AKS. $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$.
+\begin{itemize}
+\item The set of atomic propositions coincides with the one of $\sigma$ : $AP_{\overline{\sigma}} = {AP}_i$
+\item Build a state $s_T$, and for each state $s_i$ in $\sigma$, build two states $s'_i$ and $s"_i$.  $s_T \in S_{\overline{\sigma}}$ and forall $i$ in $[0..n-1]$ : $s'_i \in S_{\overline{\sigma}}$ and $s"_i \in S_{\overline{\sigma}}.$
+\item State labeling : $s'_i$ represents the (concrete) configuration of state $s_i$ and state $s"_i$  represents all configurations 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 in the second step.
+\item States $s'_0$ and $s"_0$ are initial states.
+\item Transitions : Forall $i$ in $[1..n-1]$, connect $s'_i$ and $s"_i$ to their predecessor state $s'_{i-1}$: $(s'_{i-1},s'_i) \in R_{\overline{\sigma}}$ and $(s'_{i-1},s"_i) \in R_{\overline{\sigma}}$ and connect all $s"$ states as predecessor of the $s_T$ state : $(s"_i,s_T) \in R_{\overline{\sigma}}$.
+\item \TODO{FAIRNESS}
+\end{itemize}
+The size of this structure is linear with the size of the counter-example, however it is not a strict AKS since the representation of the set of configurations in states $s"$ may lead to a union of labels.
 
-a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.
+\subsubsection{Step 2 : Expand state configurations representing the negation of a concrete configuration.}
+We return back to the labeling of states of $AKS(\overline{\sigma})$. As states $s'$ are associated with the same (concrete) configuration as their corresponding state in $\sigma$, their labeling is straightforward : $\forall i \in [0..n-1], {L}_{\overline{\sigma}}(s'_i) = \widehat{L}_{i}(s_i)$.
+The set of configurations associated with a state $s"_i$ represents the negation of the one represented by ${L}_{\overline{\sigma}}(s'_i)$. This negation is not representable by the label of a single state but rather by a union of $\mid AP \mid$ labels.
 
-b) The negation of an configuration may be represented by a set of abstract configurations
+\emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1, \ldots$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ meaning 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}\}\}$.
 
-c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS
+To build the final AKS representing all sequences but spurious counter-example $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $s"_i$ by $n = \mid AP_{\overline\sigma} \mid$ states $s"_i^k$ with $k \in [0..n-1]$ and assigns to each of them a label of $n$ variables $\{v_0, \ldots, v_{n-1}\}$ defined such that : ${L}(s"_i^k) = \{\forall l \in [0..k], v_l = \neg  {L}_{i}(s'_i)[v_l], \forall l \in [k+1..n-1], v_l = \top\}$.
+\TODO{connexion des $s"_i^k$}
 
+This final AKS presents a number of states which is linear with the length of the counter-example and the number of atomic propositions.
+
+\TODO{Revoir notation def 3 pour f,t,top et introduire notation ${L}_{i}(s'_i)[v_l]$}
+
+Removing the spurious counter-example only has little chance to converge.
 
 %\bigskip