model_checking_seminar: slides/src/slides.tex@271b2a5270c1

     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:program}{Program}

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

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

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

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

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

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

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

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

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

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

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

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

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

    65 \theoremstyle{plain}

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

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

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

    70 \theoremstyle{plain}

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

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

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

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

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

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

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

    79 \author{Eugen Sawin}

    80 \institute[University of Freiburg]

    81 {

    82   Research Group for Foundations in Artificial Intelligence\\

    83   Computer Science Department\\

    84   University of Freiburg

    85 }

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

    87 \subject{Model Checking}

    89 \begin{document}

    90 \frame{\titlepage}

    92 \begin{frame}

    93 \frametitle{Motivation}

    94 \framesubtitle{Model Checking 1/2}

    95 \begin{center}

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

    97 \[\M \models \varphi\]

    98 \end{center}

    99 \end{frame}

   101 \begin{frame}

   102 \frametitle{Motivation}

   103 \framesubtitle{Model Checking 2/2}

   104 \begin{center}

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

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

   107 \end{center}

   108 \end{frame}

   110 \begin{frame}

   111 \frametitle{Motivation}

   112 \framesubtitle{Industry}

   113 \begin{figure}

   114 \centering

   115 \only<1>{

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

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

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

   119 }

   120 \only<2>{

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

   122 }

   123 \end{figure}

   124 \end{frame}

   126 {

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

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

   129 \usebeamercolor*{normal text}

   130 \usebeamercolor*{frametitle}

   131 \begin{frame}

   132 \frametitle{Linear Temporal Logic}

   133 \framesubtitle{Natural language 1/2}

   134 \begin{center}

   135 ``It is dark.''\\

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

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

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

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

   140 \end{center}

   141 \end{frame}

   142 }

   144 \begin{frame}

   145 \frametitle{Linear Temporal Logic}

   146 \framesubtitle{Natural language 2/2}

   147 \begin{center}

   148 \only<1->{

   149 \color{white}

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

   151 \visible<2->{

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

   153 }

   154 \end{center}

   155 \end{frame}

   157 \begin{frame}

   158 \frametitle{Linear Temporal Logic}

   159 \framesubtitle{Syntax}

   160 \begin{def:syntax}

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

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

   163 \begin{itemize}

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

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

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

   167 \end{itemize}

   168 \end{def:syntax}

   169 \end{frame}

   171 \begin{frame}

   172 \frametitle{Linear Temporal Logic}

   173 \framesubtitle{Semantics}

   174 \begin{def:frames}

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

   176 \begin{itemize}

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

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

   179 \end{itemize}

   180 \end{def:frames}

   182 \begin{def:models}

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

   184 \begin{itemize}

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

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

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

   188 \end{itemize}

   189 \end{def:models}

   190 \end{frame}

   192 \begin{frame}

   193 \frametitle{Linear Temporal Logic}

   194 \framesubtitle{Model Example}

   195 \begin{figure}

   196 \centering

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

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

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

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

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

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

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

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

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

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

   207 \path[->]

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

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

   210 \path[dashed,->]

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

   212 \end{tikzpicture}

   213 \end{figure}

   214 \end{frame}

   216 \begin{frame}

   217 \frametitle{Linear Temporal Logic}

   218 \framesubtitle{Satisfiability}

   219 \begin{def:satisfiability}

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

   221 \begin{itemize}

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

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

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

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

   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$

   227 \end{itemize}

   228 \end{def:satisfiability}

   229 \end{frame}

   231 \begin{frame}

   232 \frametitle{Reactive Systems}

   233 \framesubtitle{Infinite inputs}

   234 \begin{center}

   235 \begin{figure}

   236 \setcounter{subfigure}{0}

   237 \subfigure[Terminating program]{

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

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

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

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

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

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

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

   245 \end{tikzpicture}

   246 }

   247 \hspace{10pt}

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

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

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

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

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

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

   254 \path[->]

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

   256 \end{tikzpicture}

   257 }}

   258 \end{figure}

   259 \end{center}

   260 \end{frame}

   262 \begin{frame}

   263 \frametitle{Automata}

   264 \framesubtitle{Example 1/2}

   265 \begin{figure}

   266 \centering

   267 \only<-3>{

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

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

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

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

   272     ]

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

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

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

   276 \path[->]

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

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

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

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

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

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

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

   284 \end{tikzpicture}\\

   285 \vspace{10pt}

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

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

   288 \vspace{10pt}

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

   290 }

   292 \only<4>{

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

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

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

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

   297     ]

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

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

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

   301 \path[->]

   302 (q_0)

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

   304 (q_1)

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

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

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

   308 \color{green}

   309 \path[->]

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

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

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

   313 \end{tikzpicture}\\

   314 \color{black}

   315 \vspace{10pt}

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

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

   318 \vspace{10pt}

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

   320 }

   321 %Automaton $\A_1$

   322 \end{figure}

   323 \end{frame}

   325 \begin{frame}

   326 \frametitle{Automata}

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

   328 \begin{figure}

   329 \centering

   330 \only<1>{

   331   \subfigure

   332             {

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

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

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

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

   337                 ]

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

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

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

   341                 \path[->]

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

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

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

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

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

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

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

   349               \end{tikzpicture}

   350             }

   351 }

   352 \only<2>{

   353   \subfigure

   354             {

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

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

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

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

   359                 ]

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

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

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

   363                 \path[->]

   364                 (q_0)

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

   366                 (q_1)

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

   368                 \color{red}

   369                 \path[->]

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

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

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

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

   374               \end{tikzpicture}  \color{red}

   375             }

   376  \color{black}

   377 }

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

   379   \subfigure[Complement automaton \cross]

   380             {

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

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

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

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

   385                 ]

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

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

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

   389                 \path[->]

   390                 (q_0)

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

   392                 (q_1)

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

   394                 \path[->]

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

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

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

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

   399               \end{tikzpicture}  \color{red}

   400             }

   401  \color{black}

   402 }

   403 %\hspace{10pt}

   404 \visible<3->{

   405   \subfigure[Complement automaton \checkmark]

   406             {

   407               \label{fig:complement automaton}

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

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

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

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

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

   413                 \path[->]

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

   415                 edge node {$b$} (q_2)

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

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

   418                 (q_2)

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

   420               \end{tikzpicture}\color{green}

   421             }\\

   422 \color{black}

   423 \vspace{20pt}

   424 Accepts all inputs with finite many $ab$.

   425 }

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

   427 \end{figure}

   428 \end{frame}

   429 \color{black}

   431 \begin{frame}

   432 \frametitle{Automata}

   433 \framesubtitle{Definition}

   434 \begin{def:buechi automata}

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

   436 \begin{itemize}

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

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

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

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

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

   442 \end{itemize}

   443 \end{def:buechi automata}

   444 \end{frame}

   446 \begin{frame}

   447 \frametitle{Automata}

   448 \framesubtitle{Runs}

   449 \begin{def:automata runs}

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

   451 \begin{itemize}

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

   453 \begin{itemize}

   454 \item $s_0 \in S_0$.

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

   456 \end{itemize}

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

   458 \end{itemize}

   459 \end{def:automata runs}

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

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

   462 \end{frame}

   464 \begin{frame}

   465 \frametitle{Automata}

   466 \framesubtitle{Acceptance}

   467 \begin{def:inf}

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

   469 \begin{itemize}

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

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

   472 \end{itemize}

   473 \end{def:inf}

   475 \begin{def:automata acceptance}

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

   477 \begin{itemize}

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

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

   480 \end{itemize}

   481 \end{def:automata acceptance}

   482 \end{frame}

   484 \begin{frame}

   485 \frametitle{Automata}

   486 \framesubtitle{Language}

   487 \begin{def:automata language}

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

   489 \begin{itemize}

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

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

   492 \end{itemize}

   493 \end{def:automata language}

   494 \end{frame}

   496 \begin{frame}

   497 \frametitle{Generalised Automata}

   498 \begin{def:general automata}

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

   500 \begin{itemize}

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

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

   503 \end{itemize}

   504 \end{def:general automata}

   506 \begin{def:general acceptance}

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

   508 \begin{itemize}

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

   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.

   511 \end{itemize}

   512 \end{def:general acceptance}

   514 \begin{prop:general equiv}

   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:

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

   517 \end{prop:general equiv}

   518 \end{frame}

   520 \begin{frame}

   521 \frametitle{Automata Construction}

   522 \framesubtitle{Formula automata}

   523 \begin{center}

   524 Model $\M_\varphi$ for formula $\varphi$\\

   525 $\Downarrow$\\

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

   527 $\Downarrow$\\

   528 Automaton $\A_\varphi$ for $\varphi$\\

   529 \vspace{20pt}

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

   531 \end{center}

   532 \end{frame}

   534 \begin{frame}

   535 \frametitle{Automata Construction}

   536 \framesubtitle{System automata 1/2}

   537 \begin{def:program}

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

   539 \begin{itemize}

   540 \begin{multicols}{2}

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

   542 \item $s_0$ is the initial state.

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

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

   545 \end{multicols}

   546 \end{itemize}

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

   548 \end{def:program}

   550 \begin{def:program automaton}

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

   552 \begin{itemize}

   553 \begin{multicols}{2}

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

   555 \item $S = S_P$

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

   557 \item $F = S$

   558 \end{multicols}

   559 \vspace{-1.1em}

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

   561 \end{itemize}

   562 \end{def:program automaton}

   563 \end{frame}

   565 \begin{frame}

   566 \frametitle{Automata Construction}

   567 \framesubtitle{System automata 2/2}

   568 \begin{prop:computation set=language}

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

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

   571 \end{prop:computation set=language}

   572 \end{frame}

   574 \begin{frame}

   575 \frametitle{Verification}

   576 \begin{center}

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

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

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

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

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

   582 \end{center}

   583 \end{frame}

   585 \begin{frame}[allowframebreaks]

   586 \frametitle<presentation>{Literature}

   587 \begin{thebibliography}{10}

   589 %\beamertemplatearticlebibitems

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

   591 Madhavan Mukund.

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

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

   595 %\beamertemplatearticlebibitems

   596 \bibitem{ref:alternating verification}

   597 Moshe Y. Vardi.

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

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

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

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

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

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

   606 \beamertemplatebookbibitems

   607 \bibitem{ref:handbook}

   608 Patrick Blackburn, Frank Wolter and Johan van Benthem.

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

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

   612 \beamertemplatearticlebibitems

   613 \bibitem{ref:automated verification}

   614 Moshe Y. Vardi.

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

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

   618 \end{thebibliography}

   619 \end{frame}

   621 \end{document}

author	Eugen Sawin <sawine@me73.com>
	Fri, 22 Jul 2011 23:11:53 +0200
changeset 73	271b2a5270c1
parent 72	722ec2a3cabe
child 74	9938ea8ed067
permissions	-rw-r--r--