CTL Operatoren < Sonstiges < Hochschule < Mathe < Vorhilfe
|
Status: |
(Frage) für Interessierte | Datum: | 19:27 Mo 23.05.2005 | Autor: | supertux |
Als Erstposter folge ich den Befehlen: Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt. :)
Also, in der Vorlesung (Rechnerachitektur) haben wir eine kleine Einführung der CTL bekommen, eigentlich nur eine Vorstellung der CTL Operatoren. Und da es für mich viel zu wenig war, versuche ich selber ein bisschen mehr über die CTL in Erfahrung zu bringen.
Gleich habe ich gemerkt, dass die Negation von CTL Formel nicht ganz Identisch wie in der Logik der ersten Stufe ist. Ich versuche [mm] EF(\phi) [/mm] anders zu schreiben, da habe ich mir gedacht, ich schreib so [mm] ¬(¬EF(\phi)) [/mm] nur bei [mm] ¬EF(\phi) [/mm] war nicht für mich trivial. Dann habe ich so veruscht: ¬(AG [mm] ¬\phi)) [/mm] aber ich denke, dass das nicht ganz korrekt ist. Ich denke, ich habe ein Gegenbeispiel gefunden.
Dannn habe ich mir E(xUy) angeschaut und sah, dass
[mm] EF(\phi) \equiv E(true\ U \phi)[/mm] aber wieso true U [mm] \phi? [/mm] Könnte man nicht [mm] EU\phi [/mm] schreiben?
---
[mm] E(AG(¬\phi)) [/mm] ist in diesem Fall kein CTL-Ausdruck, oder?
Danke.
Gruss
Pablo
|
|
|