Changeset 79 for papers/FDL2012/framework.tex

Timestamp:

Mar 30, 2012, 5:02:20 PM (12 years ago)

Author:

cecile

Message:

correction counter-example and its negation representation

File:

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

papers/FDL2012/framework.tex

@@ -108 +108 @@
 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
@@ -114 +115 @@
 %\bigskip
 
-\begin{definition} An \emph{Abstract model} $\widehat{M}$is obtained by
+\begin{definition} An \emph{Abstract model} $\widehat{M}$ is obtained by
 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]$:
@@ -149 +150 @@
 \end{definition}
 
-\begin{property}
-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$.
+\begin{property}[Concretization]
+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$.
 \end{property}
 \begin{proof}
@@ -158 +162 @@
 \end{proof}
 
-\TODO{Name the simulation/concretization relation}
+\begin{property}[Compostion 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}$.
+\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$.
+\end{proof}
 
 \subsection{Initial abstraction}