diff -r ac847263ce98 -r 78929f746a5c paper/src/paper.tex
--- a/paper/src/paper.tex	Tue Jun 14 01:36:04 2011 +0200
+++ b/paper/src/paper.tex	Wed Jun 22 20:06:27 2011 +0200
@@ -5,6 +5,7 @@
 \usepackage{typearea}
 \usepackage{algorithm}
 \usepackage{algorithmic}
+%\usepackage{fullpage}
 %\usepackage[T1]{fontenc}
 %\usepackage{arev}
 
@@ -29,7 +30,9 @@
 \newtheorem*{def:regular languages closure}{Regular closure}
 \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
 \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
-
+\newtheorem*{def:buechi automata}{Automata}
+\newtheorem*{def:automata runs}{Runs}
+\newtheorem*{def:automata acceptance}{Acceptance}
 \begin{document}
 
 \maketitle
@@ -83,7 +86,7 @@
 
 \section{$\omega$-regular languages}
 \begin{def:finite words}
-Let $\Sigma$ be a non-empty set of symbols, called the alphabet. $\Sigma^*$ is the set of all \emph{finite} words over $\Sigma$. A \emph{finite} word $w \in \Sigma^*$ is a \emph{finite} sequence $v_0...v_{n-1}$ of symbols from alphabet $\Sigma$ with length $n = |w|$. $\varepsilon$ denotes the empty word with length $|\varepsilon| = 0$.
+Let $\Sigma$ be a non-empty set of symbols, called the alphabet. $\Sigma^*$ is the set of all \emph{finite} words over $\Sigma$. A \emph{finite} word $w \in \Sigma^*$ is a \emph{finite} sequence $v_0,...,v_{n-1}$ of symbols from alphabet $\Sigma$ with length $n = |w|$. $\varepsilon$ denotes the empty word with length $|\varepsilon| = 0$.
 \end{def:finite words}
 
 \begin{def:regular languages}
@@ -107,7 +110,7 @@
 \end{def:regular languages closure}
 
 \begin{def:infinite words}
-$\Sigma^\omega$ is the set of all \emph{infinite} words over $\Sigma$. An \emph{infinite} word $w \in \Sigma^\omega$ is an \emph{infinite} sequence $v_0...v_\infty$ with length $\infty$. To address the elements of the infinite sequence $w$, view the word as a function $w : \mathbb{N}_0 \to \Sigma$ with $w(i) = v_i$; thus $w(i)$ denotes the symbol at sequence position $i$ of word $w$; another notation used for $w(i)$ is $w_i$.
+$\Sigma^\omega$ is the set of all \emph{infinite} words over $\Sigma$. An \emph{infinite} word $w \in \Sigma^\omega$ is an \emph{infinite} sequence $v_0,...,v_\infty$ with length $\infty$. To address the elements of the infinite sequence $w$, we view the word as a function $w : \mathbb{N}_0 \to \Sigma$ with $w(i) = v_i$; thus $w(i)$ denotes the symbol at sequence position $i$ of word $w$; another notation used for $w(i)$ is $w_i$.
 \end{def:infinite words}
 
 \begin{def:omega regular languages}
@@ -124,7 +127,24 @@
 
 
 \section{B\"uchi automata}
-Automata are good.
+\begin{def:buechi automata}
+A non-deterministic B\"uchi automaton is a tuple $A = (\Sigma, S, S_0, \Delta, F)$, where $\Sigma$ is a finite non-empty \emph{alphabet}, $S$ is a finite non-empty set of \emph{states}, $S_0 \subseteq S$ is the set of \emph{initial states}, $F \subseteq S$ is the set of \emph{accepting states} and $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}. When suitable we will use the arrow notation for the transitions, where $s \xrightarrow{a} s' \iff (s, a, s') \in \Delta$.
+
+A deterministic B\"uchi automaton is a specialisation where the \emph{transition relation} $\Delta$ is a \emph{transition function} $\delta: S \times \Sigma \to S$ and the set $S_0$ of \emph{initial states} contains only a single state $s_0$.
+
+Within this text \emph{automata/automaton} will refer to non-deterministic B\"uchi automata/automaton, unless otherwise noted. 
+\end{def:buechi automata}
+
+\begin{def:automata runs}
+Let $A = (\Sigma, S, S_0, \Delta, F)$ be an automaton, a run $\rho$ of $A$ on an infinite word $w = a_0,a_1,...$ over alphabet $\Sigma$ is a sequence $\rho = s_0,s_1,...$, where $s_0 \in S_0$ and $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$. Again we may view the run sequence as a function $\rho : \mathbb{N}_0 \to S$, where $\rho(i) = s_i$ denotes the state at the $i^{th}$ sequence position.
+\end{def:automata runs}
+
+\begin{def:automata acceptance}
+Let $A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $A$, we define $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \mathbb{N}_0}: \rho(n) = s\}$, where $\exists^\omega$ denotes the existential quantifier for infinitely many occurances, i.e., $s$ occurs infinitely often in $\rho$.
+
+The run $\rho$ is \emph{accepting}, iff $inf(\rho) \cap F \neq \emptyset$, i.e., there exists an \emph{accepting state} which occurs infinitely often in the run $\rho$. The automaton $A$ \emph{accepts} an input word $w$, iff there exists a run $\rho$ of $A$ on $w$, such that $\rho$ is \emph{accepting}.
+\end{def:automata acceptance}
+
 \section{Linear temporal logic}
 
 \section{Model checking}