# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1311186725 -7200
# Node ID 9cde5c0bf4d3c1ffa5ba93c56fe90fd5d3e57756
# Parent  f00c214f8e3661c3e04b327197a9781e77bfd745
LTL begin.

diff -r f00c214f8e36 -r 9cde5c0bf4d3 slides/src/slides.tex
--- a/slides/src/slides.tex	Wed Jul 20 15:32:09 2011 +0200
+++ b/slides/src/slides.tex	Wed Jul 20 20:32:05 2011 +0200
@@ -6,13 +6,15 @@
 %\usecolortheme{seagull}
 
 \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
-\usepackage{color}
+\usepackage{xcolor}
 \usepackage{ulem}
 \usepackage{graphicx}
 \usepackage{tikz}
 \usetikzlibrary{automata}
 \usepackage{subfigure}
 
+\renewcommand{\emph}{\textit}
+\renewcommand{\em}{\textit}
 \newcommand{\M}{\mathcal{M}}
 \newcommand{\N}{\mathbb{N}_0}
 \newcommand{\F}{\mathcal{F}}
@@ -39,6 +41,9 @@
 \newtheorem*{def:automata language}{Recognised language}
 \newtheorem*{def:general automata}{Generalised automaton}
 \newtheorem*{def:general acceptance}{Acceptance}
+\newtheorem*{def:syntax}{Syntax}
+
+
 \newtheorem*{def:vocabulary}{Vocabulary}
 \newtheorem*{def:frames}{Frames}
 \newtheorem*{def:models}{Models}
@@ -256,6 +261,7 @@
 %\caption{Automata from Example \ref{ex:automaton}}
 \end{figure}
 \end{frame}
+\color{black}  
 
 \begin{frame}
 \frametitle{Automata}
@@ -354,9 +360,43 @@
 \end{prop:general equiv}
 \end{frame}
 
+{
+\setbeamercolor{normal text}{bg=black, fg=white}
+\setbeamercolor{frametitle}{fg=white!30!black}
+\usebeamercolor*{normal text} 
+\usebeamercolor*{frametitle} 
 \begin{frame}
 \frametitle{Linear Temporal Logic}
-\framesubtitle{Motivation}
+\framesubtitle{Motivation 1/2}
+\begin{center}
+``It is dark.''\\
+\visible<2->{``It is \emph{always} dark.''\\}
+\visible<3->{``It is \emph{currently} dark.''\\}
+\visible<4->{``It will \emph{eventually} be dark.''}
+\end{center}
+\end{frame}
+}
+
+\begin{frame}
+\frametitle{Linear Temporal Logic}
+\framesubtitle{Motivation 2/2}
+\begin{center}
+\colorbox{black}{\color{white} ``It is dark} \colorbox{black!30}{\color{white} until someone puts on the light.''}
+\end{center}
+\end{frame}
+
+\begin{frame}
+\frametitle{Linear Temporal Logic}
+\framesubtitle{Syntax}
+\begin{def:syntax}
+Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions:
+\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
+\end{def:syntax}
+\end{frame}
+
+\begin{frame}
+\frametitle{Linear Temporal Logic}
+\framesubtitle{Semantics}
 \end{frame}
 
 \begin{frame}