3
$\begingroup$

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}

$\endgroup$
  • $\begingroup$ What is your question? $\endgroup$ – mrp Aug 25 at 15:04
  • $\begingroup$ My question is if there are any papers on this or similar extensions to the pi calculus. $\endgroup$ – Ulrik Rasmussen Aug 25 at 15:10
  • $\begingroup$ If I may ask, what books for learning about pi calculus (and maybe among others)? $\endgroup$ – Tim Aug 25 at 19:19
  • $\begingroup$ 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. $\endgroup$ – Ulrik Rasmussen Aug 28 at 17:12
  • 1
    $\begingroup$ 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. $\endgroup$ – Bromind Aug 28 at 22:35
1
$\begingroup$

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

| cite | improve this answer | |
$\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.