1.1 --- a/paper/src/paper.tex	Wed Jun 29 18:39:07 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Wed Jun 29 18:56:22 2011 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4  
     1.5  \subsection{Semantics}
     1.6  \begin{def:frames}
     1.7 -A LTL-\emph{frame} is a tuple $\F = (S, R)$, where $S = \{s_i \mid i \in \N\}$ is the set of states and $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ the set of accessibility relations. Hence $S$ is an isomorphism of $\N$ and $R$ an isomorphism of the strict linear order $(\N, <)$, which corresponds to the linear progression of time. 
     1.8 +A LTL-\emph{frame} is a tuple $\F = (S, R)$, where $S = \{s_i \mid i \in \N\}$ is the set of states and $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ the set of accessibility relations. Hence $S$ is an isomorphism of $\N$ and $R$ an isomorphism of the strict linear order $(\N, <)$, which corresponds to the linear progression of discrete time. 
     1.9  \end{def:frames}
    1.10  
    1.11  \begin{def:models}