1.1 --- a/paper/src/paper.tex	Fri Jul 15 23:39:56 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue Jul 19 02:33:21 2011 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4 -\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
     1.5 +\documentclass{beamer}
     1.6 +%\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
     1.7  \usepackage{graphicx}
     1.8  %\usepackage[latin1]{inputenc}
     1.9  \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
    1.10 @@ -278,7 +279,7 @@
    1.11  An 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.12  \end{def:frames}
    1.13  %
    1.14 -\noindent The frame defines the structure of linear time and the flow temporal events. To perfect our structure for temporal reasoning, we need to give those events a formal meaning. We do so by assigning a value to each atomic proposition.
    1.15 +\noindent The frame defines the structure of linear time and the temporal flow of events. To perfect our structure for temporal reasoning, we need to give those events a formal meaning. We do so by assigning a value to each atomic proposition.
    1.16  
    1.17  \begin{def:models}
    1.18  An LTL-\emph{model} is a tuple $\M = (\F, V)$, where $\F$ is a \emph{frame} and $V: S \to 2^\Prop$ a \emph{valuation function}. Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.