Changeset 92 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Apr 6, 2012, 10:37:41 PM (13 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

• papers/FDL2012/abstraction_refinement.tex (modified) (3 diffs)

papers/FDL2012/abstraction_refinement.tex

@@ -8 +8 @@
 
 \begin{definition} An efficient \emph{refinement} verifies the following properties:
+\vspace*{-2mm}
 \begin{enumerate}
+\itemsep -0.3em
 \item The new refinement is an over-approximation of the concrete model:
 $\widehat{M} \sqsubseteq \widehat{M}_{i+1}$.
@@ -46 +48 @@
 \widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
 \rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
+%\vspace*{-2mm}
 \begin{itemize}
+%\topsep 0pt
+\itemsep -0.3em
 \item All its variables are concrete: $\forall s_i$ and $\forall p\in
 \widehat{AP}_i$, $p$ is either true or false according to $\widehat{L_i}$.
@@ -66 +71 @@
 \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
 \widehat{F}_{\overline{\sigma}} \rangle$ is such that :
+\vspace*{-2mm}
 \begin{itemize}
+%\topsep 0pt
+\itemsep -0.3em
 \item $AP_{\overline{\sigma}} = {AP}_i$:
 The set of atomic propositions coincides with the one of $\sigma$