数理解析研究所講究録996 巻 1997 年 111-124

111

Multi-action -calculus$\pi$

Yukihiro ODA

Masaki MURAKAMI

Okayama University$\mathrm{E}$-mail:$\{\mathrm{o}\mathrm{d}\mathrm{a},\mathrm{m}\mathrm{u}\mathrm{r}\mathrm{a}\mathrm{k}\mathrm{a}\mathrm{m}\mathrm{i}\}@\mathrm{m}\mathrm{o}\mathrm{m}\mathrm{o}$.

$\mathrm{i}\mathrm{t}.\mathrm{o}\mathrm{k}\mathrm{a}\mathrm{y}\mathrm{a}\mathrm{m}\mathrm{a}^{-}\mathrm{u}.\mathrm{a}\mathrm{C}.\mathrm{j}\mathrm{p}$Abstract
We propose a new truly-concurrent semantics for the. We extend thelabelled transition system of the -calculus to use multi-sets of actions as labels. We
call this extension multi-action -calculus. The multi-action -calculus can describe
concurrent behavior of agents. Strong bisimilarity defined in the multi-action
calculus is closed under input-prefixings and parallel compositions.
$\pi- \mathrm{c}\mathrm{a}\mathrm{l}\mathrm{C}\mathrm{u}\mathrm{l}\mathrm{u}\mathrm{s}[1]$

$\pi$

$\pi$

$\pi$

$\pi-$

1

Introduction

In recent years, studies of process algebra, especially the $\pi- calCuluS[1]$ , have a lot of attention. The -calculus is an extension of. Agents of the -calculus can modify theirlinkage structures dynamically via name-passing mechanism. The observation equivalence
is proposed as a semantics, an equivalence relation over the -calculus agents. This semantics is called interleaving semantics, because this semantics is based on the notion ofinterleaving. In the view of the interleaving, concurrent (or parallel) executions are described by non-deterministic alternations of sequential executions. For example, agents $a|b$
and $a.b+b.a$ are regarded as same. This property is characterized as the expansion $law[2]$ .
The expansion law
very convenient to use CCS-like languages as formal specification
languages.
On the other hand, semantics those are not based on the interleaving are proposed.
These semantics are called non-interleaving semantics or truly-concurrent semantics. Thesesemantics focus the following problems:$\pi$$\mathrm{C}\mathrm{C}\mathrm{S}[2]$

$\pi$

$\pi$

$\mathrm{i}.\mathrm{s}$$\bullet$$\bullet$

CCS-like languages can describe concurrent systems of agents. But the interleaving
can not describe the concurrent behavior of agents truly. Any concurrent agent issequentialized in the interleaving semantics.
In the -calculus, the observation equivalence (even strong ground bisimilarity)
is not closed under input prefixings. That is, the expansion law is not correct inthe -calculus. For example,
but $x’(y).( \overline{X}Z|y(w))\oint$$x’(y).(\overline{x}z.y(w)+y(w).\overline{X}Z)$ .
Because the left-side agent can perform a action but
the right-side agent can not. This problem is caused via identification of concurrent
executions and sequential executions without consideration to communication ability
given by name-passing.
$\pi$

$\pi$

$\overline{x}z|y(w)\sim\overline{x}z.y(w)+y(w)_{\overline{X}}.Z$$\tau$

112
semantics
are already proposed as truly-concurrent semantics. These semantics improved the concurrency and the inconvenience involved with the name-passing. But these semantics havethe following problems:$\mathrm{L}\mathrm{o}\mathrm{C}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}[3][4][5],$$\bullet$$\bullet$$\mathrm{c}\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{t}\mathrm{y}[6][7][8][9],$$\mathrm{P}\mathrm{e}\mathrm{t}\mathrm{r}\mathrm{i}-\mathrm{N}\mathrm{e}\mathrm{t}[10]$, graph rewriting$\mathrm{s}\mathrm{y}\mathrm{s}\mathrm{t}\mathrm{e}\mathrm{m}[11]$We must analyze semantics of each agent to capture the concurrent behavior of suchagents. The concurrent behavior of agents should be captured from its semantics
directly.
Especially in the location based semantics, the concurrency that is captured by observation and that is determined by semantics are not equivalent. That is, concurrent
executions of an agent are regarded as sequential executions by semantics. This ruinscongruence of semantics by the similar way to the expansion law.

We discuss these problems again in Section 6.
We propose another truly-concurrent semantics for the -calculus to improve the above
two problems. The idea of our new semantics is to -define the notion of actions using
multi-actions. One multi-action means that two or more actions (or events) are performed.
concurrently and observed. For example, we infer a transition
We extend the labelled transition system of the -calculus to use multi-actions as labels anddefine bisimilarities over the extended -calculus. We call this extension of the -calculus
multi-action -calculus.
. But we canMulti-action approaches are already proposed for non-mobile
not adopt these works simply for the -calculus. Because the special treatment for name, also work
extrusion is required. In the -calculus, restriction operators, denoted byan agent
example,us
letconsider
way
the
CCS.
For
to
as sequentializers by the different$P=\overline{X}Zdef.Q_{1}|z(y).Q_{2}|w(y)$and $z(y)$ concurrently.
. Intuitively, $P$ performs action $w(y),$Suppose an agent $(\nu z)P$ . $(\nu z)P$ reaches deadlock after $w(y)$ in the framework of nonmobile calculi. Because executions of actions containing name are prohibited. On thefollowed by $z(y)$ .
other hand, in the -calculus, $(\nu z)P$ performs action $w(y)$ andeliminatesfrom the agent. But $z(y)$ can not be performed before
Becauseand these two actions are no longer performed concurrently. On the other hand, . $(y)$ andare concurrent. We must determine that which actions are concurrently executablewith a name-extrusion, when we use the Open Rule. This requirement of special treatment. We can consider many kinds
is similar to the case of the causality for theof treatments of name-extrusion. Congruence of semantics depends on the choice of thetreatments.
$\pi$$\mathrm{r}\mathrm{e}$$a.P|b.Q|(c+R)| \overline{c}\frac{a|b|\tau_{\backslash }}{/}P|Q$

$\pi$

$\pi$

$\pi$

$\pi$

$\mathrm{c}\mathrm{a}1_{\mathrm{C}\mathrm{u}}1\mathrm{i}[12]$$\pi$$(\nu z)$$\pi$$\overline{x}z$$z$$\overline{x}(z)$$\pi$$\overline{X}(Z)$$(\nu z)$$\overline{x}(Z)$$w$$\overline{x}(z)$$\pi- \mathrm{c}\mathrm{a}\mathrm{l}\mathrm{C}\mathrm{u}\mathrm{l}\mathrm{u}\mathrm{s}[6]$Outline of this paper: We introduce the -calculus and its bisimilarity in section 2. We
propose the multi-actions and the multi-action -calculus in section 3. And we propose
strong bisimilarity for the multi-action -calculus and prove its congruence (outline) in
section 4. We discuss the concurrency via multi-action in section 5. Finally, we compare
multi-action based semantics with other truly-concurrent semantics in section 6.
$\pi$

$\pi$

$\pi$

113

2

$\pi$

-calculus

In this section, we define the -calculus and its (observational) strong ground bisimilarity.
Furthermore, we show an example to demonstrate the problems mentioned in the previous
section.
$\pi$

DEFINITION 2.1 (Actions) Let $N$ be an infinite set of names. We define a set Act defined
as follows:
Act $def=\{xy, x(y),\overline{x}y,\overline{x}(y)|X, y\in N\}\cup\{\tau\}$range over Act. We identify and .
range over $N$ andWe letWhen we have no interest in the bject-part of an action, we omit it.
$x,$

$y,$

$\cdots$

$a,$

$b,$

$\overline{\overline{x}}$$x$$\cdots$$\dot{\mathrm{o}}$DEFINITION 2.2 (Agents) We define a set$\prime p$of all terms generated by the following rule:$P::=0|N(N).P|\overline{N}N.P|\tau.P|(\nu N)P$. $|P+P|P|P$

an agent. We abbreviate
We call each element of$Z=\{z_{1},z_{2},\cdots,Z_{n}\}$ . And we identify
as $(\nu Z)P$ with the multi-set.
.
usual way.
and structural congruence

where $N$ is an element of $N$ .
$(\nu z_{1})(\nu Z_{2})\cdots(\nu z_{n})P$.
and
We define$(\nu\emptyset)P$$bn(\cdot),$$fn(\cdot),$

$P$

$P$

$n(\cdot),$$obj(\cdot),$$sub(\cdot)$$\equiv \mathrm{i}\mathrm{n}$REMARK 2.3 Replication, denoted by $!P$ usually, is not considered.

DEFINITION 2.4 (name substitution) A name-substitution is a full function : $Narrow$$N$ . We write application of a name-substitution
to name as . Let be the identity
name-substitution and $\{x’/x\}$ is the same name-substitution to except $x\{x’/x\}=x’$ .
We also define application of a name-substitution to agents in usual way.
$\theta$$\theta$$x\theta$$x$$\iota$$\iota$ASSUMPTION 2.5 In order to simplify the following discussion, we assume that any boundname in an agent is distinct from any free name in such agent. That is, bound names arerenamed fresh names automatically in the agent.
DEFINITION 2.6 ($(P, Act,arrow)$$\mathrm{n}_{\mathrm{a}\mathrm{n}\mathrm{S}}\mathrm{i}\mathrm{t}\mathrm{i}_{0}\mathrm{n}$System) We define the labelled transition system $L=$
is the relation given by the transitive closure of$\mathrm{w}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}arrow\subset P\cross Act\cross \mathcal{P}$114

the following inference rules.
Input$\overline{xz}$$x(y).Parrow P\{z/y\}$Prefix$\overline{\alpha}$$\alpha.Parrow P$$\frac{Farrow P’a}{P+Qaarrow P’}$Sum$\frac{P\frac{\overline{x}y_{1}}{/}P’Q\frac{xy_{1}}{\prime}Q’}{P|Q\mathcal{T}arrow P’|Q’}$$\frac{Paarrow P’z\not\in n(a)}{(\nu z)Parrow(a\nu z)P’}$

Communication

Restriction$\frac{P\frac{\overline{x}(z)_{\backslash }}{/}P’Qarrow Q’x(z)}{P|Q\tauarrow(\nu Z)(P’|Q/)}$

Close, Open$\frac{P\overline{x}arrow P’ww\neq x}{(\nu w)Parrow P\overline{x}(w)}$$\frac{P\equiv QQaarrow Q’Q’\equiv P;}{Paarrow P’}$

Structure$\frac{Parrow P’a}{P|Qaarrow P’|Q}$

Parallel.

REMARK 2.7 Without ASSUMPTION 2.5, the side condition $bn(a)\cap fn(Q)=\emptyset$ is needed for
the Parallel Rule.

DEFINITION 2.8 (strong ground bisimilarity) A symmetric relation,strong ground bisimulation if and only if for every$\mathcal{R}\subseteq \mathcal{P}\cross \mathcal{P}$is a$(P, Q)\in \mathcal{R}$$Parrow P’a$(where $bn(a)\cap fn(P,$$Q)=\emptyset$)$\Rightarrow\exists Q’$. $Qarrow Q’a$ and$P’\mathcal{R}Q’$.

DEFINITION $2.9\sim def=$ (the largest strong ground bisimulation).
EXAMPLE 2.10 Please recall these two agent appeared in the Section 1.
$P_{0}$$def=\overline{x}z|y(w)$$Q_{0}$$def=\overline{x}z.y(w)+y(w).\overline{x}Z$

performs sequentially.
can not distinguishperforms actions concurrently but
have same interleaved (thatandagents via their concurrent behavior. Because bothis, sequential) transitions. For instance,.
$x’(y).P_{0}$$x’(y).Q0$. These two agent no longer
Suppose the following two agent
and. Because we have a transition
but we have $x’(y).Q0arrow x’x_{\#+}$
identified
always. Thus,
is not closed under input-prefixings.
$Q_{0}$$P_{0}$$\sim$$P_{0}$$arrowarrow\overline{x}zyw,$$-^{yw\overline{x}}arrow^{z},$$Q_{0}$$\cdots$$x’(y).P_{0}arrowarrow x’x\tau$$\mathrm{b}\mathrm{y}\sim$$\sim$

3

Multi-action -calculus$\pi$

In this section, we extend the -calculus. The extended calculus, multi-action -calculus,
uses the same syntax to the -calculus. But its labelled transition system uses multi-actions
$\pi$

$\pi$

$\pi$

115
as labels. A multi-action is a cluster of actions. Intuitively, the multi-action means that
actions in it are performed concurrently and observed. We des..cribe the concurrent behaviorof agents directly using multi-actions.

DEFINITION 3.1 Let be an infix 2-ary operator symbol. We define a set $A_{Act,|}$ of terms
generated from the rule:$A::=Act|A|A$ .
$|$range over $A_{Act,|}$ .
We let $A,$ $B,$Let
be the smallest binary relation over $A_{Act,|}$ that satisfies the following conditions:$\cdots$$=_{s}$$\bullet$$\bullet$

It is an equivalence relation,$(A|B)|c=_{s}A|(B|C)$ , and$\bullet A|B=_{s}B|A$.

We abbreviate $A_{Act,|/}=_{S}$ (the quotient set of $A_{Act,|}$ by
DEFINITION 3.2 We define a binary operator

A$A|_{A}B^{de}=^{f}\{$over$|_{A}$$=_{s}$) as $A$ , and$[A]_{=_{S}}$

as

$A$

.

$A\cup\{\emptyset\}$,,otherwise.
$B=\emptyset$$B$$A=\emptyset$$A|B$

More specifically, the final line means that $[A]_{=_{S}}|_{A}[B]_{=_{S}}def=[A|B]_{=_{S}}$ .
DEFINITION 3.3 Let $b\in Act.$ and are communicatable if and only ifnote that any bound action and free action are not communicatable.
$a,$

$b$

$a$

$a=\overline{b}$. Please

DEFINITION 3.4$\tau|_{A}(A\prime \mathrm{M}B’)$$A\mathrm{N}B$$def=$

if$\exists a,$$A|_{A}B$

andotherwise.

$\{y\}\cup+\mathrm{T}\mathrm{l}\mathrm{E}(A’, B’)$

$def=$$\{$$\mathrm{T}\mathrm{l}\mathrm{E}(A, B)$$\emptyset$. $A=a|A’,$ $B=b|B’$ andare communicatable,$b\in Act$

$a$

$\{$

if

$b$

$y\in N$ . ( $A=\overline{x}(y)|A’$ and $B=x(y)|B/$ ) or
$A=x(y)|A’$(
and $B=\overline{x}(y)|B’$ ),$\exists x,$otherwise.

wherethe multi-set union operator. Thus, TIE $(A, B)$ takes two elements of $A$ andreturns a multi-set of names.
$\cup+\mathrm{i}\mathrm{s}$Intuitively,
invokes interactions between communicatable actions in and simultaneously. TIE $(A, B)$ gives names required to bind after interactions between bound actionsin and .
$A\triangleright\triangleleft B$

$A$

$B$

$A$

$B$

116
EXAMPLE 3.5$\overline{a}(z)|b(w)|cy|d\mathrm{N}\overline{b}(w)|a(z)|\overline{C}y$$\mathrm{T}\mathrm{t}\mathrm{E}(\overline{a}(z)|b(w)|cy|d, \overline{b}(w)|a(Z)|\overline{c}y)$

LEMMA 3.6 Let
is the unit element of$M_{\mathrm{S}}\mathrm{t}\mathrm{r}\mathrm{o}\mathrm{n}\mathrm{g}=def(A\cup\{\emptyset\}, \emptyset, |_{A})$$M_{\mathrm{S}\mathrm{t}\circ}\mathrm{r}\mathrm{n}\mathrm{g}$. Then,$M_{\mathrm{S}\mathrm{t}\circ}\mathrm{r}\mathrm{n}\mathrm{g}$$=\tau|\tau|_{\mathcal{T}}|d$$=$$\{w, z\}$is a commutative monoid and$\emptyset$.

$\mathrm{D}\mathrm{E}\mathrm{F}\mathrm{I}\mathrm{N}\mathrm{I}\mathrm{T}\iota.1.\mathrm{O}\mathrm{N}3.7(\mathrm{M}\mathrm{u}\mathrm{l}\mathrm{t}\mathrm{i}-\mathrm{a}\mathbb{C}\mathrm{t}\mathrm{i}\mathrm{o}\prime \mathrm{n})$.

We call each.ment of$\mathrm{e}\mathrm{l}\mathrm{e}$$M_{\mathrm{S}\mathrm{t}\mathrm{r}\circ \mathrm{n}}\mathrm{g}$

a

$.m$

ulti-action.

We can use any structure as the multi-actions if it follows the definitions. For example, we
can use the multi-set of actions and multi-set union as the multi-actions.
.
asas . For convenience, we write
We abbreviate$|_{A}$$\Pi_{i\leq n}A_{i}$$|$$A_{1}|A_{2}|\cdots|A_{n}$EXAMPLE 3.8 $\{a|b|c, c|a|b, b|a|c\}$ is a set of same multi-actions.
and $\{a|\tau, a\}$ are sets of different multi-actions.

$\{a|b, a|a|b, a|b|\tau\}$,$\{a|\overline{a}, \tau, \tau|\tau\}$

DEFINITION 3.9 We define a function$f_{\dot{i}}(\cdot)$over multi-actions:. $A=xy|A’$ ,ifotherwise.
$\exists x,$$f_{\dot{i}}(A)def=\{$$xy|f\dot{i}(A’\emptyset)$$y$

We also define $fo(A)$extraction of free-output from ), $bi(A)$ (extraction of bound-input from ) and $bo(A)$(extraction of bound-output from ).
We define a function $bo2fo(\cdot)$ as follows:$fi(A)$ is the multi-action constructed from free-input actions in $A$ .

$($

$A$

$A$

$A$

$\overline{x}y|bo2fo(A’)$$bo2f_{\mathit{0}}(A)=^{f}de\{$

$A$

if
.
otherwise.
$\exists x,$$y$$A=\overline{x}(y)|A^{J}$,

is the multi-action obtained by replacing each bound-output.
corresponding$bo2fo(A)$$\overline{x}(y)$

of

$A$

with

$\mathrm{f}_{\Gamma \mathrm{e}\mathrm{e}- \mathrm{o}\mathrm{u}\mathrm{t}\mathrm{u}}\mathrm{P}\mathrm{t}\overline{X}y$DEFINITION 3.10 (Multi-action bansition System) We define the labelled transition
systemis the relation given by the transitive closure$L_{M}=(P, A,\prec)\mathrm{M}\mathrm{h}\mathrm{W}\mathrm{e}\mathrm{r}\mathrm{e}arrow\subset \mathrm{M}P\cross A\cross P$

117of the following inference rules.
$\overline{\alpha}$$\alpha.P*P$$\frac{Parrow P’A\mathrm{M}}{P+Q\mathrm{M}arrow AP’}$Input$\overline{xz}$$x(y).Parrow P\{\mathrm{M}z/y\}$PrefixSum$\frac{Parrow P’Z\not\in \mathrm{M}nA(A)}{(\nu Z)Parrow(\mathrm{M}\nu z)AP’}$

Restriction, Communication$\frac{Parrow_{\mathrm{M}}PJQ\mathrm{M}arrow Q’A_{P}AQ}{P|Qarrow_{\mathrm{M}}A_{P}\triangleright\triangleleft A_{Q}(\nu \mathrm{T}1\mathrm{E}(AP,AQ))(P’|Q)}$,$\frac{Parrow_{\mathrm{M}}P’w\neq Xw\not\in A|\overline{x}wSub(A)\cup obj(f_{\dot{i}}(A))}{(\nu w)Parrow PA|\overline{x}(w\mathrm{M})}$$\frac{P\equiv QQ\mathrm{M}arrow Q’Q’\equiv AP;}{Parrow P’,\mathrm{M}A}$StructureOpen$\frac{Parrow P’\mathrm{M}A}{P|Q\mathrm{M}arrow P’|QA}$

Parallel

REMARK 3.11 Without ASSUMPTION 2.5, the Communication Rule must have complexedside conditions. That is, “bound actions ofcome fromdo not bind any freename in agent and $Q’$ , and vise versa. Furthermore, names in TIE $(A_{P}, A_{Q})$ are distinct”.
from names in
Of course, the side condition $bn(A)\cap fn(Q)=\emptyset$ is needed for the Parallel Rule.
$A_{P}\triangleright\triangleleft A_{Q}$$A_{P}$$Q$$A_{P}\mathrm{M}A_{Q}$“”

EXAMPLE 3.12 We can obtain a transition $a|b(w).P|(\nu Z)(\overline{b}Z|z.Q)-_{\mathrm{M}}a|\tau(\nu z)(P\{z/w\}|Z.Q)$
by the following inference:$\underline{\overline{b}zarrow^{z}0\overline{b}\mathrm{M}}$$\frac{aarrow 0ba(\mathrm{M})w.Parrow P\{\mathrm{M}Z/w\}b(z)}{a|b(w).P\frac{a|b(z)_{\backslash }}{\underline \mathrm{M}}P\{z/w\}},\frac{\overline{b}z|\mathcal{Z}.Q\mathrm{M}arrow z.QzZ\neq bZ\in\emptyset\overline{b}}{(\nu z)(\overline{b}Z|z.Q)\mathrm{M}arrow Z.Q\overline{b}(z)}$$a|b(w).P|(\nu z)(\overline{b}z|Z.Q)arrow_{\mathrm{M}}(a|\cdot\tau\nu z)(P\{z/w\}|z.Q)$

On the other hand, we can not obtainthe transition

4$(\nu z)(\overline{b}Z|z.Q)-_{\mathrm{M}}\overline{b}(z)|zQ$$a|b(w).P|( \nu Z)(\overline{b}Z|z.Q)\frac{a|\tau|z\backslash }{\mathrm{M}},$.

$(\nu z)(P\{z/w\}|Q)$

becauseis prohibited.

Strong Bisimilarity

In this section, we propose strong ground bisimilarity for the multi-action -calculus andwe show congruent results for this bisimilarity.
$\pi$

118
DEFINITION 4.1 (strong ground multi-action bisimilarity) A symmetric relation,$P\cross P$ is a strong ground multi-action bisimulation if and only if for every$\mathcal{R}\subseteq$$(P, Q)\in \mathcal{R}$$Parrow P’A\mathrm{M}$

DEFINITION(where $bn(A)\cap fn(P,$$4.2\sim \mathrm{M}def=$$Q)=\emptyset$)$\Rightarrow\exists Q’$.

and$P\prime \mathcal{R}AQ’$$Q\mathrm{M}arrow Q’$(the largest strong ground multi-action bisimulation).

in usual way. We can show
We also define strong ground multi-action bisimulation up
is athat if a relation 7? is a strong ground multi-action bisimulation up
strong ground multi-action bisimulation.
$to\sim \mathrm{M}$$\mathrm{t}\mathrm{o}\sim \mathrm{M}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\sim \mathrm{M}\mathcal{R}\sim \mathrm{M}$

THEOREMpositions.
THEOREM$4.3\sim \mathrm{M}$$4.4\sim \mathrm{M}$is closed under -prefixings,$\tau$$\mathrm{o}\mathrm{u}\mathrm{t}\mathrm{p}\mathrm{u}\mathrm{t}-.\mathrm{p}_{\Gamma \mathrm{e}}\mathrm{f}\mathrm{i}\mathrm{X}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{s}$, restrictions and sum com-

is closed under parallel compositions.

is
DISCUSSION 4.5 By the side-conditions of the Open Rule in the DEFINITION 3.10,$w\not\in sub(A)\cup obj(f\dot{i}(A))$ checks eachpreserved for parallel compositions. The side-condition
action’s independency of extruded name . We can consider many kinds of independency(or dependency) involved with name-extrusion. For example, link $dependency[6]$ , enabling$dependency[6]$ and object $dependency[6][8]$ are considered. But these dependencies are notappropriate.
$\sim \mathrm{M}$$w$$\frac{\underline{\mathrm{d}\mathrm{e}\mathrm{P}\mathrm{e}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{y}\mathrm{a}\mathrm{C}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{s}\mathrm{d}\mathrm{e}\mathrm{p}\mathrm{e}\mathrm{n}\mathrm{d}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{o}\mathrm{n}\overline{X}(a)}}{1\mathrm{i}\mathrm{n}\mathrm{k}\subset_{\iota_{n}k}\overline{a}Z,\overline{a}(_{Z}),az,a(z)}$object$\ll_{obj}$

enabling$\subset_{lnk}’$-action$\overline{y}a,$$ya$$\overline{a}z,\overline{a}(Z),$$az,$ $a(z),\overline{y}a,$ $\overline{y}(a),$ $ya$$aZ,$ $a(Z),$ $ya$$\underline{\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{t}\mathrm{i}}$$\overline{a}z,$$\overline{a}(Z),$The link dependency is not appropriate in the sense of the concurrency. Because it allows. This transition do not satisfy confluencetransitions likefor parallel(see Section 5). Furthermore, such transitions do not contribute to’withalways can perform
compositions. Because agent
candependency
enabling$z’,$
theis preserved. The object dependency andfresh namecongruence for parallel compositions. For example, let
not make. Both dependencies prohibit agent $P$ to performand. But parallel composed agent $P|(x_{1}(y)|x2(y))$ is not strongly. Thus,$( \nu z)(\overline{X_{1}}Z.Z|X_{2}(y).\overline{y}+R)\frac{\overline{x_{1}}(z)|x_{2}z\backslash }{\mathrm{M}},$$\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{S}\mathrm{e}\mathrm{r}\mathrm{v}\mathrm{e}\sim \mathrm{M}$$\overline{X_{1}}(Z)|x_{2}(Z)$$(\nu z)(\overline{X_{1}}Z.Z|X_{2}(y).\overline{y}+R)$$\sim \mathrm{M}$$Pdef=(\nu z)(\overline{X1}z|\overline{x_{2}}z)$$\sim \mathrm{M}$$Q^{def}=(\nu z)(\overline{x1}^{Z}\cdot\overline{x2}Z)+(\nu z)(\overline{X2}Z.\overline{x1}Z)$$\overline{x_{1}}(z)|\overline{X2}Z$$P\sim \mathrm{M}Q$

bisimilar to $Q|(x_{1}(y)|X2(y))$ . Because$Q|(x_{1}(y)|x2(y))\star_{\mathrm{M}}^{|\tau}\mathcal{T}arrow$

..

.

.
DISCUSSION 4.6 In the previous DISCUSSION 4.5, we focus the transition
in a weak bisimilarity.
This transition raise a question whether we should identify and$P|(x_{1}(y)|X2(y))\neq_{\mathrm{M}}arrow\tau|\tau$$\tau$$\tau|\tau$119
Let us consider the following systems:$Mem^{def}=\overline{read}v.Mem+write(v).Mem$

Exec

$\{$

$def=exec(v).\mathcal{T}.\overline{wr\dot{i}te}$v.Exec$=r$
Fetchl $defead(v).\overline{decode}v.Fet_{C}h1$

Decode 1 $def=deCode(v).\overline{exec}$ v.Decode 1$Sys^{def}=(\nu\{deCode, read\})(FetCh1|DeCode_{1}|Mem)$$Fetch2=rdefead(v).(\overline{deCode}v|Fetch_{2})$$\{$$Decode2=ddefecode(v).(\overline{exeC}v|Decode_{2})$PLSys $def=(\nu\{deCode, read\})(Fetch_{2}|DeCode_{2}|Mem)$ .
If we adopt the view of “”, then system $Sys$ and PLSys are weakly multi-action
bisimilar, furthermore weakly multi-action congruent. Thus whole system $Sys|Exec$ and$PLs_{ys}|EXec$ are regarded as same. But we consider the system $PLSys|EXec$ is moredesirable because PLSys is pipe-lined. $Sys$ performs fetch-decode stage sequentially as the. On the other, PLSys can perform fetch-decode stage concurrently
or in parallel) as theIf we refine an agent via its degree of the concurrency,
then we should distinguish and.
$\tau=\tau|\tau$$\mathrm{t}_{\mathrm{f}\mathrm{a}\mathrm{n}\mathrm{S}}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}-\tau i\mathrm{p}\mathcal{T}$$($$\mathrm{h}\mathrm{a}\mathrm{n}\tau|\tau \mathrm{d}$$\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{S}\mathrm{i}\mathrm{t}\mathrm{i}0\mathrm{n}-\mathrm{M}^{\cdot}$$\tau|\tau$$\tau$

THEOREM$4.7\sim \mathrm{M}$is closed under input-prefixings.

Outline of. Let a relation $\mathcal{R}def=\{((\nu Z)(P\theta), (\nu Z)(Q\theta))|P\sim \mathrm{M}Q\}$ . We showthat 7? is strong ground multi-action bisimilar up to. We prove that
Consider.
. In the case analysis of , the mostandsignificant case is.
. When, there always exists a multi-action’$A’$and a multi-set of names $Z$ that satisfy
and $(\nu Z)(PJ’\theta)\equiv P’$ . $A’$ and are
obtained from the inference tree of the transition
constructively. By the definitionof. Thus, there existsthat satisfies
and. By the definitionof. On the other hand, for same $A,$ $A’$ and $Z$ , when,
there always exists $Q’$ that satisfies.
Therefore,
and
$Q’$
when
there existsthat satisfies
and$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{o}\mathrm{f}\cdot$$P\theta$$\sim \mathrm{M}^{\cdot}$$P\thetaarrow_{\mathrm{M}}AP’\Rightarrow\exists Q’$$Q\thetaarrow_{\mathrm{M}}AQ’$$\exists A^{u}$$A$$P_{\mathrm{M}\mathrm{M}}’\sim \mathcal{R}\sim Q’$$A=\tau|A\prime\prime$$P\thetaarrow_{\mathrm{M}}AP’$$P-_{\mathrm{M}}A’P’$$Z$$P\theta \mathcal{T}arrow P’\mathrm{M}$$\mathcal{R},$$\mathcal{R},$$Q\mathrm{M}arrow A’Q’’$$Q^{n}$$P\sim \mathrm{M}Q$$P\prime\prime\sim \mathrm{M}Q’’$$Q\mathrm{M}arrow Q’A’/$$(\nu Z)(P^{n}\theta)\mathcal{R}(\nu Z)(Q\prime\prime\theta)$$Q\thetaarrow_{\mathrm{M}}AQ’$$P\thetaarrow P’A\mathrm{M}$’$(\nu Z)(Q\prime\prime\theta)\equiv Q’$$Q\thetaarrow Q’\mathrm{M}A$$\equiv\subset\sim \mathrm{M}^{\cdot}$$P_{\mathrm{M}}’\sim \mathcal{R}\sim Q’\mathrm{M}^{\cdot}$$\square$DISCUSSION 4.8 If we introduce the notion of multi-action for congruence of (strong)bisimulation, then it is sufficient to introduce double-actions. A double-action is a multiaction the length of that is one or two. But double-actions can not describe the concurrency.
For example, suppose priority composition (denoted) and the following transition
rule:
Priority$\mathrm{b}\mathrm{y}\triangleright$$\frac{Paarrow P’}{P\triangleright Qaarrow P|Q},$.

120
are strongly bisimilarand
In double-action framework, agent,
and its bisimilarity is preserved in any context. But the former agent performs
concurrently and the later agent can not perform those actions concurrently. Similar
example can be shown for weak bisimilarity without priority compositions.
$(a|\overline{b})\triangleright c+(c|\overline{b})\triangleright a+(a|C)\triangleright\overline{b}$$a|\overline{b}|c$$\overline{b}$

$a,$

$c$

Concurrency

5

The concurrency described via multi-actions is characterized by confluence of transitions.
And we define anotherTo show that, we refine the multi-action transition
multi-action transition
usin.g a notion of confluence. Finally, we obtain that.
$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}\prec \mathrm{M}^{\cdot}$$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}-\mathrm{M}t’$$arrow=- \mathrm{M}\mathrm{M}\mathit{4}’$DEFINITION 5.1 Let
lowing conditions$\bullet$$=_{b}$

be the smallest binary relation over

$A=_{s}B\Rightarrow A=_{b}B$$A_{Act,|}$that satisfies the fol-

, and$\bullet\overline{x_{1}}(z)|\overline{x_{2}}Z|A=_{b}\overline{X1}^{Z}|_{\overline{X_{2}}}(Z)|A$.

and the operation
We can consider
as $A’$
the following, we abbreviate$|_{A’}$$A_{Act,|/_{=_{b}}}$on this set in the similar way to$|_{A}$. In$A_{Act,/_{=_{b}}}|$. Then,LEMMA 5.2 Let
is the unit element.

is a commutative monoid and$M_{\mathrm{S}\mathrm{t}}^{\mathrm{i}/_{\mathrm{r}\mathrm{o}}}\mathrm{e}\mathrm{n}\mathrm{g}$$M_{\mathrm{S}\mathrm{t}}^{\mathrm{i}/_{\mathrm{r}}}\mathrm{e}de=\circ \mathrm{n}\mathrm{g}f(A’\cup\{\emptyset\}, \emptyset, |_{A’})$$\emptyset$

Now, we$\mathrm{r}\mathrm{e}$-define the transition

DEFINITION 5.3
THEOREM 5.4$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\prec \mathrm{M}$using$M_{\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{o}\mathrm{n}\mathrm{g}}^{\mathrm{i}/\mathrm{e}}$.

$-\mathrm{M}\mathrm{f}=def\{(P, [A]_{=_{b}}, P’)|Parrow P’\}\mathrm{M}A$$P \frac{\overline{x_{1}}(z)|\overline{x_{2}}z|A_{\backslash }}{\mathrm{M}},$$P’ \Rightarrow P\frac{\overline{x_{1}}z|\overline{x_{2()1}}zA_{\backslash }}{\mathrm{M}/}P’$.

have same computations. And the
REMARK 5.5 THEOREM 5.4 means
information “which action extrude the name” in a multi-action are not needed for ouris not preserved for parallel compurpose. If these information make some sense,
positions (see DISCUSSION 4.5). Required information for a multi-action are “which names
are extruded” To emphasis this property, we introduce the notation defined in$\mathrm{a}\mathrm{n}\mathrm{d}arrow \mathrm{M}$$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}arrow_{\mathrm{M}}$$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\sim \mathrm{M}$$\mathrm{N}_{\mathrm{o}\mathrm{T}\mathrm{A}\mathrm{T}}1\mathrm{o}\mathrm{N}$

$5.6$

.

In the following, we use$\mathrm{t}\mathrm{h}\mathrm{e}arrow \mathrm{M}$as$\mathrm{t}\mathrm{h}\mathrm{e}arrow \mathrm{M}$.

. We denote this element as $(\nu Z)A’$ wherebe an element of
NOTATION 5.6 Let$Z–obj(bo(A))$ and $A’=bo2fo(A)$ . A $(\nu Z)A$ is valid if and only if $Z\subseteq_{M}obj(fo(A))$ .
$[A]_{=_{b}}$$M_{\mathrm{S}\mathrm{t}\mathrm{o}\mathrm{n}\mathrm{g}}^{\mathrm{i}/}\mathrm{r}\mathrm{e}$We define another multi-action transition$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}-\mathrm{M}l$using the confluence of transitions.

121
DEFINITION 5.7 (link independency predicate) We define a binary predicate$A’$ . Let $(\nu Z_{1})A1,$ $(\nu Z_{2})A2\in A’$ .

$\nu$

over

$(\nu Z_{1})A1\nu(\nu Z_{2})A2\Leftrightarrow obj(fo((\nu Z1)A1))\cap Z_{2}=\emptyset$

where $(\nu Z_{1})A1$ and $(\nu Z_{2})A2$ are valid.
EXAMPLE 5.8
But

. And

$(\nu z)(\overline{x1}z|\overline{X2}z|\overline{x_{3}}y)\nu\overline{x_{1}}y|\overline{x_{2}}z$$(\nu Z, Z)(\overline{X1}Z|\overline{X2}z|\overline{X_{3y}})\nu(\nu z)(\overline{X1}y|\overline{X2}z)$.

.

$(\nu Z, Z)(\overline{X1}Z|\overline{X2}z|\overline{X_{3y}})t(\nu z, y)(\overline{x_{1}}y|\overline{X2}z)$be multi-actions, $P,$ $P’$ be agents and
DEFINITION 5.9 (Confluence) Let
multi-set of names. $A_{1^{arrow}P,P’},ZA2$ if and only if the following condition is satisfied:$A_{1},$ $A_{2}$For every$(\nu Z_{12})A_{2}$where$Z_{11},$ $Z_{1}2,$

and$C,$ $C’,$$Z21,$ $Z22$

$Z$

be a

, those satisfy $Z_{11}|z_{12}=Z_{21}|z_{22}=Z,$ $(\nu Z_{11})A_{1}\nu$, the following diagram is commuted.

$(\nu Z_{21})A_{2}\mathrm{r}(\nu Z_{22})A_{1}$$C_{1}$

andare two-hole contexts. The transition$C_{2}$$C[P_{1}, P_{2}]arrow_{\mathrm{M}}^{1}(\nu Z_{1})A1$

must be caused by the internal transition’ where. The other transitions must be also restricted to
is a (multi-set) subset ofor .
transitions caused by$P_{1}-(\nu Z_{11}’)A_{1}P_{1}’\mathrm{M}$$C_{1}[P_{1’ 2}’P]$$Z_{11}’$$Z_{11}$$P_{1}$$P_{2}$

DEFINITION 5.10
if $(\nu Z)A=a$
for any $A_{1}|A_{2}=A$ . $A_{1P,P}arrow’,z^{A_{2}}$ , otherwise$Paarrow P’$$Parrow_{\mathrm{M}}P^{\prime^{d}}(\nu Z)A’ef’=\{$

THEOREM$5.11arrow_{\mathrm{M}}=A_{\mathrm{M}}’$,.

REMARK 5.12 By THEOREM 5.11,$P \frac{a|b_{\backslash }}{\mathrm{M}},$$P’ \Rightarrow P\frac{ab}{\mathrm{M}\mathrm{M}}P’$

and$P \frac{ba}{\mathrm{M}\mathrm{M}}$. This is similar

. The
and
to the expansion law. But please note that
preserved.
locationstoberequires
kind
of
some
confluence defined by DEFINITION 5.9$Parrowarrow^{b}P’\mathrm{M}\mathrm{M}a$6$P arrowarrow \mathrm{M}\mathrm{M}ba\Leftrightarrow P\frac{a|b_{\backslash }}{\mathrm{M}’}P’$

Comparing with other approaches

In this section, we compare the multi-action approach with other approaches, $l_{oCat}ion[3][4][5]$and $causal_{i}ty[6][7][8][9]$ . For other approaches, for instance, $Petri- Net[10]$ and $graph-rewr\dot{i}ting[11]$ ,we can adopt the same discussion to the causality.
.
We mention the recent truly-concurrent congruence$\mathrm{r}\mathrm{e}\mathrm{s}\mathrm{u}\mathrm{l}\mathrm{t}[9]$

122
6.1

Versus Locations

One agent is made by parallel composition of some sub-agents. A location is the information
which sub-agents an action occurred at. That is, the location is the “birthplace” of theaction. The location and location based semantics (location bisimulation) are proposed
to distinguish agents via the spatial distribution essentially.
On the other hand, actions whose locations are not related each other have possibility tobe performed concurrently. Thus, we can consider to describe the concurrent behavior of
can not be performed on.. urrently in general. Let
agents via locations. But suchus see this example:$\mathrm{c}$$\mathrm{a}\mathrm{c},\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{s}$$\mathrm{c}’$$def=$$(\nu z)(\overline{x}z.\overline{z})$$P_{1}$$def=$$Q_{1}$The location bisimulation distinguishes$(\nu z)(\overline{x}z|_{\overline{Z}})$$P_{1}$

and$Q_{1}$.

. Because$Q_{1}$

has a computation$Q_{1}-_{\iota\iota}\overline{x}(z)\overline{z}\prec 01$

only. In the sense of the concurrency
has a computation, but
does not.
“becausecan performaredistinguishedexplainandlocations,that
we canvia
and concurrently (the locations of these actions are not related) but)”. But, in fact,
performs these actions sequentially (the location is the prefix of
andperformand sequentially. We have no need to distinguishbothand. Another example is shown:$0$$P_{1}-_{\iota_{0}\iota_{0}}\overline{x}(z)\overline{z_{l_{1}}}\prec \mathrm{o}$$P_{1}$$P_{1}$$P_{1}$$Q_{1}$$Q_{1}$$P_{1}$$\overline{z}$$\mathrm{a}\mathrm{c}\mathrm{t}\mathrm{i}_{0}\mathrm{n}\overline{x}(z)$$l_{0}l_{1}$$l_{0}$$P_{1}$$Q_{1}$$\overline{X}(Z)$$P_{1}$$\overline{z}$$Q_{1}$$def=$$P_{2}$$Q_{2}$$def=$$a|b$$(\nu c)(a.\overline{c}|C.b)+(\nu c)(b.c|\overline{c}.a)$andbecause both of these agents can perform
The location bisimulation identifies
fact,
can not perform these actions concurrently.
action and concurrently. But, in
We should distinguish these agents. This miss-identification is more serious than the previous example. Because agent $x(b).P_{2}$ and $x(b).Q_{2}$ are no longer identified by the location
bisimulation. This shows that the location bisimulation is not closed under (input) prefixings.
In the multi-action bisimulation, these problems do not occur. The multi-action bisimTheseulation identifies
and . Because both of these agent can only
are distinguished. Becauseandare sequential agents. On the other hand, agents$a|b$
is a sequential
is,agent but
perform
is
a
but
can
not.
That
concurrent
canagent.
$P_{2}$$a$$b$$Q_{2}$$Q_{2}$$\mathrm{p}\mathrm{e}\Gamma \mathrm{f}_{0}\mathrm{r}\mathrm{m}-_{\mathrm{M}}^{z}\overline{x}()arrow^{\overline{z}}\mathrm{M}^{\cdot}$$Q_{1}$$P_{1}$$P_{2}$$Q_{2}$

6.2$P_{2}$$P_{2}$$Q_{2}$$Q_{2}$

Versus Causality

Causality is a set of dependencies between transitions. The causality is denoted by a labelled tree or a partial order introduced over transitions. By causality based semantics, weconsider that transitions those have no dependencies each other can be performed concurrently. For the agents appeared in Section 6.1, we can extract the following causalities

$($

123
dependencies) and concurrency.

rrency$\mathrm{a}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{S}\mathrm{i}\mathrm{t}\mathrm{i}_{0},\mathrm{n}\mathrm{s}\mathrm{d}\mathrm{e}\mathrm{p}\mathrm{e}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{n}_{\overline{Z}}\mathrm{c}\mathrm{i}\mathrm{e}\mathrm{s}\mathrm{C}\mathrm{o}\mathrm{n}.\mathrm{C}\mathrm{u}$$\overline{\overline{P_{1}P_{1}\frac{\overline{x}(z)_{\mathrm{c}}}{}\overline{z}arrow\overline{X}(z)\subseteq}}$$Q_{1}arrowarrow^{\overline{z}}\overline{x}(z)$$Q_{1}$$\overline{x}(z)\subseteq\overline{z}$$P_{2}$$Q_{2}$$P_{2}\underline{ab}$or$P_{2}\underline{ba}$$Q_{2}\underline{ab}$or$Q_{2}\underline{ba}$identity$a\subseteq b$or$a_{\wedge}^{\vee}b$$b\subseteq a$(where a dependency is denoted as a partial order over transitions and each transition isdisplayed by whose labels.
means that the transition labelled and.the transition
andorlabelled is concurrent. The dependencies ofoccur because restriction
prefixwork as sequentializers. ) Like this, the concurrency based on the causality issame to the concurrency based on multi-actions. We can use both semantics to capture
the concurrent behavior of agents. But the causality requires analysis of dependencies of
agents to do that. On the other hand, multi-actions can treat that directly. For example,
let us suppose agent $R^{def}=(a.b)|(c.d)$ . We can extract the dependencies and concurrency
from transitions of $R$ .
$a\wedge\vee b$

$a$

$b$

$Q_{1}$$(\nu z)$$Q_{2}$$c,\overline{c}$agent$(a.b)|(c.d)$concurrency

dependencies$a\subseteq b,$$c\subseteq d$$a_{\wedge}^{\vee}c,$$a_{\wedge}^{\vee}d,$$b_{\wedge}^{\vee}c,$$b_{\wedge}^{\vee}d$

The analysis of semantics is required to capture the following concurrent behavior of$Rarrowarrowarrow a|cbd,$$Raarrowarrow b|Cdarrow,$$Rarrow^{c}arrow a|darrow^{b},$$\cdots$

$R$

:

.

This analysis is not easy. On the other hand, multi-actions collect these transitions directly.

6.3

Versus Other Ruly-Concurrent Congruence Relation, it is shown that the weak causality semantics (weak causal bisimIn the recent
ulation) is a congruence relation in the -calculus with the slight syntactic restriction.
We can define weak ground multi-action bisimilarity by employing as the unit element. We can also define weak
. We call this commutative monoidof’ instead ofmulti-action congruence.
$\mathrm{p}\mathrm{a}\mathrm{p}\mathrm{e}\mathrm{r}[9]$$\pi$$\tau$$\emptyset$$M_{\mathrm{w}\mathrm{e}\mathrm{a}\mathrm{k}}$$M_{\mathrm{S}\mathrm{t}\circ}\mathrm{r}\mathrm{n}\mathrm{g}$7Conclusion

We extended -calculus to use the multi-actions as labels. The multi-action -calculus
can describe the concurrent behavior of agents and its transitions are characterized byconfluence. We proposed a new truly-concurrent semantics for -calculus, strong bisimilarity defined over multi-action -calculus. Strong bisimilarity defined over multi-action-calculus is closed under input-prefixings and parallel compositions.
In the future works, we propose the weak multi-action bisimilarity and congruence.
$\pi$

$\pi$

$\pi$

$\pi$

$\pi$

124

References[1] Robin Milner, Joachim Parrow, and David Walker. A Calculus of Mobile Processes,
Parts I and II. Information and Computation, 100:1-77, 1992.

[2] Robin Milner. Communication and Concurency. Prentice Hall, 1989.
[3] G. Boudol, I. Castellani, Matthew Hennessy, and A. Kiehn. A Theory of Processes
with Localities (Extended Abstract). In Proc. of 3rd CONCUR, volume 630 of LNCS.
Springer-Verlag, 1992.

[4] G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn. Observing localities. Theoretical
Comp uter Science, 114:31-61, 1993.
[5] Davide Sangiorgi. Locality and True-concurrency in calculi for mobile processes. In
Proc. of TACS, volume 789 of LNCS. Springer-Verlag, 1994.
[6] Pierpaolo Degano and Corrado Priami. Causality for Mobile Processes. In Proc. of
ICALP, 1995.

[7] Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality in the-calculus. ECS-LFCS-94297, Univ. of Edinburgh, 1994.
$\pi$[8] Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality in the-calculus. In Proc. of 12th STACS, volume 900 of LNCS. Springer-Verlag, 1995.
$\pi$[9] Michele Boreale and Davide Sangiorgi. Some Congruence Properties for -calculus
Bisimilarities. Technical Report RR-2870, INRIA, Sophia-Antipolis, 1996.
$\pi$[10] Nadia Busi and Roberto Gorrieri. A Petri Net Semantics for -calculus. In Proc. of
6th CONCUR, volume 962 of LNCS. Springer-Verlag, 1995.
$\pi$[11] Ugo Montanari and Marco Pistore. Concurrent Semantics for the -calculus. In Proc.
of MFPS, volume ENCS 1. Elsevier, 1995.
$\pi$[12] J.C.M. Baeten and J.A. Bergstra. Non Interleaving Process Algebra. In Proc. of 4th
CONCUR, volume 715 of LNCS. Springer-Verlag, 1993.