[MaLo] Übung 10

[FoSAP] Formale Systeme, Automaten, Prozesse
[BuK] Berechenbarkeit und Komplexität
[MaLo] Mathematische Logik

Beitragvon kb » 15.01.07 23:19

Ich möchte gern mal auf einiges Hinweisen, wie ich es aus dem Skript verstehe:

- Es wird für CTL-Formeln vorausgesetzt, dass jeder Knoten einen Nachfolger hat (S. 69 oben)

- die Quantoren "E" und "A" quantifizieren über unendliche Pfade in K (S.69 oben)

Nun zu meiner 1)
a) AG EF P
"An jedem unendlichen Pfad gilt überall (also an jedem Knoten), dass es von dort aus einen unendlichen Pfad gibt, über den ein Zustand erreicht werden kann, an dem P gilt".
Heißt für mich, man kann immer einen Zustand P erreichen.
=> CTL Formel ist FALSCH, denn das Gilt schon bei dem Unendlichen Pfad "3 -> 3 -> 3..." nicht!

b) (die direkte sprachliche Übersetzung lass ich mal aus).
Man kann von überall aus zu einem unendlichen Pfad gelangen, an dem !P gilt.
=> WAHR, denn man kann von überall aus zu dem unendlichen Pfad "3 -> 3 -> ..." gelangen.

c) Es gibt einen unendlichen Pfad, auf dem abwechselnd P und !P gilt.
=> WAHR, der Pfad "1 -> 2 -> 1 -> 2..."

Deshalb verstehe ich das "Auswerten" auch als "wahr oder falsch", und nicht als eine Angabe der Knotenmenge.
Vielleicht hab ich die Quantoren auf falsch gedeutet??
Benutzeravatar
kb
 
Beiträge: 1237
Registriert: 06.04.06 21:20
Wohnort: Aachen / Köln

Beitragvon pulsar » 16.01.07 00:50

kb hat geschrieben:"An jedem unendlichen Pfad gilt überall (also an jedem Knoten), dass es von dort aus einen unendlichen Pfad gibt, über den ein Zustand erreicht werden kann, an dem P gilt".


Das ist falsch. Dieses Missverständnis von "globally" hatte ich aber auch. Globally bedeutet hier nicht "an allen Knoten im Graph", sondern "an allen Knoten auf jedem ausgehenden Pfad". Die CTL wertet nämlich auch wie die ML knotenweise aus!

"Auswerten" bedeutet also, herauszufinden, an welchen Knoten die Formel gilt und an welchen Knoten nicht.
pulsar
 
Beiträge: 831
Registriert: 11.09.05 12:49
Wohnort: Aachen
Studiengang: Informatik (Dipl.)
Studiert seit: fertig
Anwendungsfach: Psycho

Beitragvon kb » 16.01.07 00:58

Ich meinte auch an jedem Knoten auf dem Pfad, und weil ich davor "ALLE unendlichen Pfade" gesagt habe, wären das im Endeffekt auch alle Knoten im Graphen.
(--edit-- wie gesagt, WÄRE, aber da ich ja falsch gedacht hab, ists eh egal)

Hm...also praktisch einen Knoten als Ausgangsknoten auffassen und alle davon ausgehenden unendlichen Pfade betrachten...
Zuletzt geändert von kb am 16.01.07 12:13, insgesamt 1-mal geändert.
Benutzeravatar
kb
 
Beiträge: 1237
Registriert: 06.04.06 21:20
Wohnort: Aachen / Köln

Beitragvon seth » 16.01.07 08:19

Es geht darum an welchen Knoten es gilt und an welchen nicht. Die CTL-Formeln sind nicht wahr oder falsch für den ganzen Graphen.
7.4.2008 AGo: Benutzer ist gebannt.
seth
 
Beiträge: 239
Registriert: 16.09.05 10:40
Wohnort: AC

Beitragvon Coolcat » 16.01.07 12:54

Zudem sollte man die Formeln schrittweise auswerten, da die Schritte auch Punkte geben. Wurde zumindest gestern so im Tutorium gesagt.
My software never has bugs. It just develops random features.
Benutzeravatar
Coolcat
Promoter
 
Beiträge: 2574
Registriert: 28.11.05 21:26
Wohnort: Kohlscheid / Düsseldorf
Studiengang: Informatik (Dipl.)
Studiert seit: fertig
Anwendungsfach: BWL

Beitragvon Sebi » 16.01.07 16:17

verpostet :/
Sebi
 
Beiträge: 107
Registriert: 27.11.06 10:05

Beitragvon kb » 16.01.07 20:51

Also hier mein Lösungsvorschlag zu der 1:

a) wie bereits gesagt, gilt an keinem Zustand.

b) gilt an ALLEN Zuständen:
"Von jedem ausgehenden unendlichen Pfad gelangt man irgendwann zu der Möglichkeit, auf einen Pfad zu gelangen ('wechseln'), auf dem immer !P gilt".
von 6,5,4 ausgehende ist das klar, da sie eh irgendwann auf die 3-Schleife treffen. Die 1-2-Schleife hat jedoch auch die MÖGLICHKEIT, irgendwann, nämlich wenn an Knoten 2 angekommen, auf einen solchen Pfad zu wechseln. Also alle Zustände.

c) Gilt an {1, 2}
Ist klar, dass schonmal nicht an 3 gilt => nicht an 4 gilt => nicht an 5 gilt => nicht an 6 gilt (da die Abwechslungsbedingung am kompletten Graphen gelten muss). Kann also höchstens an 1 oder 2 gelten, wenn man 1-2-Schleife langgeht. Und bei der ist das auch erfüllt.


Habs also bis auf die b wie Coolcat, mit der Begründung, dass die Möglichkeit ausschlaggebend ist.


Frage zur Aufgabe 2c)
"Pfade der Länge 4" : Ich dachte wir betrachten unendliche Pfade. Ist damit gemeint "vom aktuellen Zustand 4 weiter" ?
Benutzeravatar
kb
 
Beiträge: 1237
Registriert: 06.04.06 21:20
Wohnort: Aachen / Köln

Beitragvon Coolcat » 16.01.07 22:10

Die 1-2-Schleife hat jedoch auch die MÖGLICHKEIT, irgendwann (..)

Nein, hat sie nicht. :)
\llbracket EG \neg P \rrbracket^K = \{ 3, 4 \}
Auf dem einen Pfad der immer nur zwischen 1 und 2 wechselt kommst du niemals an 3 oder 4 vorbei. Für alle anderen Pfade, beispielsweise der, der 42-mal hin und her wechselt und dann zur 3 läuft gilt die Formel. Aber eben nicht für alle Pfade.

Coolcat
My software never has bugs. It just develops random features.
Benutzeravatar
Coolcat
Promoter
 
Beiträge: 2574
Registriert: 28.11.05 21:26
Wohnort: Kohlscheid / Düsseldorf
Studiengang: Informatik (Dipl.)
Studiert seit: fertig
Anwendungsfach: BWL

Beitragvon PsY » 16.01.07 23:02

hi,

wir haben bei der 2) c) mal versucht das mit der negation zu machen, haben folgendes:

\neg EX(1 \rightarrow EX(1 \rightarrow EX(1 \rightarrow EX \neg P )))

sind uns aber nicht sicher, was meint ihr?

MfG

PsY
"Ich habe mir immer gewünscht, dass mein Computer so leicht zu bedienen ist wie mein Telefon; mein Wunsch ging in Erfüllung: mein Telefon kann ich jetzt auch nicht mehr bedienen." - Bjarne Stroustrup
Benutzeravatar
PsY
 
Beiträge: 93
Registriert: 06.12.06 16:57
Wohnort: Aachen
Studiengang: Informatik (Dipl.)
Studiert seit: fertig
Anwendungsfach: Psycho

Beitragvon SpatzenArsch » 16.01.07 23:06

PsY hat geschrieben:hi,

wir haben bei der 2) c) mal versucht das mit der negation zu machen, haben folgendes:

\neg EX(1 \rightarrow EX(1 \rightarrow EX(1 \rightarrow EX \neg P )))

sind uns aber nicht sicher, was meint ihr?

MfG

PsY

Hi!

Wir haben es ohne Negation so: AX(AX(AX(AX P)))
SpatzenArsch
 
Beiträge: 202
Registriert: 15.04.06 12:14

Beitragvon Lupus » 16.01.07 23:16

auch ohne Negation - dafür auch ohne Klammern :-)
AXAXAXAX P
Es gibt 10 Arten von Menschen: Diejenigen, welche Binärcode verstehen und die, die es nicht tun.
Lupus
 
Beiträge: 125
Registriert: 19.05.06 16:28
Wohnort: Aachen
Studiengang: Informatik (Dipl.)
Anwendungsfach: Physik

Beitragvon foogy » 16.01.07 23:42

PsY hat geschrieben:hi,

wir haben bei der 2) c) mal versucht das mit der negation zu machen, haben folgendes:

\neg EX(1 \rightarrow EX(1 \rightarrow EX(1 \rightarrow EX \neg P )))

sind uns aber nicht sicher, was meint ihr?

MfG

PsY

Wofür die Implikationen?? M.E. nach überflüssig, jedoch nicht falsch.
Sätze mit "Wenn du mal Zeit hast ..." oder "Du studierst doch Informatik ..." können der eigenen Gesundheit schaden. Also lasst es!
Benutzeravatar
foogy
 
Beiträge: 1186
Registriert: 12.09.05 19:18
Wohnort: Oche!
Studiengang: Informatik (Dipl.)
Studiert seit: WS 06/07
Anwendungsfach: BWL

Beitragvon Raf » 17.01.07 00:14

zu 1b

Auf allen Pfaden gilt irgendwann, dass es einen Pfad gibt auf dem immer nichtP gilt. Implizert dieses "irgendwann" dass die pfade unendlich sein sollen, denn sonst ist nur 5,4,3 modell, von allen anderen knoten aus, kann man einen pfad konstruieren von dem aus man über nen P stolpert auf dem Weg zur 3.

Zb: 6 ... gibt kein pfad von dort aus an dem immer nP gilt

Gruß
Raf
 
Beiträge: 10
Registriert: 06.12.06 21:29
Wohnort: Aachen, Germany

Beitragvon kb » 17.01.07 00:23

hm, also ich hab da einfach nur AXXXXP stehen, was meiner Meinung nach ausreicht

Coolcat hat geschrieben:
Die 1-2-Schleife hat jedoch auch die MÖGLICHKEIT, irgendwann (..)

Nein, hat sie nicht. :)
\llbracket EG \neg P \rrbracket^K = \{ 3, 4 \}
Auf dem einen Pfad der immer nur zwischen 1 und 2 wechselt kommst du niemals an 3 oder 4 vorbei. Für alle anderen Pfade, beispielsweise der, der 42-mal hin und her wechselt und dann zur 3 läuft gilt die Formel. Aber eben nicht für alle Pfade.
OK, {1,2} sind nicht dabei, aber nicht aus dem von dir genannten Grund, sondern weil an 2 ein P steht. Denn EG!P heißt, dass von dem Zustand aus ein Graph (undzwar ein beliebiger, denn wenn er in dem Graphen, in dem ich mich befinde wäre, würd das keinen Sinn machen) erreicht werden kann. Ob ich mich nun die ganze Zeit auf 1-2 bewege macht keinen Unterschied, denn ich müsste bei EG!P eine erneute Überprüfung am aktuellen Zustand machen, undzwar auf die ganze Struktur bezogen.

--edit--
hm, vielleicht hast du das ja schon mit deinem \llbracket EG \neg P \rrbracket^K = \{ 3, 4 \} impliziert...naja, ich denke das hat sich geregelt ^^

--edit2--
@Raf
es werden afaik in CTL nur unendliche Pfade betrachtet
Zuletzt geändert von kb am 17.01.07 13:32, insgesamt 1-mal geändert.
Benutzeravatar
kb
 
Beiträge: 1237
Registriert: 06.04.06 21:20
Wohnort: Aachen / Köln

Beitragvon fw » 17.01.07 01:58

kb hat geschrieben:hm, also ich hab da einfach nur AXXXXP stehen


das ist nur leider keine (syntaktisch korrekte) CTL Formel :-)
Benutzeravatar
fw
 
Beiträge: 1356
Registriert: 17.05.06 19:37
Studiengang: Informatik (Dipl.)
Studiert seit: fertig
Anwendungsfach: Mathe

VorherigeNächste

Zurück zu Theoretische Informatik