<p>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.</p>
<p>[1] Milner, R. Calculi for synchrony and asynchrony. 1983. <a href="https://www.sciencedirect.com/science/article/pii/0304397583901147" rel="nofollow noreferrer">https://www.sciencedirect.com/science/article/pii/0304397583901147</a></p>

CC BY-SA 4.0
2020-09-09T11:39:59.473Z
2020-09-09T11:39:59.473Z
Ulrik Rasmussen
<p>I am interested in using the <span class="math-container">$\pi$</span>-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.</p>
<p>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:
<span class="math-container">\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}</span></p>
<p>We define the usual congruence relation <span class="math-container">$\equiv$</span> with scope extrusion on processes, and such that processes with composition forms a commutative monoid with neutral element <span class="math-container">$0$</span>, and such that sums with choice form a commutative monoid also with neutral element <span class="math-container">$0$</span>. Furthermore, actions with simultaneous also form a commutative monoid with neutral element <span class="math-container">$\tau$</span>, and furthermore the submonoid generated by channel names <span class="math-container">$a$</span> has a group structure with <span class="math-container">$a^{-1} = \overline{a}$</span>. For example, <span class="math-container">$a \&amp; b \&amp; \overline{a} \equiv b$</span>.</p>
<p>The operational semantics has communication rule</p>
<p><span class="math-container">\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}</span>
and scoping rule
<span class="math-container">\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}</span></p>
<p>The group structure on actions ensure that matching queries and signals cancel each other out. For example:
<span class="math-container">\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}</span></p>
<p>But also:
<span class="math-container">\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}</span></p>

CC BY-SA 4.0
2020-08-25T15:04:37.203Z
What is your question?
mrp
CC BY-SA 4.0
2020-08-25T15:10:37.157Z
My question is if there are any papers on this or similar extensions to the pi calculus.
Ulrik Rasmussen
CC BY-SA 4.0
2020-08-25T19:19:07.840Z
If I may ask, what books for learning about pi calculus (and maybe among others)?
Tim
CC BY-SA 4.0
2020-08-28T17:12:45.653Z
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. http://hdl.handle.net/2299/4879.
Ulrik Rasmussen
CC BY-SA 4.0
2020-08-28T22:35:12.520Z
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) https://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.
Bromind
<reference-request><pl.programming-languages><concurrency><formal-modeling><pi-calculus>
Reference request: pi-calculus with simultaneous events
Ulrik Rasmussen
# Reference request: pi-calculus with simultaneous events

(Asked by: username_0 on 2020-08-25)

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}

**Tags:** reference-request, pl.programming-languages, concurrency, formal-modeling, pi-calculus
> **Comments:**
> **username_1**: What is your question?  
> **username_0**: My question is if there are any papers on this or similar extensions to the pi calculus.  
> **username_2**: If I may ask, what books for learning about pi calculus (and maybe among others)?  
> **username_0**: 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. http://hdl.handle.net/2299/4879.  
> **username_3**: 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) https://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.  

---

## 1 answers

### Answer by username_0 on 2020-09-09. Score: 1

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>


---

