|
sawine@55
|
1 |
\documentclass[9pt]{beamer}
|
|
sawine@55
|
2 |
\usetheme{Boadilla}
|
|
sawine@58
|
3 |
\usecolortheme{dove}
|
|
sawine@58
|
4 |
\usecolortheme{orchid}
|
|
sawine@58
|
5 |
\usecolortheme{dolphin}
|
|
sawine@58
|
6 |
%\usecolortheme{seagull}
|
|
sawine@58
|
7 |
|
|
sawine@60
|
8 |
\usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
|
|
sawine@62
|
9 |
\usepackage{pifont}
|
|
sawine@61
|
10 |
\usepackage{xcolor}
|
|
sawine@58
|
11 |
\usepackage{ulem}
|
|
sawine@66
|
12 |
\usepackage{graphics}
|
|
sawine@58
|
13 |
\usepackage{tikz}
|
|
sawine@58
|
14 |
\usetikzlibrary{automata}
|
|
sawine@58
|
15 |
\usepackage{subfigure}
|
|
sawine@55
|
16 |
|
|
sawine@61
|
17 |
\renewcommand{\emph}{\textit}
|
|
sawine@66
|
18 |
\renewcommand{\em}{\it}
|
|
sawine@62
|
19 |
|
|
sawine@62
|
20 |
\newcommand{\cross}{\ding{55}}
|
|
sawine@55
|
21 |
\newcommand{\M}{\mathcal{M}}
|
|
sawine@55
|
22 |
\newcommand{\N}{\mathbb{N}_0}
|
|
sawine@55
|
23 |
\newcommand{\F}{\mathcal{F}}
|
|
sawine@57
|
24 |
\newcommand{\Fs}{\mathbb{F}}
|
|
sawine@55
|
25 |
\newcommand{\Prop}{\mathcal{P}}
|
|
sawine@55
|
26 |
\newcommand{\A}{\mathcal{A}}
|
|
sawine@55
|
27 |
\newcommand{\X}{\mathcal{X}}
|
|
sawine@55
|
28 |
\newcommand{\U}{\mathcal{U}}
|
|
sawine@55
|
29 |
\newcommand{\V}{\mathcal{V}}
|
|
sawine@55
|
30 |
\newcommand{\dnf}{\mathsf{dnf}}
|
|
sawine@55
|
31 |
\newcommand{\consq}{\mathsf{consq}}
|
|
sawine@55
|
32 |
|
|
sawine@55
|
33 |
\theoremstyle{definition} %plain, definition, remark, proof, corollary
|
|
sawine@55
|
34 |
\newtheorem*{def:finite words}{Finite words}
|
|
sawine@55
|
35 |
\newtheorem*{def:infinite words}{Infinite words}
|
|
sawine@55
|
36 |
\newtheorem*{def:regular languages}{Regular languages}
|
|
sawine@55
|
37 |
\newtheorem*{def:regular languages closure}{Regular closure}
|
|
sawine@55
|
38 |
\newtheorem*{def:omega regular languages}{$\omega$-regular languages}
|
|
sawine@55
|
39 |
\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
|
|
sawine@55
|
40 |
\newtheorem*{def:buechi automata}{Automaton}
|
|
sawine@56
|
41 |
\newtheorem*{def:automata runs}{Run}
|
|
sawine@56
|
42 |
\newtheorem*{def:inf}{Infinite occurrences}
|
|
sawine@55
|
43 |
\newtheorem*{def:automata acceptance}{Acceptance}
|
|
sawine@56
|
44 |
\newtheorem*{def:automata language}{Recognised language}
|
|
sawine@57
|
45 |
\newtheorem*{def:general automata}{Generalised automaton}
|
|
sawine@55
|
46 |
\newtheorem*{def:general acceptance}{Acceptance}
|
|
sawine@61
|
47 |
\newtheorem*{def:syntax}{Syntax}
|
|
sawine@61
|
48 |
|
|
sawine@61
|
49 |
|
|
sawine@55
|
50 |
\newtheorem*{def:vocabulary}{Vocabulary}
|
|
sawine@62
|
51 |
\newtheorem*{def:frames}{Frame}
|
|
sawine@62
|
52 |
\newtheorem*{def:models}{Model}
|
|
sawine@55
|
53 |
\newtheorem*{def:satisfiability}{Satisfiability}
|
|
sawine@55
|
54 |
\newtheorem*{def:fs closure}{Closure}
|
|
sawine@55
|
55 |
\newtheorem*{def:atoms}{Atoms}
|
|
sawine@55
|
56 |
\newtheorem*{def:rep function}{Representation function}
|
|
sawine@55
|
57 |
\newtheorem*{def:next}{Next function}
|
|
sawine@55
|
58 |
\newtheorem*{def:dnf}{Disjunctive normal form}
|
|
sawine@55
|
59 |
\newtheorem*{def:positive formulae}{Positive formulae}
|
|
sawine@55
|
60 |
\newtheorem*{def:consq}{Logical consequences}
|
|
sawine@55
|
61 |
\newtheorem*{def:partial automata}{Partial automata}
|
|
sawine@55
|
62 |
|
|
sawine@55
|
63 |
\theoremstyle{plain}
|
|
sawine@55
|
64 |
\newtheorem{prop:vocabulary sat}{Proposition}[section]
|
|
sawine@55
|
65 |
\newtheorem{prop:general equiv}{Proposition}[section]
|
|
sawine@55
|
66 |
\newtheorem{prop:computation set=language}{Proposition}[section]
|
|
sawine@55
|
67 |
|
|
sawine@55
|
68 |
\theoremstyle{plain}
|
|
sawine@55
|
69 |
\newtheorem{thm:model language}{Theorem}[section]
|
|
sawine@55
|
70 |
\newtheorem{cor:mod=model language}{Corollary}[thm:model language]
|
|
sawine@55
|
71 |
\newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
|
|
sawine@55
|
72 |
\newtheorem{thm:model checking}{Theorem}[section]
|
|
sawine@55
|
73 |
\newtheorem{lem:dnf}{Lemma}[section]
|
|
sawine@55
|
74 |
\newtheorem{lem:consq}[lem:dnf]{Lemma}
|
|
sawine@55
|
75 |
|
|
sawine@55
|
76 |
\title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}
|
|
sawine@55
|
77 |
\author{Eugen Sawin}
|
|
sawine@55
|
78 |
\institute[University of Freiburg]
|
|
sawine@55
|
79 |
{
|
|
sawine@55
|
80 |
Research Group for Foundations in Artificial Intelligence\\
|
|
sawine@55
|
81 |
Computer Science Department\\
|
|
sawine@55
|
82 |
University of Freiburg
|
|
sawine@55
|
83 |
}
|
|
sawine@55
|
84 |
\date[SS 2011]{Seminar: Automata Constructions in Model Checking}
|
|
sawine@55
|
85 |
\subject{Model Checking}
|
|
sawine@55
|
86 |
|
|
sawine@55
|
87 |
\begin{document}
|
|
sawine@55
|
88 |
\frame{\titlepage}
|
|
sawine@66
|
89 |
|
|
sawine@55
|
90 |
\begin{frame}
|
|
sawine@55
|
91 |
\frametitle{Motivation}
|
|
sawine@67
|
92 |
\framesubtitle{Model Checking 1/2}
|
|
sawine@66
|
93 |
\begin{center}
|
|
sawine@66
|
94 |
%\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}
|
|
sawine@67
|
95 |
\[\M \models \varphi\]
|
|
sawine@66
|
96 |
\end{center}
|
|
sawine@66
|
97 |
\end{frame}
|
|
sawine@66
|
98 |
|
|
sawine@66
|
99 |
\begin{frame}
|
|
sawine@66
|
100 |
\frametitle{Motivation}
|
|
sawine@67
|
101 |
\framesubtitle{Model Checking 2/2}
|
|
sawine@67
|
102 |
\begin{center}
|
|
sawine@67
|
103 |
Given a program $P$ and specification $\varphi$:\\
|
|
sawine@67
|
104 |
\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}
|
|
sawine@67
|
105 |
\end{center}
|
|
sawine@67
|
106 |
\end{frame}
|
|
sawine@67
|
107 |
|
|
sawine@67
|
108 |
\begin{frame}
|
|
sawine@67
|
109 |
\frametitle{Motivation}
|
|
sawine@67
|
110 |
\framesubtitle{Industry}
|
|
sawine@66
|
111 |
\begin{figure}
|
|
sawine@66
|
112 |
\centering
|
|
sawine@67
|
113 |
\subfigure{\includegraphics[width=70pt,height=50pt]{images/intel.jpg}}
|
|
sawine@67
|
114 |
\subfigure{\includegraphics[width=70pt,height=50pt]{images/airbag.jpg}}
|
|
sawine@67
|
115 |
\subfigure{\includegraphics[width=70pt,height=50pt]{images/atc.jpg}}
|
|
sawine@66
|
116 |
\end{figure}
|
|
sawine@55
|
117 |
\end{frame}
|
|
sawine@55
|
118 |
|
|
sawine@67
|
119 |
{
|
|
sawine@67
|
120 |
\setbeamercolor{normal text}{bg=black, fg=white}
|
|
sawine@67
|
121 |
\setbeamercolor{frametitle}{fg=white!30!black}
|
|
sawine@67
|
122 |
\usebeamercolor*{normal text}
|
|
sawine@67
|
123 |
\usebeamercolor*{frametitle}
|
|
sawine@67
|
124 |
\begin{frame}
|
|
sawine@67
|
125 |
\frametitle{Linear Temporal Logic}
|
|
sawine@70
|
126 |
\framesubtitle{Natural language 1/2}
|
|
sawine@67
|
127 |
\begin{center}
|
|
sawine@67
|
128 |
``It is dark.''\\
|
|
sawine@67
|
129 |
\visible<2->{``It is \emph{always} dark.''\\}
|
|
sawine@67
|
130 |
\visible<3->{``It is \emph{currently} dark.''\\}
|
|
sawine@69
|
131 |
\visible<4->{``It will \emph{necessarily} be dark.''\\}
|
|
sawine@67
|
132 |
\visible<5->{``It is dark \emph{until} someone puts the light on.''}
|
|
sawine@67
|
133 |
\end{center}
|
|
sawine@67
|
134 |
\end{frame}
|
|
sawine@67
|
135 |
}
|
|
sawine@67
|
136 |
|
|
sawine@67
|
137 |
\begin{frame}
|
|
sawine@67
|
138 |
\frametitle{Linear Temporal Logic}
|
|
sawine@70
|
139 |
\framesubtitle{Natural language 2/2}
|
|
sawine@67
|
140 |
\begin{center}
|
|
sawine@67
|
141 |
\only<1->{
|
|
sawine@67
|
142 |
\color{white}
|
|
sawine@67
|
143 |
\colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\
|
|
sawine@67
|
144 |
\visible<2->{
|
|
sawine@67
|
145 |
\colorbox{black}{\makebox(50,10){$p_0$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$p_1$}}}
|
|
sawine@67
|
146 |
}
|
|
sawine@67
|
147 |
\end{center}
|
|
sawine@67
|
148 |
\end{frame}
|
|
sawine@67
|
149 |
|
|
sawine@67
|
150 |
\begin{frame}
|
|
sawine@67
|
151 |
\frametitle{Linear Temporal Logic}
|
|
sawine@67
|
152 |
\framesubtitle{Syntax}
|
|
sawine@67
|
153 |
\begin{def:syntax}
|
|
sawine@67
|
154 |
Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions:
|
|
sawine@67
|
155 |
\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
|
|
sawine@67
|
156 |
\begin{itemize}
|
|
sawine@67
|
157 |
\item $\neg, \lor$ corresponds to the Boolean \emph{negation} and \emph{disjunction}.
|
|
sawine@67
|
158 |
\item $\X$ reads \emph{next}.
|
|
sawine@67
|
159 |
\item $\U$ reads \emph{until}.
|
|
sawine@67
|
160 |
\end{itemize}
|
|
sawine@67
|
161 |
\end{def:syntax}
|
|
sawine@67
|
162 |
\end{frame}
|
|
sawine@67
|
163 |
|
|
sawine@67
|
164 |
\begin{frame}
|
|
sawine@67
|
165 |
\frametitle{Linear Temporal Logic}
|
|
sawine@67
|
166 |
\framesubtitle{Semantics}
|
|
sawine@67
|
167 |
\begin{def:frames}
|
|
sawine@67
|
168 |
An LTL-\emph{frame} is a tuple $\F = (S, R)$:
|
|
sawine@67
|
169 |
\begin{itemize}
|
|
sawine@67
|
170 |
\item $S = \{s_i \mid i \in \N\}$ is the set of states.
|
|
sawine@67
|
171 |
\item $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ is the accessibility relation.
|
|
sawine@67
|
172 |
\end{itemize}
|
|
sawine@67
|
173 |
\end{def:frames}
|
|
sawine@67
|
174 |
|
|
sawine@67
|
175 |
\begin{def:models}
|
|
sawine@67
|
176 |
An LTL-\emph{model} is a tuple $\M = (\F, V)$:
|
|
sawine@67
|
177 |
\begin{itemize}
|
|
sawine@67
|
178 |
\item $\F$ is a \emph{frame}.
|
|
sawine@67
|
179 |
\item $V: S \to 2^\Prop$ is a \emph{valuation function}.
|
|
sawine@67
|
180 |
\item Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.
|
|
sawine@67
|
181 |
\end{itemize}
|
|
sawine@67
|
182 |
\end{def:models}
|
|
sawine@67
|
183 |
\end{frame}
|
|
sawine@67
|
184 |
|
|
sawine@67
|
185 |
\begin{frame}
|
|
sawine@67
|
186 |
\frametitle{Linear Temporal Logic}
|
|
sawine@67
|
187 |
\framesubtitle{Model Example}
|
|
sawine@67
|
188 |
\begin{figure}
|
|
sawine@67
|
189 |
\centering
|
|
sawine@67
|
190 |
\begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth
|
|
sawine@67
|
191 |
,accepting/.style={fill, gray!50!black, text=white}]
|
|
sawine@67
|
192 |
\node[state, initial, initial text=] (s_0) {$\{p_0\}$};
|
|
sawine@67
|
193 |
\path (s_0) [late options={label=below:$s_0$}];
|
|
sawine@67
|
194 |
\node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$};
|
|
sawine@67
|
195 |
\path (s_1) [late options={label=below:$s_1$}];
|
|
sawine@67
|
196 |
\node[state] (s_2) [right of= s_1] {$\{p_1\}$};
|
|
sawine@67
|
197 |
\path (s_2) [late options={label=below:$s_2$}];
|
|
sawine@67
|
198 |
\node[state] (s_i) [right of= s_2] {$\{p_1\}$};
|
|
sawine@67
|
199 |
\path (s_i) [late options={label=below:$s_i$}];
|
|
sawine@67
|
200 |
\path[->]
|
|
sawine@67
|
201 |
(s_0) edge node {$R$} (s_1)
|
|
sawine@67
|
202 |
(s_1) edge node {$R$} (s_2);
|
|
sawine@67
|
203 |
\path[dashed,->]
|
|
sawine@67
|
204 |
(s_2) edge node {$R$} (s_i);
|
|
sawine@67
|
205 |
\end{tikzpicture}
|
|
sawine@67
|
206 |
\end{figure}
|
|
sawine@67
|
207 |
\end{frame}
|
|
sawine@67
|
208 |
|
|
sawine@67
|
209 |
\begin{frame}
|
|
sawine@67
|
210 |
\frametitle{Linear Temporal Logic}
|
|
sawine@67
|
211 |
\framesubtitle{Satisfiability}
|
|
sawine@67
|
212 |
\begin{def:satisfiability}
|
|
sawine@67
|
213 |
A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
|
|
sawine@67
|
214 |
\begin{itemize}
|
|
sawine@67
|
215 |
\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
|
|
sawine@67
|
216 |
\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
|
|
sawine@67
|
217 |
\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
|
|
sawine@67
|
218 |
\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
|
|
sawine@67
|
219 |
\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$
|
|
sawine@67
|
220 |
\end{itemize}
|
|
sawine@67
|
221 |
\end{def:satisfiability}
|
|
sawine@67
|
222 |
\end{frame}
|
|
sawine@67
|
223 |
|
|
sawine@55
|
224 |
\begin{frame}
|
|
sawine@70
|
225 |
\frametitle{Reactive Systems}
|
|
sawine@70
|
226 |
\framesubtitle{Infinite inputs}
|
|
sawine@66
|
227 |
\begin{figure}
|
|
sawine@66
|
228 |
\centering
|
|
sawine@70
|
229 |
|
|
sawine@70
|
230 |
\subfigure{
|
|
sawine@70
|
231 |
\begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth
|
|
sawine@70
|
232 |
,accepting/.style={fill, gray!50!black, text=white}]
|
|
sawine@70
|
233 |
\node[state, initial, initial text=$input$] (p) {$Program$};
|
|
sawine@70
|
234 |
\coordinate (b) at (1.1,0);
|
|
sawine@70
|
235 |
%\coordinate (b) at ($(a)+1/2*(3,3)$);
|
|
sawine@70
|
236 |
\draw (p) edge[->] node[right] {$\,output$} (b);
|
|
sawine@70
|
237 |
%\draw[->] (p) -- (b);
|
|
sawine@70
|
238 |
\end{tikzpicture}
|
|
sawine@70
|
239 |
}
|
|
sawine@70
|
240 |
|
|
sawine@70
|
241 |
\subfigure{
|
|
sawine@66
|
242 |
\begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth
|
|
sawine@66
|
243 |
,accepting/.style={fill, gray!50!black, text=white}]
|
|
sawine@66
|
244 |
\node[state, initial, initial text=] (s_0) {$a$};
|
|
sawine@66
|
245 |
\node[state] (s_1) [right of= s_0] {$b$};
|
|
sawine@66
|
246 |
\node[state] (s_2) [right of= s_1] {$a$};
|
|
sawine@66
|
247 |
\node[state] (s_i) [right of= s_2] {$a$};
|
|
sawine@66
|
248 |
\path[->]
|
|
sawine@66
|
249 |
(s_0) edge node {} (s_1)
|
|
sawine@66
|
250 |
(s_1) edge node {} (s_2);
|
|
sawine@66
|
251 |
\path[dashed,->]
|
|
sawine@66
|
252 |
(s_2) edge node {} (s_i);
|
|
sawine@66
|
253 |
\end{tikzpicture}
|
|
sawine@70
|
254 |
}
|
|
sawine@66
|
255 |
\end{figure}
|
|
sawine@55
|
256 |
\end{frame}
|
|
sawine@55
|
257 |
|
|
sawine@55
|
258 |
\begin{frame}
|
|
sawine@56
|
259 |
\frametitle{Automata}
|
|
sawine@59
|
260 |
\framesubtitle{Example 1/2}
|
|
sawine@58
|
261 |
\begin{figure}
|
|
sawine@58
|
262 |
\centering
|
|
sawine@60
|
263 |
\only<-3>{
|
|
sawine@58
|
264 |
\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
|
|
sawine@58
|
265 |
%every state/.style={fill, draw=none, gray, text=white},
|
|
sawine@58
|
266 |
,accepting/.style={fill, gray!50!black, text=white}
|
|
sawine@58
|
267 |
%initial/.style ={gray, text=white}]%, thick]
|
|
sawine@58
|
268 |
]
|
|
sawine@58
|
269 |
\node[state,initial, initial text=] (q_0) {$q_0$};
|
|
sawine@58
|
270 |
\node[state] (q_1) [above right of= q_0] {$q_1$};
|
|
sawine@58
|
271 |
\node[state,accepting](q_2) [below right of= q_1] {$q_2$};
|
|
sawine@58
|
272 |
\path[->]
|
|
sawine@58
|
273 |
(q_0) edge node {$a$} (q_1)
|
|
sawine@58
|
274 |
edge [loop above] node {$b$} ()
|
|
sawine@58
|
275 |
(q_1) edge node {$b$} (q_2)
|
|
sawine@58
|
276 |
edge [loop above] node {$a$} ()
|
|
sawine@58
|
277 |
(q_2) %edge node {$a$} (q_1)
|
|
sawine@58
|
278 |
edge node {$b$} (q_0);
|
|
sawine@58
|
279 |
\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
|
|
sawine@60
|
280 |
\end{tikzpicture}\\
|
|
sawine@60
|
281 |
\vspace{10pt}
|
|
sawine@60
|
282 |
\visible<2-3>{$w_1 = \overline{bbaa} \implies \rho_1 = q_0q_0\overline{q_0q_1q_1q_2}$}\\
|
|
sawine@60
|
283 |
\visible<3>{$w_2 = bb\overline{ab} \implies \rho_2 = q_0q_0\overline{q_1q_2}$}\\
|
|
sawine@60
|
284 |
\vspace{10pt}
|
|
sawine@60
|
285 |
\visible<4>{Accepts all inputs with infinite occurrences of $ab$.}
|
|
sawine@58
|
286 |
}
|
|
sawine@58
|
287 |
|
|
sawine@60
|
288 |
\only<4>{
|
|
sawine@58
|
289 |
\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
|
|
sawine@58
|
290 |
%every state/.style={fill, draw=none, gray, text=white},
|
|
sawine@58
|
291 |
,accepting/.style={fill, gray!50!black, text=white}
|
|
sawine@58
|
292 |
%initial/.style ={gray, text=white}]%, thick]
|
|
sawine@58
|
293 |
]
|
|
sawine@58
|
294 |
\node[state,initial, initial text=] (q_0) {$q_0$};
|
|
sawine@58
|
295 |
\node[state] (q_1) [above right of= q_0] {$q_1$};
|
|
sawine@58
|
296 |
\node[state,accepting](q_2) [below right of= q_1] {$q_2$};
|
|
sawine@58
|
297 |
\path[->]
|
|
sawine@58
|
298 |
(q_0)
|
|
sawine@58
|
299 |
edge [loop above] node {$b$} ()
|
|
sawine@58
|
300 |
(q_1)
|
|
sawine@58
|
301 |
edge [loop above] node {$a$} ()
|
|
sawine@58
|
302 |
(q_2) %edge node {$a$} (q_1)
|
|
sawine@58
|
303 |
edge node {$b$} (q_0);
|
|
sawine@58
|
304 |
\color{green}
|
|
sawine@58
|
305 |
\path[->]
|
|
sawine@58
|
306 |
(q_0) edge node {$a$} (q_1)
|
|
sawine@58
|
307 |
(q_1) edge node {$b$} (q_2);
|
|
sawine@58
|
308 |
\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
|
|
sawine@59
|
309 |
\end{tikzpicture}\\
|
|
sawine@58
|
310 |
\color{black}
|
|
sawine@60
|
311 |
\vspace{10pt}
|
|
sawine@60
|
312 |
\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}}$}\\
|
|
sawine@60
|
313 |
\visible<3->{$w_2 = bb\overline{\textcolor{green}{ab}} \implies \rho_2 = q_0q_0\overline{q_1\textcolor{green}{q_2}}$}\\
|
|
sawine@60
|
314 |
\vspace{10pt}
|
|
sawine@60
|
315 |
\visible<4>{Accepts all inputs with infinite occurrences of $ab$.}
|
|
sawine@58
|
316 |
}
|
|
sawine@58
|
317 |
%Automaton $\A_1$
|
|
sawine@58
|
318 |
\end{figure}
|
|
sawine@58
|
319 |
\end{frame}
|
|
sawine@58
|
320 |
|
|
sawine@58
|
321 |
\begin{frame}
|
|
sawine@58
|
322 |
\frametitle{Automata}
|
|
sawine@59
|
323 |
\framesubtitle{Example 2/2 (Complement)}
|
|
sawine@58
|
324 |
\begin{figure}
|
|
sawine@58
|
325 |
\centering
|
|
sawine@60
|
326 |
\only<1>{
|
|
sawine@58
|
327 |
\subfigure
|
|
sawine@58
|
328 |
{
|
|
sawine@58
|
329 |
\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
|
|
sawine@58
|
330 |
%every state/.style={fill, draw=none, gray, text=white},
|
|
sawine@58
|
331 |
,accepting/.style={fill, gray!50!black, text=white}
|
|
sawine@58
|
332 |
%initial/.style ={gray, text=white}]%, thick]
|
|
sawine@58
|
333 |
]
|
|
sawine@58
|
334 |
\node[state,initial, initial text=, accepting] (q_0) {$q_0$};
|
|
sawine@58
|
335 |
\node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
|
|
sawine@58
|
336 |
\node[state](q_2) [below right of= q_1] {$q_2$};
|
|
sawine@58
|
337 |
\path[->]
|
|
sawine@58
|
338 |
(q_0) edge node {$a$} (q_1)
|
|
sawine@58
|
339 |
edge [loop above] node {$b$} ()
|
|
sawine@58
|
340 |
(q_1) edge node {$b$} (q_2)
|
|
sawine@58
|
341 |
edge [loop above] node {$a$} ()
|
|
sawine@58
|
342 |
(q_2) %edge node {$a$} (q_1)
|
|
sawine@58
|
343 |
edge node {$b$} (q_0);
|
|
sawine@58
|
344 |
\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
|
|
sawine@58
|
345 |
\end{tikzpicture}
|
|
sawine@58
|
346 |
}
|
|
sawine@58
|
347 |
}
|
|
sawine@58
|
348 |
\only<2>{
|
|
sawine@58
|
349 |
\subfigure
|
|
sawine@58
|
350 |
{
|
|
sawine@58
|
351 |
\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
|
|
sawine@58
|
352 |
%every state/.style={fill, draw=none, gray, text=white},
|
|
sawine@58
|
353 |
,accepting/.style={fill, gray!50!black, text=white}
|
|
sawine@58
|
354 |
%initial/.style ={gray, text=white}]%, thick]
|
|
sawine@58
|
355 |
]
|
|
sawine@58
|
356 |
\node[state,initial, initial text=, accepting] (q_0) {$q_0$};
|
|
sawine@58
|
357 |
\node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
|
|
sawine@58
|
358 |
\node[state](q_2) [below right of= q_1] {$q_2$};
|
|
sawine@58
|
359 |
\path[->]
|
|
sawine@58
|
360 |
(q_0)
|
|
sawine@58
|
361 |
edge [loop above] node {$b$} ()
|
|
sawine@58
|
362 |
(q_1)
|
|
sawine@58
|
363 |
edge [loop above] node {$a$} ();
|
|
sawine@58
|
364 |
\color{red}
|
|
sawine@58
|
365 |
\path[->]
|
|
sawine@58
|
366 |
(q_0) edge node {$a$} (q_1)
|
|
sawine@58
|
367 |
(q_1) edge node {$b$} (q_2)
|
|
sawine@58
|
368 |
(q_2) edge node {$b$} (q_0);
|
|
sawine@58
|
369 |
\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
|
|
sawine@58
|
370 |
\end{tikzpicture} \color{red}
|
|
sawine@58
|
371 |
}
|
|
sawine@58
|
372 |
\color{black}
|
|
sawine@58
|
373 |
}
|
|
sawine@58
|
374 |
\only<3->{ \setcounter{subfigure}{0}
|
|
sawine@62
|
375 |
\subfigure[Complement automaton \cross]
|
|
sawine@58
|
376 |
{
|
|
sawine@58
|
377 |
\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
|
|
sawine@58
|
378 |
%every state/.style={fill, draw=none, gray, text=white},
|
|
sawine@58
|
379 |
,accepting/.style={fill, gray!50!black, text=white}
|
|
sawine@58
|
380 |
%initial/.style ={gray, text=white}]%, thick]
|
|
sawine@58
|
381 |
]
|
|
sawine@58
|
382 |
\node[state,initial, initial text=, accepting] (q_0) {$q_0$};
|
|
sawine@58
|
383 |
\node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
|
|
sawine@58
|
384 |
\node[state](q_2) [below right of= q_1] {$q_2$};
|
|
sawine@58
|
385 |
\path[->]
|
|
sawine@58
|
386 |
(q_0)
|
|
sawine@58
|
387 |
edge [loop above] node {$b$} ()
|
|
sawine@58
|
388 |
(q_1)
|
|
sawine@58
|
389 |
edge [loop above] node {$a$} ();
|
|
sawine@58
|
390 |
\path[->]
|
|
sawine@58
|
391 |
(q_0) edge node {$a$} (q_1)
|
|
sawine@58
|
392 |
(q_1) edge node {$b$} (q_2)
|
|
sawine@58
|
393 |
(q_2) edge node {$b$} (q_0);
|
|
sawine@58
|
394 |
\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
|
|
sawine@58
|
395 |
\end{tikzpicture} \color{red}
|
|
sawine@58
|
396 |
}
|
|
sawine@58
|
397 |
\color{black}
|
|
sawine@58
|
398 |
}
|
|
sawine@60
|
399 |
%\hspace{10pt}
|
|
sawine@58
|
400 |
\visible<3->{
|
|
sawine@62
|
401 |
\subfigure[Complement automaton \checkmark]
|
|
sawine@58
|
402 |
{
|
|
sawine@58
|
403 |
\label{fig:complement automaton}
|
|
sawine@58
|
404 |
\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
|
|
sawine@58
|
405 |
,accepting/.style={fill, gray!50!black, text=white}]
|
|
sawine@58
|
406 |
\node[state, initial, initial text=] (q_0) {$q_0$};
|
|
sawine@58
|
407 |
\node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
|
|
sawine@58
|
408 |
\node[state, accepting](q_2) [below right of= q_1] {$q_2$};
|
|
sawine@58
|
409 |
\path[->]
|
|
sawine@58
|
410 |
(q_0) edge node {$a$} (q_1)
|
|
sawine@58
|
411 |
edge node {$b$} (q_2)
|
|
sawine@58
|
412 |
edge [loop above] node {$a, b$} ()
|
|
sawine@58
|
413 |
(q_1) edge [loop above] node {$a$} ()
|
|
sawine@58
|
414 |
(q_2)
|
|
sawine@58
|
415 |
edge [loop above] node {$b$} ();
|
|
sawine@58
|
416 |
\end{tikzpicture}\color{green}
|
|
sawine@59
|
417 |
}\\
|
|
sawine@58
|
418 |
\color{black}
|
|
sawine@59
|
419 |
\vspace{20pt}
|
|
sawine@66
|
420 |
Accepts all inputs with finite many $ab$.
|
|
sawine@58
|
421 |
}
|
|
sawine@58
|
422 |
%\caption{Automata from Example \ref{ex:automaton}}
|
|
sawine@58
|
423 |
\end{figure}
|
|
sawine@58
|
424 |
\end{frame}
|
|
sawine@61
|
425 |
\color{black}
|
|
sawine@58
|
426 |
|
|
sawine@58
|
427 |
\begin{frame}
|
|
sawine@58
|
428 |
\frametitle{Automata}
|
|
sawine@56
|
429 |
\framesubtitle{Definition}
|
|
sawine@55
|
430 |
\begin{def:buechi automata}
|
|
sawine@56
|
431 |
A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:
|
|
sawine@55
|
432 |
\begin{itemize}
|
|
sawine@57
|
433 |
\item $\Sigma$ is a finite \emph{alphabet}.
|
|
sawine@57
|
434 |
\item $S$ is a finite set of \emph{states}.
|
|
sawine@57
|
435 |
\item $S_0 \subseteq S$ is the set of \emph{initial states}.
|
|
sawine@57
|
436 |
\item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}.
|
|
sawine@57
|
437 |
\item $F \subseteq S$ is the set of \emph{accepting states}.
|
|
sawine@55
|
438 |
\end{itemize}
|
|
sawine@55
|
439 |
\end{def:buechi automata}
|
|
sawine@55
|
440 |
\end{frame}
|
|
sawine@55
|
441 |
|
|
sawine@55
|
442 |
\begin{frame}
|
|
sawine@56
|
443 |
\frametitle{Automata}
|
|
sawine@56
|
444 |
\framesubtitle{Runs}
|
|
sawine@56
|
445 |
\begin{def:automata runs}
|
|
sawine@56
|
446 |
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
|
|
sawine@56
|
447 |
\begin{itemize}
|
|
sawine@56
|
448 |
\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
|
449 |
\begin{itemize}
|
|
sawine@57
|
450 |
\item $s_0 \in S_0$.
|
|
sawine@57
|
451 |
\item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$.
|
|
sawine@56
|
452 |
\end{itemize}
|
|
sawine@57
|
453 |
\item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$.
|
|
sawine@56
|
454 |
\end{itemize}
|
|
sawine@56
|
455 |
\end{def:automata runs}
|
|
sawine@66
|
456 |
\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}}\]
|
|
sawine@66
|
457 |
\[w_2 = bb\overline{\textcolor{green}{ab}} \implies \rho_2 = q_0q_0\overline{q_1\textcolor{green}{q_2}}\]}
|
|
sawine@56
|
458 |
\end{frame}
|
|
sawine@56
|
459 |
|
|
sawine@56
|
460 |
\begin{frame}
|
|
sawine@56
|
461 |
\frametitle{Automata}
|
|
sawine@56
|
462 |
\framesubtitle{Acceptance}
|
|
sawine@56
|
463 |
\begin{def:inf}
|
|
sawine@56
|
464 |
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
|
|
sawine@56
|
465 |
\begin{itemize}
|
|
sawine@59
|
466 |
\item $\exists^\omega$ denotes the existential quantifier for \emph{infinitely} many occurrences.
|
|
sawine@57
|
467 |
\item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$.
|
|
sawine@56
|
468 |
\end{itemize}
|
|
sawine@56
|
469 |
\end{def:inf}
|
|
sawine@56
|
470 |
|
|
sawine@56
|
471 |
\begin{def:automata acceptance}
|
|
sawine@56
|
472 |
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:
|
|
sawine@56
|
473 |
\begin{itemize}
|
|
sawine@56
|
474 |
\item $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$.
|
|
sawine@59
|
475 |
\item $\A$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is accepting.
|
|
sawine@56
|
476 |
\end{itemize}
|
|
sawine@56
|
477 |
\end{def:automata acceptance}
|
|
sawine@56
|
478 |
\end{frame}
|
|
sawine@56
|
479 |
|
|
sawine@56
|
480 |
\begin{frame}
|
|
sawine@56
|
481 |
\frametitle{Automata}
|
|
sawine@56
|
482 |
\framesubtitle{Language}
|
|
sawine@56
|
483 |
\begin{def:automata language}
|
|
sawine@56
|
484 |
Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:
|
|
sawine@56
|
485 |
\begin{itemize}
|
|
sawine@57
|
486 |
\item $L_\omega(\A) = \{w \in \Sigma^\omega \mid \A \text{ accepts } w\}$, we say $\A$ recognises language $L_\omega(\A)$.
|
|
sawine@57
|
487 |
\item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
|
|
sawine@56
|
488 |
\end{itemize}
|
|
sawine@56
|
489 |
\end{def:automata language}
|
|
sawine@56
|
490 |
\end{frame}
|
|
sawine@56
|
491 |
|
|
sawine@56
|
492 |
\begin{frame}
|
|
sawine@57
|
493 |
\frametitle{Generalised Automata}
|
|
sawine@57
|
494 |
\begin{def:general automata}
|
|
sawine@65
|
495 |
A \emph{generalised B\"uchi automaton} is a tuple $\A_G = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:
|
|
sawine@57
|
496 |
\begin{itemize}
|
|
sawine@57
|
497 |
\item $\{F_i\}$ is a finite set of sets for a given $k$.
|
|
sawine@57
|
498 |
\item Each $F_i \subseteq S$ is a finite set of accepting states.
|
|
sawine@57
|
499 |
\end{itemize}
|
|
sawine@57
|
500 |
\end{def:general automata}
|
|
sawine@57
|
501 |
|
|
sawine@57
|
502 |
\begin{def:general acceptance}
|
|
sawine@65
|
503 |
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$:
|
|
sawine@57
|
504 |
\begin{itemize}
|
|
sawine@57
|
505 |
\item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$.
|
|
sawine@65
|
506 |
\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.
|
|
sawine@57
|
507 |
\end{itemize}
|
|
sawine@57
|
508 |
\end{def:general acceptance}
|
|
sawine@57
|
509 |
|
|
sawine@57
|
510 |
\begin{prop:general equiv}
|
|
sawine@65
|
511 |
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:
|
|
sawine@65
|
512 |
\[L_\omega(\A_G) = \bigcap_{i < k} L_\omega(\A_i)\]
|
|
sawine@57
|
513 |
\end{prop:general equiv}
|
|
sawine@57
|
514 |
\end{frame}
|
|
sawine@57
|
515 |
|
|
sawine@65
|
516 |
\begin{frame}
|
|
sawine@68
|
517 |
\frametitle{Automata Construction}
|
|
sawine@68
|
518 |
\framesubtitle{Formula automata}
|
|
sawine@68
|
519 |
\begin{center}
|
|
sawine@68
|
520 |
Model $\M_\varphi$ for formula $\varphi$\\
|
|
sawine@68
|
521 |
$\Downarrow$\\
|
|
sawine@68
|
522 |
Closure $CL(\varphi)$ of $\varphi$\\
|
|
sawine@68
|
523 |
$\Downarrow$\\
|
|
sawine@68
|
524 |
Automaton $\A_\varphi$ for $\varphi$\\
|
|
sawine@68
|
525 |
\vspace{20pt}
|
|
sawine@68
|
526 |
\textcolor{red}{On-the-fly methods} \`a la Gerth et al.
|
|
sawine@68
|
527 |
\end{center}
|
|
sawine@68
|
528 |
\end{frame}
|
|
sawine@68
|
529 |
|
|
sawine@68
|
530 |
\begin{frame}
|
|
sawine@68
|
531 |
\frametitle{Automata Construction}
|
|
sawine@68
|
532 |
\framesubtitle{System automata}
|
|
sawine@68
|
533 |
\begin{center}
|
|
sawine@68
|
534 |
Model $\M_\varphi$ for formula $\varphi$\\
|
|
sawine@68
|
535 |
$\Downarrow$\\
|
|
sawine@68
|
536 |
Closure $CL(\varphi)$ of $\varphi$\\
|
|
sawine@68
|
537 |
$\Downarrow$\\
|
|
sawine@68
|
538 |
Automaton $\A_\varphi$ for $\varphi$
|
|
sawine@68
|
539 |
\end{center}
|
|
sawine@68
|
540 |
\end{frame}
|
|
sawine@68
|
541 |
|
|
sawine@68
|
542 |
\begin{frame}
|
|
sawine@55
|
543 |
\frametitle{Model Checking}
|
|
sawine@67
|
544 |
\framesubtitle{Definition}
|
|
sawine@66
|
545 |
\begin{thm:model checking}
|
|
sawine@66
|
546 |
\label{thm:model checking}
|
|
sawine@66
|
547 |
Let $\A_P$ be the automaton for program $P$ and let $\A_\varphi$ be the automaton for formula $\varphi$.\\
|
|
sawine@66
|
548 |
P satisfies $\varphi$ iff:
|
|
sawine@66
|
549 |
\begin{itemize}
|
|
sawine@66
|
550 |
\item $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$.
|
|
sawine@66
|
551 |
\item $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.
|
|
sawine@66
|
552 |
\end{itemize}
|
|
sawine@66
|
553 |
\end{thm:model checking}
|
|
sawine@55
|
554 |
\end{frame}
|
|
sawine@55
|
555 |
|
|
sawine@55
|
556 |
\begin{frame}[allowframebreaks]
|
|
sawine@55
|
557 |
\frametitle<presentation>{Literature}
|
|
sawine@55
|
558 |
\begin{thebibliography}{10}
|
|
sawine@55
|
559 |
|
|
sawine@55
|
560 |
\beamertemplatearticlebibitems
|
|
sawine@55
|
561 |
\bibitem{ref:ltl&büchi}
|
|
sawine@55
|
562 |
Madhavan Mukund.
|
|
sawine@55
|
563 |
\newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.
|
|
sawine@55
|
564 |
\newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
|
|
sawine@55
|
565 |
|
|
sawine@55
|
566 |
\beamertemplatearticlebibitems
|
|
sawine@55
|
567 |
\bibitem{ref:alternating verification}
|
|
sawine@55
|
568 |
Moshe Y. Vardi.
|
|
sawine@55
|
569 |
\newblock {\em Alternating Automata and Program Verification}.
|
|
sawine@55
|
570 |
\newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
|
|
sawine@55
|
571 |
|
|
sawine@55
|
572 |
\beamertemplatebookbibitems
|
|
sawine@55
|
573 |
\bibitem{ref:handbook}
|
|
sawine@55
|
574 |
Patrick Blackburn and Frank Wolter and Johan van Benthem.
|
|
sawine@55
|
575 |
\newblock {\em Handbook of Modal Logic}.
|
|
sawine@55
|
576 |
\newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.
|
|
sawine@55
|
577 |
|
|
sawine@55
|
578 |
\end{thebibliography}
|
|
sawine@55
|
579 |
\end{frame}
|
|
sawine@55
|
580 |
|
|
sawine@55
|
581 |
\end{document}
|