Index: papers/FDL2012/framework.tex
===================================================================
--- papers/FDL2012/framework.tex	(revision 79)
+++ papers/FDL2012/framework.tex	(revision 81)
@@ -3,12 +3,17 @@
 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 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}.
+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$ presumably 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}
-In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
-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 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
+%In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
+%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 the global property $\Phi$ is in the ACTL fragment,
+As show in \cite{clarke94model} for over-approximation abstraction, if $\Phi$
+holds on the the abstract model then it holds in the concrete model as well.
+However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample has been analyzed.
+The test of spurious counter-example is then translated into a
 SAT problem as in \cite{clarke00cegar}. When a counterexample is proven to be spurious, the refinement phase occurs, injecting more preciseness into the (abstract) model to be analyzed.
 
@@ -40,7 +45,6 @@
 
 \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 $\Phi$.
-
-
+As mention earlier, our concrete model consists of several components and each
+component comes with its specification.
 The concrete system is a synchronous composition of components, each of which
 described as a Moore machine.
@@ -48,7 +52,7 @@
 A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where,
 \begin{itemize}
-\item $I$ is a finite set of boolean inputs signals.
-\item $O$ is a finite set of boolean outputs signals.
-\item $R$ is a finite set of boolean sequential elements (registers).
+\item $I$ is a finite set of Boolean inputs signals.
+\item $O$ is a finite set of Boolean outputs signals.
+\item $R$ is a finite set of Boolean sequential elements (registers).
 \item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function.
 \item $\lambda : 2^R \rightarrow 2^O$ is the output function.
@@ -57,5 +61,5 @@
 \end{definition}
 
-\emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements.
+\emph{States} (or configurations) of the circuit correspond to Boolean configurations of all the sequential elements.
 
 \begin{definition}
@@ -70,5 +74,5 @@
 \subsection{Abstraction definition}
 
-Our abstraction consists in reducing the size of the representation model by
+Our abstraction reduces the size of the representation model by
 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
@@ -132,5 +136,5 @@
 %\subsection{Characterization of AKS}
 
-In an abstract Kripke structure a state where a variable $p$ is {\it unknown}
+In an AKS a state where a variable $p$ is {\it unknown}
 can simulate all states in which $p$ is either true or false. It
 is a concise representation of the set of more concrete states in which $p$
@@ -151,44 +155,61 @@
 
 \begin{property}[Concretization]
+\label{prop:concrete}
 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_i \sqsubseteq A_j$.
+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$ and $A_j$
+concretizes $A_i$ , 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 $A_j$ is a subtree of the one of $A_i$. Then  $A_i$ simulates $A_j$.
+AKS. The unroll execution tree of $A_j$ is a sub-tree of the one of $A_i$. Then
+$A_i$ simulates $A_j$.
 \end{proof}
 
-\begin{property}[Compostion and Concretization]
+\begin{property}[Composition and Concretization]
 \label{prop:concrete_compose}
 Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property
 of a component $C_j$ of M,  $\widehat{M}_{i+1} = \widehat{M_i}\parallel
-AKS(\varphi_j^k) $ is simulated by $ \widehat{M_i}$, $\widehat{M_i}
-\sqsubseteq \widehat{M}_{i+1}$.
+AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M_{i+1}}
+\sqsubseteq \widehat{M}_i$.
 \end{property}
 
 \begin{proof}
-By the property of the parallel composition, we have directly  $\widehat{M_i}
-\sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$.
+Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$ 
+and $s_{\varphi_j^k} \in S_{\varphi_j^k}$.
+The label of $s_{i+1}$ respects the Belnap logic operator. For all $p \in
+AP_i \cup AP_{\varphi_j^k}$ we have the following label~:
+\begin{itemize}
+\topsep -.5em
+\itemsep -0.5em
+\item  $\widehat{L}_{i+1}[p] = \top$ iff  p is {\it unknown} in both states or
+does not belong to the set of atomic proposition.
+\item  $\widehat{L}_{i+1}[p] = \mathbf{t}$ (or $\mathbf{f}$) iff $p$ is true
+(or false) in $s_{\varphi_j^k}$ (resp. $s_i$)  and {\it unknown} in $s_i$
+(resp. $s_{\varphi_j^k}$).
+\end{itemize}
+By property \ref{prop:concrete}, $M_{i+1}$ is more concrete than $M_i$ and by 
+the property of parallel composition, 
+$\widehat{M_i} \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$).
 \end{proof}
 
 \subsection{Initial abstraction}
-We suppose that our concrete model is a composition of several components and
-each component has been previously verified. Hence, we have a set of verified
-properties for each component of the concrete model. The main idea of this
-technique is that we would like to make use of these properties to generate a
-better abstract model. Properties of the components that appear to be related
-to the global property to be verified, $\Phi$ are selected to generate the
-abstract model $\widehat{M}_i$. This method is particularly interesting as it
-gives a possibility to converge quicker to an abstract model that is
-sufficient to satisfy the global property $\Phi$.
-In the following, we will name primary variables the set of variable that
-appears in the global property.
-
-In the initial abstraction generation, all primary variables have to be
+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$.
+%We suppose that our concrete model is a composition of several components and
+%each component has been previously verified. Hence, we have a set of verified
+%properties for each component of the concrete model. The main idea of this
+%technique is that we would like to make use of these properties to generate a
+%better abstract model. Properties of the components that appear to be related
+%to the global property to be verified, $\Phi$ are selected to generate the
+%abstract model $\widehat{M}_i$. This method is particularly interesting as it
+%gives a possibility to converge quicker to an abstract model that is
+%sufficient to satisfy the global property $\Phi$.
+%In the following, we will name primary variables the set of variable that
+%appears in the global property.
+In the initial abstraction generation, all variables that appear int $\Phi$ have to be
 represented. Therefore the properties in the specification of each component
-where the primary variables are present will be used to generate the initial
+where these variables are present will be used to generate the initial
 abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the
 global property $\Phi$ on this abstract model. If the model-checking failed and the counterexample given is found to be spurious, we will then proceed with the refinement process.
