(Wie) können Sie Sendungen im Pi-Kalkül modellieren?

Können Sie zuverlässige Sendungen im Pi-Kalkül modellieren?

Wenn das so ist, wie?

Wenn nicht: Gibt es ähnliche Prozessalgebren, wo Sie können?

Was ich ausprobiert habe:

Wenn der Absender eine Nachricht an alle bis senden möchte , können Sie schreiben ! ( und bis . Aber wie können Sie sicherstellen, dass mal repliziert wird, dh dass keine Nachrichten verloren gehen? Ich weiß nicht im Voraus. Ist es (nur) möglich, zwischen allen beteiligten Prozessen mehrere Nachrichten hin und her zu senden?$S$$y$$P_1$$P_n$
$\overline{x}y).S$$x(z).P_1$$x(z).P_n$$(\overline{x}y)$$n$$n$

... oder verstehe ich das nicht deterministische Verhalten der Replikation falsch?

Vor etwa einem Jahrzehnt haben Ene und Muntean gezeigt, dass der Rundfunk keine vernünftige kompositorische Kodierung im Kalkül hat [1]. Das Wesen ihrer Trennung zwischen Punkt-zu-Punkt-Kommunikation und Nachrichtenübermittlung ist leicht zu verstehen: Punkt-zu-Punkt ist "zu asynchron". Das bedeutet, dass in einem Rundfunksystem ein Rundfunksender in einem atomaren Schritt für ein beliebiges an Prozesse senden kann . OTOH, wenn ein Prozess mit Prozessen über eine Punkt-zu-Punkt-Kommunikation kommunizieren möchte , kann dies nur über$\pi$$n$$n$$n$$n$(oder mehr) separate Nachrichtenaustausche, die Zwischenzustände haben (z. B. der Absender hat Nachrichten an 100 Empfänger gesendet und muss weitere 150 senden). Ein Kontext kann diese Zwischenzustände beobachten, interagieren und stören, was mit den atomaren Rundfunknachrichten nicht möglich ist. Um dieses Manko des Kalküls (oder irgendeines Kalküls, das auf der Weitergabe von Punkt-zu-Punkt-Nachrichten basiert) zu beheben, schlagen Ene und Muntean eine Sendevariante b [2, 3] vor, die auf früheren Arbeiten von Prasad auf CBS basiert eine Variante von CCS mit Rundfunk.$\pi$$\pi$

Mehr technisch, [1] fordert eine Codierung vernünftig , wenn Folgendes der Fall ist.$e$

• Die Kodierung bewahrt die parallele Zusammensetzung, dh .$e(P|Q) = e(P) | e(Q)$
• Die Codierung bewahrt die injektive Umbenennung, dh für ein beliebiges injektives Umbenennen .$e(P\sigma) = e(P)\sigma$$\sigma$
• Die Codierung erfüllt einige technische Bedingungen für die Beibehaltung von Eingabe- und Ausgabeaktionen, siehe [1] für Einzelheiten.

Dann zeigt [1], dass keine sinnvolle Kodierung von b nach existieren kann. Sie ermitteln dieses Trennungsergebnis mit einer Variante der Wahlsystembeweismethode von Palamidessi [5].$\pi$$\pi$

Zu diesem Thema wurde bereits gearbeitet, seit [1-4] veröffentlicht wurden, z. B. von M. Hennessy, aber das sind die wegweisenden Arbeiten.

Im Übrigen wird Broadcast in der Regel als ein Sender verstanden, der mit vielen Empfängern kommuniziert. Es ist jedoch auch möglich, die Punkt-zu-Punkt-Kommunikation in die andere Richtung zu verallgemeinern, wenn ein Empfänger mit mehreren Sendern synchronisiert (dies wird z. B. in Petri-Netzen verwendet) ) oder Hybridformen von beiden. I. Phillips hat ein Trennungsergebnis aufgestellt, das zeigt, dass diese Form des Sendens auch nicht in -calculus codiert werden kann. Ich bin nicht sicher, ob dieses Ergebnis veröffentlicht wurde oder nicht.$\pi$

[1] C. Ene, T. Muntean, Ausdruckskraft der Punkt-zu-Punkt-Kommunikation im Vergleich zur Rundfunkkommunikation .

[2] C. Ene, T. Muntean, ein rundfunkbasierter Kalkül für Kommunikationssysteme .

[3] C. Ene, T. Muntean, Prüfungstheorien für Rundfunkprozesse .

[4] KVS Prasad, ein Kalkül von Rundfunksystemen .

[5] C. Palamidessi, Vergleich der Ausdruckskraft der synchronen und der asynchronen Kalküle$\pi$ .