Changeset 86 for papers/FDL2012/framework.tex

Timestamp:

Apr 6, 2012, 11:24:24 AM (13 years ago)

Author:

ema

Message:

 

File:

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

papers/FDL2012/framework.tex

@@ -6 +6 @@
 attached to each component. This set refers to the specification of the
 component. We would like to verify whether a concrete model, $M$ presumably
-big sized and composed of several components, satisfies a global ACTL property $\Phi$. 
+big 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}.
@@ -126 +126 @@
 
 \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; 
+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]$:
 
@@ -183 +183 @@
 
 \begin{proof}
-Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$ 
+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 logic operator and
-to 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 to 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}
@@ -197 +196 @@
 (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, 
+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}