model_checking_seminar: slides/src/slides.tex@1da31f35eae3

     1 \documentclass[9pt]{beamer}

     2 \usetheme{Boadilla}

     3 \usecolortheme{dove}

     4 \usecolortheme{orchid}

     5 \usecolortheme{dolphin}

     6 %\usecolortheme{seagull}

     8 \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}

     9 \usepackage{pifont}

    10 \usepackage{xcolor}

    11 \usepackage{ulem}

    12 \usepackage{graphics}

    13 \usepackage{tikz}

    14 \usetikzlibrary{automata}

    15 \usepackage{subfigure}

    17 \renewcommand{\emph}{\textit}

    18 \renewcommand{\em}{\it}

    20 \newcommand{\cross}{\ding{55}}

    21 \newcommand{\M}{\mathcal{M}}

    22 \newcommand{\N}{\mathbb{N}_0}

    23 \newcommand{\F}{\mathcal{F}}

    24 \newcommand{\Fs}{\mathbb{F}}

    25 \newcommand{\Prop}{\mathcal{P}}

    26 \newcommand{\A}{\mathcal{A}}

    27 \newcommand{\X}{\mathcal{X}}

    28 \newcommand{\U}{\mathcal{U}}

    29 \newcommand{\V}{\mathcal{V}}

    30 \newcommand{\dnf}{\mathsf{dnf}}

    31 \newcommand{\consq}{\mathsf{consq}}

    33 \theoremstyle{definition} %plain, definition, remark, proof, corollary

    34 \newtheorem*{def:finite words}{Finite words}

    35 \newtheorem*{def:infinite words}{Infinite words}

    36 \newtheorem*{def:regular languages}{Regular languages}

    37 \newtheorem*{def:regular languages closure}{Regular closure}

    38 \newtheorem*{def:omega regular languages}{$\omega$-regular languages}

    39 \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}

    40 \newtheorem*{def:buechi automata}{Automaton}

    41 \newtheorem*{def:automata runs}{Run}

    42 \newtheorem*{def:inf}{Infinite occurrences}

    43 \newtheorem*{def:automata acceptance}{Acceptance}

    44 \newtheorem*{def:automata language}{Recognised language}

    45 \newtheorem*{def:general automata}{Generalised automaton}

    46 \newtheorem*{def:general acceptance}{Acceptance}

    47 \newtheorem*{def:syntax}{Syntax}

    50 \newtheorem*{def:vocabulary}{Vocabulary}

    51 \newtheorem*{def:frames}{Frame}

    52 \newtheorem*{def:models}{Model}

    53 \newtheorem*{def:satisfiability}{Satisfiability}

    54 \newtheorem*{def:fs closure}{Closure}

    55 \newtheorem*{def:atoms}{Atoms}

    56 \newtheorem*{def:rep function}{Representation function}

    57 \newtheorem*{def:next}{Next function}

    58 \newtheorem*{def:dnf}{Disjunctive normal form}

    59 \newtheorem*{def:positive formulae}{Positive formulae}

    60 \newtheorem*{def:consq}{Logical consequences}

    61 \newtheorem*{def:partial automata}{Partial automata}

    63 \theoremstyle{plain}

    64 \newtheorem{prop:vocabulary sat}{Proposition}[section]

    65 \newtheorem{prop:general equiv}{Proposition}[section]

    66 \newtheorem{prop:computation set=language}{Proposition}[section]

    68 \theoremstyle{plain}

    69 \newtheorem{thm:model language}{Theorem}[section]

    70 \newtheorem{cor:mod=model language}{Corollary}[thm:model language]

    71 \newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}

    72 \newtheorem{thm:model checking}{Theorem}[section]

    73 \newtheorem{lem:dnf}{Lemma}[section]

    74 \newtheorem{lem:consq}[lem:dnf]{Lemma}

    76 \title[Algorithmic Verification]{Algorithmic Verification of Reactive Systems}

    77 \author{Eugen Sawin}

    78 \institute[University of Freiburg]

    79 {

    80   Research Group for Foundations in Artificial Intelligence\\

    81   Computer Science Department\\

    82   University of Freiburg

    83 }

    84 \date[SS 2011]{Seminar: Automata Constructions in Model Checking}

    85 \subject{Model Checking}

    87 \begin{document}

    88 \frame{\titlepage}

    90 \begin{frame}

    91 \frametitle{Motivation}

    92 \framesubtitle{Model Checking 1/2}

    93 \begin{center}

    94 %\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}

    95 \[\M \models \varphi\]

    96 \end{center}

    97 \end{frame}

    99 \begin{frame}

   100 \frametitle{Motivation}

   101 \framesubtitle{Model Checking 2/2}

   102 \begin{center}

   103 Given a program $P$ and specification $\varphi$:\\

   104 \colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}

   105 \end{center}

   106 \end{frame}

   108 \begin{frame}

   109 \frametitle{Motivation}

   110 \framesubtitle{Industry}

   111 \begin{figure}

   112 \centering

   113 \subfigure{\includegraphics[width=70pt,height=50pt]{images/intel.jpg}}

   114 \subfigure{\includegraphics[width=70pt,height=50pt]{images/airbag.jpg}}

   115 \subfigure{\includegraphics[width=70pt,height=50pt]{images/atc.jpg}}

   116 \end{figure}

   117 \end{frame}

   119 {

   120 \setbeamercolor{normal text}{bg=black, fg=white}

   121 \setbeamercolor{frametitle}{fg=white!30!black}

   122 \usebeamercolor*{normal text}

   123 \usebeamercolor*{frametitle}

   124 \begin{frame}

   125 \frametitle{Linear Temporal Logic}

   126 \framesubtitle{Motivation 1/2}

   127 \begin{center}

   128 ``It is dark.''\\

   129 \visible<2->{``It is \emph{always} dark.''\\}

   130 \visible<3->{``It is \emph{currently} dark.''\\}

   131 \visible<4->{``It will \emph{eventually} be dark.''\\}

   132 \visible<5->{``It is dark \emph{until} someone puts the light on.''}

   133 \end{center}

   134 \end{frame}

   135 }

   137 \begin{frame}

   138 \frametitle{Linear Temporal Logic}

   139 \framesubtitle{Motivation 2/2}

   140 \begin{center}

   141 \only<1->{

   142 \color{white}

   143 \colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\

   144 \visible<2->{

   145 \colorbox{black}{\makebox(50,10){$p_0$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$p_1$}}}

   146 }

   147 \end{center}

   148 \end{frame}

   150 \begin{frame}

   151 \frametitle{Linear Temporal Logic}

   152 \framesubtitle{Syntax}

   153 \begin{def:syntax}

   154 Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions:

   155 \[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]

   156 \begin{itemize}

   157 \item $\neg, \lor$ corresponds to the Boolean \emph{negation} and \emph{disjunction}.

   158 \item $\X$ reads \emph{next}.

   159 \item $\U$ reads \emph{until}.

   160 \end{itemize}

   161 \end{def:syntax}

   162 \end{frame}

   164 \begin{frame}

   165 \frametitle{Linear Temporal Logic}

   166 \framesubtitle{Semantics}

   167 \begin{def:frames}

   168 An LTL-\emph{frame} is a tuple $\F = (S, R)$:

   169 \begin{itemize}

   170 \item $S = \{s_i \mid i \in \N\}$ is the set of states.

   171 \item $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ is the accessibility relation.

   172 \end{itemize}

   173 \end{def:frames}

   175 \begin{def:models}

   176 An LTL-\emph{model} is a tuple $\M = (\F, V)$:

   177 \begin{itemize}

   178 \item $\F$ is a \emph{frame}.

   179 \item $V: S \to 2^\Prop$ is a \emph{valuation function}.

   180 \item Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.

   181 \end{itemize}

   182 \end{def:models}

   183 \end{frame}

   185 \begin{frame}

   186 \frametitle{Linear Temporal Logic}

   187 \framesubtitle{Model Example}

   188 \begin{figure}

   189 \centering

   190 \begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth

   191     ,accepting/.style={fill, gray!50!black, text=white}]

   192 \node[state, initial, initial text=] (s_0) {$\{p_0\}$};

   193 \path (s_0) [late options={label=below:$s_0$}];

   194 \node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$};

   195 \path (s_1) [late options={label=below:$s_1$}];

   196 \node[state] (s_2) [right of= s_1] {$\{p_1\}$};

   197 \path (s_2) [late options={label=below:$s_2$}];

   198 \node[state] (s_i) [right of= s_2] {$\{p_1\}$};

   199 \path (s_i) [late options={label=below:$s_i$}];

   200 \path[->]

   201 (s_0) edge node {$R$} (s_1)

   202 (s_1) edge node {$R$} (s_2);

   203 \path[dashed,->]

   204 (s_2) edge node {$R$} (s_i);

   205 \end{tikzpicture}

   206 \end{figure}

   207 \end{frame}

   209 \begin{frame}

   210 \frametitle{Linear Temporal Logic}

   211 \framesubtitle{Satisfiability}

   212 \begin{def:satisfiability}

   213 A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:

   214 \begin{itemize}

   215 \item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$

   216 \item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$

   217 \item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$

   218 \item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$

   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$

   220 \end{itemize}

   221 \end{def:satisfiability}

   222 \end{frame}

   224 \begin{frame}

   225 \frametitle{Infinity}

   226 \framesubtitle{Word as function}

   227 \begin{figure}

   228 \centering

   229 \begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth

   230     ,accepting/.style={fill, gray!50!black, text=white}]

   231 \node[state, initial, initial text=] (s_0) {$a$};

   232 \node[state] (s_1) [right of= s_0] {$b$};

   233 \node[state] (s_2) [right of= s_1] {$a$};

   234 \node[state] (s_i) [right of= s_2] {$a$};

   235 \path[->]

   236 (s_0) edge node {} (s_1)

   237 (s_1) edge node {} (s_2);

   238 \path[dashed,->]

   239 (s_2) edge node {} (s_i);

   240 \end{tikzpicture}

   241 \end{figure}

   242 \end{frame}

   244 \begin{frame}

   245 \frametitle{Automata}

   246 \framesubtitle{Example 1/2}

   247 \begin{figure}

   248 \centering

   249 \only<-3>{

   250 \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth

   251     %every state/.style={fill, draw=none, gray, text=white},

   252     ,accepting/.style={fill, gray!50!black, text=white}

   253     %initial/.style ={gray, text=white}]%,  thick]

   254     ]

   255 \node[state,initial, initial text=] (q_0) {$q_0$};

   256 \node[state] (q_1) [above right of= q_0] {$q_1$};

   257 \node[state,accepting](q_2) [below right of= q_1] {$q_2$};

   258 \path[->]

   259 (q_0) edge node {$a$} (q_1)

   260   edge [loop above] node {$b$} ()

   261 (q_1) edge node {$b$} (q_2)

   262   edge [loop above] node {$a$} ()

   263 (q_2) %edge node {$a$} (q_1)

   264   edge node {$b$} (q_0);

   265 \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);

   266 \end{tikzpicture}\\

   267 \vspace{10pt}

   268 \visible<2-3>{$w_1 = \overline{bbaa} \implies \rho_1 = q_0q_0\overline{q_0q_1q_1q_2}$}\\

   269 \visible<3>{$w_2 = bb\overline{ab} \implies \rho_2 = q_0q_0\overline{q_1q_2}$}\\

   270 \vspace{10pt}

   271 \visible<4>{Accepts all inputs with infinite occurrences of $ab$.}

   272 }

   274 \only<4>{

   275 \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth

   276     %every state/.style={fill, draw=none, gray, text=white},

   277     ,accepting/.style={fill, gray!50!black, text=white}

   278     %initial/.style ={gray, text=white}]%,  thick]

   279     ]

   280 \node[state,initial, initial text=] (q_0) {$q_0$};

   281 \node[state] (q_1) [above right of= q_0] {$q_1$};

   282 \node[state,accepting](q_2) [below right of= q_1] {$q_2$};

   283 \path[->]

   284 (q_0)

   285   edge [loop above] node {$b$} ()

   286 (q_1)

   287   edge [loop above] node {$a$} ()

   288 (q_2) %edge node {$a$} (q_1)

   289   edge node {$b$} (q_0);

   290 \color{green}

   291 \path[->]

   292 (q_0) edge node {$a$} (q_1)

   293 (q_1) edge node {$b$} (q_2);

   294 \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);

   295 \end{tikzpicture}\\

   296 \color{black}

   297 \vspace{10pt}

   298 \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}}$}\\

   299 \visible<3->{$w_2 = bb\overline{\textcolor{green}{ab}} \implies \rho_2 = q_0q_0\overline{q_1\textcolor{green}{q_2}}$}\\

   300 \vspace{10pt}

   301 \visible<4>{Accepts all inputs with infinite occurrences of $ab$.}

   302 }

   303 %Automaton $\A_1$

   304 \end{figure}

   305 \end{frame}

   307 \begin{frame}

   308 \frametitle{Automata}

   309 \framesubtitle{Example 2/2 (Complement)}

   310 \begin{figure}

   311 \centering

   312 \only<1>{

   313   \subfigure

   314             {

   315               \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth

   316                   %every state/.style={fill, draw=none, gray, text=white},

   317                   ,accepting/.style={fill, gray!50!black, text=white}

   318                   %initial/.style ={gray, text=white}]%,  thick]

   319                 ]

   320                 \node[state,initial, initial text=, accepting] (q_0) {$q_0$};

   321                 \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};

   322                 \node[state](q_2) [below right of= q_1] {$q_2$};

   323                 \path[->]

   324                 (q_0) edge node {$a$} (q_1)

   325                 edge [loop above] node {$b$} ()

   326                 (q_1) edge node {$b$} (q_2)

   327                 edge [loop above] node {$a$} ()

   328                 (q_2) %edge node {$a$} (q_1)

   329                 edge node {$b$} (q_0);

   330                 \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);

   331               \end{tikzpicture}

   332             }

   333 }

   334 \only<2>{

   335   \subfigure

   336             {

   337               \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth

   338                   %every state/.style={fill, draw=none, gray, text=white},

   339                   ,accepting/.style={fill, gray!50!black, text=white}

   340                   %initial/.style ={gray, text=white}]%,  thick]

   341                 ]

   342                 \node[state,initial, initial text=, accepting] (q_0) {$q_0$};

   343                 \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};

   344                 \node[state](q_2) [below right of= q_1] {$q_2$};

   345                 \path[->]

   346                 (q_0)

   347                 edge [loop above] node {$b$} ()

   348                 (q_1)

   349                 edge [loop above] node {$a$} ();

   350                 \color{red}

   351                 \path[->]

   352                 (q_0) edge node {$a$} (q_1)

   353                 (q_1) edge node {$b$} (q_2)

   354                 (q_2) edge node {$b$} (q_0);

   355                 \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);

   356               \end{tikzpicture}  \color{red}

   357             }

   358  \color{black}

   359 }

   360 \only<3->{ \setcounter{subfigure}{0}

   361   \subfigure[Complement automaton \cross]

   362             {

   363               \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth

   364                   %every state/.style={fill, draw=none, gray, text=white},

   365                   ,accepting/.style={fill, gray!50!black, text=white}

   366                   %initial/.style ={gray, text=white}]%,  thick]

   367                 ]

   368                 \node[state,initial, initial text=, accepting] (q_0) {$q_0$};

   369                 \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};

   370                 \node[state](q_2) [below right of= q_1] {$q_2$};

   371                 \path[->]

   372                 (q_0)

   373                 edge [loop above] node {$b$} ()

   374                 (q_1)

   375                 edge [loop above] node {$a$} ();

   376                 \path[->]

   377                 (q_0) edge node {$a$} (q_1)

   378                 (q_1) edge node {$b$} (q_2)

   379                 (q_2) edge node {$b$} (q_0);

   380                 \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);

   381               \end{tikzpicture}  \color{red}

   382             }

   383  \color{black}

   384 }

   385 %\hspace{10pt}

   386 \visible<3->{

   387   \subfigure[Complement automaton \checkmark]

   388             {

   389               \label{fig:complement automaton}

   390               \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth

   391                   ,accepting/.style={fill, gray!50!black, text=white}]

   392                 \node[state, initial, initial text=] (q_0) {$q_0$};

   393                 \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};

   394                 \node[state, accepting](q_2) [below right of= q_1] {$q_2$};

   395                 \path[->]

   396                 (q_0) edge node {$a$} (q_1)

   397                 edge node {$b$} (q_2)

   398                 edge [loop above] node {$a, b$} ()

   399                 (q_1) edge [loop above] node {$a$} ()

   400                 (q_2)

   401                 edge [loop above] node {$b$} ();

   402               \end{tikzpicture}\color{green}

   403             }\\

   404 \color{black}

   405 \vspace{20pt}

   406 Accepts all inputs with finite many $ab$.

   407 }

   408 %\caption{Automata from Example \ref{ex:automaton}}

   409 \end{figure}

   410 \end{frame}

   411 \color{black}

   413 \begin{frame}

   414 \frametitle{Automata}

   415 \framesubtitle{Definition}

   416 \begin{def:buechi automata}

   417 A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:

   418 \begin{itemize}

   419 \item $\Sigma$ is a finite \emph{alphabet}.

   420 \item $S$ is a finite set of \emph{states}.

   421 \item $S_0 \subseteq S$ is the set of \emph{initial states}.

   422 \item $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}.

   423 \item $F \subseteq S$ is the set of \emph{accepting states}.

   424 \end{itemize}

   425 \end{def:buechi automata}

   426 \end{frame}

   428 \begin{frame}

   429 \frametitle{Automata}

   430 \framesubtitle{Runs}

   431 \begin{def:automata runs}

   432 Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:

   433 \begin{itemize}

   434 \item A run $\rho$ of $\A$ on an infinite word $w = a_0,a_1,...$ is a sequence $\rho = s_0,s_1,...$:

   435 \begin{itemize}

   436 \item $s_0 \in S_0$.

   437 \item $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$.

   438 \end{itemize}

   439 \item Alternative view of a run $\rho$ as a function $\rho : \N \to S$, with $\rho(i) = s_i$.

   440 \end{itemize}

   441 \end{def:automata runs}

   442 \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}}\]

   443 \[w_2 = bb\overline{\textcolor{green}{ab}} \implies \rho_2 = q_0q_0\overline{q_1\textcolor{green}{q_2}}\]}

   444 \end{frame}

   446 \begin{frame}

   447 \frametitle{Automata}

   448 \framesubtitle{Acceptance}

   449 \begin{def:inf}

   450 Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:

   451 \begin{itemize}

   452 \item $\exists^\omega$ denotes the existential quantifier for \emph{infinitely} many occurrences.

   453 \item $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$.

   454 \end{itemize}

   455 \end{def:inf}

   457 \begin{def:automata acceptance}

   458 Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $\A$:

   459 \begin{itemize}

   460 \item $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$.

   461 \item $\A$ \emph{accepts} an input word $w$ iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is accepting.

   462 \end{itemize}

   463 \end{def:automata acceptance}

   464 \end{frame}

   466 \begin{frame}

   467 \frametitle{Automata}

   468 \framesubtitle{Language}

   469 \begin{def:automata language}

   470 Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton:

   471 \begin{itemize}

   472 \item $L_\omega(\A) = \{w \in \Sigma^\omega \mid \A \text{ accepts } w\}$, we say $\A$ recognises language $L_\omega(\A)$.

   473 \item Language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.

   474 \end{itemize}

   475 \end{def:automata language}

   476 \end{frame}

   478 \begin{frame}

   479 \frametitle{Generalised Automata}

   480 \begin{def:general automata}

   481 A \emph{generalised B\"uchi automaton} is a tuple $\A_G = (\Sigma, S, S_0, \Delta, \{F_i\}_{i<k})$:

   482 \begin{itemize}

   483 \item $\{F_i\}$ is a finite set of sets for a given $k$.

   484 \item Each $F_i \subseteq S$ is a finite set of accepting states.

   485 \end{itemize}

   486 \end{def:general automata}

   488 \begin{def:general acceptance}

   489 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$:

   490 \begin{itemize}

   491 \item $\rho$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$.

   492 \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.

   493 \end{itemize}

   494 \end{def:general acceptance}

   496 \begin{prop:general equiv}

   497 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:

   498 \[L_\omega(\A_G) = \bigcap_{i < k} L_\omega(\A_i)\]

   499 \end{prop:general equiv}

   500 \end{frame}

   502 \begin{frame}

   503 \frametitle{Automata Construction}

   504 \framesubtitle{Formula automata}

   505 \begin{center}

   506 Model $\M_\varphi$ for formula $\varphi$\\

   507 $\Downarrow$\\

   508 Closure $CL(\varphi)$ of $\varphi$\\

   509 $\Downarrow$\\

   510 Automaton $\A_\varphi$ for $\varphi$\\

   511 \vspace{20pt}

   512 \textcolor{red}{On-the-fly methods} \`a la Gerth et al.

   513 \end{center}

   514 \end{frame}

   516 \begin{frame}

   517 \frametitle{Automata Construction}

   518 \framesubtitle{System automata}

   519 \begin{center}

   520 Model $\M_\varphi$ for formula $\varphi$\\

   521 $\Downarrow$\\

   522 Closure $CL(\varphi)$ of $\varphi$\\

   523 $\Downarrow$\\

   524 Automaton $\A_\varphi$ for $\varphi$

   525 \end{center}

   526 \end{frame}

   528 \begin{frame}

   529 \frametitle{Model Checking}

   530 \framesubtitle{Definition}

   531 \begin{thm:model checking}

   532 \label{thm:model checking}

   533 Let $\A_P$ be the automaton for program $P$ and let $\A_\varphi$ be the automaton for formula $\varphi$.\\

   534 P satisfies $\varphi$ iff:

   535 \begin{itemize}

   536 \item $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$.

   537 \item $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.

   538 \end{itemize}

   539 \end{thm:model checking}

   540 \end{frame}

   542 \begin{frame}

   543 \frametitle{On-the-fly Methods}

   544 \framesubtitle{A bit more information about this}

   546 \end{frame}

   548 \begin{frame}[allowframebreaks]

   549 \frametitle<presentation>{Literature}

   550 \begin{thebibliography}{10}

   552 \beamertemplatearticlebibitems

   553 \bibitem{ref:ltl&büchi}

   554 Madhavan Mukund.

   555 \newblock {\em Linear-Time Temporal Logic and B\"uchi Automata}.

   556 \newblock Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.

   558 \beamertemplatearticlebibitems

   559 \bibitem{ref:alternating verification}

   560 Moshe Y. Vardi.

   561 \newblock {\em Alternating Automata and Program Verification}.

   562 \newblock Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.

   564 \beamertemplatebookbibitems

   565 \bibitem{ref:handbook}

   566 Patrick Blackburn and Frank Wolter and Johan van Benthem.

   567 \newblock {\em Handbook of Modal Logic}.

   568 \newblock 3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.

   570 \end{thebibliography}

   571 \end{frame}

   573 \end{document}

author	Eugen Sawin <sawine@me73.com>
	Fri, 22 Jul 2011 15:52:20 +0200
changeset 68	1da31f35eae3
parent 67	46709047b260
child 69	3ebfd8683b18
permissions	-rw-r--r--