Index: papers/FDL2012/framework.tex
===================================================================
--- papers/FDL2012/framework.tex	(revision 68)
+++ papers/FDL2012/framework.tex	(revision 76)
@@ -1,7 +1,7 @@
 The model-checking technique we propose is based on the Counterexample-guided
 Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall
-descritpion of our methodology is shown in figure \ref{cegar}.
+description of our methodology is shown in figure \ref{cegar}.
 We take into account the structure of the system as a set of synchronous components,
-each of which has been previously verified and a set of CTL properties is attached to each component. This set refers to the specification of the component. We would like to verify whether a concrete model, $M$ presumedly huge sized composed of several components, satisfies a global property $\Phi$. Due to state space combinatorial explosion phenomenon that occurs when verifying huge and complex systems, an abstraction or approximation of the concrete model has to be done in order to be able to verify the system with model-checking techniques. Instead of building the product of the concrete components, we replace each concrete component by an abstraction of its behavior derived from a subset of the CTL properties it satisfies. Each abstract component represents an over-approximation of the set of behaviors of its related concrete component \cite{braunstein07ctl_abstraction}.
+each of which has been previously verified and a set of CTL properties is attached to each component. This set refers to the specification of the component. We would like to verify whether a concrete model, $M$ presumedly huge sized and composed of several components, satisfies a global ACTL property $\Phi$. Due to state space combinatorial explosion phenomenon that occurs when verifying huge and complex systems, an abstraction or approximation of the concrete model has to be done in order to be able to verify the system with model-checking techniques. Instead of building the product of the concrete components, we replace each concrete component by an abstraction of its behavior derived from a subset of the CTL properties it satisfies. Each abstract component represents an over-approximation of the set of behaviors of its related concrete component \cite{braunstein07ctl_abstraction}.
 
 %\subsection{Overall Description of our methodology}
@@ -9,13 +9,7 @@
 concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
 generated and tested in the model-checker. As the abstract model is an
-over-approximation of the concrete model and we have restrained our
-verification to ACTL properties only. As shown in \cite{clarke94model} if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well.
-However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample,
-$\sigma$ given by the model-checker has been analyzed.
+over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment, if $\Phi$ holds on the the abstract model then it holds in the concrete model as well \cite{clarke94model}. However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample, $\sigma$, given by the model-checker has been analyzed.
+In this last case, the test of spurious counter-example is translated into a SAT problem \TODO{citer ref SAT spurious}. When a counterexample is proven to be spurious, the refinement phase occurs, injecting more preciseness into the (abstract) model to be analyzed.
 
-In the case where model-checking failed, the counterexample given by the
-model-checker  has to be analysed. We use a SAT solver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase.
-\TODO{ref du papier sur le spurious + petite explication sur SAT et
-dÃ©roulement}
 %\bigskip
 %\begin{definition}
@@ -45,8 +39,8 @@
 
 \subsection{Concrete system definition}
-As mention earlier, in our verification methodology, we have a concrete model which consists of several components and each component comes with its specification or more precisely, properties that hold in the component. Given a global property $\Phi$, the property to be verified by the composition of the concrete components model, an abstract model is generated by selecting some of the properties of the components which are relevant to $\varphi$.
+As mention earlier, in our verification methodology, we have a concrete model which consists of several components and each component comes with its specification or more precisely, properties that hold in the component. Given a global property $\Phi$, the property to be verified by the composition of the concrete components model, an abstract model is generated by selecting some of the properties of the components which are relevant to $\Phi$.
 
 
-The concrete system is a synchronous compositon of components, each of which
+The concrete system is a synchronous composition of components, each of which
 described as a Moore machine.
 \begin{definition}
@@ -70,5 +64,5 @@
 Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots
 \varphi_i^k\}$ Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
-propositions $AP$ belongs to $\{I_i\cup O_i\cup R_i\}$ .
+propositions $AP$ belong to $\{I_i\cup O_i\cup R_i\}$ .
 \end{definition}
 
@@ -76,10 +70,10 @@
 
 Our abstraction consists in reducing the size of the representation model by
-freeing some of its variables. The point is to determine the good set of variable
+letting free some of its variables. The point is to determine the good set of variable
 to be freed and when to free them. We take advantage of the CTL specification
 of each component: a CTL property may be seen as a partial view of the tree of
 behaviors of its variables. All the variables not specified by the property
 can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly
-specifies when the variable of the prperty can be freed.
+specifies when the variable of the property can be freed.
 The abstraction of a component is represented by an AKS,
 derived from a subset of the CTL properties the component satisfies.
@@ -87,6 +81,6 @@
 $\varphi$, simulates all execution trees whose initial state satisfies
 $\varphi$. In AKS($\varphi$), states are tagged with the truth values of
-$\varphi$'s atomic propositions, among four truth values : inconsistent,
-false, true and unknown (either true or false).
+$\varphi$'s atomic propositions, among the four truth values of Belnap's logic \cite{belnap77}: inconsistent ($\bot$),
+false ($\mathbf{f}$), true ($\mathbf{t}$) and unknown ($\top$)).
 States with inconsistent truth values are not represented since they refer to non possible
 assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles.
@@ -103,11 +97,5 @@
 \item { $\widehat{S}$ : a finite set of states}
 \item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
-\item { $\widehat{L} : \widehat{S} \rightarrow 2^{Lit}$ : a labeling function which labels each state with the set of atomic propositions true in that state. Lit is a set of literals such that $Lit = AP \cup \{\bar{p} | p \in AP \}$. With this labeling definition, an atomic proposition in a state can have 4 different values as detailed below:}
-		\begin{itemize}
-			\item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s }
-			\item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s}
-			\item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s}
-		  \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) :  p $\emph{ is \textbf{inconsistent} in} s}
-		\end{itemize}
+\item { $\widehat{L} : \widehat{S} \rightarrow \cal{B}^{\mid AP \mid}$ with $\cal{B} = \{\bot, \mathbf{f}, \mathbf{t},\top\}$: a labeling function which labels each state with configuration of current value of each atomic proposition.}
 \item { $\widehat{R} \subseteq \widehat{S} \times \widehat{S}$ : a transition relation where $ \forall s \in \widehat{S}, \exists s' \in \widehat{S}$ such that $(s,s') \in \widehat{R}$ }
 \item { $\widehat{F}$ : a set of fairness constraints (generalized B\"uchi
@@ -117,14 +105,15 @@
 %\bigskip
 
+We denote by $\widehat{L}(s)$ the configuration of atomic propositions in state $s$ and by $\widehat{L}(s)[p]$ the projection of configuration $\widehat{L}(s)$ according to atomic proposition $p$.
 
 As the abstract model $\widehat{M}$ is generated from the conjunction of verified properties of the components in the concrete model $M$, it can be seen as the composition of the AKS of each property.
 The AKS composition has been defined in \cite{braunstein_phd07}; it extends
-the classical synchrounous composition of Moore machine to deal with
+the classical synchronous composition of Moore machine to deal with
 four-valued variables.
 %\bigskip
 
 \begin{definition} An \emph{Abstract model} $\widehat{M}$is obtained by
-synchronous composition of components abstractions.
-Let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$:
+synchronous composition of components abstractions. Let $n$ be the number of components in the model and $m$ be the number of selected verified properties of a component; 
+let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$:
 
 \begin{itemize}
@@ -133,22 +122,15 @@
 \end{itemize}
 
-\hspace*{3mm}with :\\
-\hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\
-\hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component
-
 \end{definition}
-%\bigskip
 
 
-The generation of an abstract model in the form of AKS from CTL formulas,
-based on the works of Braunstein \cite{braunstein07ctl_abstraction},
-has been successfully implemented by Bara \cite{bara08abs_composant}.
+The generation of an abstract model in the form of AKS from CTL formulas is described in \cite{braunstein07ctl_abstraction} and has been implemented (\cite{bara08abs_composant}).
 
 
 %\subsection{Characterization of AKS}
 
-In an abstract kripke structure a state where a variable $p$ is {\it unknown}
+In an abstract Kripke structure a state where a variable $p$ is {\it unknown}
 can simulate all states in which $p$ is either true or false. It
-is concise representation of the set of more concrete states in which $p$
+is a concise representation of the set of more concrete states in which $p$
 is either true or false.  A state $s$ is said to be an \emph{abstract state}
 if one its variable $p$ is {\it unknown}.
@@ -167,10 +149,10 @@
 
 \begin{property}
-Let A1 and A2 two abstractions such that A2 is obtained by concretizing one abstract variable of A1 (resp A1 is obtained by abstracting one variable in A2). Then A1 simulates A2.
+Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by concretizing one abstract variable of $A_i$ (resp $A_i$ is obtained by abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by $A_j \sqsubseteq A_i$.
 \end{property}
 \begin{proof}
 As the concretization of state reduces the set of concrete configuration the
 abstract state represents but does not affect the transition relation of the
-AKS. The unroll execution tree of A2 is a subtree of the one of A1. Then  A1 simulates A2.
+AKS. The unroll execution tree of $A_j$ is a subtree of the one of $A_i$. Then  $A_i$ simulates $A_j$.
 \end{proof}
 
