|
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@57
|
8 |
\newcommand{\Fs}{\mathbb{F}}
|
|
sawine@55
|
9 |
\newcommand{\Prop}{\mathcal{P}}
|
|
sawine@55
|
10 |
\newcommand{\A}{\mathcal{A}}
|
|
sawine@55
|
11 |
\newcommand{\X}{\mathcal{X}}
|
|
sawine@55
|
12 |
\newcommand{\U}{\mathcal{U}}
|
|
sawine@55
|
13 |
\newcommand{\V}{\mathcal{V}}
|
|
sawine@55
|
14 |
\newcommand{\dnf}{\mathsf{dnf}}
|
|
sawine@55
|
15 |
\newcommand{\consq}{\mathsf{consq}}
|
|
sawine@55
|
16 |
|
|
sawine@55
|
17 |
\theoremstyle{definition} %plain, definition, remark, proof, corollary
|
|
sawine@55
|
18 |
\newtheorem*{def:finite words}{Finite words}
|
|
sawine@55
|
19 |
\newtheorem*{def:infinite words}{Infinite words}
|
|
sawine@55
|
20 |
\newtheorem*{def:regular languages}{Regular languages}
|
|
sawine@55
|
21 |
\newtheorem*{def:regular languages closure}{Regular closure}
|
|
sawine@55
|
22 |
\newtheorem*{def:omega regular languages}{$\omega$-regular languages}
|
|
sawine@55
|
23 |
\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
|
|
sawine@55
|
24 |
\newtheorem*{def:buechi automata}{Automaton}
|
|
sawine@56
|
25 |
\newtheorem*{def:automata runs}{Run}
|
|
sawine@56
|
26 |
\newtheorem*{def:inf}{Infinite occurrences}
|
|
sawine@55
|
27 |
\newtheorem*{def:automata acceptance}{Acceptance}
|
|
sawine@56
|
28 |
\newtheorem*{def:automata language}{Recognised language}
|
|
sawine@57
|
29 |
\newtheorem*{def:general automata}{Generalised automaton}
|
|
sawine@55
|
30 |
\newtheorem*{def:general acceptance}{Acceptance}
|
|
sawine@55
|
31 |
\newtheorem*{def:vocabulary}{Vocabulary}
|
|
sawine@55
|
32 |
\newtheorem*{def:frames}{Frames}
|
|
sawine@55
|
33 |
\newtheorem*{def:models}{Models}
|
|
sawine@55
|
34 |
\newtheorem*{def:satisfiability}{Satisfiability}
|
|
sawine@55
|
35 |
\newtheorem*{def:fs closure}{Closure}
|
|
sawine@55
|
36 |
\newtheorem*{def:atoms}{Atoms}
|
|
sawine@55
|
37 |
\newtheorem*{def:rep function}{Representation function}
|
|
sawine@55
|
38 |
\newtheorem*{def:next}{Next function}
|
|
sawine@55
|
39 |
\newtheorem*{def:dnf}{Disjunctive normal form}
|
|
sawine@55
|
40 |
\newtheorem*{def:positive formulae}{Positive formulae}
|
|
sawine@55
|
41 |
\newtheorem*{def:consq}{Logical consequences}
|
|
sawine@55
|
42 |
\newtheorem*{def:partial automata}{Partial automata}
|
|
sawine@55
|
43 |
|
|
sawine@55
|
44 |
\theoremstyle{plain}
|
|
sawine@55
|
45 |
\newtheorem{prop:vocabulary sat}{Proposition}[section]
|
|
sawine@55
|
46 |
\newtheorem{prop:general equiv}{Proposition}[section]
|
|
sawine@55
|
47 |
\newtheorem{prop:computation set=language}{Proposition}[section]
|
|
sawine@55
|
48 |
|
|
sawine@55
|
49 |
\theoremstyle{plain}
|
|
sawine@55
|
50 |
\newtheorem{thm:model language}{Theorem}[section]
|
|
sawine@55
|
51 |
\newtheorem{cor:mod=model language}{Corollary}[thm:model language]
|
|
sawine@55
|
52 |
\newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
|
|
sawine@55
|
53 |
\newtheorem{thm:model checking}{Theorem}[section]
|
|
sawine@55
|
54 |
\newtheorem{lem:dnf}{Lemma}[section]
|
|
sawine@55
|
55 |
\newtheorem{lem:consq}[lem:dnf]{Lemma}
|
|
sawine@55
|
56 |
|
|
sawine@55
|
57 |
\title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}
|
|
sawine@55
|
58 |
\author{Eugen Sawin}
|
|
sawine@55
|
59 |
\institute[University of Freiburg]
|
|
sawine@55
|
60 |
{
|
|
sawine@55
|
61 |
Research Group for Foundations in Artificial Intelligence\\
|
|
sawine@55
|
62 |
Computer Science Department\\
|
|
sawine@55
|
63 |
University of Freiburg
|
|
sawine@55
|
64 |
}
|
|
sawine@55
|
65 |
\date[SS 2011]{Seminar: Automata Constructions in Model Checking}
|
|
sawine@55
|
66 |
\subject{Model Checking}
|
|
sawine@55
|
67 |
|
|
sawine@55
|
68 |
\begin{document}
|
|
sawine@55
|
69 |
\frame{\titlepage}
|
|
sawine@55
|
70 |
\begin{frame}
|
|
sawine@55
|
71 |
\frametitle{Motivation}
|
|
sawine@55
|
72 |
\tableofcontents[currentsection]
|
|
sawine@55
|
73 |
\end{frame}
|
|
sawine@55
|
74 |
|
|
sawine@55
|
75 |
\begin{frame}
|
|
sawine@55
|
76 |
\frametitle{Infinity}
|
|
sawine@55
|
77 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
78 |
\end{frame}
|
|
sawine@55
|
79 |
|
|
sawine@55
|
80 |
\begin{frame}
|
|
sawine@56
|
81 |
\frametitle{Automata}
|
|
sawine@56
|
82 |
\framesubtitle{Definition}
|
|
sawine@55
|
83 |
\begin{def:buechi automata}
|
|
sawine@56
|
84 |
A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:
|
|
sawine@55
|
85 |
\begin{itemize}
|
|
sawine@57
|
86 |
\item $\Sigma$ is a finite \emph{alphabet}.
|
|
sawine@57
|
87 |
\item $S$ is a finite set of \emph{states}.
|
|
sawine@57
|
88 |
\item $S_0 \subseteq S$ is the set of \emph{initial states}.
|
|
sawine@57
|
89 |
\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}.
|
|
sawine@57
|
90 |
\item $F \subseteq S$ is the set of \emph{accepting states}.
|
|
sawine@55
|
91 |
\end{itemize}
|
|
sawine@55
|
92 |
\end{def:buechi automata}
|
|
sawine@55
|
93 |
\end{frame}
|
|
sawine@55
|
94 |
|
|
sawine@55
|
95 |
\begin{frame}
|
|
sawine@56
|
96 |
\frametitle{Automata}
|
|
sawine@56
|
97 |
\framesubtitle{Runs}
|
|
sawine@56
|
98 |
\begin{def:automata runs}
|
|
sawine@56
|
99 |
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
|
|
sawine@56
|
100 |
\begin{itemize}
|
|
sawine@56
|
101 |
\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
|
102 |
\begin{itemize}
|
|
sawine@57
|
103 |
\item $s_0 \in S_0$.
|
|
sawine@57
|
104 |
\item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$.
|
|
sawine@56
|
105 |
\end{itemize}
|
|
sawine@57
|
106 |
\item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$.
|
|
sawine@56
|
107 |
\end{itemize}
|
|
sawine@56
|
108 |
\end{def:automata runs}
|
|
sawine@56
|
109 |
\end{frame}
|
|
sawine@56
|
110 |
|
|
sawine@56
|
111 |
\begin{frame}
|
|
sawine@56
|
112 |
\frametitle{Automata}
|
|
sawine@56
|
113 |
\framesubtitle{Acceptance}
|
|
sawine@56
|
114 |
\begin{def:inf}
|
|
sawine@56
|
115 |
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
|
|
sawine@56
|
116 |
\begin{itemize}
|
|
sawine@56
|
117 |
\item $\exists^\omega$ denotes the existential quantifier for infinitely many occurrences.
|
|
sawine@57
|
118 |
\item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$.
|
|
sawine@56
|
119 |
\end{itemize}
|
|
sawine@56
|
120 |
\end{def:inf}
|
|
sawine@56
|
121 |
|
|
sawine@56
|
122 |
\begin{def:automata acceptance}
|
|
sawine@56
|
123 |
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
|
|
sawine@56
|
124 |
\begin{itemize}
|
|
sawine@56
|
125 |
\item $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$.
|
|
sawine@56
|
126 |
\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
|
127 |
\end{itemize}
|
|
sawine@56
|
128 |
\end{def:automata acceptance}
|
|
sawine@56
|
129 |
\end{frame}
|
|
sawine@56
|
130 |
|
|
sawine@56
|
131 |
\begin{frame}
|
|
sawine@56
|
132 |
\frametitle{Automata}
|
|
sawine@56
|
133 |
\framesubtitle{Language}
|
|
sawine@56
|
134 |
\begin{def:automata language}
|
|
sawine@56
|
135 |
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
|
|
sawine@56
|
136 |
\begin{itemize}
|
|
sawine@57
|
137 |
\item $L_\omega(\A) = \{w \in \Sigma^\omega \mid \A \text{ accepts } w\}$, we say $\A$ recognises language $L_\omega(\A)$.
|
|
sawine@57
|
138 |
\item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
|
|
sawine@57
|
139 |
\item The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages.
|
|
sawine@56
|
140 |
\end{itemize}
|
|
sawine@56
|
141 |
\end{def:automata language}
|
|
sawine@56
|
142 |
\end{frame}
|
|
sawine@56
|
143 |
|
|
sawine@56
|
144 |
\begin{frame}
|
|
sawine@57
|
145 |
\frametitle{Generalised Automata}
|
|
sawine@57
|
146 |
\framesubtitle{Definition}
|
|
sawine@57
|
147 |
\begin{def:general automata}
|
|
sawine@57
|
148 |
A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:
|
|
sawine@57
|
149 |
\begin{itemize}
|
|
sawine@57
|
150 |
\item $\{F_i\}$ is a finite set of sets for a given $k$.
|
|
sawine@57
|
151 |
\item Each $F_i \subseteq S$ is a finite set of accepting states.
|
|
sawine@57
|
152 |
\end{itemize}
|
|
sawine@57
|
153 |
\end{def:general automata}
|
|
sawine@57
|
154 |
\end{frame}
|
|
sawine@57
|
155 |
|
|
sawine@57
|
156 |
\begin{frame}
|
|
sawine@57
|
157 |
\frametitle{Generalised Automata}
|
|
sawine@57
|
158 |
\framesubtitle{Acceptance}
|
|
sawine@57
|
159 |
\begin{def:general acceptance}
|
|
sawine@57
|
160 |
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
|
161 |
\begin{itemize}
|
|
sawine@57
|
162 |
\item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$.
|
|
sawine@57
|
163 |
\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
|
164 |
\end{itemize}
|
|
sawine@57
|
165 |
\end{def:general acceptance}
|
|
sawine@57
|
166 |
\end{frame}
|
|
sawine@57
|
167 |
|
|
sawine@57
|
168 |
\begin{frame}
|
|
sawine@57
|
169 |
\frametitle{Generalised Automata}
|
|
sawine@57
|
170 |
\framesubtitle{Language}
|
|
sawine@57
|
171 |
\begin{prop:general equiv}
|
|
sawine@57
|
172 |
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
|
173 |
\[L_\omega(\A) = \bigcap_{i < k} L_\omega(\A_i)\]
|
|
sawine@57
|
174 |
\end{prop:general equiv}
|
|
sawine@57
|
175 |
\end{frame}
|
|
sawine@57
|
176 |
|
|
sawine@57
|
177 |
\begin{frame}
|
|
sawine@55
|
178 |
\frametitle{Linear Temporal Logic}
|
|
sawine@55
|
179 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
180 |
\end{frame}
|
|
sawine@55
|
181 |
|
|
sawine@55
|
182 |
\begin{frame}
|
|
sawine@55
|
183 |
\frametitle{Model Checking}
|
|
sawine@55
|
184 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
185 |
|
|
sawine@55
|
186 |
\end{frame}
|
|
sawine@55
|
187 |
|
|
sawine@55
|
188 |
\begin{frame}
|
|
sawine@55
|
189 |
\frametitle{On-the-fly Methods}
|
|
sawine@55
|
190 |
\framesubtitle{A bit more information about this}
|
|
sawine@55
|
191 |
|
|
sawine@55
|
192 |
\end{frame}
|
|
sawine@55
|
193 |
|
|
sawine@55
|
194 |
\begin{frame}[allowframebreaks]
|
|
sawine@55
|
195 |
\frametitle<presentation>{Literature}
|
|
sawine@55
|
196 |
\begin{thebibliography}{10}
|
|
sawine@55
|
197 |
|
|
sawine@55
|
198 |
\beamertemplatearticlebibitems
|
|
sawine@55
|
199 |
\bibitem{ref:ltl&büchi}
|
|
sawine@55
|
200 |
Madhavan Mukund.
|
|
sawine@55
|
201 |
\newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
|
|
sawine@55
|
202 |
\newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
|
|
sawine@55
|
203 |
|
|
sawine@55
|
204 |
\beamertemplatearticlebibitems
|
|
sawine@55
|
205 |
\bibitem{ref:alternating verification}
|
|
sawine@55
|
206 |
Moshe Y. Vardi.
|
|
sawine@55
|
207 |
\newblock {\em Alternating Automata and Program Verification}.
|
|
sawine@55
|
208 |
\newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
|
|
sawine@55
|
209 |
|
|
sawine@55
|
210 |
\beamertemplatebookbibitems
|
|
sawine@55
|
211 |
\bibitem{ref:handbook}
|
|
sawine@55
|
212 |
Patrick Blackburn and Frank Wolter and Johan van Benthem.
|
|
sawine@55
|
213 |
\newblock {\em Handbook of Modal Logic}.
|
|
sawine@55
|
214 |
\newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.
|
|
sawine@55
|
215 |
|
|
sawine@55
|
216 |
\end{thebibliography}
|
|
sawine@55
|
217 |
\end{frame}
|
|
sawine@55
|
218 |
|
|
sawine@55
|
219 |
\end{document}
|