Changeset 82 for papers/FDL2012/framework.tex

Timestamp:

Apr 5, 2012, 12:05:33 PM (13 years ago)

Author:

cecile

Message:

correction label AKS(cex)

File:

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

papers/FDL2012/framework.tex

@@ -3 +3 @@
 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$ presumably huge sized and composed of several components, satisfies a global ACTL property $\Phi$. 
+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
+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}.
@@ -89 +92 @@
 false ($\mathbf{f}$), true ($\mathbf{t}$) and unknown ($\top$)).
 States with inconsistent truth values are not represented since they refer to non possible
-assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles.
+assignments of the atomic propositions. A set of fairness constraints
+eliminates non-progress cycles. The transformation algorithm of a
+CTL$\setminus$X property into an AKS is described in
+\cite{braunstein07ctl_abstraction,braunstein_phd07}.
 
 
@@ -158 +164 @@
 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$ and $A_j$
-concretizes $A_i$ , denoted by
+abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by
 $A_j \sqsubseteq A_i$.
 \end{property}
@@ -180 +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}$ respects the Belnap logic operator. For all $p \in
+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
 AP_i \cup AP_{\varphi_j^k}$ we have the following label~:
 \begin{itemize}
@@ -209 +215 @@
 %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
+In the initial abstraction generation, all variables that appear in $\Phi$ have to be
 represented. Therefore the properties in the specification of each component
 where these variables are present will be used to generate the initial