Vorlesung 12 (Model Checking): Folie 8 - Frage

aloifolia
Mausschubser
Mausschubser
Beiträge: 63
Registriert: 22. Sep 2011 11:37

Vorlesung 12 (Model Checking): Folie 8 - Frage

Beitrag von aloifolia »

Im Modelchecking-Skript verstehe ich einen Zusammenhang auf Folie 8 nicht. Dort steht
(EF)phi = !E(TUphi)

Wenn ich das mal ausformuliere hast das doch:
"Es gibt einen Nachfolgerpfad, bei dem in irgendeinem Zustand phi gilt"
=
"Es gibt keinen Nachfolgerpfad, bei dem alle Zustände wahr sind bis phi (ab einem Zustand x) gilt."

Wo ist da der Zusammenhang?

Woyzeck
Erstie
Erstie
Beiträge: 18
Registriert: 13. Mär 2011 15:30

Re: Vorlesung 12 (Model Checking): Folie 8 - Frage

Beitrag von Woyzeck »

Ich bin auch der Meinung, dass dort die Verneinung am Anfang nicht hingehört, schließlich heißt E(T U phi) so viel wie: "Es gibt einen Pfad, in dem irgendwann einmal phi gilt" und das ist ja durchaus äquivalent zu der Aussage EF phi.

Vergleiche auch: http://de.wikipedia.org/wiki/Computation_Tree_Logic
(Unten sind die gleichen Äquivalenzen aufgeführt, aber die angesprochene eben ohne die Verneinung)

Antworten

Zurück zu „Archiv“