(Como) você pode modelar transmissões no cálculo pi?

Você pode modelar transmissões confiáveis ​​no cálculo pi?

Se sim: como?

Caso contrário: existem álgebras de processo semelhantes onde você pode?

O que eu tentei:

Se o remetente quiser enviar uma mensagem y para todos os P 1 a P n , você poderá escrever ! ( ¯ x y ) . S e x ( z ) . P 1 a x ( z ) . P n . Mas como você garante que ( ¯ x y ) seja replicado n vezes, ou seja, nenhuma mensagem será perdida? Eu não sei $S$$y$$P_1$$P_n$
$\overline{x}y).S$$x(z).P_1$$x(z).P_n$$(\overline{x}y)$$n$$n$antecipadamente. É (apenas) possível com o envio de várias mensagens entre todos os processos envolvidos?

... ou entendo mal o comportamento não determinístico da replicação?

Cerca de uma década atrás, Ene e Muntean mostraram que a transmissão não possui codificação composicional razoável para o cálculo [1]. A essência de sua separação entre comunicação ponto a ponto e passagem de mensagens é fácil de entender: ponto a ponto é "muito assíncrono". Isso significa que em um sistema de transmissão, um remetente pode enviar para n processos em uma etapa atômica para n arbitrário . OTOH, se um processo deseja se comunicar com n processos usando comunicação ponto a ponto, isso só pode ser feito usando $\pi$$n$$n$$n$$n$(ou mais) trocas de mensagens separadas, que possuem estados intermediários (por exemplo, o remetente enviou mensagens para 100 destinatários e precisa enviar outras 150). Um contexto pode observar, interagir e interferir com esses estados intermediários, o que não é possível com as mensagens de transmissão atômica. Para lidar com essa deficiência de cálculo (ou mesmo qualquer cálculo baseado na passagem de mensagens ponto a ponto), Ene e Muntean propõem uma variante de transmissão b π [2, 3], com base em trabalhos anteriores de Prasad na CBS, variante do CCS com transmissão [4].$\pi$$\pi$

Mais tecnicamente, [1] chama uma codificação razoável se o seguinte for o caso.$e$

• A codificação preserva a composição paralela, ou seja, .$e(P|Q) = e(P) | e(Q)$
• A codificação preserva a renomeação injetiva, ou seja, para qualquer renomeação injetiva σ .$e(P\sigma) = e(P)\sigma$$\sigma$
• A codificação satisfaz algumas condições técnicas sobre a preservação das ações de entrada e saída, consulte [1] para detalhes.

Então [1] mostra que nenhuma codificação razoável de b a π pode existir. Eles estabelecem esse resultado de separação usando uma variante da técnica de prova de sistemas eleitorais de Palamidessi [5].$\pi$$\pi$

Há trabalhos sobre esse assunto desde que [1-4] foram publicados, por exemplo, por M. Hennessy, mas esses são os trabalhos pioneiros.

Além disso, a transmissão é geralmente entendida como um remetente se comunicando com muitos receptores, mas também é possível generalizar a comunicação ponto a ponto na outra direção em que você tem um receptor sincronizado com vários remetentes (isso é usado, por exemplo, em redes de Petri ) ou formas híbridas de ambos. I. Phillips estabeleceu um resultado de separação que mostra que essa forma de transmissão também não pode ser codificada no cálculo. Não tenho certeza se esse resultado foi publicado ou não.$\pi$

[1] C. Ene, T. Muntean, Expressividade de comunicações ponto a ponto versus transmissão .

[2] C. Ene, T. Muntean, um cálculo baseado em broadcast para sistemas de comunicação .

[3] C. Ene, T. Muntean, testando teorias para processos de radiodifusão .

[4] KVS Prasad, um cálculo de sistemas de radiodifusão .

$\pi$