Übungsblatt 11

Aufgabe 1: Ampeln und Kreuzungen

Eine Kreuzung besteht aus zwei sich kreuzenden Straßen und einer Fußgängerampel. Fußgänger können die Straße überqueren, indem sie einen Knopf an der Fußgängerampel betätigen und darauf warten, dass die Ampel grün wird. (Fußgänger überqueren die Straße nicht bei Rot.)

Die Straßenampeln haben folgende Zustände (die sie in dieser Reihenfolge durchlaufen): Rot, Rot-Gelb, Grün, Gelb (und dann wieder Rot); die Fußgängerampel hat nur Rot und Grün. Die Autos können entweder auf der vertikalen oder horizontalen Straße die Kreuzung passieren (natürlich nur, wenn die Ampel nicht Rot zeigt); Abbiegen ist nicht erlaubt.

Als FSM modelliert hat die Straßenkreuzung damit einen Zustandsraum \(\Sigma\), der aus den Zuständen für die Fußgängerampel \(\Sigma_{lightped}\) und der beiden Autoampeln \(\Sigma_{lightv}, \Sigma_{lighth}\) sowie der Fußgänger \(\Sigma_{ped}\) und der Autos \(\Sigma_{carv}, \Sigma_{carh}\) besteht:

$$ \begin{array}{rcl} \Sigma & = & \Sigma_{lightped} \times \Sigma_{lightv} \times \Sigma_{lighth} \times \Sigma_{ped} \times \Sigma_{carv} \times \Sigma_{carh} \\ \Sigma_{lightped} & = & \{red,green\}\\ \Sigma_{lightv} = \Sigma_{lighth} & = & \{red,yellowred,green,yellow\}\\ \Sigma_{ped} & = & \{away,button,waiting,xing\}\\ \Sigma_{carv} = \Sigma_{carh} & = & \{away,appr,xing\}\\ \end{array} $$

Aus den Zuständen ergeben sich die Basisaussagen \(Prop\) in der Form wie beispielsweise \(lightped = green\) oder \(carv = xing\) wie in der Vorlesung vorgestellt.

Formulieren Sie folgende Sicherheitseigenschaften in linearer Temporallogik:

  1. Fußgänger und Autos kreuzen niemals den Fußgängerüberweg zur selben Zeit:

  2. Es können nie zwei Autos gleichzeitg die Kreuzung passieren:

  3. Es kann nie die Fußgängerampel und die Straßenampel auf der Horizontalstraße gleichzeitig grün sein:

  4. Es können nie die beiden Straßenampeln auf Horizontal- und Vertikalstraße gleichzeigt grün sein:

Bonus: Beachten Sie auch das Bonusblatt

Autoren
Name Matrikelnummer E-Mail
1.
2.
3.

Es werden keine Daten übertragen. Per Klick auf "Ergebnis speichern" kann eine Datei gespeichert werden, welche die eingegebenen Ergebnisse enthält. Diese Datei sendet ihr bitte rechtzeitig bis Dienstag 23:59:59 an martin (punkt) ring (klammeraffe) dfki (punkt) de. Ihr könnt eure Abgabe später auch wieder laden und ansehen indem ihr auf "Ergebnis laden" klickt.

Ergebnis speichern | Ergebnis laden: