# Reference request: pi-calculus with simultaneous events

I am interested in using the $$\pi$$-calculus as a basis for modeling workflows, and came up with an extension that proved useful in my modeling, namely the ability to specify that two or more channel communications should take place simultaneously. I can only imagine that a similar extension has been treated before, but I just cannot find it mentioned anywhere, most likely because I don't know what to search for.

I will describe the basic idea with a simplified variant of the calculus with only signal/query events (i.e. no passing of names over channels) but extended with a simultaneous events: \begin{align} \mathsf{Action}\quad \alpha ::={}& a && \text{query} \\ {}\mid{} & \overline{a} && \text{signal} \\ {}\mid{} & \alpha_1\& \alpha_2 && \text{simultaneous composition} \\ {}\mid{} & \tau && \text{silent} \\ \\ \mathsf{Sum}\quad S ::={}& \alpha.P && \text{prefix} \\ {}\mid{}& S_1 + S_2 && \text{choice} \\ {}\mid{}& 0 && \text{inert process} \\\\ \mathsf{Process}\quad P ::={}& P_1 \mid P_2 && \text{composition} \\ {}\mid{}& \nu a\ldotp P && \text{new channel} \\ {}\mid{}& !P && \text{replication} \\ {}\mid{}& S && \text{synchronization} \end{align}

We define the usual congruence relation $$\equiv$$ with scope extrusion on processes, and such that processes with composition forms a commutative monoid with neutral element $$0$$, and such that sums with choice form a commutative monoid also with neutral element $$0$$. Furthermore, actions with simultaneous also form a commutative monoid with neutral element $$\tau$$, and furthermore the submonoid generated by channel names $$a$$ has a group structure with $$a^{-1} = \overline{a}$$. For example, $$a \& b \& \overline{a} \equiv b$$.

The operational semantics has communication rule

\begin{align} \frac{P \stackrel{\alpha_1}{\to} P' \quad Q \stackrel{\alpha_2}{\to} Q'}{P \mid Q \stackrel{\alpha_1 \& \alpha_2}{\to} P' \mid Q'} \end{align} and scoping rule \begin{align} \frac{P \stackrel{\alpha}{\to} P'}{\nu a\ldotp P \stackrel{\alpha}{\to} \nu a\ldotp P'}(\text{a \not\in \alpha}) \end{align}

The group structure on actions ensure that matching queries and signals cancel each other out. For example: \begin{align} a\&\overline{b}\ldotp P \mid b\ldotp Q \mid c\&\overline{a}\ldotp R \stackrel{c}{\to} P\mid Q \mid R \end{align}

But also: \begin{align} a\&\overline{b}\ldotp P \mid b\ldotp Q \mid c\&\overline{a}\ldotp R \stackrel{a}{\to} P\mid Q \mid c\&\overline{a}\ldotp R \end{align}

– mrp
Aug 25 '20 at 15:04
• My question is if there are any papers on this or similar extensions to the pi calculus. Aug 25 '20 at 15:10
• If I may ask, what books for learning about pi calculus (and maybe among others)?
– Tim
Aug 25 '20 at 19:19
• I found the following reference which extends CCS with simultaneous actions in a style similar to the above: Baillie, J., Smith, D. "A conservative extension to CCS for true concurrency semantics", 1994. hdl.handle.net/2299/4879. Aug 28 '20 at 17:12
• This makes me think of composition rules. You can for instance look to (maybe not the best nor cleanest choice, and a bit of self promotion, but it's past midnight here and that's the first paper that comes to my mind) link.springer.com/chapter/10.1007/978-3-030-21759-4_14 on p.8 (numbered 249) the rule (Comp). As a matter of fact, your extended pi-calculus is (quite directly) an instance of the hypercell framework presented here. However, I don't remember having seen a presentation as clean as you're doing, based directly on the plain pi calculus. Aug 28 '20 at 22:35