CTL Basisoperatoren

Hi
Ich habe eine wilde Vermutung, was den CTL Basisoperatoren und der Aufgabe 1 des Übungsblatt 3 angeht. Und zwar sitze ich schon eine Zeit lang an manchen Teilaufgaben und denke, dass z.b. e) gar nicht lösbar ist, weil diese ein Basisoperator ist und nicht mit "Existenzquantoren" (ich meine mit existiert ein Pfad ...) ausdruckbar ist.

Meine Vermutung ist, dass die Vorlesung falsch an dieser Stelle ist, weil wir nur von 3 Basisoperatoren ausgingen, jedoch denke ich, dass z.b EF,AG ebenfalls Basisoperatoren sind. Insbesondere habe ich in einigen Model Checking Skripte gefunden, dass sie über 8 Basisoperatoren und nicht über 3, z.b. Quelle: [flp.cs.tu-berlin.de]

Nun, wer hat dann Recht?

Gruss
Pablo

Hi

Nein, sowohl EF als auch AG lassen sich durch eine Kombination der auf dem Übungsblatt angegebenen fünf Basisoperatoren ausdrücken.

Ein Hinweis zu EF: Vergleiche mal EFb und EaUb. Folgt eines der beiden aus dem anderen?

Wenn Du EF hast, ist AG auch nicht mehr schwer.

Grüße
Tobias Nopper

und ist das hier z.b gueltige ctl formeln:

not (EX (not phi))

phi or AX (E (NOT phi U phi))

felix

felix Wrote:
-------------------------------------------------------
> phi or AX (E (NOT phi U phi))
ok, die is wohl nich ganz korrekt.

hab aber noch ne frage zu E(aUb):

wenn a ab einem Zustand Z auf einem Pfad IMMER gilt, gilt dann Z |= E(aUb)

und

wenn b ab einem Zustand Z auf einem Pfad IMMER gilt, gilt dann auch Z|= E(aUb)

oder muessen a UND b immer auftauchen?

felix

Hi

felix schrieb:
a) wenn a ab einem Zustand Z auf einem Pfad IMMER gilt, gilt dann Z |= E(aUb)?
b) wenn b ab einem Zustand Z auf einem Pfad IMMER gilt, gilt dann auch Z|= E(aUb)?

Langsam, langsam. Du redest hier über Pfade, schreibst aber dann Zustandsformeln hin.

1. Ein Pfad, für den in jedem Zustand a gilt aber niemals b, erfüllt _nicht_ (aUb).
2. Ein Pfad, für den in jedem Zustand b gilt, _erfüllt_ (aUb).

Quantisierung über die Pfade (A/E) liefert dann den Rest.

Übrigens: Wenn Z|=c gilt, gilt für beliebige CTL-Formeln d auch Z|=E(dUc) und Z|=A(dUc).

Grüße
Tobias Nopper

P.S.: Ich habe in diesem Thread zwei Postings gelöscht, deren Inhalt redundand war.



Edited 1 time(s). Last edit at 05/17/2005 01:35PM by nopper.

Koennte man auch zwei Moeglichkeiten haben aequivalente Formeln zu definieren ?
z.B.
fuer AFa:
1. !EG!a
2. !E!(!aUa)
wobei ! einfach not darstellen sollte.

DANKE

Hi

Ich gehe jetzt nicht auf Deine Beispiele ein; schließlich will ich hier weder eine Muster-Lösung noch eine Muster-Nichtlösung angeben. ;)

Generell gibt es natürlich für alle Eigenschaften mehrere Möglichkeiten, sie aufzuschreiben - genau genommen sogar unendlich viele. Ein ganz einfaches Beispiel wäre a, !!a, !!!!a, !!!!!!a, ...; mit CTL-Operatoren geht das aber genauso.

Vorsicht aber mit !E!(!aUa), das ist keine CTL-Formel; zwischen E und ( darf keine Negation stehen. Schau Dir die Definition von CTL in der Aufgabe nochmal an.

Grüße
Tobias Nopper

nopper Wrote:
-------------------------------------------------------
> 1. Ein Pfad, für den in jedem Zustand a gilt aber
> niemals b, erfüllt _nicht_ (aUb).
> 2. Ein Pfad, für den in jedem Zustand b gilt,
> _erfüllt_ (aUb).


> Übrigens: Wenn Z|=c gilt, gilt für beliebige
> CTL-Formeln d auch Z|=E(dUc) und Z|=A(dUc).


Hi Norbert,

jetzt noech eine letzte Frage zu aUb:

Muss, sobald das a durch das b "abgeloest" wurde b in _jedem_ darauffolgenden Zustand gelten, oder reicht einmal b?

Veranschaulicht:

a->a->b->b->b->b //hier gilt aUb
a->a->a->b->!b->!b //und hier, und falls ja
b->!b->!b->!b //dann wohl auch hier?

Ciao,
Felix

Ciao,
Felix

Hi

Tobias _Nopper_... nicht Norbert... ;)

Zu Deiner Frage: Einmal reicht.

Grüße
Tobias Nopper

Noch ne Frage:
Müssen wir beweisen, dass unsere Lösungen stimmen? Ich meine, reicht es einfach nur die Lösung hinzuschrieben?