Some more definitions.
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}