Kripke Struktur und CTL Formeln

allein
Mausschubser
Mausschubser
Beiträge: 60
Registriert: 15. Okt 2008 00:01

Kripke Struktur und CTL Formeln

Beitrag von allein » 10. Mär 2012 23:41

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.

charfi90
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 8. Sep 2010 15:40

Re: Kripke Struktur und CTL Formeln

Beitrag von charfi90 » 11. Mär 2012 11:50

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ß

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Kripke Struktur und CTL Formeln

Beitrag von fscheepy » 11. Mär 2012 14:20

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.

Uhr
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 30. Sep 2010 17:14

Re: Kripke Struktur und CTL Formeln

Beitrag von Uhr » 11. Mär 2012 14:33

Wo kann man denn diese Übungen bekommen? Im Elzi sehe ich nur welche bis 08/09.

charfi90
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 8. Sep 2010 15:40

Re: Kripke Struktur und CTL Formeln

Beitrag von charfi90 » 11. Mär 2012 14:37

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

charfi90
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 8. Sep 2010 15:40

Re: Kripke Struktur und CTL Formeln

Beitrag von charfi90 » 11. Mär 2012 14:40

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:(
Zuletzt geändert von charfi90 am 11. Mär 2012 14:54, insgesamt 2-mal geändert.

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Kripke Struktur und CTL Formeln

Beitrag von fscheepy » 11. Mär 2012 14:50

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.

ElGamal
Nichts ist wie es scheint
Beiträge: 23
Registriert: 19. Dez 2011 20:56

Re: Kripke Struktur und CTL Formeln

Beitrag von ElGamal » 11. Mär 2012 14:54

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?

Uhr
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 30. Sep 2010 17:14

Re: Kripke Struktur und CTL Formeln

Beitrag von Uhr » 11. Mär 2012 15:05

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.

m2c1
Windoof-User
Windoof-User
Beiträge: 41
Registriert: 20. Dez 2010 10:39

Re: Kripke Struktur und CTL Formeln

Beitrag von m2c1 » 11. Mär 2012 15:25

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.
Zuletzt geändert von m2c1 am 11. Mär 2012 15:27, insgesamt 1-mal geändert.

allein
Mausschubser
Mausschubser
Beiträge: 60
Registriert: 15. Okt 2008 00:01

Re: Kripke Struktur und CTL Formeln

Beitrag von allein » 11. Mär 2012 15:26

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

m2c1
Windoof-User
Windoof-User
Beiträge: 41
Registriert: 20. Dez 2010 10:39

Re: Kripke Struktur und CTL Formeln

Beitrag von m2c1 » 11. Mär 2012 15:30

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.

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Kripke Struktur und CTL Formeln

Beitrag von fscheepy » 11. Mär 2012 15:43

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.

m2c1
Windoof-User
Windoof-User
Beiträge: 41
Registriert: 20. Dez 2010 10:39

Re: Kripke Struktur und CTL Formeln

Beitrag von m2c1 » 11. Mär 2012 15:47

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)).

Woyzeck
Erstie
Erstie
Beiträge: 18
Registriert: 13. Mär 2011 15:30

Re: Kripke Struktur und CTL Formeln

Beitrag von Woyzeck » 11. Mär 2012 15:53

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?

Antworten

Zurück zu „Archiv“