1.1 --- a/slides/src/slides.tex	Wed Jul 20 15:32:09 2011 +0200
     1.2 +++ b/slides/src/slides.tex	Wed Jul 20 20:32:05 2011 +0200
     1.3 @@ -6,13 +6,15 @@
     1.4  %\usecolortheme{seagull}
     1.5  
     1.6  \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
     1.7 -\usepackage{color}
     1.8 +\usepackage{xcolor}
     1.9  \usepackage{ulem}
    1.10  \usepackage{graphicx}
    1.11  \usepackage{tikz}
    1.12  \usetikzlibrary{automata}
    1.13  \usepackage{subfigure}
    1.14  
    1.15 +\renewcommand{\emph}{\textit}
    1.16 +\renewcommand{\em}{\textit}
    1.17  \newcommand{\M}{\mathcal{M}}
    1.18  \newcommand{\N}{\mathbb{N}_0}
    1.19  \newcommand{\F}{\mathcal{F}}
    1.20 @@ -39,6 +41,9 @@
    1.21  \newtheorem*{def:automata language}{Recognised language}
    1.22  \newtheorem*{def:general automata}{Generalised automaton}
    1.23  \newtheorem*{def:general acceptance}{Acceptance}
    1.24 +\newtheorem*{def:syntax}{Syntax}
    1.25 +
    1.26 +
    1.27  \newtheorem*{def:vocabulary}{Vocabulary}
    1.28  \newtheorem*{def:frames}{Frames}
    1.29  \newtheorem*{def:models}{Models}
    1.30 @@ -256,6 +261,7 @@
    1.31  %\caption{Automata from Example \ref{ex:automaton}}
    1.32  \end{figure}
    1.33  \end{frame}
    1.34 +\color{black}  
    1.35  
    1.36  \begin{frame}
    1.37  \frametitle{Automata}
    1.38 @@ -354,9 +360,43 @@
    1.39  \end{prop:general equiv}
    1.40  \end{frame}
    1.41  
    1.42 +{
    1.43 +\setbeamercolor{normal text}{bg=black, fg=white}
    1.44 +\setbeamercolor{frametitle}{fg=white!30!black}
    1.45 +\usebeamercolor*{normal text} 
    1.46 +\usebeamercolor*{frametitle} 
    1.47  \begin{frame}
    1.48  \frametitle{Linear Temporal Logic}
    1.49 -\framesubtitle{Motivation}
    1.50 +\framesubtitle{Motivation 1/2}
    1.51 +\begin{center}
    1.52 +``It is dark.''\\
    1.53 +\visible<2->{``It is \emph{always} dark.''\\}
    1.54 +\visible<3->{``It is \emph{currently} dark.''\\}
    1.55 +\visible<4->{``It will \emph{eventually} be dark.''}
    1.56 +\end{center}
    1.57 +\end{frame}
    1.58 +}
    1.59 +
    1.60 +\begin{frame}
    1.61 +\frametitle{Linear Temporal Logic}
    1.62 +\framesubtitle{Motivation 2/2}
    1.63 +\begin{center}
    1.64 +\colorbox{black}{\color{white} ``It is dark} \colorbox{black!30}{\color{white} until someone puts on the light.''}
    1.65 +\end{center}
    1.66 +\end{frame}
    1.67 +
    1.68 +\begin{frame}
    1.69 +\frametitle{Linear Temporal Logic}
    1.70 +\framesubtitle{Syntax}
    1.71 +\begin{def:syntax}
    1.72 +Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions:
    1.73 +\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
    1.74 +\end{def:syntax}
    1.75 +\end{frame}
    1.76 +
    1.77 +\begin{frame}
    1.78 +\frametitle{Linear Temporal Logic}
    1.79 +\framesubtitle{Semantics}
    1.80  \end{frame}
    1.81  
    1.82  \begin{frame}