1.1 --- a/paper/src/paper.tex	Mon Jun 27 19:16:05 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue Jun 28 00:16:13 2011 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  \documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
     1.5  \usepackage{graphicx}
     1.6  %\usepackage[latin1]{inputenc}
     1.7 -\usepackage{amsmath, amsthm, amssymb}
     1.8 +\usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
     1.9  \usepackage{typearea}
    1.10  \usepackage{algorithm}
    1.11  \usepackage{algorithmic}
    1.12 @@ -33,6 +33,9 @@
    1.13  \newtheorem*{def:buechi automata}{Automata}
    1.14  \newtheorem*{def:automata runs}{Runs}
    1.15  \newtheorem*{def:automata acceptance}{Acceptance}
    1.16 +\newtheorem*{def:vocabulary}{Vocabulary}
    1.17 +
    1.18 +\newtheorem{prop:vocabulary sat}{Proposition}
    1.19  \begin{document}
    1.20  
    1.21  \maketitle
    1.22 @@ -167,6 +170,24 @@
    1.23  \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.24  \end{itemize}
    1.25  
    1.26 +\begin{def:vocabulary}
    1.27 +Let $\varphi$ be a LTL-formula over atomic propositions $P$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
    1.28 +\begin{itemize}
    1.29 +\item $Voc(p) = \{p\}$ for $p \in P$
    1.30 +\item $Voc(\neg \varphi) = Voc(\varphi)$
    1.31 +\item $Voc(\varphi \lor \psi) = Voc(\varphi) \cup Voc(\psi)$
    1.32 +\item $Voc(X \varphi) = Voc(\varphi)$
    1.33 +\item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$
    1.34 +\end{itemize}
    1.35 +Let $M$ be a model and $\varphi$ a LTL-formula, we define model $M_{Voc(\varphi)}$:
    1.36 +\[\forall{i \in \mathbb{N}}: M_{Voc(\varphi)} = M(i) \cap Voc(\varphi)\]
    1.37 +\end{def:vocabulary}
    1.38 +
    1.39 +\begin{prop:vocabulary sat}
    1.40 +Let $M$ be a model and $\varphi$ a LTL-formula, then following holds:
    1.41 +\[\forall{i \in \mathbb{N}}: M,i \models \varphi \iff M_{Voc(\varphi)},i \models \varphi\] 
    1.42 +\end{prop:vocabulary sat}
    1.43 +
    1.44  \section{Model checking}
    1.45  \begin{thebibliography}{99}
    1.46  \bibitem{ref:ltl&büchi}