# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1311252723 -7200
# Node ID befbd30f5d219fef05df1c73db876ecc453c9dcd
# Parent  f8c1499ae6d3f10e9d1553fc85324d98a437793b
Some rearrangements.

diff -r f8c1499ae6d3 -r befbd30f5d21 slides/src/slides.tex
--- a/slides/src/slides.tex	Thu Jul 21 01:41:30 2011 +0200
+++ b/slides/src/slides.tex	Thu Jul 21 14:52:03 2011 +0200
@@ -325,41 +325,31 @@
 \begin{itemize}
 \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})$:
+A \emph{generalised B\"uchi automaton} is a tuple $\A_G = (\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$:
+Let $\A_G = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$ be a generalised automaton and let $\rho$ be a run of $\A_G$:
 \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 accepting. 
+\item $\A_G$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A_G$ on $w$, such that $\rho$ is 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)\]
+Let $\A_G = (\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:
+\[L_\omega(\A_G) = \bigcap_{i < k} L_\omega(\A_i)\]
 \end{prop:general equiv}
 \end{frame}
 
@@ -431,21 +421,6 @@
 
 \begin{frame}
 \frametitle{Linear Temporal Logic}
-\framesubtitle{Satisfiability}
-\begin{def:satisfiability}
-A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
-\begin{itemize}
-\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
-\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
-\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
-\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
-\item $\M,i \models \varphi \U \psi \iff \exists{k \geq i}: \M,k \models \psi$ and $\forall{i \leq j < k}: \M,j \models\varphi$
-\end{itemize}
-\end{def:satisfiability}
-\end{frame}
-
-\begin{frame}
-\frametitle{Linear Temporal Logic}
 \framesubtitle{Model Example}
 \begin{figure}
 \centering
@@ -469,6 +444,21 @@
 \end{frame}
 
 \begin{frame}
+\frametitle{Linear Temporal Logic}
+\framesubtitle{Satisfiability}
+\begin{def:satisfiability}
+A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
+\begin{itemize}
+\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
+\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
+\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
+\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
+\item $\M,i \models \varphi \U \psi \iff \exists{k \geq i}: \M,k \models \psi$ and $\forall{i \leq j < k}: \M,j \models\varphi$
+\end{itemize}
+\end{def:satisfiability}
+\end{frame}
+
+\begin{frame}
 \frametitle{Model Checking}
 \framesubtitle{A bit more information about this}