1.1 --- a/paper/src/paper.tex	Fri Jul 15 20:07:34 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Fri Jul 15 22:26:36 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  \usetikzlibrary{automata}
     1.5  \usepackage{sidecap}
     1.6  \usepackage{wrapfig}
     1.7 +\usepackage{subfig}
     1.8  %\usepackage{fullpage}
     1.9  %\usepackage{a4wide}
    1.10  \usepackage[left=3.9cm, right=3.9cm]{geometry}
    1.11 @@ -187,18 +188,21 @@
    1.12  
    1.13  \subsection{Example}
    1.14  \label{ex:automaton}
    1.15 -%\begin{figure}[h]
    1.16 -\begin{wrapfigure}{r}{0.5\textwidth}
    1.17 +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\}$, $\Delta = \{(q_0, a, q_0), (q_0, b, q_0), (q_1, a, q_1), (q_1, b, q_2), (q_2, a, q_1), (q_2, b, q_0)\}$ and $F = \{q_2\}$.
    1.18 +
    1.19 +\begin{figure}[h]
    1.20 +\centering
    1.21 +%\begin{wrapfigure}{r}{0.5\textwidth}
    1.22 +\subfloat[Automaton for $L_\omega(\A_1)$]
    1.23 +{
    1.24  \label{fig:automaton}
    1.25 -\vspace{-22pt}
    1.26 -%\centering
    1.27 -\begin{center}
    1.28 -\begin{tikzpicture}[shorten >=0pt, node distance=2cm, auto, semithick, >=stealth
    1.29 +%\vspace{-22pt}
    1.30 +%\begin{center}
    1.31 +\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
    1.32      %every state/.style={fill, draw=none, gray, text=white},
    1.33      ,accepting/.style={fill, gray!50!black, text=white}
    1.34      %initial/.style ={gray, text=white}]%,  thick]
    1.35      ]
    1.36 -%\draw[help lines] (0,0) grid (3,2);
    1.37  \node[state,initial, initial text=] (q_0) {$q_0$};
    1.38  \node[state] (q_1) [above right of= q_0] {$q_1$};
    1.39  \node[state,accepting](q_2) [below right of= q_1] {$q_2$};
    1.40 @@ -211,26 +215,34 @@
    1.41    edge node {$b$} (q_0);
    1.42  \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
    1.43  \end{tikzpicture}
    1.44 -\end{center}
    1.45 -\caption{B\"uchi automaton $\A_1$ (\ref{ex:automaton} Example)}
    1.46 -\vspace{-42pt}
    1.47 -%\end{figure}
    1.48 -\end{wrapfigure}
    1.49 +}
    1.50 +\hspace{2cm}
    1.51 +\subfloat[Automaton for $\overline{L_\omega(\A_1)}$]
    1.52 +{
    1.53 +\label{fig:complement automaton}
    1.54 +\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth   
    1.55 +    ,accepting/.style={fill, gray!50!black, text=white}]
    1.56 +\node[state, initial, initial text=] (q_0) {$q_0$};
    1.57 +\node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
    1.58 +\node[state, accepting](q_2) [below right of= q_1] {$q_2$};
    1.59 +\path[->] 
    1.60 +(q_0) edge node {$a$} (q_1)
    1.61 +  edge node {$b$} (q_2)
    1.62 +  edge [loop above] node {$a, b$} ()
    1.63 +(q_1) edge [loop above] node {$a$} ()
    1.64 +(q_2) 
    1.65 +  edge [loop above] node {$b$} ();
    1.66 +\end{tikzpicture}
    1.67 +}
    1.68 +\caption{Automata from Example \ref{ex:automaton}}
    1.69 +\end{figure}
    1.70 +%\end{wrapfigure}
    1.71 +%
    1.72 +\noindent Figure \ref{fig:automaton} shows $\A_1$; the initial state $q_0$ is marked with an unlabelled incoming arrow and the only accepting state $q_2$ is a filled circle. By some further investigation of the automaton, we identify the recognised language $L = L_\omega(\A_1)$ of the automaton, it is the set of all infinite words with infinitely many occurrences of the sequence $ab$.
    1.73  
    1.74 -Let $\A_1 = (\Sigma, S, S_0, \Delta, F)$ be an automaton with:
    1.75 -\begin{itemize}
    1.76 -\item $\Sigma = \{a, b\}$
    1.77 -\item $S = \{q_0, q_1, q_2\}$
    1.78 -\item $S_0 = \{q_0\}$
    1.79 -\item $\Delta = \{(q_0, a, q_0), (q_0, b, q_0),$\\
    1.80 -\hspace*{0.9cm}$(q_1, a, q_1), (q_1, b, q_2),$\\
    1.81 -\hspace*{0.9cm}$(q_2, a, q_1), (q_2, b, q_0)\}$
    1.82 -\item $F = \{q_2\}$
    1.83 -\end{itemize}
    1.84 -%
    1.85 -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.86 +The complement language $\overline{L} = \overline{L_\omega(\A_1)}$ of $L$ is the set of all infinite words $w$, such that $w \notin L$, i.e., $\overline{L}$ does \emph{not} contain a word with an infinite sequence of $ab$. From the infinity of the input words, it follows that $\overline{L} = A \cup B \setminus A \cap B$, with $A = \{w \in \Sigma^\omega \mid w \text{ has infinitely many } a\}$ and $B = \{w \in \Sigma^\omega \mid w \text{ has infinitely many } b\}$.
    1.87  
    1.88 -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.89 +Figure \ref{fig:complement automaton} shows the automaton for $\overline{L}$. We noticed that, in contrast to $\A_1$, it is non-deterministic. As stated in \cite{ref:ltl&büchi}, when dealing with B\"uchi automata, deterministic and non-deterministic automata are not of equivalent power, like we know it from automata theory on finite inputs. For some non-deterministic automata, we can not construct equivalent deterministic counterparts.
    1.90  
    1.91  \subsection{Generalised B\"uchi automata}
    1.92  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.
    1.93 @@ -273,6 +285,32 @@
    1.94  An LTL-\emph{model} is a tuple $\M = (\F, V)$, where $\F$ is a \emph{frame} and $V: S \to 2^\Prop$ a \emph{valuation function}. Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$. 
    1.95  %A \emph{model} is a function $\M: \N \to 2^\Prop$ over \emph{frame} $\F$. The frame constitutes a linear order over $\N$, which corresponds to the linear progression of time from the \emph{present/past} into the \emph{future}. Therefore $\M(i)$ assigns a set of \emph{positive atomic propositions} to each state of time instant $i$. Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in \M(i)$.
    1.96  \end{def:models}
    1.97 +
    1.98 +\subsubsection{Example}
    1.99 +Figure \ref{fig:model} shows a model over $\Prop = \{p_0, p_1, p_2\}$ with $V = \{(s_0, \{p_0\}), (s_1, \{p_0, p_2\}),$ $(s_2, \{p_1\}), ...\}$, where each time instant $i$ is represented by a circle, the accessibility relations via the arrows and the image of the valuation function as sets within the circles.
   1.100 +
   1.101 +\begin{figure}[h]
   1.102 +\centering
   1.103 +\begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth   
   1.104 +    ,accepting/.style={fill, gray!50!black, text=white}]
   1.105 +\node[state, initial, initial text=] (s_0) {$\{p_0\}$};
   1.106 +\path (s_0) [late options={label=below:$s_0$}];
   1.107 +\node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$};
   1.108 +\path (s_1) [late options={label=below:$s_1$}];
   1.109 +\node[state] (s_2) [right of= s_1] {$\{p_1\}$};
   1.110 +\path (s_2) [late options={label=below:$s_2$}];
   1.111 +\node[state] (s_i) [right of= s_2] {$...$};
   1.112 +\path (s_i) [late options={label=below:$s_i$}];
   1.113 +\path[->] 
   1.114 +(s_0) edge node {$R$} (s_1) 
   1.115 +(s_1) edge node {$R$} (s_2);
   1.116 +\path[dashed,->] 
   1.117 +(s_2) edge node {$R$} (s_i); 
   1.118 +\end{tikzpicture}
   1.119 +\caption{Model example}
   1.120 +\label{fig:model}
   1.121 +\end{figure}
   1.122 +
   1.123  %
   1.124  \begin{def:satisfiability}
   1.125  A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$. Satisfiability of a formula $\varphi$ is defined inductively over the structure of $\varphi$: