Diskussion:Model Checking

Quellen fuer Bewertung der Model-Checking-Tools Bearbeiten

Woher stammen die Bewertungen unter der der Ueberschrift 5 (Maßstab: { sehr schlecht } --- | -- | - | o | + | ++ | +++ { sehr gut } oder { niedrig } bis { hoch })?

Moege der/die AutorIn dieses Abschnittes die Quellen angeben..

Symbolisches Model Checking Bearbeiten

Letzter Kommentar: vor 17 Jahren2 Kommentare1 Person ist an der Diskussion beteiligt

Der Abschnitt zum symbolischen Model Checking ist so falsch. Beispielsweise die weiterführenden Arbeiten von E. Clarke wiederlegen die Behauptungen dort. Dort werden u.A. SAT Solver für ECTL* und ACTL* benutzt. Außerdem kann man mit BDDs µ-Calculus benutzen (was deutlich stärker als CTL ist).

Momentan fehlt mir die Zeit den Artikel zu verbessern, werde mich aber hoffentlich bald daran machen können.

Das Tool [mc]square benutzt übrigens auch symbolisches Model-Checking um CTL Formeln zu überprüfen!

Abgesehen davon, dass ich mich mit den aktuellen Entwicklungen nicht auskenne. Wo behauptet der Artikel das Gegenteil? E. Clarke (wer auch immer das ist) wiederlegt ganz sicher nicht, dass man das dort beschriebene tun kann, schließlich wird/wurde es getan!? Niemand hat behauptet, das nicht mehr möglich ist. Also bitte mal die Behauptungen präzisieren/richtigstellen! --Koethnig 14:00, 16. Jan. 2007 (CET)Beantworten

Jetzt nicht mehr. Als ich den Kommentar geschrieben habe, hatte der Artikel noch 3 "z.B." weniger. Da standen in den Klammern keine "z.B.", so dass der Eindruck entstand, dass dies verbindlich wäre. Dem widerspricht Clarke dadurch, dass er auch CTL-Formeln mit SAT-Methoden bearbeitet. Edmund Clarke ist Professor an der Carnegie Mellon University und Autor der einzigen Quelle des Artikels, daher habe ich mich auf ihn bezogen. In der aktuellen Version ist der Artikel zwar noch sehr oberflächlich, aber zumindest nicht mehr falsch, da die kritischen Behauptungen durch "z.B." entschärft wurden.

Jo, die "z.B." habe ich eingefügt, weil ohne wars tatsächlich irreführend, aber die Worte "falsch" oder "wiederlegt" fand ich doch etwas übertrieben. Die Quelle kenn ich nicht, die hat jemand anderes hinzugefügt! Möglicherweise war es auch eine Quelle meines damaligen Dozenten?! --Koethnig 00:28, 17. Jan. 2007 (CET)Beantworten

Explizites Model Checking Bearbeiten

Letzter Kommentar: vor 17 Jahren2 Kommentare1 Person ist an der Diskussion beteiligt

Reduktionen durch partielle Ordnungen und Bisimulation sind nicht fester Bestandteil des expliziten Model Checkings und nur ein winziger Teil Werkzeuge mit denen man den Zustandsraum kleiner kriegt. Solche Verbesserungen sollten einen eigenen Abschnitt bekommen und um wichtigere Techniken wie On-The-Fly und Abstraktion erweitert werden. Außerdem könnte man die Model Checking Algorithmen (in Pseudo Code) angeben.

Wo bitte im Artkiel kommt das Wort Bisimulation vor? Wo steht, dass es zusammen mit partial order reduktion "fester Bestandteil" sei? Natürlich sind weitere Verfahren möglich und denkbar! --Koethnig 14:00, 16. Jan. 2007 (CET)Beantworten

"Ausnutzen von Symmetrien" in Verbindung mit "Partial Order Reduction" brachte mich dazu davon auszugehen, dass der Autor von Bisimulation spricht (also der Reduktion des Zustandsraums durch einen Bisimulations-Quotienten). Auch hier fehlte das "z.B." und das "kann", so dass der Eindruck entstand, diese Techniken seien Teil des Model Checking Algorithmus.

"Bisimulation" habe ich noch nie gehört. Aber ich hatte ja auch nur eine Vorlesung zu dem Thema und die ist wie gesagt schon ne Weile her. Symmetrien und Partial Order Reduktion sind so weit ich mich erinnere unabhängige aber gleichzeitig funktioierende Konzepte zur Reduktion des Zustandsraumes. Aber nach 2 Jahren leg ich meine Hand dafür auch nichts mehr ins Feuer und das Skript kram ich jetzt auch nicht mehr raus :-). --Koethnig 00:28, 17. Jan. 2007 (CET)Beantworten

Modellprüfung zurück nach Model Checking verschieben? Bearbeiten

Letzter Kommentar: vor 15 Jahren3 Kommentare2 Personen sind an der Diskussion beteiligt

Was haltet ihr davon, den Artikel zurück nach Model Checking zu verschieben und eine Weiterleitung von Modellprüfung dorthin anzulegen? Ich finde die deutsche Übersetzung sehr künstlich. Auch viele Vorlesungen an deutschen Unis benutzen dieses Wort nicht, sondern den englischen Term.

Eine kurze Anfrage bei Google liefert 27.900 Seiten aus dem deutschsprachigen Raum für Model Checking, jedoch nur 4.820 für Modellprüfung. --Marco Bakera 08:57, 2. Mai 2008 (CEST)Beantworten

wurde erledigt. --84.188.197.181 13:11, 9. Nov. 2008 (CET)Beantworten

Danke. :) --Marco Bakera 22:22, 30. Nov. 2008 (CET)Beantworten

Endlicher Zustandsraum Bearbeiten

Letzter Kommentar: vor 15 Jahren1 Kommentar1 Person ist an der Diskussion beteiligt

Im zweiten Absatz steht: "Der Zustandsraum des Systems muss nicht notwendigerweise endlich, jedoch endlich repräsentierbar sein." Das glaube ich so irgendwie nicht. Wenn der Zustandsraum unendlich sein darf, dann kann man mit Model Checking plötzlich das Halteproblem entscheiden, oder nicht?

Und überhaupt, was heißt "endlich repräsentierbar"? Die Menge der reellen Zahlen ist auch endlich repräsentierbar, nämlich durch den einzelnen Buchstaben $\mathbb {R}$ . Und die Menge der reellen Zahlen ist wirklich eine sehr große Menge (überabzählbar). --OmicronPersei8 22:18, 23. Sep. 2008 (CEST)Beantworten

Nein, warum sollte das so sein? Natürlich können Eigenschaften auf unendlichen Zustandsräumen überprüft werden, ohne dadurch das Halteproblem zu entscheiden. Empfehle dazu, z.B. die Arbeiten von Esparza zu studieren.

Abschnitt Weblinks Bearbeiten

Letzter Kommentar: vor 15 Jahren1 Kommentar1 Person ist an der Diskussion beteiligt

bitte mal gemäß Wikipedia:Weblinks entrümpeln. --84.188.197.181 13:11, 9. Nov. 2008 (CET)Beantworten

Linkfarm entfernt Bearbeiten

Letzter Kommentar: vor 15 Jahren1 Kommentar1 Person ist an der Diskussion beteiligt

Folgende Linkfarm habe ich entfernt, vgl. WP:WEB bitte vor erneuter Aufnahme einzelner Links diese einzeln diskutieren: --Complex 09:26, 2. Jan. 2009 (CET)Beantworten

Abschnitt hinzufügen