1.1 --- a/paper/src/paper.tex	Tue Jul 12 17:39:08 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue Jul 12 17:54:45 2011 +0200
     1.3 @@ -196,9 +196,9 @@
     1.4  \noindent The equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata follows intuitively.
     1.5  
     1.6  \section{Linear temporal logic}
     1.7 -Nothing escapes time, but time has successfully escaped its formalisation until the rise of the modal logics in the second half of the 20th century \cite{ref:handbook}. All arts and sciences interpret time in some way; where historians prefer the past tense, do science-fiction novels live in the future. Physics knows many time arrows, one of which constitutes the thermodynamic arrow of time, which happens to be the one we perceive by remembering the past and not the future. We compensate our inability to control the direction of time, by the use of rigorous language constructs when reasoning about temporal events.
     1.8 +Nothing escapes time, but time has successfully escaped its formalisation in computer science until the rise of the modal logics in the second half of the 20th century \cite{ref:handbook}. All arts and sciences interpret time in some way; where historians prefer the past tense, do science-fiction novels live in the future. Physics knows many time arrows, one of which constitutes the thermodynamic arrow of time, which happens to be the one we perceive by remembering the past and not the future. We compensate our inability to control the direction of time, by the use of rigorous language constructs when reasoning about temporal events.
     1.9  
    1.10 -When natural language fails in providing unambiguousness, we have to resort to formal languages. To handle time, we use \emph{propositional logic} as the base and extend it by some more or less modal connectives.
    1.11 +When natural language fails in providing unambiguousness, we have to resort to formal languages. To handle time, we use \emph{propositional logic} as the base and extend it by some more or less modal connectives. There are two major temporal logics used in the specification of system properties, \emph{linear temporal logic (LTL)} and \emph{branching temporal logic (CTL - for Computation Tree Logic)}. Temporal logics are interpreted over computation paths; in LTL such a path depicts a linear sequence, where in CTL the path is a tree, with branching connectives. Throughout this text, we will restrict our attention to LTL.
    1.12  
    1.13  \subsection{Syntax}
    1.14  Let $\Prop$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(\Prop)$ is $\Prop \cup \{\neg, \lor, \X, \U\}$. We define the $L_{LTL}(\Prop)$-\emph{formulae} $\varphi$ using following productions:
    1.15 @@ -207,7 +207,7 @@
    1.16  \subsection{Interpretation}
    1.17  The intuition should go as follows: $\neg$ and $\lor$ correspond to the Boolean \emph{negation} and \emph{disjunction}, the unary temporal operator $\X$ reads as \emph{next} and the binary temporal operator $\U$ reads as \emph{until}.
    1.18  
    1.19 -LTL is interpreted over \emph{computation paths}, where a computation corrensponds to a model over a \emph{Kripke-frame} constructed by the order of natural numbers.
    1.20 +LTL is interpreted over \emph{computation paths}, where a computation corresponds to a model over a \emph{Kripke-frame} constructed by the order of natural numbers.
    1.21  
    1.22  \subsection{Semantics}
    1.23  \begin{def:frames}