# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1309212973 -7200
# Node ID 68fff3a1453ee237c4f4318241337762eef50403
# Parent  b3f554e2a5932f6bbb295f7018d978965f4cdbe9
Some more LTL content.

diff -r b3f554e2a593 -r 68fff3a1453e paper/src/paper.tex
--- a/paper/src/paper.tex	Mon Jun 27 19:16:05 2011 +0200
+++ b/paper/src/paper.tex	Tue Jun 28 00:16:13 2011 +0200
@@ -1,7 +1,7 @@
 \documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
 \usepackage{graphicx}
 %\usepackage[latin1]{inputenc}
-\usepackage{amsmath, amsthm, amssymb}
+\usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
 \usepackage{typearea}
 \usepackage{algorithm}
 \usepackage{algorithmic}
@@ -33,6 +33,9 @@
 \newtheorem*{def:buechi automata}{Automata}
 \newtheorem*{def:automata runs}{Runs}
 \newtheorem*{def:automata acceptance}{Acceptance}
+\newtheorem*{def:vocabulary}{Vocabulary}
+
+\newtheorem{prop:vocabulary sat}{Proposition}
 \begin{document}
 
 \maketitle
@@ -167,6 +170,24 @@
 \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}
 
+\begin{def:vocabulary}
+Let $\varphi$ be a LTL-formula over atomic propositions $P$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
+\begin{itemize}
+\item $Voc(p) = \{p\}$ for $p \in P$
+\item $Voc(\neg \varphi) = Voc(\varphi)$
+\item $Voc(\varphi \lor \psi) = Voc(\varphi) \cup Voc(\psi)$
+\item $Voc(X \varphi) = Voc(\varphi)$
+\item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$
+\end{itemize}
+Let $M$ be a model and $\varphi$ a LTL-formula, we define model $M_{Voc(\varphi)}$:
+\[\forall{i \in \mathbb{N}}: M_{Voc(\varphi)} = M(i) \cap Voc(\varphi)\]
+\end{def:vocabulary}
+
+\begin{prop:vocabulary sat}
+Let $M$ be a model and $\varphi$ a LTL-formula, then following holds:
+\[\forall{i \in \mathbb{N}}: M,i \models \varphi \iff M_{Voc(\varphi)},i \models \varphi\] 
+\end{prop:vocabulary sat}
+
 \section{Model checking}
 \begin{thebibliography}{99}
 \bibitem{ref:ltl&büchi}