Übung 13 - Aufgabe 1

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

Re: Übung 13 - Aufgabe 1

Beitrag von Streber » 14. Mär 2011 17:29

Wie kann man eigentlich die Implikation hier verstehen? Vor allem teil b.)

Kann jmd die Kripke-Struktur posten?

Danke :)

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

Re: Übung 13 - Aufgabe 1

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

Streber hat geschrieben:Wie kann man eigentlich die Implikation hier verstehen? Vor allem teil b.)
Implikation bedeutet dasselbe wie sonst auch in der Aussagenlogik, von der CTL ja eine Erweiterung ist: \(\phi \rightarrow \psi \equiv \neg\phi \vee \psi\). Meintest du das?

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 17:39

Mich wundert nur, dass ihr immer \(\rightarrow\) anstelle von \(\Rightarrow\) verwendet. In der Mathematik st für Implikationen doch ausschließlich \(\Rightarrow\) zu verwenden.

jno
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 144
Registriert: 18. Mai 2007 09:41

Re: Übung 13 - Aufgabe 1

Beitrag von jno » 14. Mär 2011 17:40

tud hat geschrieben:Mich wundert nur, dass ihr immer \(\rightarrow\) anstelle von \(\Rightarrow\) verwendet. In der Mathematik st für Implikationen doch ausschließlich \(\Rightarrow\) zu verwenden.
Die Logiker kochen notationstechnisch immer so ein bisschen ihr eigenes Süppchen ^^

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

Re: Übung 13 - Aufgabe 1

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

Achso. Ich weiß nicht genau, aber wurde in FGdI nicht auch \(\rightarrow\) benutzt? Wie auch immer; das ist ja eine reine Syntaxfrage, beides meint eine Implikation. Ich glaube, \(\rightarrow\) wird eher in der Logik verwendet, während \(\Rightarrow\) mehr so allgemeine mathematische Notation ist.

Wegen der Kripke-Strukturen für b):
1. Eine Struktur mit nur einem Zustand ohne Markierung und einer Transition von diesem Zustand zu sich selbst. Nicht in allen zukünftigen Zuständen, nämlich in keinem, gilt p, also ist die Implikation wahr, weil die Prämisse falsch ist.
2. Eine Struktur mit nur einem Zustand, der mit p markiert ist, und einer Transition von diesem Zustand zu sich selbst. In allen zukünftigen Zuständen gilt p, und insbesondere auch in mindestens einem zukünftigen.
3. Eine Struktur mit zwei Zuständen, einer ohne Markierung, der andere mit p markiert, die jeweils eine Transition zum anderen Zustand haben. Betrachtet man nun den nicht-markierten Zustand, so sind alle nächsten Zustände mit p markiert, aber es gibt einen zukünftigen Zustand (oder sogar den jetzigen Zustand selbst), in dem p nicht gilt.

jno
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 144
Registriert: 18. Mai 2007 09:41

Re: Übung 13 - Aufgabe 1

Beitrag von jno » 14. Mär 2011 17:53

Die b) würde mich jedenfalls auch mal interessieren. Ich weiß auch nicht so genau, wie man eine solchen Kripke-Struktur visualisiert oder aufschreibt. Da das ja so eine Art FSM ist, würde ich jetzt einfach einen gerichteten Graphen zeichnen, dessen Knoten die Zustände sind, markiert mit den dort geltenden Formeln. Die Kanten sind entsprechend die Übergänge. Für die 3 CTL-Formeln würde ich jetzt sagen:

1. Gilt nie.
2. Man nimmt eine Struktur, wo in jedem Zustand p gilt.
3. | ZUSTAND 1, p gilt nicht | -------> |Zustand 2, p gilt|---------->|Zustand 3, p gilt nicht|

Was meint ihr?
dschneid hat geschrieben: Wegen der Kripke-Strukturen für b):
1. Eine Struktur mit nur einem Zustand ohne Markierung und einer Transition von diesem Zustand zu sich selbst. Nicht in allen zukünftigen Zuständen, nämlich in keinem, gilt p, also ist die Implikation wahr, weil die Prämisse falsch ist.
Ouh... Das is natürlich clever... ^^

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

Re: Übung 13 - Aufgabe 1

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

Bei 3. musst du aufpassen: Die Kripke-Struktur soll per Definition total sein, jeder Zustand soll also mindestens einen Nachfolger haben. Du müsstest hier also irgendwo eine Schleife einbauen.

jno
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 144
Registriert: 18. Mai 2007 09:41

Re: Übung 13 - Aufgabe 1

Beitrag von jno » 14. Mär 2011 18:07

Achja... richtig. Danke. :)

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 18:09

Ich dachte eine Kripke-Struktur hat keine Schleifen. Man baut alles immer weiter nach unten.

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

Re: Übung 13 - Aufgabe 1

Beitrag von Streber » 14. Mär 2011 18:11

Ne Kripke Struktur soll in einen Computation Tree überführt werden also in eine Baumstruktur....

Kripke Struktur hat zyklen, schleifen etc...

FGB
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 21. Jan 2006 14:41
Wohnort: Darmstadt
Kontaktdaten:

Re: Übung 13 - Aufgabe 1

Beitrag von FGB » 15. Mär 2011 10:32

Zum Aufgabenteil b.)

1. Heißt: Wenn für alle p gilt, dass in Zukunft immer p gilt, dann gilt für alle Pfade, welche aus dem 1. erreichbar sind, dass p nicht gilt.
Widerspruch in sich würde ich sagen -> Nein

2. Für alle p gilt, dass in Zukunft immer p gilt und [Wenn p für alle in Zukunft gilt, gibt es (mind.) ein p, was gilt]. Hmm richtig ? :roll:
Würde sagen, das stimmt so.

3. Wenn im nächsten Zustand p gilt (für alle Pfade), dann [wenn im darauffolgenden Zustand p gilt, gibt es einen Pfad, in dem p nicht gilt]. Hört sich doof an :/

Hm, keine Ahnung :-/


EDIT: SCHEISS CACHE. Ist doch zum kotzen. Sorry hab das oben nicht gesehen.

Antworten

Zurück zu „Archiv“