Hallo alle zusammen,

das 3. Übungsblatt steht im Netz. Der Abgabetermin ist der 5. Juni 2008, 14:00 Uhr (s.t.). Aufgrund der etwas spärlichen Abgabezahlen möchte ich euch daran erinnern, dass der klausurrelevante Stoff aus den in der Vorlesung oder in den Übungen behandelten Themen besteht.


Gruß,
Ralf.

Hallo, ich habe eine Frage zu CTL, die in meinen Augen nicht ganz klar aus den Definitionen auf dem Blatt hervorgeht:

A.) Ich bin im Zustand s_a, von dem geht eine Kante zu einem Zustand s_b. s_a erfüllt phi, s_b tut dies nicht. Welche der folgenden Aussagen ist wahr?

1.) EG(phi), da auch ein Pfad ohne Kanten schon ein Pfad ist?
2.) EF(phi), mit analoger Begründung?
3.) U(not phi E phi)?

B.) Ich bin im Zustand s_a, der phi erfüllt und vom s_a gehen keine Kanten weiter (Sackgasse)
Gilt hier AG(phi), weil es keinen Pfad gibt, auf dem mal phi nicht erfüllt ist?

Danke und Grüße,
Björn

A)
1. Wir betrachten nur unendliche Pfade. Auf einem solchen Pfad muss in jedem Zustand Phi gelten, damit EG(phi) erfüllt ist.
2. EF(phi) ist in Zustand s wahr, sobald irgendein Zustand, der von s aus erreichbar ist, phi erfüllt (phi darf dabei auch in s erfüllt sein).
3.) U(not phi E phi) ist keine gültige CTL-Formel. Du meinst wohl E(not phi U phi). Das ist äquivalent zu EF phi.

B) Wir nehmen an, dass es keine Sackgassen gibt. Ansonsten hättest Du recht.

Gruß,
Ralf.

Danke erstmal, ich habe noch eine Nachfrage
A2.) ich bin in s und s erfüllt phi und kein Nachfolgezustand von s erfüllt phi. Reicht die Tatsache, dass s phi erfüllt schon aus, damit EF(phi) in s wahr wird?

Nochmal Danke,
Björn

A2) EF phi heißt: es gibt einen von s ausgehenden Pfad, auf dem in mindestens einem Zustand phi gilt. Wenn der Pfad von s ausgeht, dann liegt s auf dem Pfad. Wenn phi in s gilt, dann erfüllt s die Formel EF phi. Somit ist die Antwort auf Deine Frage: ja.

Gruß,
Ralf.