sawine@55: \documentclass[9pt]{beamer}
sawine@55: \usetheme{Boadilla}
sawine@55: \usecolortheme{seagull}
sawine@55: 
sawine@55: \newcommand{\M}{\mathcal{M}}
sawine@55: \newcommand{\N}{\mathbb{N}_0}
sawine@55: \newcommand{\F}{\mathcal{F}}
sawine@57: \newcommand{\Fs}{\mathbb{F}}
sawine@55: \newcommand{\Prop}{\mathcal{P}}
sawine@55: \newcommand{\A}{\mathcal{A}}
sawine@55: \newcommand{\X}{\mathcal{X}}
sawine@55: \newcommand{\U}{\mathcal{U}}
sawine@55: \newcommand{\V}{\mathcal{V}}
sawine@55: \newcommand{\dnf}{\mathsf{dnf}}
sawine@55: \newcommand{\consq}{\mathsf{consq}}
sawine@55: 
sawine@55: \theoremstyle{definition} %plain, definition, remark, proof, corollary
sawine@55: \newtheorem*{def:finite words}{Finite words}
sawine@55: \newtheorem*{def:infinite words}{Infinite words}
sawine@55: \newtheorem*{def:regular languages}{Regular languages}
sawine@55: \newtheorem*{def:regular languages closure}{Regular closure}
sawine@55: \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
sawine@55: \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
sawine@55: \newtheorem*{def:buechi automata}{Automaton}
sawine@56: \newtheorem*{def:automata runs}{Run}
sawine@56: \newtheorem*{def:inf}{Infinite occurrences}
sawine@55: \newtheorem*{def:automata acceptance}{Acceptance}
sawine@56: \newtheorem*{def:automata language}{Recognised language}
sawine@57: \newtheorem*{def:general automata}{Generalised automaton}
sawine@55: \newtheorem*{def:general acceptance}{Acceptance}
sawine@55: \newtheorem*{def:vocabulary}{Vocabulary}
sawine@55: \newtheorem*{def:frames}{Frames}
sawine@55: \newtheorem*{def:models}{Models}
sawine@55: \newtheorem*{def:satisfiability}{Satisfiability}
sawine@55: \newtheorem*{def:fs closure}{Closure}
sawine@55: \newtheorem*{def:atoms}{Atoms}
sawine@55: \newtheorem*{def:rep function}{Representation function}
sawine@55: \newtheorem*{def:next}{Next function}
sawine@55: \newtheorem*{def:dnf}{Disjunctive normal form}
sawine@55: \newtheorem*{def:positive formulae}{Positive formulae}
sawine@55: \newtheorem*{def:consq}{Logical consequences}
sawine@55: \newtheorem*{def:partial automata}{Partial automata}
sawine@55: 
sawine@55: \theoremstyle{plain}
sawine@55: \newtheorem{prop:vocabulary sat}{Proposition}[section]
sawine@55: \newtheorem{prop:general equiv}{Proposition}[section]
sawine@55: \newtheorem{prop:computation set=language}{Proposition}[section]
sawine@55: 
sawine@55: \theoremstyle{plain}
sawine@55: \newtheorem{thm:model language}{Theorem}[section]
sawine@55: \newtheorem{cor:mod=model language}{Corollary}[thm:model language]
sawine@55: \newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
sawine@55: \newtheorem{thm:model checking}{Theorem}[section]
sawine@55: \newtheorem{lem:dnf}{Lemma}[section]
sawine@55: \newtheorem{lem:consq}[lem:dnf]{Lemma}
sawine@55: 
sawine@55: \title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}
sawine@55: \author{Eugen Sawin}
sawine@55: \institute[University of Freiburg]
sawine@55: { 
sawine@55:   Research Group for Foundations in Artificial Intelligence\\
sawine@55:   Computer Science Department\\
sawine@55:   University of Freiburg
sawine@55: }
sawine@55: \date[SS 2011]{Seminar: Automata Constructions in Model Checking}
sawine@55: \subject{Model Checking}
sawine@55: 
sawine@55: \begin{document}
sawine@55: \frame{\titlepage}
sawine@55: \begin{frame}
sawine@55: \frametitle{Motivation}
sawine@55: \tableofcontents[currentsection]
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@55: \frametitle{Infinity}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@56: \frametitle{Automata}
sawine@56: \framesubtitle{Definition}
sawine@55: \begin{def:buechi automata}
sawine@56: A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:
sawine@55: \begin{itemize}
sawine@57: \item $\Sigma$ is a finite \emph{alphabet}.
sawine@57: \item $S$ is a finite set of \emph{states}.
sawine@57: \item $S_0 \subseteq S$ is the set of \emph{initial states}.
sawine@57: \item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}.
sawine@57: \item $F \subseteq S$ is the set of \emph{accepting states}.
sawine@55: \end{itemize}
sawine@55: \end{def:buechi automata}
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@56: \frametitle{Automata}
sawine@56: \framesubtitle{Runs}
sawine@56: \begin{def:automata runs}
sawine@56: Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
sawine@56: \begin{itemize}
sawine@56: \item A run $\rho$ of $\A$ on an infinite word $w = a_0,a_1,...$ is a sequence $\rho = s_0,s_1,...$:
sawine@56: \begin{itemize}
sawine@57: \item $s_0 \in S_0$.
sawine@57: \item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$.
sawine@56: \end{itemize}
sawine@57: \item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$.
sawine@56: \end{itemize}
sawine@56: \end{def:automata runs}
sawine@56: \end{frame}
sawine@56: 
sawine@56: \begin{frame}
sawine@56: \frametitle{Automata}
sawine@56: \framesubtitle{Acceptance}
sawine@56: \begin{def:inf}
sawine@56: Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
sawine@56: \begin{itemize}
sawine@56: \item $\exists^\omega$ denotes the existential quantifier for infinitely many occurrences.
sawine@57: \item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$.
sawine@56: \end{itemize}
sawine@56: \end{def:inf}
sawine@56: 
sawine@56: \begin{def:automata acceptance}
sawine@56: Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
sawine@56: \begin{itemize}
sawine@56: \item $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$.
sawine@56: \item $\A$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is \emph{accepting}. 
sawine@56: \end{itemize}
sawine@56: \end{def:automata acceptance}
sawine@56: \end{frame}
sawine@56: 
sawine@56: \begin{frame}
sawine@56: \frametitle{Automata}
sawine@56: \framesubtitle{Language}
sawine@56: \begin{def:automata language}
sawine@56: Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
sawine@56: \begin{itemize}
sawine@57: \item $L_\omega(\A) = \{w \in \Sigma^\omega \mid \A \text{ accepts } w\}$, we say $\A$ recognises language $L_\omega(\A)$.
sawine@57: \item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
sawine@57: \item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages.
sawine@56: \end{itemize}
sawine@56: \end{def:automata language}
sawine@56: \end{frame}
sawine@56: 
sawine@56: \begin{frame}
sawine@57: \frametitle{Generalised Automata}
sawine@57: \framesubtitle{Definition}
sawine@57: \begin{def:general automata}
sawine@57: A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:
sawine@57: \begin{itemize}
sawine@57: \item $\{F_i\}$ is a finite set of sets for a given $k$.
sawine@57: \item Each $F_i \subseteq S$ is a finite set of accepting states.
sawine@57: \end{itemize}
sawine@57: \end{def:general automata}
sawine@57: \end{frame}
sawine@57: 
sawine@57: \begin{frame}
sawine@57: \frametitle{Generalised Automata}
sawine@57: \framesubtitle{Acceptance}
sawine@57: \begin{def:general acceptance}
sawine@57: Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$ be a generalised automaton and let $\rho$ be a run of $\A$:
sawine@57: \begin{itemize}
sawine@57: \item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$.
sawine@57: \item $\A$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is \emph{accepting}. 
sawine@57: \end{itemize} 
sawine@57: \end{def:general acceptance}
sawine@57: \end{frame}
sawine@57: 
sawine@57: \begin{frame}
sawine@57: \frametitle{Generalised Automata}
sawine@57: \framesubtitle{Language}
sawine@57: \begin{prop:general equiv}
sawine@57: 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:
sawine@57: \[L_\omega(\A) = \bigcap_{i < k} L_\omega(\A_i)\]
sawine@57: \end{prop:general equiv}
sawine@57: \end{frame}
sawine@57: 
sawine@57: \begin{frame}
sawine@55: \frametitle{Linear Temporal Logic}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@55: \frametitle{Model Checking}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: 
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}
sawine@55: \frametitle{On-the-fly Methods}
sawine@55: \framesubtitle{A bit more information about this}
sawine@55: 
sawine@55: \end{frame}
sawine@55: 
sawine@55: \begin{frame}[allowframebreaks]
sawine@55: \frametitle<presentation>{Literature}    
sawine@55: \begin{thebibliography}{10}    
sawine@55: 
sawine@55: \beamertemplatearticlebibitems
sawine@55: \bibitem{ref:ltl&büchi}
sawine@55: Madhavan Mukund.
sawine@55: \newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
sawine@55: \newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
sawine@55:   
sawine@55: \beamertemplatearticlebibitems
sawine@55: \bibitem{ref:alternating verification}
sawine@55: Moshe Y. Vardi.
sawine@55: \newblock {\em Alternating Automata and Program Verification}.
sawine@55: \newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
sawine@55: 
sawine@55: \beamertemplatebookbibitems
sawine@55: \bibitem{ref:handbook}
sawine@55: Patrick Blackburn and Frank Wolter and Johan van Benthem.
sawine@55: \newblock {\em Handbook of Modal Logic}.
sawine@55: \newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.
sawine@55: 
sawine@55: \end{thebibliography}
sawine@55: \end{frame}
sawine@55: 
sawine@55: \end{document}