1.1 --- a/slides/src/slides.tex	Thu Jul 21 00:53:49 2011 +0200
     1.2 +++ b/slides/src/slides.tex	Thu Jul 21 01:41:30 2011 +0200
     1.3 @@ -430,6 +430,45 @@
     1.4  \end{frame}
     1.5  
     1.6  \begin{frame}
     1.7 +\frametitle{Linear Temporal Logic}
     1.8 +\framesubtitle{Satisfiability}
     1.9 +\begin{def:satisfiability}
    1.10 +A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
    1.11 +\begin{itemize}
    1.12 +\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
    1.13 +\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
    1.14 +\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
    1.15 +\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
    1.16 +\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.17 +\end{itemize}
    1.18 +\end{def:satisfiability}
    1.19 +\end{frame}
    1.20 +
    1.21 +\begin{frame}
    1.22 +\frametitle{Linear Temporal Logic}
    1.23 +\framesubtitle{Model Example}
    1.24 +\begin{figure}
    1.25 +\centering
    1.26 +\begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth   
    1.27 +    ,accepting/.style={fill, gray!50!black, text=white}]
    1.28 +\node[state, initial, initial text=] (s_0) {$\{p_0\}$};
    1.29 +\path (s_0) [late options={label=below:$s_0$}];
    1.30 +\node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$};
    1.31 +\path (s_1) [late options={label=below:$s_1$}];
    1.32 +\node[state] (s_2) [right of= s_1] {$\{p_1\}$};
    1.33 +\path (s_2) [late options={label=below:$s_2$}];
    1.34 +\node[state] (s_i) [right of= s_2] {$\{p_1\}$};
    1.35 +\path (s_i) [late options={label=below:$s_i$}];
    1.36 +\path[->] 
    1.37 +(s_0) edge node {$R$} (s_1) 
    1.38 +(s_1) edge node {$R$} (s_2);
    1.39 +\path[dashed,->] 
    1.40 +(s_2) edge node {$R$} (s_i); 
    1.41 +\end{tikzpicture}
    1.42 +\end{figure}
    1.43 +\end{frame}
    1.44 +
    1.45 +\begin{frame}
    1.46  \frametitle{Model Checking}
    1.47  \framesubtitle{A bit more information about this}
    1.48