# HG changeset patch # User Eugen Sawin # Date 1311346242 -7200 # Node ID ab0b7643228aff8d08bcc98a7ae93320227fa3d8 # Parent 3ebfd8683b189c262a8925423859e5cb4acce58a Reactive systems. diff -r 3ebfd8683b18 -r ab0b7643228a slides/notes.txt --- a/slides/notes.txt Fri Jul 22 15:55:34 2011 +0200 +++ b/slides/notes.txt Fri Jul 22 16:50:42 2011 +0200 @@ -163,7 +163,7 @@ Es existiert eine verallgemeinerte Form des Büchi-Automaten, welche bei der Automatenkonstruktion Vorteile bietet. Der Unterschied liegt in der Akzeptanzbedingung. Der verallgemeinerte Büchi-Automat definiert diese über eine endliche Menge von Mengen von akzeptierenden Zuständen. -Ein Pfad RHO eines solchen Automaten ist akzeptierend gdw. es einen Zustand aus der jeweiligen Menge von akzeptierenden Zuständen gibt, der unendlich oft in RHO vorkommt. +Ein Pfad RHO eines solchen Automaten ist akzeptierend gdw. es einen Zustand aus jeder Menge Fi aus dieser Mengenfamilie gibt, der unendlich oft in RHO vorkommt. Wenn man sich die Definition anschaut, wird es offensichtlich, dass die akzeptierte Sprache eines verallgemeinerten Automaten equivalent ist zu der Schnittmenge der akzeptierten Sprachen von k Büchi-Automaten. ==> 19 diff -r 3ebfd8683b18 -r ab0b7643228a slides/src/slides.tex --- a/slides/src/slides.tex Fri Jul 22 15:55:34 2011 +0200 +++ b/slides/src/slides.tex Fri Jul 22 16:50:42 2011 +0200 @@ -123,7 +123,7 @@ \usebeamercolor*{frametitle} \begin{frame} \frametitle{Linear Temporal Logic} -\framesubtitle{Motivation 1/2} +\framesubtitle{Natural language 1/2} \begin{center} ``It is dark.''\\ \visible<2->{``It is \emph{always} dark.''\\} @@ -136,7 +136,7 @@ \begin{frame} \frametitle{Linear Temporal Logic} -\framesubtitle{Motivation 2/2} +\framesubtitle{Natural language 2/2} \begin{center} \only<1->{ \color{white} @@ -222,10 +222,23 @@ \end{frame} \begin{frame} -\frametitle{Infinity} -\framesubtitle{Word as function} +\frametitle{Reactive Systems} +\framesubtitle{Infinite inputs} \begin{figure} \centering + +\subfigure{ +\begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth + ,accepting/.style={fill, gray!50!black, text=white}] +\node[state, initial, initial text=$input$] (p) {$Program$}; +\coordinate (b) at (1.1,0); + %\coordinate (b) at ($(a)+1/2*(3,3)$); +\draw (p) edge[->] node[right] {$\,output$} (b); +%\draw[->] (p) -- (b); +\end{tikzpicture} +} + +\subfigure{ \begin{tikzpicture}[shorten >=1pt, node distance=1.5cm, semithick, >=stealth ,accepting/.style={fill, gray!50!black, text=white}] \node[state, initial, initial text=] (s_0) {$a$}; @@ -238,6 +251,7 @@ \path[dashed,->] (s_2) edge node {} (s_i); \end{tikzpicture} +} \end{figure} \end{frame}