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