1.1 --- a/paper/src/paper.tex	Thu Jun 23 01:22:53 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Mon Jun 27 19:16:05 2011 +0200
     1.3 @@ -146,6 +146,26 @@
     1.4  \end{def:automata acceptance}
     1.5  
     1.6  \section{Linear temporal logic}
     1.7 +\subsection*{Sytnax}
     1.8 +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:
     1.9 +\[\varphi ::= p \in P \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
    1.10 +
    1.11 +\subsection*{Interpretation}
    1.12 +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.13 +
    1.14 +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.15 +
    1.16 +\subsection*{Semantics}
    1.17 +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)$.
    1.18 +
    1.19 +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$:
    1.20 +\begin{itemize}
    1.21 +\item $M,i \models p$ for $p \in P$ iff $p \in M(i)$
    1.22 +\item $M,i \models \neg \varphi$ iff not $M,i \models \varphi$
    1.23 +\item $M,i \models \varphi \lor \psi$ iff $M,i \models \varphi$ or $M,i \models \psi$
    1.24 +\item $M,i \models X \varphi$ iff $M,i+1 \models \varphi$
    1.25 +\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.26 +\end{itemize}
    1.27  
    1.28  \section{Model checking}
    1.29  \begin{thebibliography}{99}