Frage zur Temporallogik

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Frage zur Temporallogik

Beitrag von null »

Hallo,

in der Vorlesung vom 20.11. steht folgende Formel:

NOT([] phi) <-> <>NOT(phi)

Wo ist in der folgenden Überlegung der Fehler?

NOT([] phi) bedeutet, dass phi nie wahr ist, also in keinem Zustand erfüllt ist. <>NOT(phi) bedeutet, dass für mindestens ein bestimmtes k phi nicht bestimmt ist.

Das ist meiner Ansicht aber nicht äquivalent. Kann mir jemand helfen?

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Frage zur Temporallogik

Beitrag von null »

Ah, ich glaube, dass ich bereits meinen eigenen Fehler gefunden habe. NOT([] phi) bedeutet nicht "nie", sondern "nicht immer". "Nie" wäre []NOT(phi).

Aber ich habe eine Frage zur Musterlösung der dritten Teilaufgabe der dritten Übung. Man sollte einen temporallogischen Term aufstellen. Mein Überlegung lautete:

r : process is acknowledged

not(r) U r OR []not(r)

Ist das auch richtig? Eigentlich bezieht sich die Frage nur auf den linken Teil des "or", da der rechte mit der Musterlösung übereinstimmt. Beim linken habe ich mir folgendes gedacht. Bis zu einem bestimmten k wird der Prozess nicht bearbeitet und dann irgendwann schon. In mindestens einem Zustand gilt also r, sodass der Prozess verarbeitet wurde.

Danke für die Hilfe

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Frage zur Temporallogik

Beitrag von yourmaninamsterdam »

Problem 3 in Übung 3 ist recht vage gehalten, in sofern würde ich nicht zu viel Hirnschmalz in das Suchen einer "perfekten" Lösung investieren. Dienen Ansatz verstehe ich allerdings nicht so ganz. Es gibt ja den Request, ein Acknowledgement und den Progress des Prozesses. Das sind schon recht unterschiedliche Sachen.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Frage zur Temporallogik

Beitrag von Nathan Wasser »

"not(r) U r" entspricht <>r. Beides sagt aus, dass es einen Zustand gibt in dem r gilt. Somit gibt es insbesondere einen ersten solchen Zustand. Die Tatsache, dass r vor diesem Zustand nicht gilt ist klar, das ist die Definition von "erster".

<>r entspricht not([]not(r)). Das folgt aus der Dualität von [] und <>.

Somit entspricht deine Formel "not(r) U r OR []not(r)" die deutlich kürzere Formel: TRUE

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Frage zur Temporallogik

Beitrag von null »

Oh, vielen Dank für die Hilfe! Ich verstehe nun meinen Fehler und finde es spannend, dass man man die Temporallogik auch so schön umformen kann.

Eine andere Sache ist mir aufgefallen, weil ich mir gerade die Musterlösun der dritten Hausübung anschaue. In dieser steht, dass Nr. 6c nicht erfüllbar ist und für 6b schwache Fairness benötigt wird.

Spin sagt mir jedoch, dass keine Fehler für das ltl Statement aus 6c vorliegen und in 6b habe ich error:0 auch ohne -f beim Aufruf der pan.

Wie kann das sein?
Danke :)

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Frage zur Temporallogik

Beitrag von yourmaninamsterdam »

Du musst pan mit '-a' aufrufen. Die Ausgabe sagt dir das auch ganz oben, wenn du es nicht tust. "Technischer" Hinweis: Spin akzeptiert nicht das aneinanderketten von Parameter, man muss also schreiben './pan -a -f'. Es geht nicht: './pan -af'

Antworten

Zurück zu „Archiv“