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 ::={}&amp; 
   a &amp;&amp; \text{query}
   \\
   {}\mid{} &amp; \overline{a} &amp;&amp; \text{signal}
   \\
   {}\mid{} &amp; \alpha_1\&amp; \alpha_2 &amp;&amp; \text{simultaneous composition}
   \\
   {}\mid{} &amp; \tau &amp;&amp; \text{silent}
   \\
   \\
\mathsf{Sum}\quad S ::={}&amp;
   \alpha.P &amp;&amp; \text{prefix}
   \\
   {}\mid{}&amp; S_1 + S_2 &amp;&amp; \text{choice}
   \\
   {}\mid{}&amp; 0 &amp;&amp; \text{inert process}
  \\\\
\mathsf{Process}\quad P ::={}&amp;
  P_1 \mid P_2 &amp;&amp; \text{composition} \\
  {}\mid{}&amp; \nu a\ldotp P &amp;&amp; \text{new channel} \\
  {}\mid{}&amp; !P &amp;&amp; \text{replication} \\
  {}\mid{}&amp; S &amp;&amp; \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 \&amp; b \&amp; \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 \&amp; \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\&amp;\overline{b}\ldotp P \mid b\ldotp Q \mid c\&amp;\overline{a}\ldotp R \stackrel{c}{\to} P\mid Q \mid R
\end{align}
But also:
\begin{align}
  a\&amp;\overline{b}\ldotp P \mid b\ldotp Q \mid c\&amp;\overline{a}\ldotp R \stackrel{a}{\to} P\mid Q \mid c\&amp;\overline{a}\ldotp R
\end{align}
Milner defines the SCCS calculus in [1]. This is a generalization of CCS where the actions form an abelian group, and where the communication rule is defined as in my question.
[1] Milner, R. Calculi for synchrony and asynchrony. 1983. https://www.sciencedirect.com/science/article/pii/0304397583901147