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