LTL begin.
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}