Vielleicht kann mir jemand zur Fairness in CTL auf die Sprünge helfen…
Es geht um S. 218 im Script Teil 2.

Dort wird die faire Semantik in CTL eingeführt.

Weiter unten heißt es dann:

M,s |=(F) p Genau dann wenn M,s |= (p && fair)

(In Zustand s gilt in der fairen Semantik, dass Formel p gilt GDW in der normalen Semantik in s p gilt und fair gilt)

wobei fair := EGTrue

Geht dabei nicht die Fairness verloren?

Nur weil es mit p zusammen eine unendliche Folge gibt, heißt doch nicht, dass ich in eine faire strenge Zusammenhangskomponente C kommen muss, die die Bedingung Pi geschnitten C != leere Menge erfüllt, oder?

Also wird doch bei M,s |= (p && fair) die Menge F = {P1, …, Pk} außer Acht gelassen?

Danke!

Ich konnte mir da bisher auch nicht den Sinn erschließen.
Hast du inzwischen etwas herausgefunden oder gibt es vielleicht doch inzwischen jemanden, der weiß, wie das funktioniert?

Ich denke auch, dass die Äquivalenz
"M,s |= p GDW M,s |=F p && fair" so
nicht stimmt. In dem ganzen Abschnitt
geht es allerdings ja um einen Algorithmus
um die Gültigkeit von Formeln bei fairer
Semantik zu überprüfen. Ich würde daher
vermuten, dass dort folgendes gemeint ist:

Wenn man in einem Algorithmus, der die
Gültigkeit der rechten Seiten überprüft, die
Teilformel "fair" speziell behandelt und auf
sie immer die faire Semantik anwendet (wegen
fair=EGTrue kann man dazu die Prozedur
CheckFairEG benutzen), kann man tatsächlich
die rechten Seiten verwenden, um die Gültigkeit
der linken zu beurteilen.

Formal könnte man das vielleicht mit (noch) einem
Quantor beschreiben. Man definiert
[img]http://mokrates.de/cgi-bin/texstring?M%2Cs%5Cmodels%20If%5CLeftrightarrow%20M%2Cs%5Cmodels_F%20f[/img]
für alle Formeln f. Dann kann man die Äquivalenzen
auf S. 218 schreiben als
[img]http://mokrates.de/cgi-bin/texstring?M%2Cs%5Cmodels_F%20p%20%5CLeftrightarrow%20M%2Cs%5Cmodels%20p%5Cwedge%20Ifair[/img]
(und die anderen analog). Jetzt sieht man, dass man
die rechte Seite prüfen kann und daher auch ein
Verfahren für die linke hat.

Danke georg,
so in der Art habe ich es mir auch vorgestellt.

Man benutzt also erst die faire Semantik um die Zustände zu labeln von denen es einen fairen Pfad gibt.
Dann steht "fair" in label(s), wenn es von s einen fairen Pfad gibt.

Und DANACH gelten diese Äquivalenzen.