1.1 --- a/slides/src/slides.tex	Wed Jul 20 20:32:05 2011 +0200
     1.2 +++ b/slides/src/slides.tex	Thu Jul 21 00:47:13 2011 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  %\usecolortheme{seagull}
     1.5  
     1.6  \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
     1.7 +\usepackage{pifont}
     1.8  \usepackage{xcolor}
     1.9  \usepackage{ulem}
    1.10  \usepackage{graphicx}
    1.11 @@ -15,6 +16,8 @@
    1.12  
    1.13  \renewcommand{\emph}{\textit}
    1.14  \renewcommand{\em}{\textit}
    1.15 +
    1.16 +\newcommand{\cross}{\ding{55}}
    1.17  \newcommand{\M}{\mathcal{M}}
    1.18  \newcommand{\N}{\mathbb{N}_0}
    1.19  \newcommand{\F}{\mathcal{F}}
    1.20 @@ -45,8 +48,8 @@
    1.21  
    1.22  
    1.23  \newtheorem*{def:vocabulary}{Vocabulary}
    1.24 -\newtheorem*{def:frames}{Frames}
    1.25 -\newtheorem*{def:models}{Models}
    1.26 +\newtheorem*{def:frames}{Frame}
    1.27 +\newtheorem*{def:models}{Model}
    1.28  \newtheorem*{def:satisfiability}{Satisfiability}
    1.29  \newtheorem*{def:fs closure}{Closure}
    1.30  \newtheorem*{def:atoms}{Atoms}
    1.31 @@ -210,7 +213,7 @@
    1.32   \color{black}
    1.33  }
    1.34  \only<3->{ \setcounter{subfigure}{0} 
    1.35 -  \subfigure[\sout{Complement automaton}]
    1.36 +  \subfigure[Complement automaton \cross]
    1.37              {
    1.38                \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
    1.39                    %every state/.style={fill, draw=none, gray, text=white},
    1.40 @@ -236,7 +239,7 @@
    1.41  }
    1.42  %\hspace{10pt}
    1.43  \visible<3->{
    1.44 -  \subfigure[Complement automaton]
    1.45 +  \subfigure[Complement automaton \checkmark]
    1.46              {
    1.47                \label{fig:complement automaton}
    1.48                \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth   
    1.49 @@ -372,7 +375,8 @@
    1.50  ``It is dark.''\\
    1.51  \visible<2->{``It is \emph{always} dark.''\\}
    1.52  \visible<3->{``It is \emph{currently} dark.''\\}
    1.53 -\visible<4->{``It will \emph{eventually} be dark.''}
    1.54 +\visible<4->{``It will \emph{eventually} be dark.''\\}
    1.55 +\visible<5->{``It is dark \emph{until} someone puts the light on.''}
    1.56  \end{center}
    1.57  \end{frame}
    1.58  }
    1.59 @@ -381,7 +385,12 @@
    1.60  \frametitle{Linear Temporal Logic}
    1.61  \framesubtitle{Motivation 2/2}
    1.62  \begin{center}
    1.63 -\colorbox{black}{\color{white} ``It is dark} \colorbox{black!30}{\color{white} until someone puts on the light.''}
    1.64 +\only<1->{
    1.65 +\color{white}
    1.66 +\colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\
    1.67 +\visible<2->{
    1.68 +\colorbox{black}{\makebox(50,10){$d$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$l$}}}
    1.69 +}
    1.70  \end{center}
    1.71  \end{frame}
    1.72  
    1.73 @@ -391,12 +400,33 @@
    1.74  \begin{def:syntax}
    1.75  Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions:
    1.76  \[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
    1.77 +\begin{itemize}
    1.78 +\item $\neg, \lor$ corresponds to the Boolean \emph{negation} and \emph{disjunction}.
    1.79 +\item $\X$ reads \emph{next}.
    1.80 +\item $\U$ reads \emph{until}.
    1.81 +\end{itemize}
    1.82  \end{def:syntax}
    1.83  \end{frame}
    1.84  
    1.85  \begin{frame}
    1.86  \frametitle{Linear Temporal Logic}
    1.87  \framesubtitle{Semantics}
    1.88 +\begin{def:frames}
    1.89 +An LTL-\emph{frame} is a tuple $\F = (S, R)$:
    1.90 +\begin{itemize}
    1.91 +\item $S = \{s_i \mid i \in \N\}$ is the set of states.
    1.92 +\item $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ is the accessibility relation.
    1.93 +\end{itemize} 
    1.94 +\end{def:frames}
    1.95 +
    1.96 +\begin{def:models}
    1.97 +An LTL-\emph{model} is a tuple $\M = (\F, V)$:
    1.98 +\begin{itemize}
    1.99 +\item $\F$ is a \emph{frame}.
   1.100 +\item $V: S \to 2^\Prop$ is a \emph{valuation function}.
   1.101 +\item Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$. 
   1.102 +\end{itemize}
   1.103 +\end{def:models}
   1.104  \end{frame}
   1.105  
   1.106  \begin{frame}