16
$\begingroup$

Can you model reliable broadcasts in the pi-calculus?

If so: How?

If not: Are there any similar process algebras where you can?


What I have tried:

If sender $S$ wants to send a message $y$ to all $P_1$ to $P_n$, you could write
!($\overline{x}y).S$ and $x(z).P_1$ to $x(z).P_n$. But how do you guarantee that $(\overline{x}y)$ is replicated $n$ times, i.e. no messages get lost? I do not know $n$ in advance. Is it (only) possible with sending several messages back and forth between all processes involved?

...or do I misunderstand the nondeterministic behavior of replication?

$\endgroup$
19
$\begingroup$

About a decade ago, Ene and Muntean showed that broadcasting has no reasonable compositional encoding into the $\pi$-calculus [1]. The essence of their separation between point-to-point communication and message passing is easy to understand: point-to-point is "too asynchronous". That means that in a broadcasting system, a broadcasting sender can send to $n$ processes in one atomic step for arbitrary $n$. OTOH, if a process wants to communicate with $n$ processes using point-to-point communication, this can only be done using $n$ (or more) separate message exchanges, which have intermediate states (e.g. the sender has sent messages to 100 receivers, and needs to send another 150). A context can observe, interact and interfere with these intermediate states, which is not possible with the atomic broadcast messages. To deal with this shortcoming of $\pi$-calculus (or indeed any calculus based on point-to-point message passing), Ene and Muntean propose a broadcasting variant b$\pi$ [2, 3], based on earlier work by Prasad on CBS, a variant of CCS with broadcasting [4].

More technically, [1] calls an encoding $e$ reasonable if the following is the case.

  • The encoding preserves parallel composition, i.e. $e(P|Q) = e(P) | e(Q)$.
  • The encoding preserves injective renaming, i.e. $e(P\sigma) = e(P)\sigma$ for any injective renaming $\sigma$.
  • The encoding satisfies some technical conditions about the preservation of input and output actions, see [1] for details.

Then [1] shows that no reasonable encoding from b$\pi$ to $\pi$ can exist. They establish this separation result using a variant of Palamidessi's electoral systems proof technique [5].

There has been work on this subject since [1-4] were published, e.g. by M. Hennessy, but those are the pioneering papers.

As an aside, broadcast is usually understood as one sender communicating with many receivers, but it is also possible to generalise point-to-point communication in the other direction where you have one receiver synchronising with multiple senders (this is used in e.g. Petri nets), or hybrid forms of both. I. Phillips has established a separation result that shows that this form of broadcasting can also not be encoded in $\pi$-calculus. I am not sure whether this result is published or not.

[1] C. Ene, T. Muntean, Expressiveness of Point-to-Point versus Broadcast Communications.

[2] C. Ene, T. Muntean, A Broadcast-based Calculus for Communicating Systems.

[3] C. Ene, T. Muntean, Testing theories for Broadcasting Processes.

[4] K. V. S. Prasad, A Calculus of Broadcasting Systems.

[5] C. Palamidessi, Comparing the Expressive Power of the Synchronous and the Asynchronous $\pi$-calculi.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.