Changeset 92 for papers/FDL2012/framework.tex

Timestamp:

Apr 6, 2012, 10:37:41 PM (12 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

• papers/FDL2012/framework.tex (modified) (10 diffs)

papers/FDL2012/framework.tex

@@ -43 +43 @@
 %   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
 %     \hspace*{-5mm}
-     \includegraphics{our_framework_cegar_png}
+     \includegraphics[scale=0.37]{our_framework_cegar_png}
    \caption{\label{cegar} Verification Process }
 \end{figure}
 
+\vspace*{-5mm}
 \subsection{Concrete system definition}
 As mentioned earlier, our concrete model consists of several components and each
@@ -54 +55 @@
 \begin{definition}
 A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where,
-\begin{itemize}
+\vspace*{-2mm}
+\begin{itemize}
+%\partopsep= -1.0em
+%\topsep -0.5em
+\itemsep -0.3em
 \item $I$ is a finite set of Boolean inputs signals.
 \item $O$ is a finite set of Boolean outputs signals.
@@ -104 +109 @@
 $AP$, An \emph{Abstract Kripke Structure}, $AKS(\varphi) =(AP, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of:
 
-\begin{itemize}
+\vspace*{-3mm}
+\begin{itemize}
+%\partopsep=0pt
+%\topsep 0pt
+\itemsep -0.3em
 \item { $AP$ : The finite set of atomic propositions of property $\varphi$ }    
 \item { $\widehat{S}$ : a finite set of states}
@@ -116 +125 @@
 %\bigskip
 
+\vspace*{-2mm}
 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$.
 
@@ -129 +139 @@
 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}
+\vspace*{-3mm}
+\begin{itemize}
+%\topsep 0pt
+\itemsep -0.3em
 \item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $}
 \item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
@@ -137 +150 @@
 
 
-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}).
+%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}).
 
 
@@ -154 +167 @@
 \begin{definition}[]
 The \emph {concretization} of an abstract state $s$ with respect to the variable $p$
-({\it unknown} in that state), assigns either true or false to $p$.
-
+({\it unknown} in that state), assigns either true or false to $p$.\\
 The \emph {abstraction} of a state $s$ with respect to the variable $p$
 (either true or false in that state), assigns  {\it unknown} to $p$.
@@ -188 +200 @@
 {\it and} to the  four-valued values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in
 AP_i \cup AP_{\varphi_j^k}$ we have the following label~:
-\begin{itemize}
-\topsep -.5em
-\itemsep -0.5em
+\vspace*{-2mm}
+\begin{itemize}
+%\topsep 0pt
+\itemsep -0.3em
 \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.
@@ -197 +210 @@
 (resp. $s_{\varphi_j^k}$).
 \end{itemize}
+\vspace*{-2mm}
 By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than
 $\widehat{M}_i$ and by
@@ -203 +217 @@
 \end{proof}
 
+\vspace*{-5mm}
 \subsection{Initial abstraction}
 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$.