infostudium.de

von **Coolcat** » 14.01.07 18:56

Es geht mir um die Definition der CTL. Genauer um die Definition von F (eventually) und G (globally).

$EF\psi \, \equiv \, E (1\, U\psi )$
$EG\psi \, \equiv \, E \neg (F \neg\psi) \, \equiv \, E \neg (1 \, U \neg\psi)$

Dabei wurde irgendwie gesagt, dass die Definition von G nicht ganz formal wäre, weil irgendwie die Negation nicht definiert wäre. Aber $1\, U\psi$ ist doch eine CTL-Formel und CTL ist unter $\neg , \vee , \wedge, \rightarrow$ abgeschlossen?

Edit: Hab dem Thread mal einen zum Thema passenden Titel gegeben, damit man ihr später wieder findet. Meine Frage habe ich ja unten irgendwo selbst beantwortet...

von **nathan99** » 14.01.07 20:29

Mal eine ganz dumme Frage, ich habe letzte Woche leider nur an der Vorlesung am Donnerstag teilnehmen können:

Welchen "Typ" hat denn die Lösung von Blatt 10 A1?

Soll man die Knoten ermitteln, an denen jeweils die Formel gilt?

von **Friedrich** » 14.01.07 20:38

@nathan
Nein, so wie ich das verstehe, spricht CTL nicht über Knoten, sondern über die ganze Struktur (also das Transsitionssystem).

Dabei sprechen die Quantoren über beliebige unendliche lange Pfade im Transsitionsystem.
Das heißt also entweder ist K Modell von einer gegebenen Formel oder eben nicht.

Wo ich noch ein Problem habe, ist nachzuvollziehen, was es genau bedeutet "psi gilt unendlich oft auf allen Pfaden" (vgl. Bsp4)
Soll das heißen, dass in jedem Knoten psi gilt? Nein, das kann nicht sein, denn das wird ausgedrückt durch
AG psi
Wie hat man sich also AGAF psi vorzustellen.

von **Coolcat** » 14.01.07 21:15

Soll man die Knoten ermitteln, an denen jeweils die Formel gilt?

Ich würde sagen die Menge der Knoten wo die Formel gilt, genau wie bei der ML, schließlich ist CTL eine Erweiterung der ML

Wie hat man sich also AGAF psi vorzustellen.

Egal wie du durch deine Kripkestruktur läufst, irgendwann kommt immer wieder ein Knoten an dem psi gilt. Wenn du dann weiter läufst kommt wieder irgendwann ein psi usw...
Für jeden Knoten auf dem Pfad gilt einfach: AF psi

Coolcat

von **foogy** » 14.01.07 21:55

Friedrich hat geschrieben:@nathan
Nein, so wie ich das verstehe, spricht CTL nicht über Knoten, sondern über die ganze Struktur (also das Transsitionssystem).

Dabei sprechen die Quantoren über beliebige unendliche lange Pfade im Transsitionsystem.
Das heißt also entweder ist K Modell von einer gegebenen Formel oder eben nicht.

Wo ich noch ein Problem habe, ist nachzuvollziehen, was es genau bedeutet "psi gilt unendlich oft auf allen Pfaden" (vgl. Bsp4)
Soll das heißen, dass in jedem Knoten psi gilt? Nein, das kann nicht sein, denn das wird ausgedrückt durch
AG psi
Wie hat man sich also AGAF psi vorzustellen.

Ist der Lösungstyp der Aufgabe nun definitv nur "1" oder "0"? Das war Freitag das erste, was mir durch mein krankes Hirn schoss. Das heißt, die Formel wird zu "1" ausgewertet, falls die durch die Formeln "geforderten" Bedingungen von jedem Konten aus gelten.
Ok, morgen ist Übung, da gibts den gleichen Aufgabentyp. Aber mir ist gerade langweilig, das muss ich mal sinnvoll ausnutzen.

von **nathan99** » 14.01.07 21:58

Mhm, da sollen wohl tatsächlich die Knoten v ermittelt werden, mit für die

K, v |= Formel

gilt.

[spoiler]
a) keiner
b) 3 4 5 6
c) 1 2
[/spoiler]

Wieviel Unsinn steckt drinn?

von **Sebi** » 14.01.07 22:07

Ich weiß nicht, aber ich habe für a,b c was ganz anderes raus für welche Knoten der Ausdruck stimmt.

[spoiler]
a) {1,6}
b) alle
c) keiner

von **foogy** » 14.01.07 22:40

Sebi hat geschrieben:Ich weiß nicht, aber ich habe für a,b c was ganz anderes raus für welche Knoten der Ausdruck stimmt.

[spoiler]
a) {1,6}
b) alle
c) keiner

Bei a) habe ich auch raus, dass die Formel für keinen Knoten gilt. Wie würdest du die Formeln denn wörtlich formulieren? Evtl. liegen hier ja Missverständnisse vor.

von **Sebi** » 14.01.07 22:45

In allen erreichbaren Zuständen gilt, ein Zustand kann erreicht werden an dem P gilt.

Ich bin mir nicht ganz sicher ob mich AG dazu zwingt, bei jedem Knoten den ich erreiche auch den Ausdruck EF P zu prüfen.

Also ich habe da ds Rekusiv zerlegt.
y1 = P
y2 = EF y1
y3 = AG y2

Demnach wären die Knoten für y1 2,5,6
Demnach wären die Knoten für y2 1,2,5,6
Und für meine Interpretation des AG würde eben 1,6 funktionieren...

von **nathan99** » 14.01.07 22:45

Meine Interpretation der Aufgabe, und es sei dazugesagt dass ich mir zwar relativ sicher bin, aber das erfahrungsgemäss in Malo nicht viel heisst:

Die Formel gildet an den Knoten, für die gilt:
Alle Pfade die ich gehen kann, haben die Eigenschaft, dass ich jederzeit einen Pfad zu einem P-Knoten gehen kann.

Für (1) würde ich dann den Pfad "1 -> 2 -> 3 -> 3 ..." vorschlagen, bei dem das nicht gilt...
Ich habs also so verstanden, dass man die Formel "in normale Worte fasst", und dann für a) alle irgendwie definierbaren Pfade betrachtet...

...was anderes:
...ist bei A2a gemeint: abwechselnd P und !P, EGAL womit es anfängt?

Also würde für v gelten dürfen dass P(v) oder !P(v), und es dann abwechselnd weitergeht?

von **foogy** » 14.01.07 23:02

Sebi hat geschrieben:In allen erreichbaren Zuständen gilt, ein Zustand kann erreicht werden an dem P gilt.

Ja, so habe ich die Formel auch aufgefasst. Dann habe ich eine Tabelle aufgestellt, welche Zustände von jedem Zustand aus erreichbar sind:

Zustand 1, erreichbar: 2,3,4,5,6
Zustand 2, erreichbar: 1,3,4,5,6
Zustand 3, erreichbar: 3
Zustand 4, erreichbar: 3
Zustand 5, erreichbar: 3,4
Zustand 6, erreichbar: 3,4,5

Aber beispielsweise von Zustand 3 aus kann kein anderer Zustand erreicht werden, an dem P gilt. Und da 3 von jedem anderen Knoten erreicht werden kann, gilt die Formel eben auch für keinen der sechs Zustände.

Jemand Einwände?

Hier mal die wörtlichen Interpretationen zu b) und c):

b) In allen erreichbaren Zuständen gilt irgendwann, dass ein Zustand erreicht werden kann, an dem P nicht gilt.
Edit: Hier für alle 1 (erfüllbar)? Die erreichbaren Zustände wie oben, und von jedem aus kann ein Zustand mit nicht P erreicht werden.

c) Es kann ein Zustand erreicht werden, an dem entweder P oder !P gilt: im Falle P gilt für alle von dort erreichbaren Zustände immer !P, im Falle !P gilt für alle von dort erreichbaren Zustände immer P.

Also gerade bei c) bin ich mir doch sehr unsicher. Intuitiv könnte man sagen, dass man irgendwann ein letztes P bzw. ein letztes !P erreicht.

von **Sebi** » 14.01.07 23:12

Kein Einwand ich habe für 1a auch KEINEN.
Für 2 habe die gleiche Interpretation wie Du.

von **heipei** » 15.01.07 09:43

hmm, die b) und c) hab ich wie nathan99. bei der a hab ich grade mal ein bisschen ueberlegt. eigentlich haette ich auch zu {1,6} tendiert, aber jetzt bin ich mir nicht mehr sicher, da AG (es gilt in allen pfaden) EF (in einem der _folgenden_ zustaende gilt) P. je nachdem wie man das jetzt verstehen soll kommen da entweder keine knoten oder {1,6} raus. heist AG EF P "gehe jeden pfad einen schritt weit und von da aus muss irgendwann P gelten" dann gilt das natuerlich fuer {1,6} nicht. heisst es "auf jedem pfad gilt irgendwann P (auch idrekt im ersten schritt)" dann schon.

hoffe ich hab nicht noch mehr verwirrung gestiftet

von **Coolcat** » 15.01.07 16:53

Also um mal auf die eigentliche Frage zurück zu kommen...

Mir ist es mittlerweile klar:
$1\, U\psi$ ist gar keine CTL-Formel. Nur $A (1\, U\psi)$ bzw. $E (1\, U\psi)$ wären eine gültige Formeln. Daher kann man $1\, U\psi$ natürlich auch nicht negieren.

von **Coolcat** » 15.01.07 17:24

Habe bezüglich der Aufgabe 1 übrigens auch das Ergebnis von nathan99.

zu b)
$\llbracket EG \neg P \rrbracket^K = \{ 3, 4 \}$
Bei allen Knoten auf denen P gilt, kann es ja sowieso schon mal nicht gelten. Vom Knoten 1 aus muss ich auf jeden Fall an einem Knoten mit P vorbei.

$\llbracket AF \, EG \neg P \rrbracket^K = \{ 3, 4, 5, 6 \}$
Alle Knoten wo man auf ALLEN Pfaden irgendwann zu einem Knoten kommt an dem $EG \neg P$ gilt. Man muss also auf ALLEN Pfaden irgendwann auf einen Knoten aus $\{ 3, 4 \}$ kommen.
Bei den Knoten 1 und 2 ist dies nicht der Fall, da man ja immer hin und her wechseln kann. (es gibt also einen Pfad wo das nicht so ist...)

zu c)
$\llbracket P \rightarrow AX \neg P \rrbracket^K = \{ 1,2,3,4,5 \}$
Bei 1, 3 und 4 gilt P nicht, also ist die Implikation wahr. Von 2 kann ich zu 1 und 3, bei beiden gilt ! P. Von 5 kann ich nur zu 4. Bei 6, kann ich nur zu 5, aber da gilt P.
$\llbracket \neg P \rightarrow AX P \rrbracket^K = \{ 1,2,5,6 \}$
Bei 2,5 und 6 gilt P, also Implikation wahr. Bei 1 kann ich zu 1,5 und 6, wo überall P gilt. Bei 3 und 4 gibt es keine P's mehr, also können die nicht drin sein.
$\llbracket ... \rrbracket^K = \{ 1,2 \}$
Nur bei 1 und 2 gibt es einen Pfad wo ich immer in beiden Mengen bleibe. (immer hin und her wechseln)

Coolcat

infostudium.de

Forum zum Informatikstudium an der RWTH Aachen

[MaLo] Übung 10

Übung 10