Kripke Struktur und CTL Formeln

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 16:02

Woyzeck hat geschrieben: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?
Die Zustände sind doch die Knoten? Die wiederum sind mit atomaren Proporsitionen (Aussagen) markiert.

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 16:03

m2c1 hat geschrieben: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)).
Was ist denn hier ein "aktueller Knoten"? Die Formeln gelten doch für den ganzen Baum (?), somit haben wir eine Art Existenzquantor: "In jedem Pfad (dafür steht das A in der CTL-Formel) gibt es einen Zustand (der imaginäre Existenzquantor :mrgreen: ), sodass im nächsten Zustand (oder in allen direkt nachfolgenden Zuständen?) p gilt"...irgendwie verwirrt mich das ganze :|

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 16:13

fscheepy hat geschrieben:
m2c1 hat geschrieben: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)).
Was ist denn hier ein "aktueller Knoten"? Die Formeln gelten doch für den ganzen Baum (?)
Ja, da hast du Recht, "aktueller Knoten" macht hier keinen Sinn.
fscheepy hat geschrieben:somit haben wir eine Art Existenzquantor: "In jedem Pfad (dafür steht das A in der CTL-Formel) gibt es einen Zustand (der imaginäre Existenzquantor :mrgreen: ), sodass im nächsten Zustand (oder in allen direkt nachfolgenden Zuständen?) p gilt"...irgendwie verwirrt mich das ganze :|
Woher nimmst du den Existenzquantor?

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 16:32

Naja ich hab ja gesagt, dass er nur imaginär ist, da meiner Meinung nach in jeder Aussage über die Pfade ("Für alle Pfade gilt...") auch ein "existiert ein Knoten, sodass..." steckt. Man macht also eine Aussage über alle Pfade, aber hat einen Existenzquantor in dem Sinne, dass man sagt, dass es in diesen Pfaden Knoten gibt, die die Formel(n) erfüllen. Beim erneuten Betrachten von Folie 7 im Foliensatz 12 ist mir außerdem folgendes aufgefallen:
M, s0 |= Formel
was ja zeigt, dass es doch einen "aktuellen Knoten" gibt. Wir stellen also in CTL eine Formel auf und suchen dann beim Model Checking die Zustände, für die diese Formel auch wirklich gilt. Ich glaube, ich habe CTL nun mehr oder weniger verstanden.

aloifolia
Mausschubser
Mausschubser
Beiträge: 63
Registriert: 22. Sep 2011 11:37

Re: Kripke Struktur und CTL Formeln

Beitrag von aloifolia » 12. Mär 2012 11:23

Meine Lösung für Teil b sieht so aus (kann durchaus fehlerhaft sein):
Generell gilt:
  • Kripke-Struktur K = (S,R,L) mit Zustandsmenge S, Zustandsübergangsrelation R aus SxS, Markierungsfunktion L aus S->2^M
  • p gilt in Zustand s, wenn p aus L(s) ist.
Ich habe für jeden Teil eine passende Kripke-Struktur gefunden:
  1. K = ({s}, {(s,s)}, { (s,{!p}) } ) <- da p in s nicht gilt, gilt p in keinem Zustand (!AGp), weshalb die Implikation direkt wahr ist.
  2. K = ({s}, {(s,s)}, { (s,{p}) } ) <- da p in s gilt, gilt p in allen Zuständen (AGp und damit auch EFp), sodass alle Teilausdrücke der Formel zu wahr auswerten.
  3. K = ({s,s'}, {(s,s'), (s',s)}, {(s,{!p}), (s',{p})} ) <- s |= phi gilt, da in allen direkten Nachfolgezuständen (also s') p gilt und es einen zukünftigen Zustand gibt, bei dem p nicht gilt (nämlich entweder direkt s in der Gegenwart oder tatsächlich in der Zukunft s->s'->s). s' |= phi gilt natürlich nicht, aber es gibt ja auch keine Vorgabe für den Zustand, von dem man ausgehen soll (es geht nur um Erfüllbarkeit), weshalb man sich den aussuchen darf.

Benutzeravatar
Ibliss
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 209
Registriert: 11. Apr 2008 04:08
Wohnort: Darmstadt

Re: Kripke Struktur und CTL Formeln

Beitrag von Ibliss » 12. Mär 2012 16:22

aloifolia hat geschrieben:Meine Lösung für Teil b sieht so aus (kann durchaus fehlerhaft sein):
Generell gilt:
  • Kripke-Struktur K = (S,R,L) mit Zustandsmenge S, Zustandsübergangsrelation R aus SxS, Markierungsfunktion L aus S->2^M
  • p gilt in Zustand s, wenn p aus L(s) ist.
Ich habe für jeden Teil eine passende Kripke-Struktur gefunden:
  1. K = ({s}, {(s,s)}, { (s,{!p}) } ) <- da p in s nicht gilt, gilt p in keinem Zustand (!AGp), weshalb die Implikation direkt wahr ist.
  2. K = ({s}, {(s,s)}, { (s,{p}) } ) <- da p in s gilt, gilt p in allen Zuständen (AGp und damit auch EFp), sodass alle Teilausdrücke der Formel zu wahr auswerten.
  3. K = ({s,s'}, {(s,s'), (s',s)}, {(s,{!p}), (s',{p})} ) <- s |= phi gilt, da in allen direkten Nachfolgezuständen (also s') p gilt und es einen zukünftigen Zustand gibt, bei dem p nicht gilt (nämlich entweder direkt s in der Gegenwart oder tatsächlich in der Zukunft s->s'->s). s' |= phi gilt natürlich nicht, aber es gibt ja auch keine Vorgabe für den Zustand, von dem man ausgehen soll (es geht nur um Erfüllbarkeit), weshalb man sich den aussuchen darf.
Zu Deiner Interpretation der letzten Struktur würde auch der Satz aus der Aufgabenstellung "Können die folgenden CTL-Formeln in einem Zustand erfüllt werden, oder nicht?" passen. Gute Lösung, finde ich.
"Honesty is the first chapter in the book of wisdom.
Alien vs Predator 2 is the movie version of that book."

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

Re: Kripke Struktur und CTL Formeln

Beitrag von allein » 12. Mär 2012 17:53

aloifolia hat geschrieben:Meine Lösung für Teil b sieht so aus (kann durchaus fehlerhaft sein):
Generell gilt:
  • Kripke-Struktur K = (S,R,L) mit Zustandsmenge S, Zustandsübergangsrelation R aus SxS, Markierungsfunktion L aus S->2^M
  • p gilt in Zustand s, wenn p aus L(s) ist.
Ich habe für jeden Teil eine passende Kripke-Struktur gefunden:
  1. K = ({s}, {(s,s)}, { (s,{!p}) } ) <- da p in s nicht gilt, gilt p in keinem Zustand (!AGp), weshalb die Implikation direkt wahr ist.
  2. K = ({s}, {(s,s)}, { (s,{p}) } ) <- da p in s gilt, gilt p in allen Zuständen (AGp und damit auch EFp), sodass alle Teilausdrücke der Formel zu wahr auswerten.
  3. K = ({s,s'}, {(s,s'), (s',s)}, {(s,{!p}), (s',{p})} ) <- s |= phi gilt, da in allen direkten Nachfolgezuständen (also s') p gilt und es einen zukünftigen Zustand gibt, bei dem p nicht gilt (nämlich entweder direkt s in der Gegenwart oder tatsächlich in der Zukunft s->s'->s). s' |= phi gilt natürlich nicht, aber es gibt ja auch keine Vorgabe für den Zustand, von dem man ausgehen soll (es geht nur um Erfüllbarkeit), weshalb man sich den aussuchen darf.
AGp bedeutet aber bei aktuellem zustand auch p gilt, deswegen könnte 1. nicht erfüllt werden. oder?
was genau "-> bedeutet eigentlich bei den Formeln?

aloifolia
Mausschubser
Mausschubser
Beiträge: 63
Registriert: 22. Sep 2011 11:37

Re: Kripke Struktur und CTL Formeln

Beitrag von aloifolia » 13. Mär 2012 10:14

Also, da AGp bei s nicht wahr ist, steht da sozusagen "falsch => [irgendwas anderes]" und das ist per Definition direkt wahr.
Die Pfeile "->" sind die aussagen-/prädikatenlogischen Implikationspfeile, die man auch gerne als "=>" schreibt. CTL ist ja gewissermaßen eine Erweiterung der Prädikatenlogik.

Antworten

Zurück zu „Archiv“