model_checking_seminar: slides/src/slides.tex@9938ea8ed067

     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{multicol}

    11 \usepackage{xcolor}

    12 \usepackage{ulem}

    13 \usepackage{graphics}

    14 \usepackage{tikz}

    15 \usetikzlibrary{automata}

    16 \usepackage{subfigure}

    18 \renewcommand{\emph}{\textit}

    19 \renewcommand{\em}{\it}

    21 \newcommand{\cross}{\ding{55}}

    22 \newcommand{\M}{\mathcal{M}}

    23 \newcommand{\N}{\mathbb{N}_0}

    24 \newcommand{\F}{\mathcal{F}}

    25 \newcommand{\Fs}{\mathbb{F}}

    26 \newcommand{\Prop}{\mathcal{P}}

    27 \newcommand{\A}{\mathcal{A}}

    28 \newcommand{\X}{\mathcal{X}}

    29 \newcommand{\U}{\mathcal{U}}

    30 \newcommand{\V}{\mathcal{V}}

    31 \newcommand{\dnf}{\mathsf{dnf}}

    32 \newcommand{\consq}{\mathsf{consq}}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    49 \newtheorem*{def:derived syntax}{Derived connectives}

    50 \newtheorem*{def:program}{Program}

    51 \newtheorem*{def:program automaton}{System automaton}

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

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

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

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

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

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

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

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

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

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

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

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

    66 \theoremstyle{plain}

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

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

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

    71 \theoremstyle{plain}

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

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

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

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

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

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

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

    80 \author{Eugen Sawin}

    81 \institute[University of Freiburg]

    82 {

    83   Research Group for Foundations in Artificial Intelligence\\

    84   Computer Science Department\\

    85   University of Freiburg

    86 }

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

    88 \subject{Model Checking}

    90 \begin{document}

    91 \frame{\titlepage}

    93 \begin{frame}

    94 \frametitle{Motivation}

    95 \framesubtitle{Model Checking 1/2}

    96 \begin{center}

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

    98 \[\M \models \varphi\]

    99 \end{center}

   100 \end{frame}

   102 \begin{frame}

   103 \frametitle{Motivation}

   104 \framesubtitle{Model Checking 2/2}

   105 \begin{center}

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

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

   108 \end{center}

   109 \end{frame}

   111 \begin{frame}

   112 \frametitle{Motivation}

   113 \framesubtitle{Industry}

   114 \begin{figure}

   115 \centering

   116 \only<1>{

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

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

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

   120 }

   121 \only<2>{

   122 \subfigure{\includegraphics[width=35pt,height=20pt]{images/sun.jpg}}

   123 \subfigure{\includegraphics[width=20pt,height=20pt]{images/hp.jpg}}

   124 \subfigure{\includegraphics[width=40pt,height=20pt]{images/siemens.jpg}}

   125 \subfigure{\includegraphics[width=15pt,height=20pt]{images/att.jpg}}

   126 %\subfigure{\includegraphics[width=20pt,height=20pt]{images/motorola.jpg}}

   127 \subfigure{\includegraphics[width=20pt,height=20pt]{images/sgi.jpg}}

   128 \subfigure{\includegraphics[width=25pt,height=20pt]{images/fujitsu.jpg}}

   129 \subfigure{\includegraphics[width=20pt,height=18pt]{images/nec.jpg}}

   130 \subfigure{\includegraphics[width=20pt,height=20pt]{images/intel2.jpg}}

   131 \subfigure{\includegraphics[width=25pt,height=20pt]{images/ibm.jpg}}

   132 }

   133 \end{figure}

   134 \end{frame}

   136 {

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

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

   139 \usebeamercolor*{normal text}

   140 \usebeamercolor*{frametitle}

   141 \begin{frame}

   142 \frametitle{Linear Temporal Logic}

   143 \framesubtitle{Natural language 1/2}

   144 \begin{center}

   145 ``It is dark.''\\

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

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

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

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

   150 \end{center}

   151 \end{frame}

   152 }

   154 \begin{frame}

   155 \frametitle{Linear Temporal Logic}

   156 \framesubtitle{Natural language 2/2}

   157 \begin{center}

   158 \only<1->{

   159 \color{white}

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

   161 \visible<2->{

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

   163 }

   164 \end{center}

   165 \end{frame}

   167 \begin{frame}

   168 \frametitle{Linear Temporal Logic}

   169 \framesubtitle{Syntax}

   170 \begin{def:syntax}

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

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

   173 \begin{itemize}

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

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

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

   177 \end{itemize}

   178 \end{def:syntax}

   180 \visible<2>{

   181 \begin{def:derived syntax}

   182 Let $\varphi$ and $\psi$ be formulae:

   183 \begin{multicols}{2}

   184 \begin{itemize}

   185 \item $\top \equiv p \lor \neg p$ for $p \in \Prop$

   186 \item $\bot \equiv \neg \top$

   187 \item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$

   188 \item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$

   189 \item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$

   190 \item $\Diamond \varphi \equiv \top \U \varphi$

   191 \item $\Box \varphi \equiv \neg \Diamond \neg \varphi$

   192 \end{itemize}

   193 \end{multicols}

   194 \end{def:derived syntax}

   195 }

   196 \end{frame}

   198 \begin{frame}

   199 \frametitle{Linear Temporal Logic}

   200 \framesubtitle{Semantics}

   201 \begin{def:frames}

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

   203 \begin{itemize}

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

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

   206 \end{itemize}

   207 \end{def:frames}

   209 \begin{def:models}

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

   211 \begin{itemize}

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

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

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

   215 \end{itemize}

   216 \end{def:models}

   217 \end{frame}

   219 \begin{frame}

   220 \frametitle{Linear Temporal Logic}

   221 \framesubtitle{Model Example}

   222 \begin{figure}

   223 \centering

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

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

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

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

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

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

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

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

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

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

   234 \path[->]

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

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

   237 \path[dashed,->]

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

   239 \end{tikzpicture}

   240 \end{figure}

   241 \end{frame}

   243 \begin{frame}

   244 \frametitle{Linear Temporal Logic}

   245 \framesubtitle{Satisfiability}

   246 \begin{def:satisfiability}

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

   248 \begin{itemize}

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

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

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

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

   253 \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$

   254 \end{itemize}

   255 \end{def:satisfiability}

   256 \end{frame}

   258 \begin{frame}

   259 \frametitle{Reactive Systems}

   260 \framesubtitle{Infinite inputs}

   261 \begin{center}

   262 \begin{figure}

   263 \setcounter{subfigure}{0}

   264 \subfigure[Terminating program]{

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

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

   267 \node[state, initial, initial text=$input$] (p) {$P$};

   268 \coordinate (b) at (1,0);

   269         %\coordinate (b) at ($(a)+1/2*(3,3)$);

   270 \draw (p) edge[->] node[right] {$\hspace{8pt}output$} (b);

   271 %\draw[->] (p) -- (b);

   272 \end{tikzpicture}

   273 }

   274 \hspace{10pt}

   275 \visible<2>{\subfigure[Reactive program]{

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

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

   278 \node[state, initial, initial text=$event$] (p) {$RP$};

   279 \coordinate (b) at (1.1,0);

   280         %\coordinate (b) at ($(a)+1/2*(3,3)$);

   281 \path[->]

   282 (p) edge [loop right] node {$action$} ();

   283 \end{tikzpicture}

   284 }}

   285 \end{figure}

   286 \end{center}

   287 \end{frame}

   289 \begin{frame}

   290 \frametitle{Automata}

   291 \framesubtitle{Example 1/2}

   292 \begin{figure}

   293 \centering

   294 \only<-3>{

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

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

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

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

   299     ]

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

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

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

   303 \path[->]

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

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

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

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

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

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

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

   311 \end{tikzpicture}\\

   312 \vspace{10pt}

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

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

   315 \vspace{10pt}

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

   317 }

   319 \only<4>{

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

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

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

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

   324     ]

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

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

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

   328 \path[->]

   329 (q_0)

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

   331 (q_1)

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

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

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

   335 \color{green}

   336 \path[->]

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

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

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

   340 \end{tikzpicture}\\

   341 \color{black}

   342 \vspace{10pt}

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

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

   345 \vspace{10pt}

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

   347 }

   348 %Automaton $\A_1$

   349 \end{figure}

   350 \end{frame}

   352 \begin{frame}

   353 \frametitle{Automata}

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

   355 \begin{figure}

   356 \centering

   357 \only<1>{

   358   \subfigure

   359             {

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

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

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

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

   364                 ]

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

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

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

   368                 \path[->]

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

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

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

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

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

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

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

   376               \end{tikzpicture}

   377             }

   378 }

   379 \only<2>{

   380   \subfigure

   381             {

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

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

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

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

   386                 ]

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

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

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

   390                 \path[->]

   391                 (q_0)

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

   393                 (q_1)

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

   395                 \color{red}

   396                 \path[->]

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

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

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

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

   401               \end{tikzpicture}  \color{red}

   402             }

   403  \color{black}

   404 }

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

   406   \subfigure[Complement automaton \cross]

   407             {

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

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

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

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

   412                 ]

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

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

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

   416                 \path[->]

   417                 (q_0)

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

   419                 (q_1)

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

   421                 \path[->]

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

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

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

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

   426               \end{tikzpicture}  \color{red}

   427             }

   428  \color{black}

   429 }

   430 %\hspace{10pt}

   431 \visible<3->{

   432   \subfigure[Complement automaton \checkmark]

   433             {

   434               \label{fig:complement automaton}

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

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

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

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

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

   440                 \path[->]

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

   442                 edge node {$b$} (q_2)

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

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

   445                 (q_2)

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

   447               \end{tikzpicture}\color{green}

   448             }\\

   449 \color{black}

   450 \vspace{20pt}

   451 Accepts all inputs with finite many $ab$.

   452 }

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

   454 \end{figure}

   455 \end{frame}

   456 \color{black}

   458 \begin{frame}

   459 \frametitle{Automata}

   460 \framesubtitle{Definition}

   461 \begin{def:buechi automata}

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

   463 \begin{itemize}

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

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

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

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

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

   469 \end{itemize}

   470 \end{def:buechi automata}

   471 \end{frame}

   473 \begin{frame}

   474 \frametitle{Automata}

   475 \framesubtitle{Runs}

   476 \begin{def:automata runs}

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

   478 \begin{itemize}

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

   480 \begin{itemize}

   481 \item $s_0 \in S_0$.

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

   483 \end{itemize}

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

   485 \end{itemize}

   486 \end{def:automata runs}

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

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

   489 \end{frame}

   491 \begin{frame}

   492 \frametitle{Automata}

   493 \framesubtitle{Acceptance}

   494 \begin{def:inf}

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

   496 \begin{itemize}

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

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

   499 \end{itemize}

   500 \end{def:inf}

   502 \begin{def:automata acceptance}

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

   504 \begin{itemize}

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

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

   507 \end{itemize}

   508 \end{def:automata acceptance}

   509 \end{frame}

   511 \begin{frame}

   512 \frametitle{Automata}

   513 \framesubtitle{Language}

   514 \begin{def:automata language}

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

   516 \begin{itemize}

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

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

   519 \end{itemize}

   520 \end{def:automata language}

   521 \end{frame}

   523 \begin{frame}

   524 \frametitle{Generalised Automata}

   525 \begin{def:general automata}

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

   527 \begin{itemize}

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

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

   530 \end{itemize}

   531 \end{def:general automata}

   533 \begin{def:general acceptance}

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

   535 \begin{itemize}

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

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

   538 \end{itemize}

   539 \end{def:general acceptance}

   541 \begin{prop:general equiv}

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

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

   544 \end{prop:general equiv}

   545 \end{frame}

   547 \begin{frame}

   548 \frametitle{Automata Construction}

   549 \framesubtitle{Formula automata}

   550 \begin{center}

   551 Model $\M_\varphi$ for formula $\varphi$\\

   552 $\Downarrow$\\

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

   554 $\Downarrow$\\

   555 Automaton $\A_\varphi$ for $\varphi$\\

   556 \vspace{20pt}

   557 \visible<2>{\textcolor{red}{On-the-fly method} \`a la Gerth et al.}

   558 \end{center}

   559 \end{frame}

   561 \begin{frame}

   562 \frametitle{Automata Construction}

   563 \framesubtitle{System automata 1/2}

   564 \begin{def:program}

   565 Given a program $P = (S_P, s_0, R, V)$:

   566 \begin{itemize}

   567 \begin{multicols}{2}

   568 \item $S$ is the set of possible states.

   569 \item $s_0$ is the initial state.

   570 \item $R : S \times \Prop \times S$ is the transition relation.

   571 \item $V : S \to 2^\Prop$ is a valuation function.

   572 \end{multicols}

   573 \end{itemize}

   574 A \emph{computation} of $P$ is a run $\rho = (V(s_0), V(s_1), ...)$.

   575 \end{def:program}

   577 \begin{def:program automaton}

   578 We construct automaton $\A_P = (\Sigma, S, S_0, \Delta, F)$ for program $P$:

   579 \begin{itemize}

   580 \begin{multicols}{2}

   581 \item $\Sigma = 2^\Prop$

   582 \item $S = S_P$

   583 \item $S_0 = \{s_0\}$

   584 \item $F = S$

   585 \end{multicols}

   586 \vspace{-1.1em}

   587 \item $\Delta = \{(s, V(s), s') \mid \exists{a \in \Prop}: (s, a, s') \in R\}$

   588 \end{itemize}

   589 \end{def:program automaton}

   590 \end{frame}

   592 \begin{frame}

   593 \frametitle{Automata Construction}

   594 \framesubtitle{System automata 2/2}

   595 \begin{prop:computation set=language}

   596 Let $\A_P = (\Sigma, S, S_0, \Delta, F)$, note that $F = S$, it follows:

   597 \[L_\omega(\A_P) = \{\rho \mid \rho \text{ is a run of } \A_P\}\]

   598 \end{prop:computation set=language}

   599 \end{frame}

   601 \begin{frame}

   602 \frametitle{Verification}

   603 \begin{center}

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

   605 \colorbox{black}{\makebox(150,10){\color{white}

   606 \only<1>{does every run of $P$ satisfy $\varphi$?}

   607 \only<2>{$L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$}

   608 \only<3>{$L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$}}}

   609 \end{center}

   610 \end{frame}

   612 \begin{frame}[allowframebreaks]

   613 \frametitle<presentation>{Literature}

   614 \begin{thebibliography}{10}

   616 %\beamertemplatearticlebibitems

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

   618 Madhavan Mukund.

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

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

   622 %\beamertemplatearticlebibitems

   623 \bibitem{ref:alternating verification}

   624 Moshe Y. Vardi.

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

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

   628 \bibitem{ref:on-the-fly verification}

   629 Rob Gerth, Doron Peled, Moshe Y. Vardi and Pierre Wolper.

   630 \newblock {\em Simple On-the-fly Automatic Verification of Linear Temporal Logic}.

   631 \newblock Proceeding IFIO/WG6.1 Symposium on Protocol Specification, Testing and Verification, Warsaw, 1995.

   633 \beamertemplatebookbibitems

   634 \bibitem{ref:handbook}

   635 Patrick Blackburn, Frank Wolter and Johan van Benthem.

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

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

   639 \beamertemplatearticlebibitems

   640 \bibitem{ref:automated verification}

   641 Moshe Y. Vardi.

   642 \newblock {\em Automated Verification: Graphs, Logic and Automata}.

   643 \newblock Proceeding of the International Joint Conference on Artificial Intelligence, Acapulco, 2003.

   645 \end{thebibliography}

   646 \end{frame}

   648 \end{document}

author	Eugen Sawin <sawine@me73.com>
	Fri, 22 Jul 2011 23:39:42 +0200
changeset 74	9938ea8ed067
parent 73	271b2a5270c1
permissions	-rw-r--r--