diff -r 3896639439a3 -r f8c1499ae6d3 slides/src/slides.tex
--- a/slides/src/slides.tex	Thu Jul 21 00:53:49 2011 +0200
+++ b/slides/src/slides.tex	Thu Jul 21 01:41:30 2011 +0200
@@ -430,6 +430,45 @@
 \end{frame}
 
 \begin{frame}
+\frametitle{Linear Temporal Logic}
+\framesubtitle{Satisfiability}
+\begin{def:satisfiability}
+A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
+\begin{itemize}
+\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
+\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
+\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
+\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
+\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$
+\end{itemize}
+\end{def:satisfiability}
+\end{frame}
+
+\begin{frame}
+\frametitle{Linear Temporal Logic}
+\framesubtitle{Model Example}
+\begin{figure}
+\centering
+\begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth   
+    ,accepting/.style={fill, gray!50!black, text=white}]
+\node[state, initial, initial text=] (s_0) {$\{p_0\}$};
+\path (s_0) [late options={label=below:$s_0$}];
+\node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$};
+\path (s_1) [late options={label=below:$s_1$}];
+\node[state] (s_2) [right of= s_1] {$\{p_1\}$};
+\path (s_2) [late options={label=below:$s_2$}];
+\node[state] (s_i) [right of= s_2] {$\{p_1\}$};
+\path (s_i) [late options={label=below:$s_i$}];
+\path[->] 
+(s_0) edge node {$R$} (s_1) 
+(s_1) edge node {$R$} (s_2);
+\path[dashed,->] 
+(s_2) edge node {$R$} (s_i); 
+\end{tikzpicture}
+\end{figure}
+\end{frame}
+
+\begin{frame}
 \frametitle{Model Checking}
 \framesubtitle{A bit more information about this}