1.1 --- a/paper/src/paper.tex	Thu Jul 14 02:10:51 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Thu Jul 14 03:09:53 2011 +0200
     1.3 @@ -200,29 +200,29 @@
     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 capture 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 novelists 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 capture 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: historians prefer the past tense, while politicians only make promises for the future. Physicists know 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 discrete 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.11 +When natural language fails in providing unambiguousness, we have to resort to formal languages. To handle discrete 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}, short LTL, and \emph{branching temporal logic}, short CTL -- for computation tree logic. Throughout this text, we will restrict our attention to linear temporal logic.
    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  \[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
    1.16 +%
    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 +\subsection{Semantics}
    1.19 +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. In the interpretation of LTL over \emph{computation paths}, a computation corresponds to a model over a \emph{Kripke-frame} constructed by the order of natural numbers.
    1.20  
    1.21 -\subsection{Interpretation}
    1.22 -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.23 -
    1.24 -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.25 -
    1.26 -\subsection{Semantics}
    1.27  \begin{def:frames}
    1.28  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.29  \end{def:frames}
    1.30 +%
    1.31 +\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.32  
    1.33  \begin{def:models}
    1.34  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)$. 
    1.35  %A \emph{model} is a function $\M: \N \to 2^\Prop$ over \emph{frame} $\F$. The frame constitutes a linear order over $\N$, which corresponds to the linear progression of time from the \emph{present/past} into the \emph{future}. Therefore $\M(i)$ assigns a set of \emph{positive atomic propositions} to each state of time instant $i$. Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in \M(i)$.
    1.36  \end{def:models}
    1.37 -
    1.38 +%
    1.39  \begin{def:satisfiability}
    1.40  A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$. Satisfiability of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
    1.41  \begin{itemize}
    1.42 @@ -232,8 +232,11 @@
    1.43  \item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
    1.44  \item $\M,i \models \varphi \U \psi \iff \exists{k \geq i}: \M,k \models \psi$ and $\forall{i \leq j < k}: \M,j \models\varphi$
    1.45  \end{itemize}
    1.46 +\end{def:satisfiability}
    1.47 +%
    1.48 +\noindent From the strict linear order of the LTL-frame accessibility relation follows that an LTL-formula $\varphi$ is \emph{satisfiable}, iff there exists a model $\M$ with $\M,0 \models \varphi$.
    1.49  
    1.50 -\end{def:satisfiability}
    1.51 +We clearly see, that atomic propositions, which are not contained within the formula $\varphi$ are redundant to the the definition of the satisfiablity. By defining the \emph{vocabulary} of a formula, we dispose such irrelevant atomic proposition from the alphabet.
    1.52  
    1.53  \begin{def:vocabulary}
    1.54  Let $\varphi$ be an LTL-formula over atomic propositions $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively: