Seite 1 von 2

Kripke Struktur und CTL Formeln

Verfasst: 10. Mär 2012 23:41
von allein
Hat jemand die Lösung zur Übung 13 von WS10/11? Ich habe Teil a gemacht, Teil b nur halb fertig.

Ich weiß nicht wie man Kripke Struktur darstellt. Kann jemand erklären oder ein Bild oder einen Link zu einem Bild (o.ä) posten?

Vielen Dank.

Giray.

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 11:50
von charfi90
Hi
Kannst du mal deine Antworten für teil a schreiben?
ich habe so gemacht.
für erste Aussage habe ich :AG(¬ P)
für 2. : EX(p)->AX(¬ P)
für 3. : EX(p) oder AG(¬ P)
ich bin nicht ganz sicher ob es so richtig ist
Gruß

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 14:20
von fscheepy
charfi90 hat geschrieben:Hi
Kannst du mal deine Antworten für teil a schreiben?
ich habe so gemacht.
für erste Aussage habe ich :AG(¬ P)
für 2. : EX(p)->AX(¬ P)
für 3. : EX(p) oder AG(¬ P)
ich bin nicht ganz sicher ob es so richtig ist
Gruß
Die erste Aussage habe ich genau so.
Steht deine zweite Aussage nicht eher für "Wenn auf einem Pfad im nächsten Zustand p gilt, gilt auf allen Pfaden im nächsten Zustand p nicht"? Man müsste meiner Meinung nach einen verschachtelten Ausdruck haben, um "in allen von diesem Zustand aus erreichbaren Zuständen" zu modellieren. Wie wäre es mit AG(p -> AG(¬q))?
Bei der dritten Aussage müsste ein "EX(p) v AG(¬p)" passen, ja, da sich die beiden CTL-Teilformeln schon gegenseitig ausschließen, müssen wir nicht weiter auf "entweder...oder" achten, sondern können es als einfaches "oder" auffassen.

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 14:33
von Uhr
Wo kann man denn diese Übungen bekommen? Im Elzi sehe ich nur welche bis 08/09.

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 14:37
von charfi90
Uhr hat geschrieben:Wo kann man denn diese Übungen bekommen? Im Elzi sehe ich nur welche bis 08/09.
http://www.seceng.informatik.tu-darmsta ... 0-11/ts10/
Nutzername und Passwort sind gleich wie dieses Jahr

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 14:40
von charfi90
fscheepy hat geschrieben:
charfi90 hat geschrieben:Hi
Kannst du mal deine Antworten für teil a schreiben?
ich habe so gemacht.
für erste Aussage habe ich :AG(¬ P)
für 2. : EX(p)->AX(¬ P)
für 3. : EX(p) oder AG(¬ P)
ich bin nicht ganz sicher ob es so richtig ist
Gruß
Die erste Aussage habe ich genau so.
Steht deine zweite Aussage nicht eher für "Wenn auf einem Pfad im nächsten Zustand p gilt, gilt auf allen Pfaden im nächsten Zustand p nicht"? Man müsste meiner Meinung nach einen verschachtelten Ausdruck haben, um "in allen von diesem Zustand aus erreichbaren Zuständen" zu modellieren. Wie wäre es mit AG(p -> AG(¬q))?
Bei der dritten Aussage müsste ein "EX(p) v AG(¬p)" passen, ja, da sich die beiden CTL-Teilformeln schon gegenseitig ausschließen, müssen wir nicht weiter auf "entweder...oder" achten, sondern können es als einfaches "oder" auffassen.
ja du hast recht:AG(p -> AG(¬q)) wäre richtig
wie hast du in teil b gemacht ?
1. Aussage ist nicht erfüllt ,denke ich
2 und 3 weiß ich nicht genau wie man das macht:(

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 14:50
von fscheepy
Bei Teil b) war ich mir auch nicht sicher:
1. dachte ich auch bis eben, dass es nicht erfüllbar wäre, aber wenn AG(p) nicht gilt, ist es doch aufgrund der Implikation egal, wie AG(¬p) ausgewertet wird. Die Formel ist nur nicht erfüllbar, wenn AG(p) wirklich gilt.
2. sollte eigentlich auch erfüllbar sein - wenn man eine Struktur hat, in der AG(p) gilt, dann gilt EF(p) sowieso.
Bei 3. bin ich mir irgendwie Unsicher wegen des AX(p). Ausgeschrieben heißt es ja "Auf allen Pfaden gilt p im nächsten Zustand" (?). Heißt das, dass p in allen Zuständen gilt? Irgendwie ist mir das noch nicht so ganz klar, da man ja über die Pfade quantifiziert, aber dann über einzelne Knoten eine Aussage macht.

Wie man eine solche Struktur nun angibt weiß ich auch nicht.

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 14:54
von ElGamal
charfi90 hat geschrieben: ja du hast recht:AG(p -> AG(¬q)) wäre recht
wie hast du teil b gemacht ?
1. Aussage ist nicht erfüllt ,denke ich
2 und 3 weiß ich nicht genau wie man das macht:(
Bei der b) habe ich folgende Lösung:
1) nicht möglich (Wenn auf allen Pfaden p gilt, dann kann daraus nicht folgen, dass auf allen Pfaden nicht p gilt)
2) das geht, stell dir einen Baum vor, in dem immer p gilt
3) tippe ich mal, dass es nicht geht, wobei ich mit AXp nicht so viel anfangen kann. Das heißt ja "auf jedem Pfad gilt im nächsten Zustand p". Ist das dann nicht gleichbedeutend mit: " es gilt immer p", also AGp?

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 15:05
von Uhr
charfi90 hat geschrieben:
Uhr hat geschrieben:Wo kann man denn diese Übungen bekommen? Im Elzi sehe ich nur welche bis 08/09.
http://www.seceng.informatik.tu-darmsta ... 0-11/ts10/
Nutzername und Passwort sind gleich wie dieses Jahr
Macht Sinn. Danke.

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 15:25
von m2c1
ElGamal hat geschrieben:[...]Bei der b) habe ich folgende Lösung:
1) nicht möglich (Wenn auf allen Pfaden p gilt, dann kann daraus nicht folgen, dass auf allen Pfaden nicht p gilt)
[...]
3) tippe ich mal, dass es nicht geht, wobei ich mit AXp nicht so viel anfangen kann. Das heißt ja "auf jedem Pfad gilt im nächsten Zustand p". Ist das dann nicht gleichbedeutend mit: " es gilt immer p", also AGp?
Zuerst hatte ich die 1) genauso, allerdings würde ich fscheepy zustimmen: wenn die Prämisse einer Implikation falsch ist (und so einen Zustand kann es ja geben), ist die Implikation wahr.

Die 3) ist meiner Meinung nach erfüllbar. Wenn für alle direkten Nachfolgerknoten des aktuellen p gilt, kann es doch weiter unten in den abgehenden Pfaden p nicht mehr gelten.

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 15:26
von allein
Ich habe so gemacht wobei ich bei a2 nicht sicher bin. Ich würde mich freuen wenn jemand mir sagen kann ob meine Antwort falsch ist und warum.

a)
1)AG(¬p)
2)AX(p)->AG(¬p)
3)EX(p) | AG(¬p)
b)
1-kann nicht erfüllt werden.
2-erfüllt werden.
3-kann nicht erfüllt werden.

jetzt ist die Frage: Wie sieht die Kripke Struktur aus? Kann jemand ein Bild von seiner Lösung posten? Oder ein anderes Beispiel, damit man versteht wie man Kripke Struktur abbilden soll.

Vielen Dank

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 15:30
von m2c1
allein hat geschrieben:Ich habe so gemacht wobei ich bei a2 nicht sicher bin. Ich würde mich freuen wenn jemand mir sagen kann ob meine Antwort falsch ist und warum.

a)
2)AX(p)->AG(¬p)
[...]
b)
[...]
3-kann nicht erfüllt werden.
Die a2) ist falsch (denke ich): es ist ein Unterschied, ob für alle direkten Nachfolgezustände etwas gilt (deine Aussage) oder für einen der Zustände (Aufgabenstellung). Wegen b3) siehe meinen letzten Post.

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 15:43
von fscheepy
m2c1 hat geschrieben: Die 3) ist meiner Meinung nach erfüllbar. Wenn für alle direkten Nachfolgerknoten des aktuellen p gilt, kann es doch weiter unten in den abgehenden Pfaden p nicht mehr gelten.
Naja die Frage, die hier bei einigen noch offen ist, ist ja, wie genau AX(p) definiert ist, ob es zu AG(p) äquivalent ist oder wie man es sonst auffassen soll.
Wenn AX(p) heißt: "In allen Pfaden gibt es einen Knoten, in dessem Nachfolger p gilt", dann müsste die Formel ja erfüllbar sein. Wäre sie nicht sogar durch den Baum
¬p -> p
erfüllt? In allen Pfaden gibt es einen Knoten, in dessen Nachfolgeknoten p gilt, außerdem gibt es einen Pfad, sodass ¬p in der Zukunft gilt.

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 15:47
von m2c1
fscheepy hat geschrieben:Naja die Frage, die hier bei einigen noch offen ist, ist ja, wie genau AX(p) definiert ist, ob es zu AG(p) äquivalent ist oder wie man es sonst auffassen soll.
Wenn AX(p) heißt: "In allen Pfaden gibt es einen Knoten, in dessem Nachfolger p gilt", dann [...]
A steht für "jeden Pfad", X(p) steht für "im nächsten Zustand gilt p". AX(p) bedeutet also für mich in allen direkt nachfolgenden Zuständen (den Kindknoten des aktuellen Knoten/Wurzelknoten) gilt p. Aber nicht zwangsläufig in allen Zuständen (AG(p)).

Re: Kripke Struktur und CTL Formeln

Verfasst: 11. Mär 2012 15:53
von Woyzeck
Eine Kripke-Struktur ist doch ein nicht abgewickelter Computational Tree, richtig?

Wie schreibt man da dann die Zustände dran? In die Kreise oder an die Übergänge? Was kommt dann an das jeweils andere?