CTL - ÜB2, Aufgabe 2d. Komische Lösung?
September 18, 2007 03:42PM
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
Re: CTL - ÜB2, Aufgabe 2d. Komische Lösung?
September 18, 2007 04:02PM
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.
Re: CTL - ÜB2, Aufgabe 2d. Komische Lösung?
September 20, 2007 12:38PM
Hallo,

ist dieser Ausdruck:

AG(!a OR b U a)

Nun denn richtig?

Vielen Danke für deine Hilfe
Re: CTL - ÜB2, Aufgabe 2d. Komische Lösung?
September 20, 2007 12:54PM
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
Re: CTL - ÜB2, Aufgabe 2d. Komische Lösung?
September 22, 2007 05:57PM
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?
Re: CTL - ÜB2, Aufgabe 2d. Komische Lösung?
September 22, 2007 06:20PM
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.
Re: CTL - ÜB2, Aufgabe 2d. Komische Lösung?
September 22, 2007 11:25PM
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
Sorry, you do not have permission to post/reply in this forum.