\documentclass[9pt]{beamer}
\usetheme{Boadilla}
\usecolortheme{dove}
\usecolortheme{orchid}
\usecolortheme{dolphin}
%\usecolortheme{seagull}

\usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
\usepackage{pifont}
\usepackage{xcolor}
\usepackage{ulem}
\usepackage{graphics}
\usepackage{tikz}
\usetikzlibrary{automata}
\usepackage{subfigure}

\renewcommand{\emph}{\textit}
\renewcommand{\em}{\it}

\newcommand{\cross}{\ding{55}}
\newcommand{\M}{\mathcal{M}}
\newcommand{\N}{\mathbb{N}_0}
\newcommand{\F}{\mathcal{F}}
\newcommand{\Fs}{\mathbb{F}}
\newcommand{\Prop}{\mathcal{P}}
\newcommand{\A}{\mathcal{A}}
\newcommand{\X}{\mathcal{X}}
\newcommand{\U}{\mathcal{U}}
\newcommand{\V}{\mathcal{V}}
\newcommand{\dnf}{\mathsf{dnf}}
\newcommand{\consq}{\mathsf{consq}}

\theoremstyle{definition} %plain, definition, remark, proof, corollary
\newtheorem*{def:finite words}{Finite words}
\newtheorem*{def:infinite words}{Infinite words}
\newtheorem*{def:regular languages}{Regular languages}
\newtheorem*{def:regular languages closure}{Regular closure}
\newtheorem*{def:omega regular languages}{$\omega$-regular languages}
\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
\newtheorem*{def:buechi automata}{Automaton}
\newtheorem*{def:automata runs}{Run}
\newtheorem*{def:inf}{Infinite occurrences}
\newtheorem*{def:automata acceptance}{Acceptance}
\newtheorem*{def:automata language}{Recognised language}
\newtheorem*{def:general automata}{Generalised automaton}
\newtheorem*{def:general acceptance}{Acceptance}
\newtheorem*{def:syntax}{Syntax}


\newtheorem*{def:vocabulary}{Vocabulary}
\newtheorem*{def:frames}{Frame}
\newtheorem*{def:models}{Model}
\newtheorem*{def:satisfiability}{Satisfiability}
\newtheorem*{def:fs closure}{Closure}
\newtheorem*{def:atoms}{Atoms}
\newtheorem*{def:rep function}{Representation function}
\newtheorem*{def:next}{Next function}
\newtheorem*{def:dnf}{Disjunctive normal form}
\newtheorem*{def:positive formulae}{Positive formulae}
\newtheorem*{def:consq}{Logical consequences}
\newtheorem*{def:partial automata}{Partial automata}

\theoremstyle{plain}
\newtheorem{prop:vocabulary sat}{Proposition}[section]
\newtheorem{prop:general equiv}{Proposition}[section]
\newtheorem{prop:computation set=language}{Proposition}[section]

\theoremstyle{plain}
\newtheorem{thm:model language}{Theorem}[section]
\newtheorem{cor:mod=model language}{Corollary}[thm:model language]
\newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
\newtheorem{thm:model checking}{Theorem}[section]
\newtheorem{lem:dnf}{Lemma}[section]
\newtheorem{lem:consq}[lem:dnf]{Lemma}

\title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}
\author{Eugen Sawin}
\institute[University of Freiburg]
{ 
  Research Group for Foundations in Artificial Intelligence\\
  Computer Science Department\\
  University of Freiburg
}
\date[SS 2011]{Seminar: Automata Constructions in Model Checking}
\subject{Model Checking}

\begin{document}
\frame{\titlepage}

\begin{frame}
\frametitle{Motivation}
\framesubtitle{Model Checking 1/2}
\begin{center}
%\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}
\[\M \models \varphi\]
\end{center}
\end{frame}

\begin{frame}
\frametitle{Motivation}
\framesubtitle{Model Checking 2/2}
\begin{center}
Given a program $P$ and specification $\varphi$:\\
\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}
\end{center}
\end{frame}

\begin{frame}
\frametitle{Motivation}
\framesubtitle{Industry}
\begin{figure}
\centering
\subfigure{\includegraphics[width=70pt,height=50pt]{images/intel.jpg}}
\subfigure{\includegraphics[width=70pt,height=50pt]{images/airbag.jpg}}
\subfigure{\includegraphics[width=70pt,height=50pt]{images/atc.jpg}}
\end{figure}
\end{frame}

{
\setbeamercolor{normal text}{bg=black, fg=white}
\setbeamercolor{frametitle}{fg=white!30!black}
\usebeamercolor*{normal text} 
\usebeamercolor*{frametitle} 
\begin{frame}
\frametitle{Linear Temporal Logic}
\framesubtitle{Natural language 1/2}
\begin{center}
``It is dark.''\\
\visible<2->{``It is \emph{always} dark.''\\}
\visible<3->{``It is \emph{currently} dark.''\\}
\visible<4->{``It will \emph{necessarily} be dark.''\\}
\visible<5->{``It is dark \emph{until} someone puts the light on.''}
\end{center}
\end{frame}
}

\begin{frame}
\frametitle{Linear Temporal Logic}
\framesubtitle{Natural language 2/2}
\begin{center}
\only<1->{
\color{white}
\colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\
\visible<2->{
\colorbox{black}{\makebox(50,10){$p_0$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$p_1$}}}
}
\end{center}
\end{frame}

\begin{frame}
\frametitle{Linear Temporal Logic}
\framesubtitle{Syntax}
\begin{def:syntax}
Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions:
\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
\begin{itemize}
\item $\neg, \lor$ corresponds to the Boolean \emph{negation} and \emph{disjunction}.
\item $\X$ reads \emph{next}.
\item $\U$ reads \emph{until}.
\end{itemize}
\end{def:syntax}
\end{frame}

\begin{frame}
\frametitle{Linear Temporal Logic}
\framesubtitle{Semantics}
\begin{def:frames}
An LTL-\emph{frame} is a tuple $\F = (S, R)$:
\begin{itemize}
\item $S = \{s_i \mid i \in \N\}$ is the set of states.
\item $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ is the accessibility relation.
\end{itemize} 
\end{def:frames}

\begin{def:models}
An LTL-\emph{model} is a tuple $\M = (\F, V)$:
\begin{itemize}
\item $\F$ is a \emph{frame}.
\item $V: S \to 2^\Prop$ is a \emph{valuation function}.
\item Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$. 
\end{itemize}
\end{def:models}
\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{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{Reactive Systems}
\framesubtitle{Infinite inputs}
\begin{center}
\begin{figure}
\setcounter{subfigure}{0} 
\subfigure[Terminating program]{
\begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth   
    ,accepting/.style={fill, gray!50!black, text=white}]
\node[state, initial, initial text=$input$] (p) {$P$};
\coordinate (b) at (1,0);
        %\coordinate (b) at ($(a)+1/2*(3,3)$);
\draw (p) edge[->] node[right] {$\hspace{8pt}output$} (b);
%\draw[->] (p) -- (b);
\end{tikzpicture}
}
\hspace{10pt}
\visible<2>{\subfigure[Reactive program]{
\begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth   
    ,accepting/.style={fill, gray!50!black, text=white}]
\node[state, initial, initial text=$event$] (p) {$RP$};
\coordinate (b) at (1.1,0);
        %\coordinate (b) at ($(a)+1/2*(3,3)$);
\path[->]
(p) edge [loop right] node {$action$} ();
\end{tikzpicture}
}}
\end{figure}
\end{center}
\end{frame}

\begin{frame}
\frametitle{Automata}
\framesubtitle{Example 1/2}
\begin{figure}
\centering
\only<-3>{
\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
    %every state/.style={fill, draw=none, gray, text=white},
    ,accepting/.style={fill, gray!50!black, text=white}
    %initial/.style ={gray, text=white}]%,  thick]
    ]
\node[state,initial, initial text=] (q_0) {$q_0$};
\node[state] (q_1) [above right of= q_0] {$q_1$};
\node[state,accepting](q_2) [below right of= q_1] {$q_2$};
\path[->] 
(q_0) edge node {$a$} (q_1)
  edge [loop above] node {$b$} ()
(q_1) edge node {$b$} (q_2)
  edge [loop above] node {$a$} ()
(q_2) %edge node {$a$} (q_1)
  edge node {$b$} (q_0);
\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
\end{tikzpicture}\\
\vspace{10pt}
\visible<2-3>{$w_1 = \overline{bbaa} \implies \rho_1 = q_0q_0\overline{q_0q_1q_1q_2}$}\\
\visible<3>{$w_2 = bb\overline{ab} \implies \rho_2 = q_0q_0\overline{q_1q_2}$}\\
\vspace{10pt}
\visible<4>{Accepts all inputs with infinite occurrences of $ab$.}
}

\only<4>{
\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
    %every state/.style={fill, draw=none, gray, text=white},
    ,accepting/.style={fill, gray!50!black, text=white}
    %initial/.style ={gray, text=white}]%,  thick]
    ]
\node[state,initial, initial text=] (q_0) {$q_0$};
\node[state] (q_1) [above right of= q_0] {$q_1$};
\node[state,accepting](q_2) [below right of= q_1] {$q_2$};
\path[->] 
(q_0) 
  edge [loop above] node {$b$} ()
(q_1) 
  edge [loop above] node {$a$} ()
(q_2) %edge node {$a$} (q_1)
  edge node {$b$} (q_0);
\color{green}
\path[->] 
(q_0) edge node {$a$} (q_1) 
(q_1) edge node {$b$} (q_2);
\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
\end{tikzpicture}\\
\color{black}
\vspace{10pt}
\visible<2->{$w_1 = \overline{\textcolor{green}{b}ba\textcolor{green}{a}} \implies \rho_1 = q_0q_0\overline{q_0q_1q_1\textcolor{green}{q_2}}$}\\
\visible<3->{$w_2 = bb\overline{\textcolor{green}{ab}} \implies \rho_2 = q_0q_0\overline{q_1\textcolor{green}{q_2}}$}\\
\vspace{10pt}
\visible<4>{Accepts all inputs with infinite occurrences of $ab$.}
}
%Automaton $\A_1$
\end{figure}
\end{frame}

\begin{frame}
\frametitle{Automata}
\framesubtitle{Example 2/2 (Complement)}
\begin{figure}
\centering
\only<1>{
  \subfigure
            {
              \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
                  %every state/.style={fill, draw=none, gray, text=white},
                  ,accepting/.style={fill, gray!50!black, text=white}
                  %initial/.style ={gray, text=white}]%,  thick]
                ]
                \node[state,initial, initial text=, accepting] (q_0) {$q_0$};
                \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
                \node[state](q_2) [below right of= q_1] {$q_2$};
                \path[->] 
                (q_0) edge node {$a$} (q_1)
                edge [loop above] node {$b$} ()
                (q_1) edge node {$b$} (q_2)
                edge [loop above] node {$a$} ()
                (q_2) %edge node {$a$} (q_1)
                edge node {$b$} (q_0);
                \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
              \end{tikzpicture}
            }
}
\only<2>{ 
  \subfigure
            {
              \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
                  %every state/.style={fill, draw=none, gray, text=white},
                  ,accepting/.style={fill, gray!50!black, text=white}
                  %initial/.style ={gray, text=white}]%,  thick]
                ]
                \node[state,initial, initial text=, accepting] (q_0) {$q_0$};
                \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
                \node[state](q_2) [below right of= q_1] {$q_2$};
                \path[->] 
                (q_0) 
                edge [loop above] node {$b$} ()
                (q_1) 
                edge [loop above] node {$a$} ();                
                \color{red}  
                \path[->] 
                (q_0) edge node {$a$} (q_1)
                (q_1) edge node {$b$} (q_2)
                (q_2) edge node {$b$} (q_0);  
                \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);              
              \end{tikzpicture}  \color{red}  
            }
 \color{black}
}
\only<3->{ \setcounter{subfigure}{0} 
  \subfigure[Complement automaton \cross]
            {
              \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
                  %every state/.style={fill, draw=none, gray, text=white},
                  ,accepting/.style={fill, gray!50!black, text=white}
                  %initial/.style ={gray, text=white}]%,  thick]
                ]
                \node[state,initial, initial text=, accepting] (q_0) {$q_0$};
                \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
                \node[state](q_2) [below right of= q_1] {$q_2$};
                \path[->] 
                (q_0) 
                edge [loop above] node {$b$} ()
                (q_1) 
                edge [loop above] node {$a$} ();                
                \path[->] 
                (q_0) edge node {$a$} (q_1)
                (q_1) edge node {$b$} (q_2)
                (q_2) edge node {$b$} (q_0);  
                \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);              
              \end{tikzpicture}  \color{red}  
            }
 \color{black}
}
%\hspace{10pt}
\visible<3->{
  \subfigure[Complement automaton \checkmark]
            {
              \label{fig:complement automaton}
              \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth   
                  ,accepting/.style={fill, gray!50!black, text=white}]
                \node[state, initial, initial text=] (q_0) {$q_0$};
                \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
                \node[state, accepting](q_2) [below right of= q_1] {$q_2$};
                \path[->] 
                (q_0) edge node {$a$} (q_1)
                edge node {$b$} (q_2)
                edge [loop above] node {$a, b$} ()
                (q_1) edge [loop above] node {$a$} ()
                (q_2) 
                edge [loop above] node {$b$} ();
              \end{tikzpicture}\color{green}  
            }\\
\color{black}  
\vspace{20pt}
Accepts all inputs with finite many $ab$.
}
%\caption{Automata from Example \ref{ex:automaton}}
\end{figure}
\end{frame}
\color{black}  

\begin{frame}
\frametitle{Automata}
\framesubtitle{Definition}
\begin{def:buechi automata}
A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:
\begin{itemize}
\item $\Sigma$ is a finite \emph{alphabet}.
\item $S$ is a finite set of \emph{states}.
\item $S_0 \subseteq S$ is the set of \emph{initial states}.
\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}.
\item $F \subseteq S$ is the set of \emph{accepting states}.
\end{itemize}
\end{def:buechi automata}
\end{frame}

\begin{frame}
\frametitle{Automata}
\framesubtitle{Runs}
\begin{def:automata runs}
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
\begin{itemize}
\item A run $\rho$ of $\A$ on an infinite word $w = a_0,a_1,...$ is a sequence $\rho = s_0,s_1,...$:
\begin{itemize}
\item $s_0 \in S_0$.
\item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$.
\end{itemize}
\item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$.
\end{itemize}
\end{def:automata runs}
\visible<2->{\[w_1 = \overline{\textcolor{green}{b}ba\textcolor{green}{a}} \implies \rho_1 = q_0q_0\overline{q_0q_1q_1\textcolor{green}{q_2}}\]
\[w_2 = bb\overline{\textcolor{green}{ab}} \implies \rho_2 = q_0q_0\overline{q_1\textcolor{green}{q_2}}\]}
\end{frame}

\begin{frame}
\frametitle{Automata}
\framesubtitle{Acceptance}
\begin{def:inf}
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
\begin{itemize}
\item $\exists^\omega$ denotes the existential quantifier for \emph{infinitely} many occurrences.
\item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$.
\end{itemize}
\end{def:inf}

\begin{def:automata acceptance}
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
\begin{itemize}
\item $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$.
\item $\A$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is accepting. 
\end{itemize}
\end{def:automata acceptance}
\end{frame}

\begin{frame}
\frametitle{Automata}
\framesubtitle{Language}
\begin{def:automata language}
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
\begin{itemize}
\item $L_\omega(\A) = \{w \in \Sigma^\omega \mid \A \text{ accepts } w\}$, we say $\A$ recognises language $L_\omega(\A)$.
\item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
\end{itemize}
\end{def:automata language}
\end{frame}

\begin{frame}
\frametitle{Generalised Automata}
\begin{def:general automata}
A \emph{generalised B\"uchi automaton} is a tuple $\A_G = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:
\begin{itemize}
\item $\{F_i\}$ is a finite set of sets for a given $k$.
\item Each $F_i \subseteq S$ is a finite set of accepting states.
\end{itemize}
\end{def:general automata}

\begin{def:general acceptance}
Let $\A_G = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$ be a generalised automaton and let $\rho$ be a run of $\A_G$:
\begin{itemize}
\item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$.
\item $\A_G$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A_G$ on $w$, such that $\rho$ is accepting. 
\end{itemize} 
\end{def:general acceptance}

\begin{prop:general equiv}
Let $\A_G = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ be a generalised automaton and let $\A_i = (\Sigma, S, S_0, \Delta, F_i)$ be non-deterministic automata:
\[L_\omega(\A_G) = \bigcap_{i < k} L_\omega(\A_i)\]
\end{prop:general equiv}
\end{frame}

\begin{frame}
\frametitle{Automata Construction}
\framesubtitle{Formula automata}
\begin{center}
Model $\M_\varphi$ for formula $\varphi$\\
$\Downarrow$\\
Closure $CL(\varphi)$ of $\varphi$\\
$\Downarrow$\\
Automaton $\A_\varphi$ for $\varphi$\\
\vspace{20pt}
\textcolor{red}{On-the-fly methods} \`a la Gerth et al.
\end{center}
\end{frame}

\begin{frame}
\frametitle{Automata Construction}
\framesubtitle{System automata}
\begin{center}
Model $\M_\varphi$ for formula $\varphi$\\
$\Downarrow$\\
Closure $CL(\varphi)$ of $\varphi$\\
$\Downarrow$\\
Automaton $\A_\varphi$ for $\varphi$
\end{center}
\end{frame}

\begin{frame}
\frametitle{Model Checking}
\framesubtitle{Definition}
\begin{thm:model checking}
\label{thm:model checking}
Let $\A_P$ be the automaton for program $P$ and let $\A_\varphi$ be the automaton for formula $\varphi$.\\
P satisfies $\varphi$ iff:
\begin{itemize}
\item $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$.
\item $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.
\end{itemize}
\end{thm:model checking}
\end{frame}

\begin{frame}[allowframebreaks]
\frametitle<presentation>{Literature}    
\begin{thebibliography}{10}    

\beamertemplatearticlebibitems
\bibitem{ref:ltl&büchi}
Madhavan Mukund.
\newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
\newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
  
\beamertemplatearticlebibitems
\bibitem{ref:alternating verification}
Moshe Y. Vardi.
\newblock {\em Alternating Automata and Program Verification}.
\newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.

\beamertemplatebookbibitems
\bibitem{ref:handbook}
Patrick Blackburn and Frank Wolter and Johan van Benthem.
\newblock {\em Handbook of Modal Logic}.
\newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.

\end{thebibliography}
\end{frame}

\end{document}
