xphilosoph:

R(S) ist die Erreichbarkeitsmenge (Def.5.3), RS(S) der Erreichbarkeitsgraph eines unbeschränkten Netzsystems S (S.139, mitte). Ich vermute, daß RG(S) und RS(S) synonym benutzt werden.

Aber auf Seite 140 sieht das ganze garnicht nach einem Graphen (also einem Tupel) aus…

[img]http://mokrates.de/cgi-bin/texstring?%24RS(S)%3D%5C%7B%20p_1%20%2B%20p_6%2C%20%5Cdots%20%5C%7D%24[/img]

RS(S) ist das gleiche wie R(S), also eine Erreichbarkeitsmenge. Das RS steht für Reachability Set.
Der Erreichbarkeitsgraph ist RG(S) für Reachability Graph.

Dann handelt es sich also nach Def. 5.4 um einen Tippfehler:

Der Erreichbarkeitsgraph RS(S) eines unbeschränkten Netzsystems S ist nicht endlich

Ja, auf alle Fälle. Habe extra im Tutorium nochmal nachgefragt.
Im Skript gibt es noch ein paar Ungereimtheiten…

Kann mir jemand folgendes erklären?

Im Beweis zu Satz 7.6 ("Es gibt keinen Konsens-Algorithmus für ein System aus n Prozessoren mit mehr als ceiling(n/3) Byzantinern") steht:

Auf T ist Satz 7.5 anwendbar. Die Vorraussetzung des Satzes lautet: maximal ein byzantinischer Prozessor

7.5 besagt, dass es keinen Konses-Algorithmus für drei Prozessoren mit einem Byzantiner gibt. Den Zusammenhang verstehe ich nicht.

Ah und noch was: Seh ich das richtig, dass beim exponentiellen byzantinischen Algorithmus, wirklich nur die Werte in den Blättern ausgewertet werden?

[edit] Keine Ahnung, warum ich "gespeichert" geschrieben habe ich meinte "ausgewertet"

nur die Blätter werden ausgewertet, ja



zum Beweis: ich verstehen den so wie er da steht auch nicht,

vielleicht gehts so:man teilt die Prozessoren von S so wie angegeben in 3 Gruppen
und zwar in eine Gruppe nur die byzantinischen,
da >= n/3 byzantinische da sind muss man eine Gruppe voll kriegen,

also kann man daraus ein System T basteln, dass wie in Beweis 7.5 funktioniert:
3 Prozessoren und mindestens einer byzantinisch,

gäbe es nun einen Algorithmus A für S dann auch für T im Widerspruch zu Beweis 7.5

Hmm, morgen Prüfung, nochmal kurz den Ausfallkonsens (nicht-byzantinisch!) angeguckt und plötzlich gewundert:

Bei 4 Prozessoren und einem Ausfall sollte das in f+1=1+1=2 Runden hinhauen. Warum klappt das nicht in meinem Beispiel?

In der ersten Runde senden alle ihren Startwert, p4 schickt nur an p1, fällt dann aus. In der zweiten Runde könnte p1 dann "9" schicken, in der dritten "2" und erst in der vierten wäre sichergestellt, dass alle die eins haben. Da das Minimum gewählt wird würde doch (in dem Fall) kein Konsens nach der 2ten Runde bestehen…

Start nach 1ter p1 {3} {3,1,9,2} p2 {9} {3,9,2} p3 {2} {3,9,2} p4 * {1} {3,9,2}

In der zweiten Runde könnte p1 dann "9" schicken, in der dritten "2" und erst in der vierten

Da ist der Fehler: Er sendet alle Elemente gleichzeitig, in einer Nachricht. (Alternativ: Er sendet alle Elemente, die er in der letzten Runde neu dazubekommen hat) In jedem Fall haben alle noch aktiven Prozessoren nach 2 Runden {1,2,3,9}.

Viel Erfolg morgen!

Das war schnell, danke, aber:

Ein unzuverlässiger Prozessor verschickt in der letzten Runde vor seinem Ausfall dieselbe Nachricht an andere Prozessoren aber nicht mehr unbedingt an alle

Edit: oder meintest Du das auf die Zeile "send bla to all processors? Das damit sozusagen synchronisiert wird?

Edit 2: Aber ist es dann nicht witzlos? Geht es dann nicht immer in einer Runde, egal wieviele ausfallen

Edit: oder meintest Du das auf die Zeile "send bla to all processors?

Genau das mein ich. Er verschickt die _Menge_ der Werte, die er noch nicht verschickt hat.

Edit 2: Aber ist es dann nicht witzlos? Geht es dann nicht immer in einer Runde, egal wieviele ausfallen

Nein. Nimm an, dass jede Runde genau ein Prozessor ausfällt, und der ausfallende Prozessor jeweils immer nur eine Nachricht an den, der in der Runde da drauf ausfallen wird, verschicken kann. Dann gelangt die Meinung des ersten ausfallenden Prozessors erst dann zu allen anderen, wenn alle unzuverlassigen Prozessoren ausgefallen sind.

"Die Menge der Werte"… [img]http://www.fb18.de/gfx/wand.gif[/img] und ich grübel mir hier n Ast. Gracias!

Und noch was. Wenn jemand noch vor 12 antwortet weiss ichs in der Prüfung:

Der polynomielle Algorithmus für den byzantinischen Konsens hat angeblich "konstante Nachrichtengröße", ich hab aber eigenlich den Eindruck, dass die Nachrichten beliebig gross werden können, was ja nicht mehr in die Ordnung konstant fallen dürfte…

jede Nachricht von der ersten bis zur letzen Runde gleich groß?

ne die sind doch sogar konstant, nur das eigene pref wird geschickt

im exponentiellen Algorithmus wird ja jeweils eine ganze Ebene des größer werdenen Baums geschicht (-> unendlich große Nachrichten)

was meinst du mit "das eigene pref(i)"? es wird jedesmal eine Teilmenge der (eigenen) menge pref verschickt. am anfang je ein element, im zweiten schritt - wenn alle zuverlässig sind - (n-1) elemente.

man könnte natürlich die nachrichtengrösse als "1" interpretieren, da "eine" Menge verschickt wird, aber das fände ich nicht sehr nützlich.

oder ist gemeint, dass die nachrichtengrösse innerhalb der Runden kostant bleibt? Ich dachte das konstant würde sich darauf beziehen, dass die Größe in Bezug auf die Teilnehmer (also n) konstant bleibt.

ich seh das so, dass jeder Prozessor seine eigene Meinung an alle schickt:
1. send < pref > to all processors

nicht mehr und schon gar nicht pro Runde wachsend viele Werte

bei der king-Runde wird auch nur ein einzelner Wert (der häufigste Wert) geschickt

Oh mann, ich hab grad den byzantinischen polynomiellen und den Ausfallkonsens völlig durcheinander bekommen. Mann, mann mann… So ich mach mal schnell die Prüfung.

@merlin und wie war die prüfung denn?????

Bin zufrieden. Ich hatte ja nur 8 Tage, weil vorher PNL anstand und die Vorlesung vor einem Jahr gehört. Dafür lief es wirklich gut. Valk ist aber auch der netteste Prüfer, den ich je erlebt hab. Protokoll schreib ich morgen

An dieser Stelle nochmal Dank an alle, die mir immer so schnell geantwortet habeb… [img]http://www.fb18.de/gfx/danke.gif[/img]

Hallo, ich habe auch einmal ein paar Fragen:

S. 18
Wieso "erzwingt" der Verdeckungsoperator Kommunikation?? Das verstehe ich nicht..

S.152
Kann mir jemand in natürlicher Sprache erklären was "konservativ" heißt?

Kann mir jemand den totally Broadcast-Algirithmus und/oder den (nur) kausalen "beschreiben" -auch natürlichsprachlich.

Meint ihr auch, dass man S.212 - S.219 getrost auslassen kann?

Was ist die "Sättigung"? Ich habe nur was über die "Sättigungsfüllung" gefunden" -oder ist das das Gleiche?

Kam schonmal bei jemandem BDDs oder Zeitstempel dran?

Wofür ist die Temporallogik eigentlich direkt? Was kann man alles damit machen?

Vielen Dank schonmal im Vorraus!

S. 18
Wieso "erzwingt" der Verdeckungsoperator Kommunikation?? Das verstehe ich nicht..

Friss oder stirb, so habe ich es verstanden. Wenn die Prozesse (Aktionen?) nicht miteinander kommunizieren wollen, führt das zum Abbruch.
-geschrieben, jemand der sich im Theorie-Bereich über einer 3.7 freut. [img]http://www.fb18.de/gfx/22.gif[/img]

S.152
Kann mir jemand in natürlicher Sprache erklären was "konservativ" heißt?

IMHO: Konservative P/T-Netze sind ``altmodisch'':

1) Ihre Plätze/Transitionen haben eine maximale Kantengewichtung
von 1 (W(x,y) <= 1) - es gibt also keine multiplen Kanten, sondern
maximal eine einzige zwischen einer Stelle zu einer Transition bzw.
eine einzige von einer Transition zu einer Stelle.

2) Naja, es wird noch eine Funktion f erwartet, die jede Stelle
einen Wert zuordnet, also jede Stelle gewichtet.
Die Summe der Gewichte aller Eingangsstellen ist gleich der Summe
der Gewichte aller Ausgangsstellen.

Die zweite Bedingung hat man wohl eingeführt, um so etwas nicht
durchgehen zu lassen:

+-------| ( ) b | ^ | | | ----- | | T |<----+ ----- ^ | ( ) a a, b: Stellen T: Transition Die erste Bedingung wird erfüllt.
Die zweite aber nicht:

Eingangsgewichte = Ausgangsgewichte
<=> f(a) + f(b) = f(b)

Hoffentlich sehe ich das jetzt richtig…

Was ist die "Sättigung"? Ich habe nur was über die "Sättigungsfüllung" gefunden" -oder ist das das Gleiche?

Wird im Skript irgendwo, dieses Wort ``Sättigung'' erwähnt?

Für BDDs reicht es glaub ich zu wissen, das es binäre Entscheidungsbäume sind, die die Variablen des Systems als boolsche Formeln repräsentieren. Dadurch kann man Zustände zusammenfassen.
BDDs benutzt man beim symbolischen Model Checking. Hierbei ist es nicht notwendig, explizit den gesamten Berechnungsbaum im Speicher aufzubauen, der zum Beispiel beim Abwickeln einer Kripke-Struktur entsteht.

Super! Vielen Dank schonmal!

Ich habe in einem Prüfungsprotokoll gelesen, dass er nach der "Sättigung" gefragt hätte..

Bitte kann mir jemand nochmal den exponentiellen und den polynomiellen byzantinischen Algorithmus einfacher erklären?
Woher weiss ich denn jetzt wer zuverlässig ist und wer nicht?
Danke

Bitte kann mir jemand nochmal den exponentiellen und den polynomiellen byzantinischen Algorithmus einfacher erklären?

Ich versuchs mal:

Beim byzantinischen exponentiellen ist die Hauptidee, dass sich jeder Prozessor
einen Baum baut, wo er die Nachrichten der anderen Prozessoren
speichert. Nach f+1 Runden lassen die Prozessoren die Funktion
resolve() auf je ihren Baum los, der dann die Mehrheitsmeinung
im Baum errechnet - am Ende hat jeder zuverlässige (= heile)
Prozessor die gleiche Meinung (Ausgangswert).

Beim polynomiellen Algorithmus benutzt man in jedem Rechenschritt
(= 2 Runden) einen anderen Prozessor als König.
Da man 2*(f+1) Runden lang diesen Algo fährt, kommt mindestens 1
zuverlässiger Prozessor als König dran. Die Konsensbedingungen -
Termination, Einigung und Gültigkeit - sind auch hier garantiert.

Woher weiss ich denn jetzt wer zuverlässig ist und wer nicht?

IMHO: Du weisst es nicht! Es ist auch egal, wer zuverlässig ist
und wer nicht. Beide Algorithmen garantieren Termination,
Gütligkeit und Einigung und nur das ist wichtig.

In einem Prüfungsprotokoll stand recht knapp "wie Paralleoperator in PA? Ableitungsregel in PA und Kalkül dazu?". Dabei fiel mir auf, dass ich noch kein Stück begriffen habe, was hier mit "im Kalkül" gemeint wäre. Ich hätte in der Prüfung jetzt erst mal die vier hier aufgeschrieben:

x -v-> # x -v-> x ' y -v-> # y -v-> y' ----------- --------------- ----------- --------------- x||y -v-> y x||y -v-> x'||y x||y -v-> x x||y -v-> x||y'
Das sind die Ableitungsregeln. Wären die das jetzt für "in PA"? Im Skript habe ich unter "Ableitung im Kalkül" nur auf Seite 9 ein Beispiel gesehen, allerdings als konkrete Anwendung für einen PA-Ausdruck. In Verallgemeinerung wüßte ich nicht, wie das nun aussehen sollte.

ohne Kalkül machts doch gar keine Spass,
in meinen Skript kommen auf Seite 17 nach Satz 2.14 die 'Axiome des PAP-Kalküls':
M1, LM2-4, CM5-10

das sind so Regeln der Art M1: x||y = (x||_y + y||_x) + x|y

Öhm. Danke. Da bin ich wohl an der Formulierung der Frage gescheitert. An die Axiome hatte ich zwar auch gedacht, aber … "Ableitungsregeln in PA und Axiome dazu?" hätte ich verständlicher gefunden. [img]http://www.fb18.de/gfx/25.gif[/img]

Ich noch mal mit was zu einfachen. [img]http://www.fb18.de/gfx/22.gif[/img]

Definition 2.24 Prozesse p1, … pn werden als eine Lösung einer rekursiven Spezifikation {X_i = t_i(X_1, …, X_n) | i e {1, …, n}} modulo Bisimulations-Äquivalenz bezeichnet, fals p_i <-> t_i(p1, …, p_n) for i e {1, …, n} gilt.

Prozesse sind hier doch als Konkretisierungen von Ausdrücken mit möglichen Rekursionsvariablen zu verstehen, oder? Also bei X = aX + a würde hier p_1 = a, p_2 = aa, … gemeint sein?

Hmm. Wo ich das Kapitel gerade zum sechsten oder siebten Mal lese. Da steht doch die Anwort gleich bei Beispiel 2.25. Nichts für ungut. [img]http://www.fb18.de/gfx/21.gif[/img]

Wir hatten hier schon ein, zwei Mal das Thema, wie dernn der Prozessgraph zu <X|X=aXb+c> aussehen würde und waren da zu dem Ergebnis gekommen:

aXb+c --a-- (aXb+c)b --a-- (aXb+c)bb | | |c |c |c |b | |b |b # # #
Was dabei aber noch nicht geklärt wurde ist, wie denn die Ableitung dafür aussieht. Ich habe mir das bis jetzt so überlegt:

Gleich c:

c -c> # ( # / v -v> #) v:=c <X|E>+c -c> # (y -v> # / x+y -v> #) v:=c
Nutzung der Rekursion:

a -a> # ( # / v -v> #) v:=a a<X|E> -a> <X|E> (x -v> # / x*y -v> y) v:=a, x:=a, y:=<X|E> a<X|E>+c -a> <X|E> (x -v> x' / x+y -v> x') v:=a, x:=a, y:=c x':=<X|E> Drei Fragen:
- Wie kann ich Formal jetzt noch schön aufschreiben, dass dieses <X|E> das <X|X = aXb+c> darstellt, sofern ich damit überhaupt richtig liege?
- Wäre das so alles an Ableitung oder müsste ich noch die "Nutzung der Rekursion" mit der Wahl von c hinzufügen? Wie würde so was aussehen?
- Ist in den Zeilen oben selbst noch was falsch?

aXb+c --a-->(aXb+c)b --a-->(aXb+c)bb --a-->.. | | | |c |c |c | | | # <----b---- b <----b----- bb <----b-..... so ist doch gleich hübscher imho [img]http://www.fb18.de/gfx/25.gif[/img]

Hi, da ich in ein paar Tagen meine PNL-Prüfung habe, wollte ich noch mal ein paar Unklarheiten klären.

1. Wurde zwar schon gefragt, aber noch nicht wirklich 100%ig beantwortet, glaube ich: Wie ist das mit der Fairness in temporaler Logik? In LTL ist die Fairness-Formel doch AGFp, oder? Entspricht das "auf allen Pfaden gilt immer wieder p"? Und ist das - wie Christoph schon fragte - nicht äquivalent zu AGAFp in CTL? Ich versteh den Unterschied noch nicht…

2. An diejenigen, die ihre Prüfung bereits hinter sich haben: wenn es um Algorithmen für total/kausal geordnete Broadcast-Kommunikation geht, wie genau musstet ihr das beantworten? Reicht das, das Prinzip des Algos zu erzählen oder muss Pseudo-Code her? Wie wollte Herr Valk das haben?

3. Wie ist das mit dem Alternierbitprotokoll? Gilt das als Verifikation bei Prozeßalgebra? Was wird da genau verifiziert?
Und reicht es, wenn man als Spezifikation des Protokolls
X = rA(d)*sD(d)*X
angibt? Oder sollen die Spzifikation von Sender und Empfänger (diese jeweils 3 Zeilen a la Sb, Tdb und Udb) angegeben werden?

Und reicht es, wenn man als Spezifikation des Protokolls
X = rA(d)*sD(d)*X
angibt? Oder sollen die Spzifikation von Sender und Empfänger (diese jeweils 3 Zeilen a la Sb, Tdb und Udb) angegeben werden?

Das reicht, wenn er nach der externen Spezifikation schreibt. Das andere will er nicht mal haben, wenn man drei Mal versucht es ihm unterzuschieben, weil man das so schön auswendig gelernt hat. [img]http://www.fb18.de/gfx/22.gif[/img]

Danke, das hört sich schonmal ein bisschen beruhigend an.
Jemand da, der noch auf die anderen Fragen antworten kann?

Kann mir denn keiner ne Antwort geben?
Vor allem die Sache zur Fairness in Temporal-Logik würde ich gerne nochmal erklärt bekommen. Ist die Formel jetz AGFp?
Und wie kann man Fairness bei Temporal-Logik schön in einem Satz ausdrücken? "Die Alternative von einer sich immer wiederholenden Alternative kommt immer wieder dran"?

wenns keiner weiß dann weiß es eben keiner,

zu Algorithmus erklären: da DENKE ich, dass Formulieren a la 'x sendet an y vektor mit blah blah' reichen,
wichtiger als Code ist auf jeden Fall zu wissen WARUM das eine total ist und das andere kausal oder was auch immer die Algorithmen garantieren