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??