CTL

hallo,

wollte mal fragen, ob es seien kann dass folgende aussagen im prinzip das selbe ausdrücken:

AG( AF a ) und AG( EF a )

das heißt, von jedem zustand in dem berechnungsbaum ist ein zustand erreichbar, indem a gilt, und das unendlich oft.

Hallo,

die beiden Aussagen sind nicht äquivalent.

siehe folgendes Gegenbeispiel:

~a->a->a->...
|
~a->a->a->...
|
~a->a->a->...
|
~a->a->a->...
|
usw.

Es gibt einen unendlich langen Pfad, der nicht a erfüllt. Von jedem Zustand gibt es aber eine Verzweigung zu einem Pfad auf dem immmer a gilt.
Dieses Beispiel erfüllt AG(EF a), aber nicht AG(AF a).

Grüße
Stefan

Stefan Disch
Lehrstuhl für Betriebssysteme
Geb. 051 / Raum 02-031

ah, ok! jetzt ist es mir klar. dankeschön!