\documentclass[a4paper,twoside,12pt]{article}
%\usepackage [reqno] {amsmath}
\usepackage{amsfonts,amstext}
\usepackage{amsmath}
\usepackage{german}
\usepackage{graphicx}
\usepackage{fullpage}

\newcommand{\ZETTELNUMMER}{4}
\newcommand{\ABGABEDATUM}{am 18. Mai 2018 bis 12 Uhr in die
Tutorenf\"acher}

\newcounter{AUFGNR}
\setcounter{AUFGNR}{1}
\newcommand{\AUFGABE}[2]{\vspace{0.3cm}\item[Aufgabe~\arabic{AUFGNR}]\stepcounter{AUFGNR} #1\hfill\emph{#2}}


\newcommand{\floor}[1]{\left\lfloor{#1}\right\rfloor}
\newcommand{\ceil}[1]{\left\lceil{#1}\right\rceil}
\newcommand{\half}[1]{\frac{#1}{2}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}



\renewcommand{\labelenumi}{(\alph{enumi})}
\renewcommand{\labelenumii}{(\roman{enumii})}


\begin{document}
\pagestyle{empty}
\hrule\medskip
\rule{0ex}{0ex}\\[-1ex]
\ZETTELNUMMER. Aufgabenblatt zur Vorlesung

\smallskip
\noindent
\large
\textbf{Nichtsequentielle und Verteilte Programmierung}\hfill SoSe 
2018 \\[0.5ex]
\normalsize
Wolfgang Mulzer, Katinka Wolter

\medskip\hrule

\smallskip
\noindent
\textbf{Abgabe} \ABGABEDATUM

\vskip 0.5cm

\begin{description}

\AUFGABE{Lineare Temporale Logik I}{10 Punkte}
\begin{enumerate}
\item Gilt die folgende Formel f\"ur alle m\"oglichen Belegungen?
  Begr\"unden Sie Ihre Antwort.
  \[
     \lozenge \Box\, p \Leftrightarrow \Box \lozenge\, p
  \]
\item Gilt die folgende Formel f\"ur alle m\"oglichen Belegungen?
  Begr\"unden Sie Ihre Antwort.
  \[
    (\Box\, p \Rightarrow \lozenge\, q) \wedge \lozenge \Box\, q 
    \Rightarrow \lozenge\, q 
  \]
\item Beweisen Sie, dass die folgenden Formeln f\"ur alle 
m\"oglichen Belegungen gelten.
\begin{enumerate}
\item $(\Box\, p \wedge \Box\, q) \Leftrightarrow \Box (p \wedge q)$
\item $(\lozenge\, p \vee \lozenge\, q) 
\Leftrightarrow \lozenge (p \vee q)$
\end{enumerate}
\end{enumerate}

\AUFGABE{Lineare Temporale Logik II}{10 Punkte}

In der linearen temporalen Logik gibt es oft noch die zus\"atzlichen
Operatoren \emph{bis} ($\mathcal{U}$) und \emph{n\"achster} 
($\bigcirc$).

Die informelle Spezifikation ist wie folgt: Seien $\alpha$ und 
$\beta$ zwei LTL Formeln. Dann ist $\alpha\, \mathcal{U}\, \beta$
genau dann wahr zu einem Zeitpunkt $i$, $i \in \N$, wenn ein Zeitpunkt 
$j \geq i$ existiert, so dass $\beta$ zum Zeitpunkt $j$ und 
$\alpha$ f\"ur alle Zeitpunkte $k = i, \dots, j-1$ wahr ist.

Es ist $\bigcirc\, \alpha $  genau dann wahr zu einem Zeitpunkt 
$i$, $i \in \N$, falls $\alpha$ zum Zeitpunkt $i + 1$ wahr ist.

\begin{enumerate}
    \item Erweitern Sie die formale Syntax und Semantik der 
      linearen temporalen Logik aus der Vorlesung um die 
      Operatoren $\mathcal{U}$ und $\bigcirc$.
      Geben Sie zwei Beispiele.
     \item Warum eignet sich der Operator $\bigcirc$ nicht zur 
       Spezifikation von Fortschrittseigenschaften?
       Was ist das Problem mit einer Formel der Form
      $\Box \big[ a_1 \Rightarrow \bigcirc\, a_2 \big]$?
     \item Definieren Sie $\Box$ und $\lozenge$ mit Hilfe von
         $\mathcal{U}$ (und den elementaren Operatoren der klassischen 
         Aussagenlogik) und beweisen Sie die Korrektheit ihrer 
         Definition.
\end{enumerate}

\newpage
\AUFGABE{Der Algorithmus von Peterson II}{10 Punkte}

Der Algorithmus von Peterson (Aufgabe 3.2) lautete folgenderma\ss{}en:
\begin{verbatim}
======================================================
  global adrin = false, bdrin = false, letzter = a
a1: U                     | b1: U
a2: adrin  <- true        | b2: bdrin  <- true
a3: letzter <- a          | b3: letzter <- b
a4: while bdrin &&        | b4: while adrin && 
          letzter = a do  |           letzter = b do
a5:     NOP               | b5:     NOP
a6: K                     | b6: K
a7: adrin <- false        | b7: bdrin <- false
\end{verbatim}


\begin{enumerate}

\item
Beweisen Sie, dass im Algorithmus von 
Peterson die folgenden Invarianten gelten:

\begin{itemize}
\item $(a_6 \wedge (b_4 \vee b_5)) \Rightarrow 
(\texttt{adrin} \wedge \texttt{letzter} = b)$
\item $((a_4 \vee a_5) \wedge b_6) \Rightarrow 
(\texttt{bdrin} \wedge \texttt{letzter} = a )$
\end{itemize}
\item Argumentieren Sie, dass
die folgenden Formeln f\"ur jede m\"ogliche Zustandsfolge 
gelten:
\begin{itemize}
  \item $\Box \big [(a_4 \wedge \Box \neg a_6) \Rightarrow
  \Box \lozenge (\texttt{bdrin} \wedge \texttt{letzter} \neq b) \big ]$,
 \item $\Box \big [\lozenge\Box (\neg \texttt{bdrin}) \vee \lozenge 
   (\texttt{letzter} = b) \big]$, und
 \item
  $\Box \big[ (a_4 \wedge \Box \neg a_6 \wedge \lozenge (\texttt{letzter} = b)) 
  \Rightarrow \lozenge\Box (\texttt{letzter} = b)) \big]$.
\end{itemize}
Sie  k\"onnen ggf.\@ die Invarianten aus (a) verwenden.
\item (\emph{freiwillig, 5 Zusatzpunkte}) Beweisen Sie, dass
    Petersons Algorithmus korrekt ist.
\end{enumerate}
\end{description}
\end{document}
