Polyadic asynchronous asymmetric pi calculus

Posted in Programming by reperiendi on 2008 January 2

$\begin{array}{rll} P :=\\& \mbox{send } \langle y_1, \ldots, y_n\rangle \mbox{ on } \bar{x}. & |\\& \mbox{receive } \langle y_1, \ldots, y_n\rangle \mbox{ on } x; P &|\\& (P|P) &|\\& \mbox{new }y; P & |\\& !P\end{array}$

where $y$ is either an input channel $x$ or an output channel $\bar{x},$ and $x$ is taken from a countably infinite set.

Structural congruence:

$\mbox{new } y; P \equiv \mbox{new } y'; P'$ [with $y'$ replacing $y$ ] if $y'$ does not appear in $P'.$ (alpha conversion)
$(P|P') \equiv (P'|P)$ (parallel processes)
$((P|P')|P'') \equiv (P|(P'|P''))$ (association)
$\mbox{new } y; \mbox{new } y'; P \equiv \mbox{new } y'; \mbox{new } y; P$ (restriction)
$!P \equiv (P|!P)$ (replication)
$\mbox{new } y; (P|P') \equiv \mbox{new } y; P|P'$ if $y$ is not free in $P'.$

Reduction rules:

$(\mbox{send } \langle y_1, \ldots, y_n \rangle \mbox{ on } \bar{x}. | \mbox{ receive } \langle y'_1, \ldots, y'_n \rangle\mbox{ on } x; P) \to P$ [with $y_i$ replacing $y'_i$ ]
If $P_1 \to P_2$ then $(P_1|P_3) \to (P_2|P_3)$
If $P_1 \to P_2$ then $\mbox{new } y; P_1 \to \mbox{new } y; P_2$
If $P_1 \equiv P_2, \; P_2 \to P_3,$ and $P_3 \equiv P_4,$ then $P_1 \to P_4$

reperiendi

Polyadic asynchronous asymmetric pi calculus

Leave a Reply

The Author

The Pages

The Search

The Associates

The Archives

The Categories

The Meta