Hallo allerseits,
Ich vermute beim aktuellen Aufgabenblatt 5
(http://www.informatik.uni-hamburg.de/TGI/lehre/vl/WS1011/FGI2/sec/fgi-a5.pdf)
einen unglücklichen (da nicht offensichtlichen) Tippfehler.
Bei 5.3.1 sollte doch in M2 und M1 die LTL-Formel ψ gültig sein und nicht die CTL-Formel ϕ.
(Gerade mit Sicht auf Aufgabe 5.3.4)

Kann das vielleicht kurz jemand bestätigen?

Der Verdacht ist leider richtig. 5.3.1 bezieht sich komplett auf die beliebige LTL-Formel und hat mir der CTL-Formel nichts zu tun. Sorry…

Ich hab irgend wie den
Gegebeispiel gefunden:

SS(M1) ist die Menge aller Pfade aus M1 und SS(M2) ist die Menge aller
Pfade aus M2

M1:

s0 <-> s1

M2:
s0 <-> s1 <-> s2

Dann SS(M1) = (s0s1)^omega und SS(M2) = (s0s1s2s1)^omega
SS(M1) ist dann eine Teilmenge von SS(M2)
(phi) ist dann F(s2) also es gibt irgend wann mal s2
M2,s0 |= F(s2)
M1,s0 aber niemals |= F(s2)

Die Aufgabe macht mich verrueckt.

Das Gegenbeispiel funktioniert nicht, weil F(s2) in M2 nicht gilt.  M2 hat ja nicht nur den genannten Pfad, sondern auch (s0s1)^omega und noch einige weitere. M2 |= F(s2) gilt nur, wenn die Formel für alle Pfade erfüllt ist.