1.1 --- a/slides/src/slides.tex	Tue Jul 19 15:23:57 2011 +0200
     1.2 +++ b/slides/src/slides.tex	Tue Jul 19 21:29:46 2011 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  \newcommand{\M}{\mathcal{M}}
     1.5  \newcommand{\N}{\mathbb{N}_0}
     1.6  \newcommand{\F}{\mathcal{F}}
     1.7 +\newcommand{\Fs}{\mathbb{F}}
     1.8  \newcommand{\Prop}{\mathcal{P}}
     1.9  \newcommand{\A}{\mathcal{A}}
    1.10  \newcommand{\X}{\mathcal{X}}
    1.11 @@ -25,7 +26,7 @@
    1.12  \newtheorem*{def:inf}{Infinite occurrences}
    1.13  \newtheorem*{def:automata acceptance}{Acceptance}
    1.14  \newtheorem*{def:automata language}{Recognised language}
    1.15 -\newtheorem*{def:general automata}{Generalised automata}
    1.16 +\newtheorem*{def:general automata}{Generalised automaton}
    1.17  \newtheorem*{def:general acceptance}{Acceptance}
    1.18  \newtheorem*{def:vocabulary}{Vocabulary}
    1.19  \newtheorem*{def:frames}{Frames}
    1.20 @@ -82,11 +83,11 @@
    1.21  \begin{def:buechi automata}
    1.22  A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:
    1.23  \begin{itemize}
    1.24 -\item $\Sigma$ is a finite non-empty \emph{alphabet}
    1.25 -\item $S$ is a finite non-empty set of \emph{states}
    1.26 -\item $S_0 \subseteq S$ is the set of \emph{initial states}
    1.27 -\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}
    1.28 -\item $F \subseteq S$ is the set of \emph{accepting states} 
    1.29 +\item $\Sigma$ is a finite \emph{alphabet}.
    1.30 +\item $S$ is a finite set of \emph{states}.
    1.31 +\item $S_0 \subseteq S$ is the set of \emph{initial states}.
    1.32 +\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}.
    1.33 +\item $F \subseteq S$ is the set of \emph{accepting states}.
    1.34  \end{itemize}
    1.35  \end{def:buechi automata}
    1.36  \end{frame}
    1.37 @@ -99,10 +100,10 @@
    1.38  \begin{itemize}
    1.39  \item A run $\rho$ of $\A$ on an infinite word $w = a_0,a_1,...$ is a sequence $\rho = s_0,s_1,...$:
    1.40  \begin{itemize}
    1.41 -\item $s_0 \in S_0$
    1.42 -\item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$
    1.43 +\item $s_0 \in S_0$.
    1.44 +\item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$.
    1.45  \end{itemize}
    1.46 -\item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$
    1.47 +\item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$.
    1.48  \end{itemize}
    1.49  \end{def:automata runs}
    1.50  \end{frame}
    1.51 @@ -114,7 +115,7 @@
    1.52  Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
    1.53  \begin{itemize}
    1.54  \item $\exists^\omega$ denotes the existential quantifier for infinitely many occurrences.
    1.55 -\item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$
    1.56 +\item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$.
    1.57  \end{itemize}
    1.58  \end{def:inf}
    1.59  
    1.60 @@ -133,17 +134,49 @@
    1.61  \begin{def:automata language}
    1.62  Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
    1.63  \begin{itemize}
    1.64 -\item Language $L_\omega(\A)$ \emph{recognised} by $\A$ is the set of all infinite words \emph{accepted} by $\A$
    1.65 -\item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$
    1.66 -\item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages
    1.67 +\item $L_\omega(\A) = \{w \in \Sigma^\omega \mid \A \text{ accepts } w\}$, we say $\A$ recognises language $L_\omega(\A)$.
    1.68 +\item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
    1.69 +\item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages.
    1.70  \end{itemize}
    1.71  \end{def:automata language}
    1.72  \end{frame}
    1.73  
    1.74  \begin{frame}
    1.75 +\frametitle{Generalised Automata}
    1.76 +\framesubtitle{Definition}
    1.77 +\begin{def:general automata}
    1.78 +A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:
    1.79 +\begin{itemize}
    1.80 +\item $\{F_i\}$ is a finite set of sets for a given $k$.
    1.81 +\item Each $F_i \subseteq S$ is a finite set of accepting states.
    1.82 +\end{itemize}
    1.83 +\end{def:general automata}
    1.84 +\end{frame}
    1.85 +
    1.86 +\begin{frame}
    1.87 +\frametitle{Generalised Automata}
    1.88 +\framesubtitle{Acceptance}
    1.89 +\begin{def:general acceptance}
    1.90 +Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$ be a generalised automaton and let $\rho$ be a run of $\A$:
    1.91 +\begin{itemize}
    1.92 +\item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$.
    1.93 +\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.94 +\end{itemize} 
    1.95 +\end{def:general acceptance}
    1.96 +\end{frame}
    1.97 +
    1.98 +\begin{frame}
    1.99 +\frametitle{Generalised Automata}
   1.100 +\framesubtitle{Language}
   1.101 +\begin{prop:general equiv}
   1.102 +Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ be a generalised automaton and let $\A_i = (\Sigma, S, S_0, \Delta, F_i)$ be non-deterministic automata, then following equivalence condition holds:
   1.103 +\[L_\omega(\A) = \bigcap_{i < k} L_\omega(\A_i)\]
   1.104 +\end{prop:general equiv}
   1.105 +\end{frame}
   1.106 +
   1.107 +\begin{frame}
   1.108  \frametitle{Linear Temporal Logic}
   1.109  \framesubtitle{A bit more information about this}
   1.110 -
   1.111  \end{frame}
   1.112  
   1.113  \begin{frame}