Changeset 93 for papers/FDL2012/framework.tex

Timestamp:

Apr 10, 2012, 4:30:02 PM (12 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

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

papers/FDL2012/framework.tex

@@ -15 +15 @@
 %generated and tested in the model-checker. As the abstract model is an
 %over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment,
-As show in \cite{clarke94model} for over-approximation abstraction, if $\Phi$
-holds on the the abstract model then it holds in the concrete model as well.
+As shown in \cite{clarke94model} for over-approximation abstraction, if $\Phi$
+holds in the abstract model then it holds in the concrete model as well.
 However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample has been analyzed.
 The test of spurious counter-example is then translated into a
@@ -60 +60 @@
 %\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.
+\item $I$ is a finite set of Boolean input signals.
+\item $O$ is a finite set of Boolean output signals.
 \item $R$ is a finite set of Boolean sequential elements (registers).
 \item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function.
@@ -76 +76 @@
 $M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a
 Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots
-\varphi_i^k\}$ Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
+\varphi_i^k\}$. Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
 propositions $AP$ belong to $\{I_i\cup O_i\cup R_i\}$ .
 \end{definition}
@@ -126 +126 @@
 
 \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$.
+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$.
 
 
@@ -155 +155 @@
 %\subsection{Characterization of AKS}
 
-In an AKS a state where a variable $p$ is {\it unknown}
+In an AKS, a state where a variable $p$ is {\it unknown}
 can simulate all states in which $p$ is either true or false. It
 is a concise representation of the set of more concrete states in which $p$
 is either true or false.  A state $s$ is said to be an \emph{abstract state}
-if one its variable $p$ is {\it unknown}.
+if one of its variable $p$ is {\it unknown}.
 
 %\begin{definition}