Fragen zum CTL

hallo, wollte mal fragen, ob beim ctl ein ausdruck wie [tex] $\neg (EG \neg \varphi)$ [/tex] gültig ist? und ob man wie in aussagelogischen ausdrücken sagen kann, dass z.B. A x = nicht (E nicht x)?

Hallo,

drdreii Wrote:
-------------------------------------------------------
> hallo, wollte mal fragen, ob beim ctl ein ausdruck
> wie $\neg (EG \neg \varphi)$ gültig ist? und ob

Eine Negation über einen gültigen Teilausdruck ist erlaubt.
So ist z.B. $\neg \varphi$ eine erlaubte Erweiterung von $\varphi$.
Dies ist in der ersten Regel auf dem Übungsblatt beschrieben, wobei
\phi immer einen gültigen Ausdruck beschreibt.

> man wie in aussagelogischen ausdrücken sagen kann,
> dass z.B. A x = nicht (E nicht x)?

Das macht keinen Sinn, da nur Pfadquantoren verwendet werden. In
CTL hat man immer Paare von Pfadquantoren und Operatoren.
z.B. AX, EX, A ... W ...
Eine allgemeine Aussage A x = nicht (E nicht x) berücksichtigt nicht die
Operatoren.

Ich hoffe das hilft.

Grüße
Stefan

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