SSQ WS 17/18

Übungsblatt 10

Aufgabe 1: Lineare Temporallogik

Wir betrachten die mysteriöse Maschine aus Übungsblatt 2. In diesem Übungsblatt lüften wir das Geheimnis und zeigen Ihnen die Kripke-Struktur, welche das Verhalten der Maschine erklärt:

$$ \begin{array}{rrrl} \textit{Prop} & = & \lbrace & S : \text{Ein Spiegelei liegt im Ausgabeschacht},\\ & & & P : \text{In der Brennkammer befindet sich Plutonium},\\ & & & A : \text{Das Alarmsignal ist aktiv},\\ & & & R : \text{Die Kreiselklingen rotieren},\\ & & & E : \text{Der Not-Aus/Selbstzerstörungs- Kombischalter wird betätigt},\\ & & & V : \text{Das System ist vollständig vaporisiert} \quad\rbrace\\ \Sigma & = & \lbrace & s_1, ... , s_6 \quad\rbrace\\ \text{I} & = & \lbrace & s_1 \quad\rbrace\\ \rightarrow & = & \lbrace & (s_1,s_2), (s_2,s_1), (s_2,s_2), (s_2,s_3), (s_2,s_4), (s_2,s_6), \\ & & & (s_3,s_1), (s_3,s_4), (s_4,s_5), (s_5,s_1), (s_5,s_6), (s_6,s_6) \quad\rbrace\\ \operatorname{V}(S) & = & \lbrace & s_3 \quad\rbrace\\ \operatorname{V}(P) & = & \lbrace & s_2 \quad\rbrace\\ \operatorname{V}(A) & = & \lbrace & s_5 \quad\rbrace\\ \operatorname{V}(R) & = & \lbrace & s_1, s_2, s_3, s_4 \quad\rbrace\\ \operatorname{V}(E) & = & \lbrace & s_4 \quad\rbrace\\ \operatorname{V}(V) & = & \lbrace & s_6 \quad\rbrace\\ \end{array} $$

Jetzt sollte alles klar sein, oder? Prüfen Sie nun, ob folgende Eigenschaften für das System gelten, indem Sie diese zunächst in LTL übersetzten. Markieren Sie dann die gültigen Aussagen mit einem Häkchen.

Wenn der Notschalter betätigt wird, darf sich kein Plutonium in der Brennkammer befinden:
Es ist möglich ein Spiegelei zu Braten (Erst Plutonium einlegen, schließlich liegt ein Spiegelei im Ausgabeschacht):
Bevor der Notschalter betätigt wird, laufen die Kreiselklingen.
Wenn Plutonium in der Brennkammer ist und solange der Notschalter noch nicht betätigt wurde, befindet sich weiterhin Plutonium in der Brennkammer oder, ein Spiegelei im Ausgabeschacht.
Wenn der Notschalter betätigt wird, wird das System schließlich vaporisiert sein.

Hinweis: Um zu prüfen, ob die Eigenschaften gelten, kann es zusätzlich hilfreich sein, ein Diagramm der Kripke-Struktur auf ein Blatt Papier zu zeichnen. (Nicht Teil der Bewertung)

Autoren

	Name	Matrikelnummer	E-Mail
1.
2.
3.

Autoren in diesem Browser merken

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:

Systeme hoher Sicherheit und Qualität

Übungsblatt 10

Aufgabe 1: Lineare Temporallogik