1.1 --- a/paper/src/paper.tex	Fri Jul 15 19:21:26 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Fri Jul 15 20:07:34 2011 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  \usepackage{multicol}
     1.5  \usepackage{tikz}
     1.6  \usetikzlibrary{automata}
     1.7 +\usepackage{sidecap}
     1.8 +\usepackage{wrapfig}
     1.9  %\usepackage{fullpage}
    1.10  %\usepackage{a4wide}
    1.11  \usepackage[left=3.9cm, right=3.9cm]{geometry}
    1.12 @@ -184,8 +186,13 @@
    1.13  Given all legal computations of an automaton, we have defined the acceptance condition. A computation is accepting, if it passes through an accepting state infinitely times. Since the set of states $S$ is finite, there must be a state $s \in S$, which occurs infinitely often within an infinite run; but it is not necessary, that $s$ is an accepting state; notice that $F$ can be an empty set.
    1.14  
    1.15  \subsection{Example}
    1.16 -Let $\A_1 = (\Sigma, S, S_0, \Delta, F)$ be an automaton with $\Sigma = \{a, b\}$, $S = \{q_0, q_1, q_2\},$ $S_0 = \{q_0\}$ and $\Delta = \{(q_0, a, q_1)\}, F = \{q_2\}$.
    1.17 -
    1.18 +\label{ex:automaton}
    1.19 +%\begin{figure}[h]
    1.20 +\begin{wrapfigure}{r}{0.5\textwidth}
    1.21 +\label{fig:automaton}
    1.22 +\vspace{-22pt}
    1.23 +%\centering
    1.24 +\begin{center}
    1.25  \begin{tikzpicture}[shorten >=0pt, node distance=2cm, auto, semithick, >=stealth
    1.26      %every state/.style={fill, draw=none, gray, text=white},
    1.27      ,accepting/.style={fill, gray!50!black, text=white}
    1.28 @@ -194,19 +201,36 @@
    1.29  %\draw[help lines] (0,0) grid (3,2);
    1.30  \node[state,initial, initial text=] (q_0) {$q_0$};
    1.31  \node[state] (q_1) [above right of= q_0] {$q_1$};
    1.32 -%\node[state] (q_2) [below right of= q_0] {$q_2$};
    1.33  \node[state,accepting](q_2) [below right of= q_1] {$q_2$};
    1.34  \path[->] 
    1.35  (q_0) edge node {$a$} (q_1)
    1.36    edge [loop above] node {$b$} ()
    1.37  (q_1) edge node {$b$} (q_2)
    1.38    edge [loop above] node {$a$} ()
    1.39 -%(q_2) edge node [swap] {$a$} (q_1)
    1.40 -%  edge [loop below] node {$b$} ()
    1.41  (q_2) %edge node {$a$} (q_1)
    1.42    edge node {$b$} (q_0);
    1.43  \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
    1.44  \end{tikzpicture}
    1.45 +\end{center}
    1.46 +\caption{B\"uchi automaton $\A_1$ (\ref{ex:automaton} Example)}
    1.47 +\vspace{-42pt}
    1.48 +%\end{figure}
    1.49 +\end{wrapfigure}
    1.50 +
    1.51 +Let $\A_1 = (\Sigma, S, S_0, \Delta, F)$ be an automaton with:
    1.52 +\begin{itemize}
    1.53 +\item $\Sigma = \{a, b\}$
    1.54 +\item $S = \{q_0, q_1, q_2\}$
    1.55 +\item $S_0 = \{q_0\}$
    1.56 +\item $\Delta = \{(q_0, a, q_0), (q_0, b, q_0),$\\
    1.57 +\hspace*{0.9cm}$(q_1, a, q_1), (q_1, b, q_2),$\\
    1.58 +\hspace*{0.9cm}$(q_2, a, q_1), (q_2, b, q_0)\}$
    1.59 +\item $F = \{q_2\}$
    1.60 +\end{itemize}
    1.61 +%
    1.62 +Figure \ref{fig:automaton} shows $\A_1$, the initial state is marked with an unlabelled incoming arrow and the only accepting state $q_2$ is a filled circle.
    1.63 +
    1.64 +By some further investigation of the automaton, we identify the recognised language $L_\omega(\A_1)$ of the automaton, it is the set of all infinite words with infinitely many occurrences of the sequence $ab$.
    1.65  
    1.66  \subsection{Generalised B\"uchi automata}
    1.67  In the following two sections, we present the modal logic, which is used for the specification of system properties and automata construction on such specifications. To provide a more convenient link between linear temporal logic and B\"uchi automata, we introduce a slightly different formalisation of automata with an extended acceptance condition.