# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1311103786 -7200
# Node ID c8b38fab3d489f8567fb43742a3caaa0303461c8
# Parent  7190dae7df066a7fe0f61ed108ff9f435b6cd9b0
Some more definitions.

diff -r 7190dae7df06 -r c8b38fab3d48 slides/src/slides.tex
--- a/slides/src/slides.tex	Tue Jul 19 15:23:57 2011 +0200
+++ b/slides/src/slides.tex	Tue Jul 19 21:29:46 2011 +0200
@@ -5,6 +5,7 @@
 \newcommand{\M}{\mathcal{M}}
 \newcommand{\N}{\mathbb{N}_0}
 \newcommand{\F}{\mathcal{F}}
+\newcommand{\Fs}{\mathbb{F}}
 \newcommand{\Prop}{\mathcal{P}}
 \newcommand{\A}{\mathcal{A}}
 \newcommand{\X}{\mathcal{X}}
@@ -25,7 +26,7 @@
 \newtheorem*{def:inf}{Infinite occurrences}
 \newtheorem*{def:automata acceptance}{Acceptance}
 \newtheorem*{def:automata language}{Recognised language}
-\newtheorem*{def:general automata}{Generalised automata}
+\newtheorem*{def:general automata}{Generalised automaton}
 \newtheorem*{def:general acceptance}{Acceptance}
 \newtheorem*{def:vocabulary}{Vocabulary}
 \newtheorem*{def:frames}{Frames}
@@ -82,11 +83,11 @@
 \begin{def:buechi automata}
 A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:
 \begin{itemize}
-\item $\Sigma$ is a finite non-empty \emph{alphabet}
-\item $S$ is a finite non-empty set of \emph{states}
-\item $S_0 \subseteq S$ is the set of \emph{initial states}
-\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}
-\item $F \subseteq S$ is the set of \emph{accepting states} 
+\item $\Sigma$ is a finite \emph{alphabet}.
+\item $S$ is a finite set of \emph{states}.
+\item $S_0 \subseteq S$ is the set of \emph{initial states}.
+\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}.
+\item $F \subseteq S$ is the set of \emph{accepting states}.
 \end{itemize}
 \end{def:buechi automata}
 \end{frame}
@@ -99,10 +100,10 @@
 \begin{itemize}
 \item A run $\rho$ of $\A$ on an infinite word $w = a_0,a_1,...$ is a sequence $\rho = s_0,s_1,...$:
 \begin{itemize}
-\item $s_0 \in S_0$
-\item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$
+\item $s_0 \in S_0$.
+\item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$.
 \end{itemize}
-\item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$
+\item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$.
 \end{itemize}
 \end{def:automata runs}
 \end{frame}
@@ -114,7 +115,7 @@
 Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
 \begin{itemize}
 \item $\exists^\omega$ denotes the existential quantifier for infinitely many occurrences.
-\item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$
+\item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$.
 \end{itemize}
 \end{def:inf}
 
@@ -133,17 +134,49 @@
 \begin{def:automata language}
 Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
 \begin{itemize}
-\item Language $L_\omega(\A)$ \emph{recognised} by $\A$ is the set of all infinite words \emph{accepted} by $\A$
-\item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$
-\item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages
+\item $L_\omega(\A) = \{w \in \Sigma^\omega \mid \A \text{ accepts } w\}$, we say $\A$ recognises language $L_\omega(\A)$.
+\item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
+\item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages.
 \end{itemize}
 \end{def:automata language}
 \end{frame}
 
 \begin{frame}
+\frametitle{Generalised Automata}
+\framesubtitle{Definition}
+\begin{def:general automata}
+A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:
+\begin{itemize}
+\item $\{F_i\}$ is a finite set of sets for a given $k$.
+\item Each $F_i \subseteq S$ is a finite set of accepting states.
+\end{itemize}
+\end{def:general automata}
+\end{frame}
+
+\begin{frame}
+\frametitle{Generalised Automata}
+\framesubtitle{Acceptance}
+\begin{def:general acceptance}
+Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$ be a generalised automaton and let $\rho$ be a run of $\A$:
+\begin{itemize}
+\item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$.
+\item $\A$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is \emph{accepting}. 
+\end{itemize} 
+\end{def:general acceptance}
+\end{frame}
+
+\begin{frame}
+\frametitle{Generalised Automata}
+\framesubtitle{Language}
+\begin{prop:general equiv}
+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:
+\[L_\omega(\A) = \bigcap_{i < k} L_\omega(\A_i)\]
+\end{prop:general equiv}
+\end{frame}
+
+\begin{frame}
 \frametitle{Linear Temporal Logic}
 \framesubtitle{A bit more information about this}
-
 \end{frame}
 
 \begin{frame}