Diskussion:Computation Tree Logic

Der Artikel behauptet CTL wuerde unter anderem Synonym fuer CTL* benutzt. CTL bezeichnet aber in den meisten Buechern eine Untermenge von CTL*. Dieser Artikel beschreibt CTL*. Der Link zur englischen Wikipedia verweist aber auf CTL als Untermenge von CTL*. Der Link ist falsch und verwirrt. -- Del 12:36, 14. Jul 2006 (CEST)

Nöö, tut er nicht, weil der Artikel den Unterschied von CTL und CTL* erklärt. Er erklärt also sowohl CTL, als auch CTL* und beides lässt sich unter dem Lemma "Computation Tree Logic" prima abhandeln. Wenn es in EN einen eigenen Artikel zu CTL* gibt, kann man immernoch dorthin den Link umbiegen. Aber löschen, oder so einen unsinngen Baustein reinsetzen, das ist echt keine Lösung... --Koethnig 14:05, 14. Jul 2006 (CEST)

Findest du den QS-Stein unsinnig? Die Definition von CTL* ist unvollstaendig (Operatoren A und E werden nicht erklaert, was Executions und Kripke-Strukturen sind auch nicht) und Quellen fehlen ganz. Ob CTL ueberhaupt irgendwo synonym fuer CTL* benutzt wird kann ich nicht sagen, aber das sind zwei Unterschiedliche Lemma mit gleichem Namen die da verlinkt werden. Das beste waere es wohl, den CTL* zu verschieben und CTL komplett fuer CTL lassen und als Stub markieren (auf dass jemand Einsatzgebiet, Ausdruecksfaehigkeit, Tools und Modelchecking-Algorithmen erweitern kann) -- Del 16:37, 14. Jul 2006 (CEST)

Die QS-Bausteine sind meistens unsinnig, weil sie dem Leser etwas erzählen, was er auch ohne sie erfährt und sie eine Verschlechterung des Artikels darstellen. Die wenigsten Artikel sind durch QS-Bausteine verbessert worden, gerade bei so speziellen Themen nicht. Und da du Ahnung zu haben scheinst, bietet es sich noch am ehesten an, wenn du selbst den Artikel verbesserst. Unter welchem Lemma würdest du denn CTL* abhandeln? CTL* ist letztlich ja auch nur eine Abkürzung. --20:33, 14. Jul 2006 (CEST)

Mir haette es einiges an Zeit erspart haette gleich ein QS-Baustein den Artikel geziert. Ein Artikel ist wertlos wenn man nicht erwarten kann dass er stimmt. Ich hoffen ich hab in ein paar Tagen genug Zeit und Know-How sowohl LTL als auch CTL aufzubesseren. -- Del 22:51, 15. Jul 2006 (CEST)

Erstens geht es bei der QS nicht darum DIR zeit zu ersparen, sondern die Artikel zu verbessern und zweitens hat seit dem QS-Baustein immernoch niemand was an dem Artikel getan?! Ausnahme deine Wenigkeit, aber auch den letzten Edit werde ich wohl reverten, denn was du rausgelöscht hast, war richtig. Wo und wie du jetzt Zeit gespart hast, ist mir dann noch schleierhaft... --Koethnig 10:32, 16. Jul 2006 (CEST)

Du meinst die Vergangenheitsoperatoren? Laut "Systems and Software Verification: Model-Checking Techniques and Tool" von Berard et al. gibt es keine solche Operatoren in CTL*. Andere Veroeffentlichungen sprechen von Erweiterungen diverser Logiken um solche Operatoren. -- Del 23:51, 16. Jul 2006 (CEST)

Mag sein, dass das nicht ganz korrekt formuliert war, aber da wäre es doch vernünftiger gewesen, den Satz entsprechen anzupassen, anstatt einfach alles rauszulöschen... --Koethnig 10:27, 17. Jul 2006 (CEST)

Das stimmt. Leider habe ich solche Erweiterungen nur konkret meist fuer LTL gesehen. Nie explizit fuer CTL* und ich wollte nicht aufs geratewohl was hinschreiben, fuer dass ich keinen Quelle hab. Wenn ich auf so etwas stosse werde ich es hinzufuegen. -- Del 11:59, 17. Jul 2006 (CEST)

Atomare Aussagen

Der Abschnitt ist viel zu formal formuliert und ohne genaue Kenntnis der Aussagenlogik (oder soll ich sagen: Ohne Informatik-Studium) völlig unverständlich. Der Abschnitt muss unbedingt in der Umgangssprache erklärt werden. Ausserdem enthält er IMHO falsche bzw. irreführende Inhalte: Eine Atomare Aussage kann keine Zustandsformel sein, denn sie ist (deswegen wird sie ja atomar genannt) genau wahr oder falsch und enthält in sich keine Parameter. Eine Formel p(s) ist daher Blödsinn, denn p ist von s unabhängig. Oder kann das jemand etwas genauer erklären? --PaterMcFly _Diskussion ^{Meine Beiträge} 11:02, 2. Sep. 2007 (CEST)

Das ist so zu verstehen, dass Atomare Formeln p einer Menge von Zuständen entsprechen und p(s) fragt lediglich danach, ob der Zustand s in dieser Menge enthalten ist. --AlgorithMan (Diskussion) 16:21, 14. Mär. 2018 (CET)

formale Definition Temporaloperatoren

Da für $X\phi$ die Formel $\phi$ ja auch wieder beliebig komplex sein darf, ist die Aussage, das $\phi$ nur den nächsten Zustand erfüllen muss, falsch. $\phi$ muss den ganzen nachfolgenden Pfad erfüllen. Für die anderen Operatoren gilt es analog. Die formale Definition habe ich dahin ausgebessert. -- PapaNappa 10:43, 22. Nov. 2010 (CET)

Das ist kompletter Unsinn. Wenn ich sage "Morgen esse ich Spaghetti", heißt das nicht, dass ich nie wieder etwas anderes als Spaghetti esse. $\phi$ könnte selber wieder die Form $X\psi$ haben, ja, aber das hieße dann "Übermorgen esse ich Spaghetti". Denn dann gilt der Satz "Morgen esse ich Spaghetti" eben erst morgen. --AlgorithMan (Diskussion) 13:23, 14. Mär. 2018 (CET)

Interpretation, formal

Unter Semantik sollte eigentlich etwas über Kripke-Strukturen stehen (gern mit Diagrammen) Zumindest sollte man den Teil mit den Bäumen schon mal besser ausführen. [ɯ:] 12:58, 24. Jan. 2012 (CET)