Verifikation geht doch so von statten das man ein Modell des Systems hat (z.B. einer Ampel) das für die reale Ampel steht und dann anhand einer Spezifikation die man erstellt hat, überprüft, ob dieses Modell die Spezifikation erfüllt. Nicht wahr?

Model Checking ist doch so eine Verifikation anhand eines Systemmodells (Kripke-Struktur oder Erreichbarkeitsgraph). Ich sehe beim Model Checking irgendwie nicht genau was nun Modell ist und was die Spezifikation und wo die Verifikation stattfindet.
Beim Erreichbarkeitsgraphen überprüfe ich doch nur bestimmte Eigenschaften wie z.B. Lebendigkeit die mein Model (das Petrinetz) hat, wo ist die genaue Systemspezifikation?
Das gleiche Problem hab ich bei der Prozessalgebra.

Kann mir da jemand auf die Sprünge helfen?
Danke! [img]http://www.fb18.de/gfx/23.gif[/img]

Verifikation geht doch so von statten das man ein Modell des Systems hat (z.B. einer Ampel) das für die reale Ampel steht und dann anhand einer Spezifikation die man erstellt hat, überprüft, ob dieses Modell die Spezifikation erfüllt. Nicht wahr?

Model Checking ist doch so eine Verifikation anhand eines Systemmodells (Kripke-Struktur oder Erreichbarkeitsgraph).

soweit alles richtig und alles was man für die Prüfung dazu wissen muss ;)

allgemeinerer: Model checking = Verifikation durch Analyse des 'Zustandsraumes'

Ich sehe beim Model Checking irgendwie nicht genau was nun Modell ist und was die Spezifikation und wo die Verifikation stattfindet.
Beim Erreichbarkeitsgraphen überprüfe ich doch nur bestimmte Eigenschaften wie z.B. Lebendigkeit die mein Model (das Petrinetz) hat, wo ist die genaue Systemspezifikation?
Das gleiche Problem hab ich bei der Prozessalgebra.

also bei Prozessalgebra ist ja nun ein perfektes Beispiel dazu angegeben:

Alternierbitprotokoll,

da gibt gewisses Spezifikationen
(etwa dass irgendwann mal korrekt übertragen wird oder ähnliches, musst mal nachlesen)

dann das Modell als PA-Ausdruck

und die Verifikation ist das Nachrechnen der Eigenschaften der Spezifikation
(diese Eigenschaften kann man da wohl auch als Formel ausdrücken)


ich erinnere weiterhin/ erkenne im Skript wieder,
dass auch bei der Temporalen Logik das System gut zu erkennen ist:

für die Mikrowelle gibts da ein System und einen netter Algorithmus,
mit dem man Spezifikationsformel a la
'wenn eingeschaltet wird Mikrowelle irgendwann auch mal heiss'
nachrechnen kann
(~Seite 171)


bei den Netzen sehe ich jetzt auch nicht das Superbeispiel,
aber die elementaren Eigenschaften eignen sich doch zumindest zur Verifikation von Spezifikationen wie
System stürzt nicht ab (Lebendigkeit),
keine Konflikte zwischen mehreren Prozessen (gegenseitiger Ausschluss),
genau definierte (Teil-) Systemzustände (Invarianten),
kein Speicherüberlauf (Beschränktheit ;) )

klingt für mich schon praktisch genug,
und es verbietet ja keiner dass man noch weitere Einzelsytem-spezifische Eigenschaften aus den Netzen erkennen kann,

(alles eher Meinungskundgabe, muss nicht überall stimmen ;) )

soweit alles richtig und alles was man für die Prüfung dazu wissen muss ;)

Na ich weiss nicht… s.u. [img]http://www.fb18.de/gfx/22.gif[/img]

also bei Prozessalgebra ist ja nun ein perfektes Beispiel dazu angegeben:

Alternierbitprotokoll,

da gibt gewisses Spezifikationen
(etwa dass irgendwann mal korrekt übertragen wird oder ähnliches, musst mal nachlesen)

dann das Modell als PA-Ausdruck

und die Verifikation ist das Nachrechnen der Eigenschaften der Spezifikation
(diese Eigenschaften kann man da wohl auch als Formel ausdrücken)

Im Prüfungsprotokoll von Christoph stand, dass sowohl das Modell als auch die Spezifikation bei PA mit Prozessausdrücken dargestellt wird und deren Verifikation dann durch Nachweis von Bisimilarität erfolgt. Hört sich für mich ganz vernünftig an.

Ich hab da noch ein paar mehr Fragen, ich hoffe das hört irgendwann mal auf ;), danke aber trotzdem schonmal für die Geduld! :hurray:

CTL (ab. S. 161) zeichnet sich ja dadurch aus, dass vor temporalen Quantoren immer Pfad-Quantoren stehen müssen. LTL-Formeln enthalten, so wie ich die Definition verstehe, überhaupt keine Pfad-Quantoren.
Wieso ist dann auf S.165 unten als Beispiel für eine LTL-Formel 'A(FGp)' aufgeführt?
Und was spräche dagegen stattdessen AF(AGp) in CTL zu schreiben? Also warum ist LTL nicht eine echte Teilmenge von CTL? Und nicht zuletzt: was ist die Schnittmenge dieser beiden (s. Grafik S. 167)

Daaanke!

soweit alles richtig und alles was man für die Prüfung dazu wissen muss ;)

Na ich weiss nicht… s.u. [img]http://www.fb18.de/gfx/22.gif[/img]

ich meinte damit, dass es so reicht, wie die Model checking erklärt hast
(und wichtig ist dass man das glaubhaft erklären kann)

nach einzelnen Beispielen wird wohl nicht gefragt ;)

LTL-Formeln enthalten, so wie ich die Definition verstehe, überhaupt keine Pfad-Quantoren.
Wieso ist dann auf S.165 unten als Beispiel für eine LTL-Formel 'A(FGp)' aufgeführt?

steht da nicht im Skript folgendes?

LTL-Formel sehen so und so aus blah blah [2 Zeilen]

und EINE Zeile darunter:

LTL Pfadformeln werden so gebildet:
* ….
* wenn f ung Pfad-Formeln sind dann auch -f, f v g, …, X f, F f, G F, …

also bei mir schon ;)
LTL-Formeln beginnen demnach mit einem A, dahinter kommt eine Pfadformel,
aufgebaut aus allen temporalen Quantoren usw.,
nur A und E dürfen nicht noch mal auftauchen

-> A(FGp) korrekt

Und was spräche dagegen stattdessen AF(AGp) in CTL zu schreiben? Also warum ist LTL nicht eine echte Teilmenge von CTL? Und nicht zuletzt: was ist die Schnittmenge dieser beiden (s. Grafik S. 167)

Schnittmenge: warm willst du bloß so viel wissen?
wenns nicht im Skript steht liess doch ein Buch ;),
na vielleicht weiss ja jemand hier eine erschöpfende Antwort,

von mir: da stehen alle Formeln, die beiden Definitionen genügen,
also zum Beispiel AGp usw., bestimmt ganz schön viele ;)


zur Frage nach AF(AGp):
das sieht schwer aus, sicher gibts da einen Unterschied,
ich kann mal ein Gegenbeispiel versuchen, weiss es aber nicht genau:

Kripkestruktur: p p Z_1 -> Z_2 -> Z_3 ^ ^ | | | | '-' '-' Berechnungsbaum: p p p p Z_1 -> Z_1 -> Z_1 -> Z_1 -> ....... | | | | v v v v Z_2 Z_2 Z_2 Z_2 | | | | v v v v Z_3 Z_3 Z_3 Z_3 p p p p | | | | v v v v ... ... ... ...

p gelte in den Z_1 und Z_3, in Z_2 aber nicht

* für jeden Pfad der in den Zustand Z_3 gelangt, gilt p dort und in allen weiteren Zuständen,
da nur noch in Z_3 geschleift wird

* für den einzigen Pfad der nicht Z_3 erreicht (der also immer in Z_1 bleibt)
gilt p schom im ersten Zustand Z1 und dann immer (da immer in Z_1)

-> A(FGp) ist erfüllt, da für jeden Pfad irgendwann mal immer p gilt


————

* für den Pfad der in Z_1 bleibt gibt es keinen Zustand, so dass für alle Pfade immer p gilt,
da es immer Pfade gibt, die nach Z_3 führen und die dann über Z_2 müssten, wo p nicht gilt

-> AF(AGp) gilt in dieser Kripke-Struktur nicht
-> AF(AGp) != A(FGp)

(ohne Gewähr ;) )

steht da nicht im Skript folgendes?

LTL-Formel sehen so und so aus blah blah [2 Zeilen]

und EINE Zeile darunter:

LTL Pfadformeln werden so gebildet:
* ….
* wenn f ung Pfad-Formeln sind dann auch -f, f v g, …, X f, F f, G F, …

also bei mir schon ;)
LTL-Formeln beginnen demnach mit einem A, dahinter kommt eine Pfadformel,
aufgebaut aus allen temporalen Quantoren usw.,
nur A und E dürfen nicht noch mal auftauchen

-> A(FGp) korrekt

Hoppla, den Einführungssatz mit dem A hab ich doch glatt überlesen. [img]http://www.fb18.de/gfx/8.gif[/img]

Schnittmenge: warm willst du bloß so viel wissen?
wenns nicht im Skript steht liess doch ein Buch ;),
na vielleicht weiss ja jemand hier eine erschöpfende Antwort,

von mir: da stehen alle Formeln, die beiden Definitionen genügen,
also zum Beispiel AGp usw., bestimmt ganz schön viele ;)

Ja ok, das ist jetzt klar.

zur Frage nach AF(AGp):
das sieht schwer aus, sicher gibts da einen Unterschied,
ich kann mal ein Gegenbeispiel versuchen, weiss es aber nicht genau:
[…]

Das ist doch ein super anschauliches Beispiel! Danke! [img]http://www.fb18.de/gfx/23.gif[/img]

Ich spiel hier mal ein wenig Michael Ende…

Thema: Exponentieller Algorithmus für den byzantinischen Konsens (S. 227)
Ich verstehe nicht genau wie der Prozessor am Ende der Phase 2 seine Entscheidung trifft. Dieses resolve wird doch auf alle Teilbäume angewendet und der am häufigsten vorkommende Wert ist dann der Wert des jeweiligen Prozesses. Das ist ja schlüssig, müsste dann jetzt aber nicht z.B. ein min(V) kommen wie beim Algorithmus 7.1 (S.221)? Ich verstehe diese kryptische Rekusionsformel und deren Terminierung da wohl nicht…

(ich hab frühestens Montag wieder mein Skript)

(ich hab frühestens Montag wieder mein Skript)

Kein Problem, das wird reichen [img]http://www.fb18.de/gfx/17.gif[/img].
Notfalls gibts aber hier noch eins:
http://www.informatik.uni-hamburg.de/TGI/lehre/vl/WS0304/PNL/pnl.html
mit dem bekannten Passwort. (Kapitel 6)

Thema: Exponentieller Algorithmus für den byzantinischen Konsens (S. 227)
Ich verstehe nicht genau wie der Prozessor am Ende der Phase 2 seine Entscheidung trifft. Dieses resolve wird doch auf alle Teilbäume angewendet und der am häufigsten vorkommende Wert ist dann der Wert des jeweiligen Prozesses. Das ist ja schlüssig, müsste dann jetzt aber nicht z.B. ein min(V) kommen wie beim Algorithmus 7.1 (S.221)? Ich verstehe diese kryptische Rekusionsformel und deren Terminierung da wohl nicht…

Beim Algorithmus 7.1 ist das entscheidene, dass alle guten Prozessoren die gleiche Menge V am Ende haben.
Ob das Ergebnis dann nun der kleinste, größte oder häufigste Wert aus dieser Menge ist
(naja bei Mengen gibts ja schlecht doppelte Werte ;) ) ist doch egal, ein separates Problem.
Wenn alle die Menge gleich bearbeiten werden sie auf jeden Fall zum gleichen Ergebnis kommen.


Analog hier, durch die bösen Prozessoren können zwar unterschiedliche Bäume
bei jedem Prozess aufgebaut werden.
Die Bedingung (n >= 3f +1) in Verbindung mit dem Mehrheitsalgortihmus garantiert aber,
dass alle zur korrekt arbeitenden zur gleichen Entscheidung kommen
(eventuell eben 'undefiniert').

Wie funktioniert der Mehrheitsalgorithmus:
Es gilt den Wert eines Knotens im Baum zu bestimmen.
Ist dieser ein Blatt, dann steht der Wert ja schon fest.

Ansonsten muss die Mehrheit der Unterknoten bestimmt werden
(eventuell rekursiv vorher diese Werte erst bestimmen).
Existiert eine Mehrheit -> Wert gefunden, ansonsten eben undefiniert.

Also das klingt doch denkbar einfach,
mir resolve(labda = Wurzel) findet man das endgültige Ergebnis des Prozessors.

(In der rekursiven Formel soll es sicher resolve(pi) statt resolve(lamda) heißen)



Frag mich jetzt bloß nicht, wieso der Algorithmus zusammen mit der (n >= 3f +1)-Bedingung
ein gleiches Endergebnis bei allen Prozessoren garantiert ;).

Da kannst du dir gerne die Seiten voller Beweise alleine durchlesen,
das kommt auch in der Prüfung nicht dran (denke ich).

Danke, das hat alles sehr geholfen!! [img]http://www.fb18.de/gfx/14.gif[/img]