1.1 --- a/slides/src/slides.tex	Thu Jul 21 01:41:30 2011 +0200
     1.2 +++ b/slides/src/slides.tex	Thu Jul 21 14:52:03 2011 +0200
     1.3 @@ -325,41 +325,31 @@
     1.4  \begin{itemize}
     1.5  \item $L_\omega(\A) = \{w \in \Sigma^\omega \mid \A \text{ accepts } w\}$, we say $\A$ recognises language $L_\omega(\A)$.
     1.6  \item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
     1.7 -\item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages.
     1.8  \end{itemize}
     1.9  \end{def:automata language}
    1.10  \end{frame}
    1.11  
    1.12  \begin{frame}
    1.13  \frametitle{Generalised Automata}
    1.14 -\framesubtitle{Definition}
    1.15  \begin{def:general automata}
    1.16 -A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:
    1.17 +A \emph{generalised B\"uchi automaton} is a tuple $\A_G = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:
    1.18  \begin{itemize}
    1.19  \item $\{F_i\}$ is a finite set of sets for a given $k$.
    1.20  \item Each $F_i \subseteq S$ is a finite set of accepting states.
    1.21  \end{itemize}
    1.22  \end{def:general automata}
    1.23 -\end{frame}
    1.24  
    1.25 -\begin{frame}
    1.26 -\frametitle{Generalised Automata}
    1.27 -\framesubtitle{Acceptance}
    1.28  \begin{def:general acceptance}
    1.29 -Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$ be a generalised automaton and let $\rho$ be a run of $\A$:
    1.30 +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$:
    1.31  \begin{itemize}
    1.32  \item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$.
    1.33 -\item $\A$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is accepting. 
    1.34 +\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. 
    1.35  \end{itemize} 
    1.36  \end{def:general acceptance}
    1.37 -\end{frame}
    1.38  
    1.39 -\begin{frame}
    1.40 -\frametitle{Generalised Automata}
    1.41 -\framesubtitle{Language}
    1.42  \begin{prop:general equiv}
    1.43 -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.44 -\[L_\omega(\A) = \bigcap_{i < k} L_\omega(\A_i)\]
    1.45 +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:
    1.46 +\[L_\omega(\A_G) = \bigcap_{i < k} L_\omega(\A_i)\]
    1.47  \end{prop:general equiv}
    1.48  \end{frame}
    1.49  
    1.50 @@ -431,21 +421,6 @@
    1.51  
    1.52  \begin{frame}
    1.53  \frametitle{Linear Temporal Logic}
    1.54 -\framesubtitle{Satisfiability}
    1.55 -\begin{def:satisfiability}
    1.56 -A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
    1.57 -\begin{itemize}
    1.58 -\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
    1.59 -\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
    1.60 -\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
    1.61 -\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
    1.62 -\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$
    1.63 -\end{itemize}
    1.64 -\end{def:satisfiability}
    1.65 -\end{frame}
    1.66 -
    1.67 -\begin{frame}
    1.68 -\frametitle{Linear Temporal Logic}
    1.69  \framesubtitle{Model Example}
    1.70  \begin{figure}
    1.71  \centering
    1.72 @@ -469,6 +444,21 @@
    1.73  \end{frame}
    1.74  
    1.75  \begin{frame}
    1.76 +\frametitle{Linear Temporal Logic}
    1.77 +\framesubtitle{Satisfiability}
    1.78 +\begin{def:satisfiability}
    1.79 +A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
    1.80 +\begin{itemize}
    1.81 +\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
    1.82 +\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
    1.83 +\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
    1.84 +\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
    1.85 +\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$
    1.86 +\end{itemize}
    1.87 +\end{def:satisfiability}
    1.88 +\end{frame}
    1.89 +
    1.90 +\begin{frame}
    1.91  \frametitle{Model Checking}
    1.92  \framesubtitle{A bit more information about this}
    1.93