CTL

Hi,

ich habe eine Frage bezüglich der Aufgabe2 c) von Übungsblatt3. Leider ist die Korrektur nicht sonderlich aufschlussreich.

Man kommt abwechselnd in einen Zustand, in dem a gilt und in einen Zustand, in dem b gilt; zwischen diesen dürfen beliebig viele Zustände liegen

Kann ich schreiben:
AG( ((a ^ !b)v(!a ^ !b))U((b ^ !a)v(!a ^ !b)) v
((b ^ !a)v(!a ^ !b))U((a ^ !b)v(!a ^ !b)) )

Wo ich mir gar nicht sicher bin: Kann ich überhaupt ein until nach einem AG schreiben? Oder muss es dann nur A heißen, da ja mit AG gemeint ist auf allen Zuständen (und nicht allen Pfaden). Auch der Rest sieht mir sehr umständlich aus, geht das kürzer?

Grüße,
Johannes

Hi

Also ein U ohne vorhergehendes A oder E geht nicht (siehe Übungsblatt). Du meinst wahrscheinlich:

AG( A((a ^ !b)v(!a ^ !b))U((b ^ !a)v(!a ^ !b)) v A((b ^ !a)v(!a ^ !b))U((a ^ !b)v(!a ^ !b)) )

Da ((a ^ !b)v(!a ^ !b)) == !b und ((b ^ !a)v(!a ^ !b)) == !a, kannst Du kurz schreiben:

AG( A(!b)U(!a) v A(!a)U(!b) )

Gegenbeispiel: Betrachte folgenden Automaten:

a -> a -> a -> a -> / -> / -> ...

Im Startzustand a und den drei folgenden Zuständen gilt a aber nicht b, sonst gilt niemals a und niemals b. Für diesen Automat wird die obige CTL-Formel erfüllt.

Grüße
Tobias Nopper

Hallo Tobias,
Ich muss einfach nochmal fragen, wie der richtige Ausdruck (also die Lösung zu der Aufgabe) aussieht, denn ich komme selbst nicht drauf. Cube Connected Cycle im Hirn.

Grüsse Nils