Verfügbare Informationen zu "Model Checking"
Qualität des Beitrags: Beteiligte Poster: Lobo - Björn - Steve Forum: PG A4 Forenbeschreibung: Forum zur Projektgruppe A4 07/08 aus dem Unterforum: Ausarbeitungen Antworten: 7 Forum gestartet am: Montag 02.04.2007 Sprache: deutsch Link zum Originaltopic: Model Checking Letzte Antwort: vor 16 Jahren, 10 Monaten, 25 Tagen, 20 Stunden, 21 Minuten
Alle Beiträge und Antworten zu "Model Checking"
Re: Model Checking
Lobo - 18.04.2007, 16:06Model Checking
Hi
ich mach mal den Anfang...
Sitze schon an der Verbesserung der "zweiten Beta-Version", unter anderem mit neuen, angepassten Layout, einigen leichten "Prosa-"Fassungen als Einleitungen und Erklärungen...
Norman und ich wollten nur erstmal was vernünfitges präsentieren können, bevor wir die dritte Version online stellen.
Björn hat schon ne klasse Meckerliste zusammengestellt. Alle Anmerkungen werden natürlich berücksichtigt.
Dachte, das die Kritikpunkte offen diskutiert werden sollen. Nehmt kein Blatt vor den Mund und zerfetzt die Ausarbeit!!!
Hier schonmal die von Björn angesprochenen Kritikpunkte:
1.1.2: Pfad ist nicht der richtige eingedeutschte Begriff
1.2.2: Omega-quer??
1..3: Eine Fußnote bzw. Skolemisierung
1.3.2: Indizierung misverständlich
1.3.6: Kritische und Wartezustände sind nicht richtig eingeführt
2.1.1: Rechtschreibfehler
2.1.2 und 2.1.4: siehe 1.1.2
sowie: wechselnde Benutzung der Folgepfeilarten, fehlendes Abbildungsverzeichnis
positiv: knappe Formulierungen, mathematische Schreibweise.
Re: Model Checking
Björn - 27.04.2007, 20:03
Andre, Norman, falls ihr eine neue Version eurer Ausarbeitung ins Netz stellt meldet ihr euch, durch ein posting in dieses Board. Denn Ich sehe ehrlich gesagt keinen Grund vorher jede Kleinigkeit in eurere Ausarbeitung ganz genau durchzugehen.
ps. In 3.1.2 (ii) , (iii) muß nach dem Folgerungspfeil ein kleiner gleich Zeichen kein Gleichheitszeichen stehen. Und wieso nennt ihr die Eigenschaften nicht gleich aufwärtsstetig bzw. abwärtsstetig? Oder liege Ich hier falsch und Ihr meint etwas anderes? Der Fixpunktsatz von Knaster-Tarski im nächsten Punkt legt aber nahe das ihr das meint...
Re: Model Checking
Lobo - 02.05.2007, 06:14
Neue Version ist fertig. Norman überfliegt nochmal alles.... Dann wird die sofort hochgeladen!
Zu den Anmerkungen:
1.1.2: Pfad ist nicht der richtige eingedeutschte Begriff
Benutzen Trace
1.2.2: Omega-quer??
Benutzen Omega *g* -- hab falsch geklickt
1..3: Eine Fußnote bzw. Skolemisierung
sollte aber aus der Logik bekannt sein
1.3.2: Indizierung misverständlich
ist sie nicht.... beidesmal ist etwas anderes gemeint!!!
1.3.6: Kritische und Wartezustände sind nicht richtig eingeführt
das Beispiel ist absolut richtig... vergleich es mal mit dem Satz aus der PL-Fassung der LT-Eigenschaft...
2.1.1: Rechtschreibfehler
korrigiert
2.1.2 und 2.1.4: siehe 1.1.2
in dem Fall ist Pfad richtig, da man ein Modell im CTL als Baum auffalten kann
sowie: wechselnde Benutzung der Folgepfeilarten, fehlendes Abbildungsverzeichnis
Abbildungsverzeichnis fehlt im Moment noch, kommt aber... wollte da noch ein bißchen rumdoktorn...
In 3.1.2 (ii) , (iii) muß nach dem Folgerungspfeil ...
naja, zu mindest habe ich den CLARKE richtig abgeschrieben, auch hier steht ein GLEICH
positiv: knappe Formulierungen, mathematische Schreibweise.
THANX
Re: Model Checking
Lobo - 03.05.2007, 08:08
Die neue Version ist online....
Wollte ggf noch ein paar Sachen als "Definition" deklarieren... und ggf. noch bis zu vier/fünf Zeilen Erklärungen schreiben....
Vorher aber die erhoffte Diskussion...
Re: Model Checking
Björn - 04.05.2007, 00:14
zu Model-Checking (Am besten in Einleitung kurz erwähnen): Eine grundlegende Sache von Model-Checking ist nicht nur das überprüfen von gesuchten Eigenschaften in einem System, sondern dient, auch dazu falls diese Eigenschaft nicht erfüllt, ist ein Gegenbeispiel zu liefern.
Zur Definition 2.2: ersetzt Struktur durch Kripke-Struktur, oder fügt eine Fußnote ein, in welchen Strukturen man dies so definiert - vgl. Mathematische Strukturen (z.b. auf wikipedia oder Algebrabücher) , welche Gruppen,Monoide,Ringe, etc. umfassen. Außerdem wurden Allgemeine Strukturen in der Ausarbeitung gar nicht definiert, es ist also egal wie solche Folgen(Sequenzen) in anderen Strukturen heißen - falls solche dort überhaupt existieren.
2.2.1 Ersetze Standartbeispiel durch Standardbeispiel.
2.2 Ersetze Modelchecker durch Model-Checker
2.3: Die Definition sieht etwas lang aus. Reicht nicht ein Satz aus für die Definition, ist das andere nicht mehr beschreibung der Eigenschaften und keine Definition?
2.3.2: ihr benutzt nicht gerne die mathematischen Symbole für für alle und für ein (bzw. es existiert)? - Außerdem es ist zwar klar was pi^{i} (etc.) bedeutet, aber dranschreiben (z.b. als Fußnote beim ersten auftauchen) dass pi^{i} der ite-Nachfolger von pi ist könnte man schon. Also schlage ergänzung im ersten Satz vor: ein Pfad, und sei pi^{0}=pi und für alle i \geq 1 pi^{i} der i-te Nachfolger von pi.
2.3.4: zweiter Satz (schlage alternative Formulierung vor): Für ausführlichere Beispiele siehe [4].
3.1.1 Das beispiel in letzten Satz ist ungeeignet (da die ersten drei Buchstaben schon = "ABA" sind) eine besseres Beispiel wäre "BBABAAA"
Beispiel Türöffner: Unvorteilhafter Seitenumbruch von Seite 8 auf Seite 9.
3.1.3: Konsequent wäre es zu Propositionen durch Eigenschaften zu ersetzten.
3.1.6: (Formatierung): Die Überschrift Distributivgesetze gehört oben in die nächste Spalte - sieht so komisch aus.
(Nach der Überschrift Existentielle Normalform): entfernt doch das Leerzeichen zwischen E und U.
3.2.2 (Algorithmus): Der Algorithmus ist kein vollständiger Algorithmus. Ergänzt doch den satz: "Sei M ... Kripkestruktur, und sei label(s) die Menge aller Zustände in denen f_{2} gilt."
3.3 Zu CTL*, benutzt doch bitte CTL^{*}, so sieht das etwas komisch aus.
4.2 (formerly 3.1.2) :(Anmerkung) Eure Definition für aufwärts und abwärtsstetig ist richtig (sorry) - in der Definition im Formale Methoden des Systementwurf Skripts von Peter Padawitz (version 12.2.2007) ist der Fehler (Seite 26) - (im Übersetzerbauskript steht es richtig).
Habe mir erst richtig die Seiten 1-12 angeguckt, rest kommt später.
Re: Model Checking
Steve - 31.05.2007, 10:49
Bin endlich durch, hier ein paar Anmerkungen über die von Björn oben hinaus. Björns Anmerkungen stimme ich zu, falls nicht, ist es unten erwähnt.
Habe Zeichensatzfehler "überlesen".
Rechtschreib- und Grammatikfehler sind durch Klammern im Text gekennzeichnet.
Fixpunktberechnung 4.2 und symbolisches Model Checking muss ich mir nochmal mit einem Script antun, um nachvollziehen zu können, ob es inhaltlich richtig ist, aber eigentlich vertraue ich euch da :D
2.1.2 (5) ... in diesem (Beispiel) aus ...
2.3.2 Anmerkung zu Björns Anmerkung: pi^i sollte auf jeden Fall kurz erklärt werden... denke aber, dass das Wort "Nachfolger" vielleicht nicht die intuitivste Bezeichnung ist. Gemeint ist (meiner Auffassung nach) der Pfad pi ab Zustand i, also für pi=p_0p_1p_2... ist zB. pi^1=p_1p_2p_3... Der "Nachfolger" eines Pfades verwirrt nur an dieser Stelle. Falls ich da was falsch verstehe, ignoriert das hier einfach =)
2.3.4 Die Formeln im Beispielbild würde ich entfernen oder in den Untertitel packen, da sie schon im Text erwähnt werden.
3.1.1 Letzter Absatz: CTL-Formel(n) , Türöffner(s) , der (der) Code
3.1.2 ... die möglich(e) Quantifizierung ...
3.1.3 ... ein(e) Menge ...
3.1.4 Einheitlich "Kripkestruktur" oder "Kripke Struktur" verwenden
dot (2): l(p) in L(p) umbenennen, da im vorigen Text so definiert (siehe auch letzter dot) oder im ersten Satz neu definieren.
3.1.5 Beipiel 2: Das Bild ist (bei mir?) zu klein, ggf. einfach auf das erste Bild verweisen...
3.1.6 Aussagenlogische(n) Dualitäten
3.2.1 ... ist das(s) Model Checking Problem ...
3.2.2 CheckEU(3): ... Rückwärt(e) ... weiter(e) ...
Algorithmus: Einheitlich "Kripkestruktur" oder "Kripke Struktur" verwenden
3.2.3 (3) ...alle Zustände, die in SCC (ungünstig formuliert, siehe auch Beispiel weiter unten)
(4) Nimm eine(n) Zustand ... (siehe auch Beispiel weiter unten)
Beispiel ganz unten bei (3): ... wieder aus T (wieder) ...
3.3 Anmerkung zu Björns Anmerkung: bei mir siehts gut aus, also wie CTL^{*}
... Liveness(-) ... Pfadformel(n) ....
3.3.1 ... CTL*-Zustandsformel(n)
Einheitlich "Pfad-Formel" oder "Pfadformel" verwenden
3.3.2 ... Krip(p)kestruktur...
Einheitlich "Kripkestruktur" oder "Kripke Struktur" verwenden
4.1 Einheitlich "Kripkestruktur" oder "Kripke Struktur" verwenden
4.2 unten: ...die im Referat erwähnten Sätze... (ungünstig ausgedrückt - welches Referat? Einfach: Satz 4 und Satz 6)
4.3.1 Einheitlich "Kripkestruktur" oder "Kripke Struktur" verwenden
Label(l)ing (Labello? ;P )
4.3.2 "Wir haben mal nur eine 1-Senke benutzt" unschön
Das Bild ist etwas klein
4.3.4 Der zweite Abschnitt ist unverständlich
... implementiert, (die) ....
... mitsamt Argumenten nimmt und ein OBDD ... (syntaktisch und semantisch unschön)
... die Formel erfüll(en).
"Bleiben die drei Funktionen noch zu klären" (syntaktisch und semantisch unschön)
Kleine Anmerkung: was ist PSPACE?
Insgesamt:
Einheitliche Bezeichnung für "Kripke Struktur" verwenden (kommt auch Kripkestruktur und Kripke-Struktur vor)
Einheitliche Bezeichnung für "Model Checking" verwenden (kommt auch Model-Checking vor)
Einheitliche Struktur für Definitionen verwenden (zB. in Kapitel 2 nummeriert, in Kapitel 3 nicht - siehe 3.2.1
Re: Model Checking
Björn - 31.05.2007, 22:55
PSPACE: Grob gesprochen: Sind alle Probleme die mit deterministisch Algorithmen auf polynomiellen Platz (bzgl. Eingabelänge) gelöst werden können - also wie P nur mit Platzschranke statt Zeitschranke.
Mit folgendem Code, können Sie den Beitrag ganz bequem auf ihrer Homepage verlinken
Weitere Beiträge aus dem Forum PG A4
Zwischenbericht - gepostet von Björn am Montag 27.08.2007
Model Checking - gepostet von Lobo am Mittwoch 18.04.2007
Kripke Control Classfile: - gepostet von Lobo am Montag 11.06.2007
Ähnliche Beiträge wie "Model Checking"
Bill das Model - Akasha (Donnerstag 24.08.2006)
Brasilianisches Model an Magersucht gestorben - Anoriel (Mittwoch 15.11.2006)
New Model Army - *Saga-Lady* (Samstag 10.06.2006)
Just Armand / Schauspiel und Model - Armand (Montag 06.03.2006)
Suzuki Burgman AN 400 K7 / 2006 Model - frehni (Sonntag 25.12.2005)
Germany's next Top-Model - Becks (Samstag 03.03.2007)
Suche Sommerkamp TS-280FM (US-Model) - soka788dx (Samstag 08.01.2005)
A Pacific Model - Ortega (Freitag 16.11.2007)
Dringend Model gesucht!!! - Just NAILS (Montag 13.03.2006)
bill wird model - jess (Donnerstag 24.08.2006)