|
sawine@55
|
1 |
\documentclass[9pt]{beamer}
|
|
sawine@55
|
2 |
\usetheme{Boadilla}
|
|
sawine@55
|
3 |
\usecolortheme{seagull}
|
|
sawine@55
|
4 |
|
|
sawine@55
|
5 |
\newcommand{\M}{\mathcal{M}}
|
|
sawine@55
|
6 |
\newcommand{\N}{\mathbb{N}_0}
|
|
sawine@55
|
7 |
\newcommand{\F}{\mathcal{F}}
|
|
sawine@55
|
8 |
\newcommand{\Prop}{\mathcal{P}}
|
|
sawine@55
|
9 |
\newcommand{\A}{\mathcal{A}}
|
|
sawine@55
|
10 |
\newcommand{\X}{\mathcal{X}}
|
|
sawine@55
|
11 |
\newcommand{\U}{\mathcal{U}}
|
|
sawine@55
|
12 |
\newcommand{\V}{\mathcal{V}}
|
|
sawine@55
|
13 |
\newcommand{\dnf}{\mathsf{dnf}}
|
|
sawine@55
|
14 |
\newcommand{\consq}{\mathsf{consq}}
|
|
sawine@55
|
15 |
|
|
sawine@55
|
16 |
\theoremstyle{definition} %plain, definition, remark, proof, corollary
|
|
sawine@55
|
17 |
\newtheorem*{def:finite words}{Finite words}
|
|
sawine@55
|
18 |
\newtheorem*{def:infinite words}{Infinite words}
|
|
sawine@55
|
19 |
\newtheorem*{def:regular languages}{Regular languages}
|
|
sawine@55
|
20 |
\newtheorem*{def:regular languages closure}{Regular closure}
|
|
sawine@55
|
21 |
\newtheorem*{def:omega regular languages}{$\omega$-regular languages}
|
|
sawine@55
|
22 |
\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
|
|
sawine@55
|
23 |
\newtheorem*{def:buechi automata}{Automaton}
|
|
sawine@55
|
24 |
\newtheorem*{def:automata runs}{Runs}
|
|
sawine@55
|
25 |
\newtheorem*{def:automata acceptance}{Acceptance}
|
|
sawine@55
|
26 |
\newtheorem*{def:general automata}{Generalised automata}
|
|
sawine@55
|
27 |
\newtheorem*{def:general acceptance}{Acceptance}
|
|
sawine@55
|
28 |
\newtheorem*{def:vocabulary}{Vocabulary}
|
|
sawine@55
|
29 |
\newtheorem*{def:frames}{Frames}
|
|
sawine@55
|
30 |
\newtheorem*{def:models}{Models}
|
|
sawine@55
|
31 |
\newtheorem*{def:satisfiability}{Satisfiability}
|
|
sawine@55
|
32 |
\newtheorem*{def:fs closure}{Closure}
|
|
sawine@55
|
33 |
\newtheorem*{def:atoms}{Atoms}
|
|
sawine@55
|
34 |
\newtheorem*{def:rep function}{Representation function}
|
|
sawine@55
|
35 |
\newtheorem*{def:next}{Next function}
|
|
sawine@55
|
36 |
\newtheorem*{def:dnf}{Disjunctive normal form}
|
|
sawine@55
|
37 |
\newtheorem*{def:positive formulae}{Positive formulae}
|
|
sawine@55
|
38 |
\newtheorem*{def:consq}{Logical consequences}
|
|
sawine@55
|
39 |
\newtheorem*{def:partial automata}{Partial automata}
|
|
sawine@55
|
40 |
|
|
sawine@55
|
41 |
\theoremstyle{plain}
|
|
sawine@55
|
42 |
\newtheorem{prop:vocabulary sat}{Proposition}[section]
|
|
sawine@55
|
43 |
\newtheorem{prop:general equiv}{Proposition}[section]
|
|
sawine@55
|
44 |
\newtheorem{prop:computation set=language}{Proposition}[section]
|
|
sawine@55
|
45 |
|
|
sawine@55
|
46 |
\theoremstyle{plain}
|
|
sawine@55
|
47 |
\newtheorem{thm:model language}{Theorem}[section]
|
|
sawine@55
|
48 |
\newtheorem{cor:mod=model language}{Corollary}[thm:model language]
|
|
sawine@55
|
49 |
\newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
|
|
sawine@55
|
50 |
\newtheorem{thm:model checking}{Theorem}[section]
|
|
sawine@55
|
51 |
\newtheorem{lem:dnf}{Lemma}[section]
|
|
sawine@55
|
52 |
\newtheorem{lem:consq}[lem:dnf]{Lemma}
|
|
sawine@55
|
53 |
|
|
sawine@55
|
54 |
\title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}
|
|
sawine@55
|
55 |
\author{Eugen Sawin}
|
|
sawine@55
|
56 |
\institute[University of Freiburg]
|
|
sawine@55
|
57 |
{
|
|
sawine@55
|
58 |
Research Group for Foundations in Artificial Intelligence\\
|
|
sawine@55
|
59 |
Computer Science Department\\
|
|
sawine@55
|
60 |
University of Freiburg
|
|
sawine@55
|
61 |
}
|
|
sawine@55
|
62 |
\date[SS 2011]{Seminar: Automata Constructions in Model Checking}
|
|
sawine@55
|
63 |
\subject{Model Checking}
|
|
sawine@55
|
64 |
|
|
sawine@55
|
65 |
\begin{document}
|
|
sawine@55
|
66 |
\frame{\titlepage}
|
|
sawine@55
|
67 |
\begin{frame}
|
|
sawine@55
|
68 |
\frametitle{Motivation}
|
|
sawine@55
|
69 |
\tableofcontents[currentsection]
|
|
sawine@55
|
70 |
\end{frame}
|
|
sawine@55
|
71 |
|
|
sawine@55
|
72 |
\begin{frame}
|
|
sawine@55
|
73 |
\frametitle{Infinity}
|
|
sawine@55
|
74 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
75 |
|
|
sawine@55
|
76 |
\end{frame}
|
|
sawine@55
|
77 |
|
|
sawine@55
|
78 |
\begin{frame}
|
|
sawine@55
|
79 |
\frametitle{B\"uchi Automata}
|
|
sawine@55
|
80 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
81 |
|
|
sawine@55
|
82 |
\begin{def:buechi automata}
|
|
sawine@55
|
83 |
A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$, with:
|
|
sawine@55
|
84 |
\begin{itemize}
|
|
sawine@55
|
85 |
\item $\Sigma$ is a finite non-empty \emph{alphabet}
|
|
sawine@55
|
86 |
\item $S$ is a finite non-empty set of \emph{states}
|
|
sawine@55
|
87 |
\item $S_0 \subseteq S$ is the set of \emph{initial states}
|
|
sawine@55
|
88 |
\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}
|
|
sawine@55
|
89 |
\item $F \subseteq S$ is the set of \emph{accepting states}
|
|
sawine@55
|
90 |
\end{itemize}
|
|
sawine@55
|
91 |
\end{def:buechi automata}
|
|
sawine@55
|
92 |
\end{frame}
|
|
sawine@55
|
93 |
|
|
sawine@55
|
94 |
\begin{frame}
|
|
sawine@55
|
95 |
\frametitle{Linear Temporal Logic}
|
|
sawine@55
|
96 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
97 |
|
|
sawine@55
|
98 |
\end{frame}
|
|
sawine@55
|
99 |
|
|
sawine@55
|
100 |
\begin{frame}
|
|
sawine@55
|
101 |
\frametitle{Model Checking}
|
|
sawine@55
|
102 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
103 |
|
|
sawine@55
|
104 |
\end{frame}
|
|
sawine@55
|
105 |
|
|
sawine@55
|
106 |
\begin{frame}
|
|
sawine@55
|
107 |
\frametitle{On-the-fly Methods}
|
|
sawine@55
|
108 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
109 |
|
|
sawine@55
|
110 |
\end{frame}
|
|
sawine@55
|
111 |
|
|
sawine@55
|
112 |
\begin{frame}[allowframebreaks]
|
|
sawine@55
|
113 |
\frametitle<presentation>{Literature}
|
|
sawine@55
|
114 |
\begin{thebibliography}{10}
|
|
sawine@55
|
115 |
|
|
sawine@55
|
116 |
\beamertemplatearticlebibitems
|
|
sawine@55
|
117 |
\bibitem{ref:ltl&büchi}
|
|
sawine@55
|
118 |
Madhavan Mukund.
|
|
sawine@55
|
119 |
\newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
|
|
sawine@55
|
120 |
\newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
|
|
sawine@55
|
121 |
|
|
sawine@55
|
122 |
\beamertemplatearticlebibitems
|
|
sawine@55
|
123 |
\bibitem{ref:alternating verification}
|
|
sawine@55
|
124 |
Moshe Y. Vardi.
|
|
sawine@55
|
125 |
\newblock {\em Alternating Automata and Program Verification}.
|
|
sawine@55
|
126 |
\newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
|
|
sawine@55
|
127 |
|
|
sawine@55
|
128 |
\beamertemplatebookbibitems
|
|
sawine@55
|
129 |
\bibitem{ref:handbook}
|
|
sawine@55
|
130 |
Patrick Blackburn and Frank Wolter and Johan van Benthem.
|
|
sawine@55
|
131 |
\newblock {\em Handbook of Modal Logic}.
|
|
sawine@55
|
132 |
\newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.
|
|
sawine@55
|
133 |
|
|
sawine@55
|
134 |
\end{thebibliography}
|
|
sawine@55
|
135 |
\end{frame}
|
|
sawine@55
|
136 |
|
|
sawine@55
|
137 |
\end{document}
|