1.1 --- a/paper/src/paper.tex	Tue Jun 14 01:36:04 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Wed Jun 22 20:06:27 2011 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  \usepackage{typearea}
     1.5  \usepackage{algorithm}
     1.6  \usepackage{algorithmic}
     1.7 +%\usepackage{fullpage}
     1.8  %\usepackage[T1]{fontenc}
     1.9  %\usepackage{arev}
    1.10  
    1.11 @@ -29,7 +30,9 @@
    1.12  \newtheorem*{def:regular languages closure}{Regular closure}
    1.13  \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
    1.14  \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
    1.15 -
    1.16 +\newtheorem*{def:buechi automata}{Automata}
    1.17 +\newtheorem*{def:automata runs}{Runs}
    1.18 +\newtheorem*{def:automata acceptance}{Acceptance}
    1.19  \begin{document}
    1.20  
    1.21  \maketitle
    1.22 @@ -83,7 +86,7 @@
    1.23  
    1.24  \section{$\omega$-regular languages}
    1.25  \begin{def:finite words}
    1.26 -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$.
    1.27 +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$.
    1.28  \end{def:finite words}
    1.29  
    1.30  \begin{def:regular languages}
    1.31 @@ -107,7 +110,7 @@
    1.32  \end{def:regular languages closure}
    1.33  
    1.34  \begin{def:infinite words}
    1.35 -$\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$.
    1.36 +$\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$.
    1.37  \end{def:infinite words}
    1.38  
    1.39  \begin{def:omega regular languages}
    1.40 @@ -124,7 +127,24 @@
    1.41  
    1.42  
    1.43  \section{B\"uchi automata}
    1.44 -Automata are good.
    1.45 +\begin{def:buechi automata}
    1.46 +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$.
    1.47 +
    1.48 +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$.
    1.49 +
    1.50 +Within this text \emph{automata/automaton} will refer to non-deterministic B\"uchi automata/automaton, unless otherwise noted. 
    1.51 +\end{def:buechi automata}
    1.52 +
    1.53 +\begin{def:automata runs}
    1.54 +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.
    1.55 +\end{def:automata runs}
    1.56 +
    1.57 +\begin{def:automata acceptance}
    1.58 +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$.
    1.59 +
    1.60 +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}.
    1.61 +\end{def:automata acceptance}
    1.62 +
    1.63  \section{Linear temporal logic}
    1.64  
    1.65  \section{Model checking}