CTL - ÜB2, Aufgabe 2d. Komische Lösung?

Ich habe eine kleine Frage zur CTL.

ÜB2, Aufgabe 2d):

(! = NOT)
Musterlösung : !E(!bUa)
Wieso heisst die Lösung nicht A(bUa) ?

Was ist falsch an :

AG(a->bUa) bzw ganz korrekt nach CTL : AG(!a OR !bU!a)

Vielen Danke

A(bUa) verlangt, dass ALLE Zustaende vor a dann b erfuellen muessen, also:

b
|
b
|
:
:
|
b
|
a

dies ist offensichtlich nicht das erwuenschte - es soll nur mind. einmal ein b vor a gelten.

Zu AG(a->bUa) bzw. AG(!a OR !bU!a)
Letzteres muss korrekt umgeformt AG(!a OR b U a) sein. Diese Formel verlangt nur, dass vor dem a ueberall (!a OR b) gilt, Also nicht unbedingt b. Bsp:

c (explizit: (!a OR b))
|
a

Sei c hierbei beliebiger CTL-Ausdruck ungleich a oder b. AG(a->bUa) erfuellt dies, was jedoch offensichtlich nicht der Fall sein sollte.

Hoffe, dass das helfen konnte.
Gruesse,
Sven

Edit: habe noch ein paar Punkte genauer/"korrekter" beschrieben.



Edited 1 time(s). Last edit at 09/19/2007 11:53AM by Sven.

Hallo,

ist dieser Ausdruck:

AG(!a OR b U a)

Nun denn richtig?

Vielen Danke für deine Hilfe

AG(!a OR b U a) ist nur die korrekte Umformung von AG(a->bUa)

Bezogen auf die gewünschte Aussage sind beide falsch, wie ich oben versucht habe zu erklären.

Grüße,
Sven

müsste der ausdruck nicht einfach A(!a OR b U a) heißen? also ohne G. weil wir bei den ganzen ausdrücken auf ÜB 2 nirgends des ausdruck AGU stehen hatten, oder kann man das beliebig zusammenwürfeln?

Hallo,

wenn man CTL benutzt, ist jeder Temporaloperator IMMER mit einem Pfadquantor verknüpft.
Sonst ist es nicht mehr CTL! Es gibt natürlich noch andere Temporallogiken,
da hat man aber auch eine andere Semantik. Diese waren nicht Gegenstand der Vorlesung!

Ausdrücke wie z.B. AG(!a OR b U a) machen deshalb keinen Sinn, da nicht angegeben ist, ob der Teilausdruck bUa nun auf allen nachfolgenden Pfaden oder nur mindestens auf einem gelten soll. Solche Ausdrücke sind schon syntaktisch falsch!

Grüße
Stefan

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



Edited 1 time(s). Last edit at 09/22/2007 06:32PM by disch.

drdreii Wrote:
-------------------------------------------------------
> müsste der ausdruck nicht einfach A(!a OR b U a)
> heißen? also ohne G. weil wir bei den ganzen
> ausdrücken auf ÜB 2 nirgends des ausdruck AGU
> stehen hatten, oder kann man das beliebig
> zusammenwürfeln?

Hoppla... das war auch mein Fehler... kommt vom copy-pasten. Sorry, muss natürlich überall A(!a OR b U a) ohne dem G sein.

Grüße,
Sven