diff -r 153633379524 -r b3f554e2a593 paper/src/paper.tex
--- a/paper/src/paper.tex	Thu Jun 23 01:22:53 2011 +0200
+++ b/paper/src/paper.tex	Mon Jun 27 19:16:05 2011 +0200
@@ -146,6 +146,26 @@
 \end{def:automata acceptance}
 
 \section{Linear temporal logic}
+\subsection*{Sytnax}
+Let $P$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(P)$ is $P \cup \{\neg, \lor, X, U\}$. We define the $L_{LTL}(P)$-\emph{formulae} $\varphi$ using following productions:
+\[\varphi ::= p \in P \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
+
+\subsection*{Interpretation}
+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}.
+
+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.
+
+\subsection*{Semantics}
+A \emph{model} is a function $M: \mathbb{N}_0 \to 2^P$ over \emph{frame} $F$. The frame constitutes a linear order over $\mathbb{N}_0$, which corresponds to the linear temporal progression from \emph{now/before} to \emph{later}. Therefore $M(i)$ assigns a set of \emph{positive atomic propositions} to each state of time instant $i$. Intuitively we say $p \in P$ is \emph{true} at time instant $i$, iff $p \in M(i)$.
+
+A model $M$ \emph{satisfies} an LTL-formula $\varphi$ at time instant $i$ is denoted by $M,i \models \varphi$. Satisfaction of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
+\begin{itemize}
+\item $M,i \models p$ for $p \in P$ iff $p \in M(i)$
+\item $M,i \models \neg \varphi$ iff not $M,i \models \varphi$
+\item $M,i \models \varphi \lor \psi$ iff $M,i \models \varphi$ or $M,i \models \psi$
+\item $M,i \models X \varphi$ iff $M,i+1 \models \varphi$
+\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$
+\end{itemize}
 
 \section{Model checking}
 \begin{thebibliography}{99}