Hi
Kann mir vielleicht einer erkläen, was die Verifikation des Alternierbitprotokolles ist? Die beiden Spezifikation(Sender, Empfänger) habe ich verstanden aber leider noch nicht ganz die Verifikation.

und welche Formel möchte Herr Valk hören, wenn er nach der Spezifikation des Alternierbit-Protokolls fragt??

und, mal was anderes: welche Komplexität haben CTL und LTL? irgendwo stand mal linear in der Größe der Kripke-Struktur, weil O(|f| * |S| + |R|), aber in einem Prüfungsprotokoll (von einem mit 1,0!!) steht, dass das Eine polynomiell und das Andere in PSpace oder so sei…?
Wie ist es denn nun??
Danke

und welche Formel möchte Herr Valk hören, wenn er nach der Spezifikation des Alternierbit-Protokolls fragt??

Keine Ahnung, was Prof. Valk hören will; ich würde ihm aber
folgendes hinmalen:
X = r_a(d) * s_c(d) * X oder so ähnlich ( Seite 38 oben )

und, mal was anderes: welche Komplexität haben CTL und LTL? irgendwo stand mal linear in der Größe der Kripke-Struktur, weil O(|f| * |S| + |R|), aber in einem Prüfungsprotokoll (von einem mit 1,0!!) steht, dass das Eine polynomiell und das Andere in PSpace oder so sei…?

Dieses O(|f|*(|S| + |R|)) rührt daher, dass beim Model Checking an
einer Kripke-Struktur nur Formel aus CTL angewendet werden (Seite 169 ff).
Das einzige PSPACE, dass IHO im Skript auftaucht (Seite 154), kommt
vom Erreichbarkeitsproblem für 1-konservative P/T-Netze…

Keine Ahnung, was Prof. Valk hören will;

Zumindest nicht die Frage "Was wollen Sie denn hören?" :-)

ich würde ihm aber
folgendes hinmalen:
X = r_a(d) * s_c(d) * X oder so ähnlich ( Seite 38 oben )

Steht auch so in diversen Gedächtnisprotokollen. Und der ganze Formelwirrwar auf den Seiten davor? Kann man den, salopp gesprochen, vergessen, oder muss man da noch was zu erklären können?

Man sollte zumindest erklären können, was diese Formel bedeutet..

Ich hötte da noch mal zwei Fragen zur Spezifikation.

Es ist immer von einer Summe die rede. Etwa:

S_b = Summe(d element groß Delta) r_A(d) * T_db

beim Schreiber. Der Sinn ist mir noch nicht ganz klar. Soll das andeuten, dass es sich hier nicht um ein einzelnes Bit, sonodern um ein Datenpaket handelt? Oder ist das wieder im Sinn von der PA eine Aneinanderkettung von oders? Also nach dem Motto wir haben die Daten 2,3 und 7 und eine davon wählt er sich jetzt mal aus und sendet die?

Bei der Spezifikation des Empfängers ist mir dann noch nicht ganz aufgegangen, was diese Mengenklammer dort zu suchen hat.

R_b = Summe(d element groß Delta) { r_B(d,b) * s_C(d) * Q_b + r_B(d, 1-b) * Q_1-b} + r_B(Error) * Q_1-b

Es ist schon ein bisschen her, aber ich meine die Summe bezog sich da auf die Aneinanderkettung, also das "oder". Damit soll sozusagen gewährleistet werden, dass für jedes Mögliche Datum d aus Delta ein Ausdruck da ist.

Fein, fein. Danke. Hat noch wer eine Idee zur Mengenklammer?

Jetzt hab ich doch mal nachgeguckt. Ich meine das soll einfach nur eine normale Klammer sein um das Summenzeichen nicht auf r_B(Error) * Q_1-b zu beziehen. Würde in diesem Kontext auch stark sinn machen [img]http://www.fb18.de/gfx/28.gif[/img]

*Schnief* Er hat es mich nicht aufschreiben lssen. [img]http://www.fb18.de/gfx/17.gif[/img]