model_checking_seminar: slides/src/slides.tex@722ec2a3cabe

     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 \subfigure{\includegraphics[width=70pt,height=50pt]{images/intel.jpg}}

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

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

   118 \end{figure}

   119 \end{frame}

   121 {

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

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

   124 \usebeamercolor*{normal text}

   125 \usebeamercolor*{frametitle}

   126 \begin{frame}

   127 \frametitle{Linear Temporal Logic}

   128 \framesubtitle{Natural language 1/2}

   129 \begin{center}

   130 ``It is dark.''\\

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

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

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

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

   135 \end{center}

   136 \end{frame}

   137 }

   139 \begin{frame}

   140 \frametitle{Linear Temporal Logic}

   141 \framesubtitle{Natural language 2/2}

   142 \begin{center}

   143 \only<1->{

   144 \color{white}

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

   146 \visible<2->{

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

   148 }

   149 \end{center}

   150 \end{frame}

   152 \begin{frame}

   153 \frametitle{Linear Temporal Logic}

   154 \framesubtitle{Syntax}

   155 \begin{def:syntax}

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

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

   158 \begin{itemize}

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

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

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

   162 \end{itemize}

   163 \end{def:syntax}

   164 \end{frame}

   166 \begin{frame}

   167 \frametitle{Linear Temporal Logic}

   168 \framesubtitle{Semantics}

   169 \begin{def:frames}

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

   171 \begin{itemize}

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

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

   174 \end{itemize}

   175 \end{def:frames}

   177 \begin{def:models}

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

   179 \begin{itemize}

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

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

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

   183 \end{itemize}

   184 \end{def:models}

   185 \end{frame}

   187 \begin{frame}

   188 \frametitle{Linear Temporal Logic}

   189 \framesubtitle{Model Example}

   190 \begin{figure}

   191 \centering

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

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

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

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

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

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

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

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

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

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

   202 \path[->]

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

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

   205 \path[dashed,->]

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

   207 \end{tikzpicture}

   208 \end{figure}

   209 \end{frame}

   211 \begin{frame}

   212 \frametitle{Linear Temporal Logic}

   213 \framesubtitle{Satisfiability}

   214 \begin{def:satisfiability}

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

   216 \begin{itemize}

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

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

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

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

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

   222 \end{itemize}

   223 \end{def:satisfiability}

   224 \end{frame}

   226 \begin{frame}

   227 \frametitle{Reactive Systems}

   228 \framesubtitle{Infinite inputs}

   229 \begin{center}

   230 \begin{figure}

   231 \setcounter{subfigure}{0}

   232 \subfigure[Terminating program]{

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

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

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

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

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

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

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

   240 \end{tikzpicture}

   241 }

   242 \hspace{10pt}

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

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

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

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

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

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

   249 \path[->]

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

   251 \end{tikzpicture}

   252 }}

   253 \end{figure}

   254 \end{center}

   255 \end{frame}

   257 \begin{frame}

   258 \frametitle{Automata}

   259 \framesubtitle{Example 1/2}

   260 \begin{figure}

   261 \centering

   262 \only<-3>{

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

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

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

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

   267     ]

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

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

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

   271 \path[->]

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

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

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

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

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

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

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

   279 \end{tikzpicture}\\

   280 \vspace{10pt}

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

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

   283 \vspace{10pt}

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

   285 }

   287 \only<4>{

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

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

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

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

   292     ]

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

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

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

   296 \path[->]

   297 (q_0)

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

   299 (q_1)

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

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

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

   303 \color{green}

   304 \path[->]

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

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

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

   308 \end{tikzpicture}\\

   309 \color{black}

   310 \vspace{10pt}

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

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

   313 \vspace{10pt}

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

   315 }

   316 %Automaton $\A_1$

   317 \end{figure}

   318 \end{frame}

   320 \begin{frame}

   321 \frametitle{Automata}

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

   323 \begin{figure}

   324 \centering

   325 \only<1>{

   326   \subfigure

   327             {

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

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

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

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

   332                 ]

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

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

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

   336                 \path[->]

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

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

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

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

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

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

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

   344               \end{tikzpicture}

   345             }

   346 }

   347 \only<2>{

   348   \subfigure

   349             {

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

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

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

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

   354                 ]

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

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

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

   358                 \path[->]

   359                 (q_0)

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

   361                 (q_1)

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

   363                 \color{red}

   364                 \path[->]

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

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

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

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

   369               \end{tikzpicture}  \color{red}

   370             }

   371  \color{black}

   372 }

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

   374   \subfigure[Complement automaton \cross]

   375             {

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

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

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

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

   380                 ]

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

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

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

   384                 \path[->]

   385                 (q_0)

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

   387                 (q_1)

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

   389                 \path[->]

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

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

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

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

   394               \end{tikzpicture}  \color{red}

   395             }

   396  \color{black}

   397 }

   398 %\hspace{10pt}

   399 \visible<3->{

   400   \subfigure[Complement automaton \checkmark]

   401             {

   402               \label{fig:complement automaton}

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

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

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

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

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

   408                 \path[->]

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

   410                 edge node {$b$} (q_2)

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

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

   413                 (q_2)

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

   415               \end{tikzpicture}\color{green}

   416             }\\

   417 \color{black}

   418 \vspace{20pt}

   419 Accepts all inputs with finite many $ab$.

   420 }

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

   422 \end{figure}

   423 \end{frame}

   424 \color{black}

   426 \begin{frame}

   427 \frametitle{Automata}

   428 \framesubtitle{Definition}

   429 \begin{def:buechi automata}

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

   431 \begin{itemize}

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

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

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

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

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

   437 \end{itemize}

   438 \end{def:buechi automata}

   439 \end{frame}

   441 \begin{frame}

   442 \frametitle{Automata}

   443 \framesubtitle{Runs}

   444 \begin{def:automata runs}

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

   446 \begin{itemize}

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

   448 \begin{itemize}

   449 \item $s_0 \in S_0$.

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

   451 \end{itemize}

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

   453 \end{itemize}

   454 \end{def:automata runs}

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

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

   457 \end{frame}

   459 \begin{frame}

   460 \frametitle{Automata}

   461 \framesubtitle{Acceptance}

   462 \begin{def:inf}

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

   464 \begin{itemize}

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

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

   467 \end{itemize}

   468 \end{def:inf}

   470 \begin{def:automata acceptance}

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

   472 \begin{itemize}

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

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

   475 \end{itemize}

   476 \end{def:automata acceptance}

   477 \end{frame}

   479 \begin{frame}

   480 \frametitle{Automata}

   481 \framesubtitle{Language}

   482 \begin{def:automata language}

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

   484 \begin{itemize}

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

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

   487 \end{itemize}

   488 \end{def:automata language}

   489 \end{frame}

   491 \begin{frame}

   492 \frametitle{Generalised Automata}

   493 \begin{def:general automata}

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

   495 \begin{itemize}

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

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

   498 \end{itemize}

   499 \end{def:general automata}

   501 \begin{def:general acceptance}

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

   503 \begin{itemize}

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

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

   506 \end{itemize}

   507 \end{def:general acceptance}

   509 \begin{prop:general equiv}

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

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

   512 \end{prop:general equiv}

   513 \end{frame}

   515 \begin{frame}

   516 \frametitle{Automata Construction}

   517 \framesubtitle{Formula automata}

   518 \begin{center}

   519 Model $\M_\varphi$ for formula $\varphi$\\

   520 $\Downarrow$\\

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

   522 $\Downarrow$\\

   523 Automaton $\A_\varphi$ for $\varphi$\\

   524 \vspace{20pt}

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

   526 \end{center}

   527 \end{frame}

   529 \begin{frame}

   530 \frametitle{Automata Construction}

   531 \framesubtitle{System automata 1/2}

   532 \begin{def:program}

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

   534 \begin{itemize}

   535 \begin{multicols}{2}

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

   537 \item $s_0$ is the initial state.

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

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

   540 \end{multicols}

   541 \end{itemize}

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

   543 \end{def:program}

   545 \begin{def:program automaton}

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

   547 \begin{itemize}

   548 \begin{multicols}{2}

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

   550 \item $S = S_P$

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

   552 \item $F = S$

   553 \end{multicols}

   554 \vspace{-1.1em}

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

   556 \end{itemize}

   557 \end{def:program automaton}

   558 \end{frame}

   560 \begin{frame}

   561 \frametitle{Automata Construction}

   562 \framesubtitle{System automata 2/2}

   563 \begin{prop:computation set=language}

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

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

   566 \end{prop:computation set=language}

   567 \end{frame}

   569 \begin{frame}

   570 \frametitle{Verification}

   571 \begin{center}

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

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

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

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

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

   577 \end{center}

   578 \end{frame}

   580 \begin{frame}[allowframebreaks]

   581 \frametitle<presentation>{Literature}

   582 \begin{thebibliography}{10}

   584 %\beamertemplatearticlebibitems

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

   586 Madhavan Mukund.

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

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

   590 %\beamertemplatearticlebibitems

   591 \bibitem{ref:alternating verification}

   592 Moshe Y. Vardi.

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

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

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

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

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

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

   601 \beamertemplatebookbibitems

   602 \bibitem{ref:handbook}

   603 Patrick Blackburn, Frank Wolter and Johan van Benthem.

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

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

   607 \beamertemplatearticlebibitems

   608 \bibitem{ref:automated verification}

   609 Moshe Y. Vardi.

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

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

   613 \end{thebibliography}

   614 \end{frame}

   616 \end{document}

author	Eugen Sawin <sawine@me73.com>
	Fri, 22 Jul 2011 23:01:19 +0200
changeset 72	722ec2a3cabe
parent 71	e7c58603ff08
child 73	271b2a5270c1
permissions	-rw-r--r--