1.1 --- a/slides/src/slides.tex	Tue Jul 19 02:33:21 2011 +0200
     1.2 +++ b/slides/src/slides.tex	Tue Jul 19 15:23:57 2011 +0200
     1.3 @@ -21,8 +21,10 @@
     1.4  \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
     1.5  \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
     1.6  \newtheorem*{def:buechi automata}{Automaton}
     1.7 -\newtheorem*{def:automata runs}{Runs}
     1.8 +\newtheorem*{def:automata runs}{Run}
     1.9 +\newtheorem*{def:inf}{Infinite occurrences}
    1.10  \newtheorem*{def:automata acceptance}{Acceptance}
    1.11 +\newtheorem*{def:automata language}{Recognised language}
    1.12  \newtheorem*{def:general automata}{Generalised automata}
    1.13  \newtheorem*{def:general acceptance}{Acceptance}
    1.14  \newtheorem*{def:vocabulary}{Vocabulary}
    1.15 @@ -72,15 +74,13 @@
    1.16  \begin{frame}
    1.17  \frametitle{Infinity}
    1.18  \framesubtitle{A bit more information about this}
    1.19 -
    1.20  \end{frame}
    1.21  
    1.22  \begin{frame}
    1.23 -\frametitle{B\"uchi Automata}
    1.24 -\framesubtitle{A bit more information about this}
    1.25 -
    1.26 +\frametitle{Automata}
    1.27 +\framesubtitle{Definition}
    1.28  \begin{def:buechi automata}
    1.29 -A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$, with:
    1.30 +A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:
    1.31  \begin{itemize}
    1.32  \item $\Sigma$ is a finite non-empty \emph{alphabet}
    1.33  \item $S$ is a finite non-empty set of \emph{states}
    1.34 @@ -92,6 +92,55 @@
    1.35  \end{frame}
    1.36  
    1.37  \begin{frame}
    1.38 +\frametitle{Automata}
    1.39 +\framesubtitle{Runs}
    1.40 +\begin{def:automata runs}
    1.41 +Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
    1.42 +\begin{itemize}
    1.43 +\item A run $\rho$ of $\A$ on an infinite word $w = a_0,a_1,...$ is a sequence $\rho = s_0,s_1,...$:
    1.44 +\begin{itemize}
    1.45 +\item $s_0 \in S_0$
    1.46 +\item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$
    1.47 +\end{itemize}
    1.48 +\item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$
    1.49 +\end{itemize}
    1.50 +\end{def:automata runs}
    1.51 +\end{frame}
    1.52 +
    1.53 +\begin{frame}
    1.54 +\frametitle{Automata}
    1.55 +\framesubtitle{Acceptance}
    1.56 +\begin{def:inf}
    1.57 +Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
    1.58 +\begin{itemize}
    1.59 +\item $\exists^\omega$ denotes the existential quantifier for infinitely many occurrences.
    1.60 +\item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$
    1.61 +\end{itemize}
    1.62 +\end{def:inf}
    1.63 +
    1.64 +\begin{def:automata acceptance}
    1.65 +Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
    1.66 +\begin{itemize}
    1.67 +\item $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$.
    1.68 +\item $\A$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is \emph{accepting}. 
    1.69 +\end{itemize}
    1.70 +\end{def:automata acceptance}
    1.71 +\end{frame}
    1.72 +
    1.73 +\begin{frame}
    1.74 +\frametitle{Automata}
    1.75 +\framesubtitle{Language}
    1.76 +\begin{def:automata language}
    1.77 +Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
    1.78 +\begin{itemize}
    1.79 +\item Language $L_\omega(\A)$ \emph{recognised} by $\A$ is the set of all infinite words \emph{accepted} by $\A$
    1.80 +\item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$
    1.81 +\item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages
    1.82 +\end{itemize}
    1.83 +\end{def:automata language}
    1.84 +\end{frame}
    1.85 +
    1.86 +\begin{frame}
    1.87  \frametitle{Linear Temporal Logic}
    1.88  \framesubtitle{A bit more information about this}
    1.89