(Jak) możesz modelować transmisje za pomocą rachunku pi?

Czy potrafisz modelować wiarygodne transmisje w rachunku różniczkowym?

Jeśli tak to jak?

Jeśli nie: Czy istnieją podobne algebry procesowe, w których możesz?

Co próbowałem:

Jeśli nadawca chce wysłać wiadomość do wszystkich do , możesz napisać ! ( i do . Ale w jaki sposób gwarantujesz, że jest replikowany razy, tzn. Żadna wiadomość nie zostanie utracona? Nie wiem z góry. Czy jest to (tylko) możliwe wysyłanie kilku wiadomości w obie strony między wszystkimi zaangażowanymi procesami?$S$$y$$P_1$$P_n$
$\overline{x}y).S$$x(z).P_1$$x(z).P_n$$(\overline{x}y)$$n$$n$

... czy też źle rozumiem niedeterministyczne zachowanie replikacji?

Około dekady temu Ene i Muntean wykazali, że nadawanie nie ma rozsądnego kodowania kompozycyjnego w calculus [1]. Istota ich separacji między komunikacją punkt-punkt a przekazywaniem wiadomości jest łatwa do zrozumienia: punkt-punkt jest „zbyt asynchroniczny”. Oznacza to, że w systemie rozgłoszeniowym nadawca może wysłać do n procesów w jednym kroku atomowym dla dowolnego n . OTOH, jeśli proces chce komunikować się z n procesami za pomocą komunikacji punkt-punkt, można to zrobić tylko za pomocą $\pi$$n$$n$$n$$n$(lub więcej) oddzielnych wymian wiadomości, które mają stany pośrednie (np. nadawca wysłał wiadomości do 100 odbiorców i musi wysłać kolejne 150). Kontekst może obserwować, oddziaływać i zakłócać te stany pośrednie, co nie jest możliwe w przypadku komunikatów emisji atomowej. Aby poradzić sobie z tym brakiem rachunku (lub nawet rachunku opartego na przekazywaniu wiadomości punkt-punkt), Ene i Muntean proponują wariant emisji b π [2, 3], oparty na wcześniejszej pracy Prasad nad CBS, a wariant CCS z nadawaniem [4].$\pi$$\pi$

Technicznie bardziej [1] wywołuje kodowania wystarczającą , jeśli następuje to przypadek.$e$

• Kodowanie zachowuje kompozycję równoległą, tj. .$e(P|Q) = e(P) | e(Q)$
• Kodowanie zachowuje iniekcyjną zmianę nazwy, tj. dla dowolnej iniekcyjnej zmiany nazwy σ .$e(P\sigma) = e(P)\sigma$$\sigma$
• Kodowanie spełnia pewne warunki techniczne dotyczące zachowania akcji wejściowych i wyjściowych, patrz [1] w celu uzyskania szczegółowych informacji.

Następnie [1] pokazuje, że nie może istnieć rozsądne kodowanie od b do π . Wynik separacji ustalają przy użyciu wariantu techniki sprawdzania systemów wyborczych Palamidessiego [5].$\pi$$\pi$

Prace nad tym tematem były publikowane [1–4], np. Przez M. Hennessy'ego, ale są to prace pionierskie.

Nawiasem mówiąc, rozgłoszenie jest zwykle rozumiane jako jeden nadawca komunikujący się z wieloma odbiornikami, ale możliwe jest również uogólnienie komunikacji punkt-punkt w innym kierunku, w którym jeden odbiornik synchronizuje się z wieloma nadawcami (jest to używane np. W sieci Petriego ) lub hybrydowe formy obu. I. Phillips ustalił wynik separacji, który pokazuje, że tej formy nadawania nie można również zakodować w rachunku. Nie jestem pewien, czy ten wynik został opublikowany, czy nie.$\pi$

[1] C. Ene, T. Muntean, Ekspresyjność komunikacji punkt-punkt a komunikacja rozgłoszeniowa .

[2] C. Ene, T. Muntean, Rachunek emisyjny dla systemów komunikacyjnych .

[3] C. Ene, T. Muntean, Testowanie teorii procesów nadawczych .

[4] KVS Prasad, Rachunek systemów nadawczych .

$\pi$