\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}

 \begin{center}

 %\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}

 \only<1>{\[\M \models \varphi\]}

 \only<2->{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}

 \begin{figure}

 \centering

 \subfigure{\includegraphics[width=100pt,height=70pt]{images/intel.jpg}}

 \subfigure{\includegraphics[width=100pt,height=70pt]{images/airbag.jpg}}

 \subfigure{\includegraphics[width=100pt,height=70pt]{images/atc.jpg}}

 \end{figure}

 \end{frame}

 \begin{frame}

 \frametitle{Infinity}

 \framesubtitle{Word as function}

 \begin{figure}

 \centering

 \begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth   

     ,accepting/.style={fill, gray!50!black, text=white}]

 \node[state, initial, initial text=] (s_0) {$a$};

 \node[state] (s_1) [right of= s_0] {$b$};

 \node[state] (s_2) [right of= s_1] {$a$};

 \node[state] (s_i) [right of= s_2] {$a$};

 \path[->] 

 (s_0) edge node {} (s_1) 

 (s_1) edge node {} (s_2);

 \path[dashed,->] 

 (s_2) edge node {} (s_i); 

 \end{tikzpicture}

 \end{figure}

 \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}

 {

 \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{Motivation 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{eventually} 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{Motivation 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{Model Checking}

 \framesubtitle{Definition 1/2}

 \begin{center}

 %\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}

 \only<1>{\[\M \models \varphi\]}

 \only<2->{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{Model Checking}

 \framesubtitle{Definition 2/2}

 \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}

 \frametitle{On-the-fly Methods}

 \framesubtitle{A bit more information about this}

 \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}