Frage zur Temporallogik

[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]

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]

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]

"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]

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]

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'