Übung 13 - Aufgabe 1

Streber
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 4. Mai 2008 13:48

Übung 13 - Aufgabe 1

Beitrag von Streber » 14. Mär 2011 12:52

Hallo,

ich habe folgendes geschrieben:

1) p gilt niemals

AG ¬p

oder

¬EF p

2) Wann immer in einem Zustand p gilt, dann gilt in allen von diesem Zustand aus
erreichbaren Zuständen q nie mehr

AF p --> AG ¬q

3) Entweder gibt es einen Nachfolgezustand in dem p gilt oder p gilt niemals

EX p v AG ¬p

Was meint ihr, ist das so richtig?

Danke im Voraus :oops:

tud
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 117
Registriert: 9. Mär 2011 14:07

Re: Übung 13 - Aufgabe 1

Beitrag von tud » 14. Mär 2011 13:04

Ich glaube 2 und 3 ist falsch. Denk am besten noch einmal drüber nach, oder willst du gleich meine Lösung?

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Übung 13 - Aufgabe 1

Beitrag von dschneid » 14. Mär 2011 13:19

a) Hab ich auch so.

b) Da habe ich stattdessen: \(AG \; p \rightarrow (AG \; \neg q)\). Ich denke, es muss \(AG\) heißen, weil das für alle noch erreichbaren Zustände gelten soll ("wann immer").

c) Hier hast du ja ein oder, aber es heißt ja in der Aufgabe "entweder ... oder". Deine Formel ist auch erfüllt, wenn es einen Nachfolgezustand mit p gibt und p niemals gilt. Könnte aber sein, dass die Formel trotzdem so passt, weil die Möglichkeit, dass beides gleichzeitig erfüllt wird, nicht möglich ist, denn wenn p nie gilt, kann auch in keinem Nachfolgezustand p gelten.

Du musst außerdem mit der Klammerung aufpassen. Bei c) müsste es glaube ich mal mindestens \((EX \; p) \vee (AG \; \neg p)\) heißen, sonst erstreckt sich das erste \(EX\) über die ganze Formel, und dein \(AG\) würde dann die Dinge von diesem anderen Zustand aus betrachten.

tud
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 117
Registriert: 9. Mär 2011 14:07

Re: Übung 13 - Aufgabe 1

Beitrag von tud » 14. Mär 2011 13:53

dschneid hat geschrieben: b) Da habe ich stattdessen: \(AG \; p \rightarrow (AG \; \neg q)\). Ich denke, es muss \(AG\) heißen, weil das für alle noch erreichbaren Zustände gelten soll ("wann immer").
Ich glaube, das ist auch falsch, auch wenn das richtige gedacht wurde. Man muss so klammern: \(AG ( p \Rightarrow AG \; \neg q)\).

Dein \((AG p) \Rightarrow ( AG \; \neg q)\) hieße nämlich, dass, wenn überall p gilt, q nirgends gilt.

tud
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 117
Registriert: 9. Mär 2011 14:07

Re: Übung 13 - Aufgabe 1

Beitrag von tud » 14. Mär 2011 14:02

dschneid hat geschrieben: c) Hier hast du ja ein oder, aber es heißt ja in der Aufgabe "entweder ... oder". Deine Formel ist auch erfüllt, wenn es einen Nachfolgezustand mit p gibt und p niemals gilt. Könnte aber sein, dass die Formel trotzdem so passt, weil die Möglichkeit, dass beides gleichzeitig erfüllt wird, nicht möglich ist, denn wenn p nie gilt, kann auch in keinem Nachfolgezustand p gelten.
Das stimmt, da habe ich mich verdacht. Die Kombination aus beiden kann ja sowieso nie gelten, so kann man hier auch das einfache oder verwenden. Eine andere Möglichkeit wäre \((AX\neg p)\Rightarrow (AG \neg p)\).

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Übung 13 - Aufgabe 1

Beitrag von dschneid » 14. Mär 2011 14:14

tud hat geschrieben:Ich glaube, das ist auch falsch, auch wenn das richtige gedacht wurde. Man muss so klammern: \(AG ( p \Rightarrow AG \; \neg q)\).

Dein \((AG p) \Rightarrow ( AG \; \neg q)\) hieße nämlich, dass, wenn überall p gilt, q nirgends gilt.
Stimmt, ich habe die Bindungsstärke der Quantoren gerade falsch herum angenommen, nämlich als niedrigste statt als höchste. Du hast natürlich Recht. Dann wäre auch mein vorheriger Einwand zur ersten für c) vorgeschlagenen Formel hinfällig.

tud
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 117
Registriert: 9. Mär 2011 14:07

Re: Übung 13 - Aufgabe 1

Beitrag von tud » 14. Mär 2011 14:18

Gut, dann sind wir uns hier ja einig.

Wie sieht es eigentlich mit (pUq) aus? Das heißt ja, dass p solange gilt, bis einmalig q gilt. Wäre (pUq) auch erfüllt, wenn p immer gilt und q nie, oder impliziert (pUq) bereits EFq?

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Übung 13 - Aufgabe 1

Beitrag von dschneid » 14. Mär 2011 14:25

Ja, ich hatte irgendwo gelesen, dass E(pUq) gelesen werden soll als "p gilt bis q gilt und q gilt irgendwann". Das würde also EF q implizieren. Daher kommt ja auch die Art, wie EF auf EU zurückgeführt wird (auch wenn das hier an einer Stelle auf den Folien falsch ist, aber im Code des Algorithmus ist es richtig).

tud
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 117
Registriert: 9. Mär 2011 14:07

Re: Übung 13 - Aufgabe 1

Beitrag von tud » 14. Mär 2011 14:29

dschneid hat geschrieben:Ja, ich hatte irgendwo gelesen, dass E(pUq) gelesen werden soll als "p gilt bis q gilt und q gilt irgendwann". Das würde also EF q implizieren. Daher kommt ja auch die Art, wie EF auf EU zurückgeführt wird (auch wenn das hier an einer Stelle auf den Folien falsch ist, aber im Code des Algorithmus ist es richtig).
Genau. Und aus ähnlichen Gründen kann F sich auch auf den aktuellen Zustand und nicht nur auf zukünftige beziehen. Das wird auf der Folie 8 durch die Rückführungen klar, folgt aber eben nicht aus der "Definition" auf Folie 7.

Streber
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 4. Mai 2008 13:48

Re: Übung 13 - Aufgabe 1

Beitrag von Streber » 14. Mär 2011 15:50

Also auf was habt ihr euch geeinigt :oops:

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Übung 13 - Aufgabe 1

Beitrag von dschneid » 14. Mär 2011 15:52

\(AG ( p \Rightarrow AG \; \neg q)\) :wink:

ms1006
Erstie
Erstie
Beiträge: 14
Registriert: 1. Mai 2009 15:58

Re: Übung 13 - Aufgabe 1

Beitrag von ms1006 » 14. Mär 2011 16:20

Ich hätte noch eine Frage zu b):
"Wann immer in einem Zustand p gilt, dann gilt in allen von diesem Zustand aus
erreichbaren Zuständen q nie mehr"

Ist ein Zustand immer von sich selbst aus erreichbar? Wenn nicht, so könnte die Formel doch auch lauten:
\(AG(p \rightarrow \ AX(AG \neg q)).\)

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Übung 13 - Aufgabe 1

Beitrag von dschneid » 14. Mär 2011 16:37

Wenn ich mir Folie 7 anschaue, scheint es so zu sein, dass jeder Zustand von sich selbst aus erreichbar ist (zumindest ist der Wurzelknoten des Baumes hier jeweils auch markiert). Wieso meinst, du dass die Formel anders aussehen müsste, wenn es nicht so ist? Dann wäre eben die Definition von Erreichbarkeit anders, aber die Formel würde doch so oder so die gewünschte Semantik haben.

ms1006
Erstie
Erstie
Beiträge: 14
Registriert: 1. Mai 2009 15:58

Re: Übung 13 - Aufgabe 1

Beitrag von ms1006 » 14. Mär 2011 16:43

Die Formel \(AG(p \Rightarrow AG \neg q)\) besagt unter Anderem, dass in einem Zustand, in dem p gilt, ebenfalls \(\neg q\) gelten muss.
In meiner Formel muss in Zuständen, in denen p gilt, nicht unbedingt \(\neg q\) gelten, sondern nur in den (echten) Nachfolgezuständen. (?)

tud
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 117
Registriert: 9. Mär 2011 14:07

Re: Übung 13 - Aufgabe 1

Beitrag von tud » 14. Mär 2011 16:53

ms1006 hat geschrieben:Die Formel \(AG(p \Rightarrow AG \neg q)\) besagt unter Anderem, dass in einem Zustand, in dem p gilt, ebenfalls \(\neg q\) gelten muss.
In meiner Formel muss in Zuständen, in denen p gilt, nicht unbedingt \(\neg q\) gelten, sondern nur in den (echten) Nachfolgezuständen. (?)
Genau das habe ich mir auch gedacht. Vermute aber, dass unsere Lösung gemeint war und sie es einfach nur unsauber formuliert haben. Denn erreichbar ist ein Zustand nicht von sich selbst aus. Deshalb haben sie auch genauso in der Definition von F geschlampt. Dort hätte man auch noch zusätzlich den Fall, dass man den Zustand selbst meint, aufführen müssen.

Antworten

Zurück zu „Archiv“