Hallo,
ich verstehe im Kapitel 5-5 in den Folien das Beispiel auf Seite 7 nicht so richtig.
Folien sind
hier Warum ist zum Beispiel unten bei s3 nicht auch ein -a eingetragen?
Müsste das nicht im Schritt f = -f1 passieren, da ich dort auf -a und -b prüfe?
Oder wie genau ist f = -f1 gemeint?
Mir wird hier nicht so ganz klar, worauf sich f = … immer bezieht, denn f wird hier doch gleichgesetzt mit f = EX[a v -b]
Vielen Dank für eure Hilfe.
Warum ist zum Beispiel unten bei s3 nicht auch ein -a eingetragen?
Weil du kein f mit f=not a in deiner zu checkenden Formel hast.
Du labelst im 1. Schritt alle Zustände, in denen a gilt, danach in denen b gilt. Weil du das nun gemacht hast, kannst du in
2. wunderbar rausfinden, in welchen Zuständen s aus S das notb gilt. Diese fügst du dann ebensfalls den entsprechenden Label(s) hinzu (du schaust ja nur nach, in welchem s dein -f1=-b gilt. Zu dem entsprechenenden machst du dann label(s)= -f1. -f1 hast du ja aber nur mit -b, nicht mit -a. Dort brauchst du es nicht, lässt es also einfach weg (ehrlich gesagt, weiß ich nicht ob du nicht wirklich alle mit -a durchlabeln musst - bei deiner eigentlichen Frage kann ich dir also nicht helfen, ich kann dir nur sagen, dass wir das weder in Ü-Aufgaben noch im Tutorium gemacht haben.)
Müsste das nicht im Schritt f = -f1 passieren, da ich dort auf -a und -b prüfe?
Oder wie genau ist f = -f1 gemeint?
Mir wird hier nicht so ganz klar, worauf sich f = … immer bezieht, denn f wird hier doch gleichgesetzt mit f = EX[a v -b]
Nunja, der Algorithmus geht bei dem f nicht immer gleich von f=EX…. aus. Das willst du am Ende nur zeigen. Dazu zerlegst du den Kram in die 6 Schritte. Anschaulicher ist es, wenn du sowas schreibst: L(a or -b)={s1, s2} Dann suchst du nicht allgemein für f= irgendwas, sondern immer konkret für eine Formel aus CTL. L() gibt dir die Zustände aus, die entsprechend gelabelt sind (hier mit (a or -b)). Macht genau das Gleiche, ich finde es aber anschaulicher, wo man gerade was macht.
Ah, ok, Danke Dir.
Das heißt anfangs nehme ich nur einfach alle atomaren Elemente, die in f vorkommen, selbst wenn sie nur negiert vorkommen, wenn ich dann die Negation betrachte nehme ich aber tatsächlich nur die negierten… Das hatte mich etwas verwirrt.
Ist es also korrekt, wenn ich den Algorithmus so verwende:
1) S(a) = {s2} S(b) = {s3}
2) S(-b) = {s1, s2}
3) S(a v -b) = S(a) vereinigt S(-b) = {s1, s2}
4) S(EX[a v -b]) = {s1, s3}
Also gilt die Formel, sofern ich in s1 oder s3 starte, oder?
EDIT: L(…) durch S(…) ersetzt, siehe Anmerkung des anonymen Users unten
Sollte es nicht viel mehr
S(a) = {s2}… heißen und nicht L(a) da ja L eine Abbildung von Zuständen auf 2^(AP)
Die Abbildung S wird im Skript zwar scheinbar nicht explizit definiert doch liegt die Vermutung mit Blick auf Seite 216 nahe…
Sollte es nicht viel mehr
S(a) = {s2}… heißen und nicht L(a) da ja L eine Abbildung von Zuständen auf 2^(AP)
Die Abbildung S wird im Skript zwar scheinbar nicht explizit definiert doch liegt die Vermutung mit Blick auf Seite 216 nahe…
Ja, das stimmt wohl, also überall S(…) statt L(…)
