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