FB18 - Das Forum für Informatik

fb18.de / Diplom Informatik / Theoretische Informatik (HS)

PNL: Beweis des Alternierbit-Protokoll

PNL: Beweis des Alternierbit-Protokoll 2004-02-15 14:40
Anonymer User
Hallo,
ich komme mit der Verwendung des Verdeckungsoperators nicht klar. Im ersten Teil des Beweises (Skript Seite 35)hat man den Ausdruck R_0||S_0 in weitere Terme aufgesplitten. Anschließend wird der Verdeckugsoperator angewendet.

[img]http://mokrates.de/cgi-bin/texstring?R_%7B0%7D%7C%7CS_%7B0%7D%20=%20%5Csum_%7Bd'%5Cin%20%5CDelta%7D%20%5C%7B%20r_%7Bb%7D(d',0)%20%5Ccdot%20((s_%7Bc%7D(d')Q_%7B0%7D)%7C%7CS_%7B0%7D)+r_%7Bb%7D(d',1)%5Ccdot%20(Q_%7B1%7D%7C%7CS_%7B0%7D)%5C%7D%0D%0A%0D%0A+r_%7Bb%7D(%5Cbot)%5Ccdot%20%20(Q_%7B1%7D%7C%7CS_%7B0%7D)%20+%5Csum_%7Bd%20%5Cin%20%5CDelta%7Dr_%7Ba%7D(d)%20%5Ccdot%20(T_%7Bd0%7D%7C%7CR_%7B0%7D)%0D%0A%0D%0AWeiter%20erhaelt%20man%20mit%20D4,%20D1,%20D2,%20D5,%20A6,%20A7%0D%0A%0D%0A%5Cpartial_%7BH%7D(R_%7B0%7D%7C%7CS_%7B0%7D)%20=%20%5Csum_%7Bd%20%5Cin%20%5CDelta%7Dr_%7Ba%7D(d)%20%5Ccdot%20%5Cpartial_%7BH%7D(T_%7Bd0%7D%7C%7CR_%7B0%7D)[/img]



Die Menge H besteht doch aus vier Kommunikations-Aktionen, daher kann der Verdeckungsoperator doch nicht Terme wie Q_{0}||S_{0} komplett verschwinden lassen, da in der Menge H nur Kommunikationsaktionen und keine atomaren Aktionen vorkommen, Was passiert den mit den Left-Merge-Ausdrücken ???

Oder habe ich die Definition der Verdeckungsmenge H fehlinterpretiert???

Re: PNL: Beweis des Alternierbit-Protokoll 2004-02-15 15:56
XPhilosoph
Oder habe ich die Definition der Verdeckungsmenge H fehlinterpretiert???

Es werden alle falschen Kommunikationen verdeckt, also sowas wie d auf die Leitung schreiben, aber bottom lesen. Bleiben dann nur noch die vier definierten Kommunikations-Aktionen über, bzw. es wird alles außer diesen gestrichen.