Changeset 89 for papers/FDL2012/framework.tex

Timestamp:

Apr 6, 2012, 4:44:06 PM (13 years ago)

Author:

cecile

Message:

corrections typos and co

File:

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

papers/FDL2012/framework.tex

@@ -48 +48 @@
 
 \subsection{Concrete system definition}
-As mention earlier, our concrete model consists of several components and each
+As mentioned 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
@@ -178 +178 @@
 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 more concrete that $ \widehat{M_i}$, $\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}
@@ -185 +185 @@
 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}$ is obtained by applying the Belnap's logic operators to four-valued values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in
+The label of $s_{i+1}$ is obtained by applying the Belnap's logic operators
+{\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}
@@ -196 +197 @@
 (resp. $s_{\varphi_j^k}$).
 \end{itemize}
-By property \ref{prop:concrete}, $M_{i+1}$ is more concrete than $M_i$ and by
+By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than
+$\widehat{M}_i$ and by
 the property of parallel composition,
 $\widehat{M_i} \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$).