\documentclass[9pt]{beamer}

\usetheme{Boadilla}

\usecolortheme{dove}

\usecolortheme{orchid}

\usecolortheme{dolphin}

%\usecolortheme{seagull}

\usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}

\usepackage{xcolor}

\usepackage{ulem}

\usepackage{graphicx}

\usepackage{tikz}

\usetikzlibrary{automata}

\usepackage{subfigure}

\renewcommand{\emph}{\textit}

\renewcommand{\em}{\textit}

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

\newtheorem*{def:models}{Models}

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

\tableofcontents[currentsection]

\end{frame}

\begin{frame}

\frametitle{Infinity}

\framesubtitle{A bit more information about this}

\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[\sout{Complement automaton}]

            {

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

            {

              \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 infinite occurrences of $a$ or $b$.\\

Does \emph{not} accept inputs where both $a$ and $b$ occur infinitely often.

}

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

\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)$.

\item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages.

\end{itemize}

\end{def:automata language}

\end{frame}

\begin{frame}

\frametitle{Generalised Automata}

\framesubtitle{Definition}

\begin{def:general automata}

A \emph{generalised B\"uchi automaton} is a tuple $\A = (\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}

\end{frame}

\begin{frame}

\frametitle{Generalised Automata}

\framesubtitle{Acceptance}

\begin{def:general acceptance}

Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$ be a generalised automaton and let $\rho$ be a run of $\A$:

\begin{itemize}

\item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \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:general acceptance}

\end{frame}

\begin{frame}

\frametitle{Generalised Automata}

\framesubtitle{Language}

\begin{prop:general equiv}

Let $\A = (\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, then following equivalence condition holds:

\[L_\omega(\A) = \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.''}

\end{center}

\end{frame}

}

\begin{frame}

\frametitle{Linear Temporal Logic}

\framesubtitle{Motivation 2/2}

\begin{center}

\colorbox{black}{\color{white} ``It is dark} \colorbox{black!30}{\color{white} until someone puts on the light.''}

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

\end{def:syntax}

\end{frame}

\begin{frame}

\frametitle{Linear Temporal Logic}

\framesubtitle{Semantics}

\end{frame}

\begin{frame}

\frametitle{Model Checking}

\framesubtitle{A bit more information about this}

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