CTL
August 20, 2005 08:46PM
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
Re: CTL
August 22, 2005 01:52PM
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
Re: CTL
August 26, 2005 10:30PM
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
Sorry, you do not have permission to post/reply in this forum.