An Algebra of Actors Based on True Concurrency

TL;DR

This paper introduces an algebra of actors with a truly concurrent semantics, extending the existing asynchronous $ extrm{A} ext{-} extrm{pi}$ calculus to better model concurrency properties.

Contribution

It develops $ extrm{A} ext{-} extrm{pi}_{tc}$, an extension of $ extrm{A} ext{-} extrm{pi}$, incorporating truly concurrent semantics with new syntax, semantics, and algebraic laws.

Findings

Defines syntax and operational semantics of $ extrm{A} ext{-} extrm{pi}_{tc}$

Provides a truly concurrent semantics model for the algebra

Establishes algebraic laws for the new calculus

Abstract

An algebra of actors $\textrm{A}\pi$ fully captures the properties of actors based on asynchronous $\pi$-calculus, but, it is based on the interleaving bisimulation semantics. We adjust $\textrm{A}\pi$ to $\textrm{A}\pi_{tc}$ to make $\textrm{A}\pi$ having a truly concurrent semantics. We give the syntax and operational semantics of $\textrm{A}\pi_{tc}$, and also the truly concurrent semantics model and algebraic laws of $\textrm{A}\pi_{tc}$.

Tables

Table 1. Table 1 : Type rules of A ​ π t ​ c A subscript 𝜋 𝑡 𝑐 \textrm{A}\pi_{tc}

$\text{NIL}\varnothing ;\left\{\right\}⊢\text{0}\text{MSG}\varnothing ;\left\{\right\}⊢\overline{x}y$

Table 2. Table 2 : Transition rules of A ​ π t ​ c A subscript 𝜋 𝑡 𝑐 \textrm{A}\pi_{tc}

$\text{INP}\frac{}{x\left(y\right).P\stackrel{xz}{\to }P\left\{z/y\right\}}\text{OUT}\frac{}{\overline{x}y.P\stackrel{\overline{x}y}{\to }P}$

Table 3. Table 3: Algebraic laws of A ​ π t ​ c A subscript 𝜋 𝑡 𝑐 \textrm{A}\pi_{tc}

$\text{A1}G+G=G\text{A2}G+\text{0}=G$

Equations

$$P::=B⟨\tilde{x};\tilde{y}⟩|\text{0}|\overline{x}y|x(y).P|(\nu x)P|\text{case }x\text{ of }(y_1:P_1,\cdots ,y_n:P_n)|P\mid P.$$

$$B⟨\tilde{x};\tilde{y}⟩\stackrel{\text{def}}{=}(\tilde{x};\tilde{y})x_1(z).P$$

$$\text{ACT}\frac{\rho ;f⊢P}{\{x\}\cup \hat{z};ch(x,\hat{z})⊢x(y).P}\text{ if }\rho -\{x\}=\hat{z},y\notin \rho ,f=ch(x,\hat{z})\text{ if }x\in \rho ;f=ch(ϵ,\hat{z})\text{ otherwise }$$

$$\text{CASE}\frac{\forall 1\le i\le n,{\rho }_i;f_i⊢P_i}{({\cup }_i{\rho }_i);(f_1\oplus \cdots \oplus f_n)⊢\text{ case }x\text{ of }(y_1:P_1,\cdots ,y_n:P_n)}\text{ if }{f}_i\text{ are mutually compatible}$$

$$\text{COMP}\frac{{\rho }_1;f_1⊢P_1{\rho }_2;f_2⊢P_2}{{\rho }_1\cup {\rho }_2;f_1\oplus f_2⊢P_1\mid P_2}\text{ if }{\rho }_1\cap {\rho }_2=\varnothing$$

$$\text{RES}\frac{\rho ;f⊢P}{\rho -\{x\};f|(\rho -\{x\})⊢(\nu x)P}$$

$$\text{INST}\{\tilde{x}\};ch(\tilde{x})⊢B⟨\tilde{x};\tilde{y}⟩\text{ if }len(\tilde{x})=2\text{ implies }{x}_1\ne x_2$$

$$\text{BINP}\frac{P\stackrel{xy}{\to }{P}^{\prime }}{P\stackrel{x(y)}{\to }{P}^{\prime }}(y\notin fn(P))\text{RES}\frac{P\stackrel{\alpha }{\to }{P}^{\prime }}{(\nu y)P\stackrel{\alpha }{\to }(\nu y)P^{\prime }}(y\notin n(\alpha ))$$

$$\text{OPEN}\frac{P\stackrel{\overline{x}y}{\to }{P}^{\prime }}{(\nu y)P\stackrel{\overline{x}(y)}{\to }{P}^{\prime }}(x\ne y)$$

$${\text{PAR}}_1\frac{P\stackrel{\alpha }{\to }{P}^{\prime }Q\nrightarrow }{P\mid Q\stackrel{\alpha }{\to }{P}^{\prime }\mid Q}(bn(\alpha )\cap fn(Q)=\varnothing ){\text{PAR}}_2\frac{Q\stackrel{\alpha }{\to }{Q}^{\prime }P\nrightarrow }{P\mid Q\stackrel{\alpha }{\to }P\mid Q^{\prime }}(bn(\alpha )\cap fn(P)=\varnothing )$$

$${\text{PAR}}_3\frac{P\stackrel{\alpha }{\to }{P}^{\prime }Q\stackrel{\beta }{\to }{Q}^{\prime }}{P\mid Q\stackrel{\{\alpha ,\beta \}}{\to }{P}^{\prime }\mid Q^{\prime }}(\beta \ne \overline{\alpha },bn(\alpha )\cap bn(\beta )=\varnothing ,bn(\alpha )\cap fn(Q)=\varnothing ,bn(\beta )\cap fn(P)=\varnothing )$$

$${\text{PAR}}_4\frac{P\stackrel{x_1(z)}{\to }{P}^{\prime }Q\stackrel{x_2(z)}{\to }{Q}^{\prime }}{P\mid Q\stackrel{\{x_1(w),x_2(w)\}}{\to }{P}^{\prime }\{w/z\}\mid Q^{\prime }\{w/z\}}(w\notin fn((z)P)\cup fn((z)Q))$$

$$\text{COM}\frac{P\stackrel{\overline{x}y}{\to }{P}^{\prime }Q\stackrel{xy}{\to }{Q}^{\prime }}{P\mid Q\stackrel{\tau }{\to }{P}^{\prime }\mid Q^{\prime }}$$

$$\text{CLOSE}\frac{P\stackrel{\overline{x}(y)}{\to }{P}^{\prime }Q\stackrel{xy}{\to }{Q}^{\prime }}{P\mid Q\stackrel{\tau }{\to }(\nu y)(P^{\prime }\mid Q^{\prime })}(y\notin fn(Q))$$

$$\text{BEHV}\frac{x_1(z).P\{(\tilde{u},\tilde{v})/(\tilde{x},\tilde{y})\}\stackrel{\alpha }{\to }{P}^{\prime }}{B⟨\tilde{u};\tilde{v}⟩\stackrel{\alpha }{\to }{P}^{\prime }}(B⟨\tilde{x};\tilde{y}⟩\stackrel{\text{def}}{=}(\tilde{x};\tilde{y})x_1(z).P)$$

$$\text{BRNCH}\frac{}{\text{case }x\text{ of }(y_1:P_1,\cdots ,y_n:P_n)\stackrel{\tau }{\to }{P}_i}(\text{if }x=y_i)$$

$$(\nu x)(x(u).P\mid \overline{x}x\mid \overline{y}x)\stackrel{\{x(u),\overline{x}x,\overline{y}x\}}{\to }P$$

$$Diverge⟨x⟩\mid \overline{x}u\mid y(v).\overline{v}v\mid \overline{y}v$$

$$\{(C_1,f,C_2)|C_1\in \mathcal{C}({\mathcal{E}}_1),C_2\in \mathcal{C}({\mathcal{E}}_2),f:C_1\to C_2\text{ isomorphism}\}.$$

$$\text{A3}P\mid \text{0}=P\text{A4}P\mid Q=Q\mid P\text{A5}(P\mid Q)\mid R=P\mid (Q\mid R)$$

$$\text{A6}(\nu x)(\sum _{i\in I}{P}_i)=\sum _{i\in I}(\nu x)P_i$$

$$\text{A7}(\nu x)(P\mid Q)=P\mid (\nu x)Q(x\notin n(P))$$

$$\text{A8}(\nu x)(\overline{x}y\mid \alpha .P)=\alpha .(\nu x)(\overline{x}y\mid P)(x\notin n(\alpha ))$$

$$\text{A9}(\nu x)(\overline{x}y\mid x(z).P)=(\nu x)(P\{y/z\})$$

$$\text{A10}(\nu x)(y(z).P)=y(z).(\nu x)P(x\ne y,x\ne z)$$

$$\text{A11}\overline{x}y\mid \sum _{i\in I}{P}_i=\sum _{i\in I}(\overline{x}y\mid P_i)(I\ne \varnothing )$$

$$\text{A12}\alpha .\sum _{i\in I}{P}_i=\sum _{i\in I}\alpha .P_i(I\ne \varnothing )$$

$$\text{A13}P=\sum P$$

$$\text{A14}\overline{u}v\mid (x(y).P)=(\overline{u}v\mid x(y)).P(y\ne u,y\ne v)$$

$$\text{A15}(\overline{u}v.P)\mid x(y)=(\overline{u}v\mid x(y)).P(y\ne u,y\ne v)$$

Full text

1 Introduction

There are lots of work on true concurrency, including structures for true concurrency [5] [6] [7], truly concurrent bisimilarities such as pomset bisimilarity, step bisimilarity, history-preserving (hp-)bisimilarity and the finest hereditary history-preserving (hhp-)bisimilarity [8] [9]. And also several kinds of logics for true concurrency were presented, such as a logic with reverse modalities [10] [11], SFL logic [12], a uniform logic for true concurrency [13] [14] and a logic for weakly true concurrency [15]. We also done several work on process algebra for true concurrency, including a calculus for true concurrency CTC [17], algebraic laws for true concurrency APTC [16] and a calculus of truly concurrent mobile processes $\pi_{tc}$.

On the other hand, the actor computational model is a well-known truly concurrent computational model [1] [2] [3] [4]. An algebra of actors $\textrm{A}\pi$ [4] fully captures the properties of actors based on asynchronous $\pi$-calculus [19] [20], but, it is based on the interleaving bisimulation semantics. In this paper, we adjust $\textrm{A}\pi$ to $\textrm{A}\pi_{tc}$ to make $\textrm{A}\pi_{tc}$ having a truly concurrent semantics.

This paper is organized as follows. In section 2, we briefly introduce the actor computational model. Then we introduce the syntax and operational semantics of $\textrm{A}\pi_{tc}$ in section 3. In section 4.1, we make $\textrm{A}\pi_{tc}$ to have a truly concurrent semantics. Finally, in section 5, we conclude this paper.

2 Actor Model

An actor is a concurrent object that encapsulates a set of states, a control thread and a set of local computations. It has a unique mail address and maintains a mail box to accept messages sent by other actors. Actors do local computations by means of processing the messages stored in the mail box sequentially and block when their mail boxes are empty. During processing a message in mail box, an actor may perform three candidate actions:

Send action sends messages asynchronously to other actors by their mail box addresses; 2. 2.

Create action creates new actors with new behaviors; 3. 3.

Ready action makes the actor ready to process the next message from the mail box or block if the mail box is empty.

The illustration of an actor model as shows in Fig.1 which is first shown in [1].

Actors have the following three properties:

Uniqueness: each actor has a unique name; 2. 2.

Freshness: actors cannot be created with well-known names or names received in a message; 3. 3.

Persistence: actors are persistent, they do not disappear after processing a message.

Professor Gul Agha have done significant work on actors [2] [3] [4], in which, $\textrm{A}\pi$ [4] is an algebra of actors that implements the above full properties of actors based on $\pi$-calculus [19] [20].

3 Syntax and Operational Semantics

We assume an infinite set $\mathcal{N}$ of (action or event) names, and use $a,b,c,\cdots$ to range over $\mathcal{N}$, use $x,y,z,w,u,v$ as meta-variables over names. We denote by $\overline{\mathcal{N}}$ the set of co-names and let $\overline{a},\overline{b},\overline{c},\cdots$ range over $\overline{\mathcal{N}}$. Then we set $\mathcal{L}=\mathcal{N}\cup\overline{\mathcal{N}}$ as the set of labels, and use $l,\overline{l}$ to range over $\mathcal{L}$. We extend complementation to $\mathcal{L}$ such that $\overline{\overline{a}}=a$. Let $\tau$ denote the silent step (internal action or event) and define $Act=\mathcal{L}\cup\{\tau\}$ to be the set of actions, $\alpha,\beta$ range over $Act$. And $K,L$ are used to stand for subsets of $\mathcal{L}$ and $\overline{L}$ is used for the set of complements of labels in $L$.

We write $\mathcal{P}$ for the set of configurations. Let $\widetilde{x}=x_{1},\cdots,x_{ar(A)}$ and $\widetilde{y}=y_{1},\cdots,y_{ar(A)}$ be tuples of distinct name variables, then $B\langle\widetilde{x};\widetilde{y}\rangle$ is called a configuration constant. Let the variable $\hat{z}$ range over $\{\emptyset,\{z\}\}$. The symbol $\widetilde{x},\widetilde{y}$ denotes the result of appending $\widetilde{y}$ to $\widetilde{x}$. The symbol $\widetilde{x},\hat{z}$ means that $\widetilde{x},z$ if $\hat{z}=\{z\}$; $\widetilde{x}$ otherwise. While $(\nu\hat{z})P$ means that $(\nu z)P$ if $\hat{z}=\{z\}$; $P$ otherwise. The symbol $\equiv_{\alpha}$ denotes equality under standard alpha-convertibility, note that the subscript $\alpha$ has no relation to the action $\alpha$.

Following $\textrm{A}\pi$ [4], we retype the syntax and semantics of $\textrm{A}\pi_{tc}$, and adjust them to be suitable for true concurrency as follows.

3.1 Syntax

We give the syntax of $\textrm{A}\pi_{tc}$ as follows.

Definition 3.1** (Syntax)**

A truly concurrent configuration $P$ in $\textrm{A}\pi_{tc}$ is defined inductively by the following formation rules:

$B\langle\widetilde{x};\widetilde{y}\rangle\in\mathcal{P}$; 2. 2.

$\textbf{0}\in\mathcal{P}$; 3. 3.

the Output $\overline{x}y\in\mathcal{P}$, for $x,y\in Act$; 4. 4.

if $P\in\mathcal{P}$, then the Input $x(y).P\in\mathcal{P}$, for $x,y\in Act$; 5. 5.

if $P\in\mathcal{P}$, then the Restriction $(\nu x)P\in\mathcal{P}$, for $x\in Act$; 6. 6.

if $P_{1},\cdots,P_{n}\in\mathcal{P}$, then $\textrm{case }x\textrm{ of }(y_{1}:P_{1},\cdots,y_{n}:P_{n})\in\mathcal{P}$; 7. 7.

if $P,Q\in\mathcal{P}$, then the Composition $P\mid Q\in\mathcal{P}$;

The standard BNF grammar of syntax of $\textrm{A}\pi_{tc}$ can be summarized as follows:

[TABLE]

For each behavior instantiation $B\langle\widetilde{x};\widetilde{y}\rangle$, a defining equation of the form

[TABLE]

is assumed, where $P$ is a configuration.

The intuitions of the above constructs for actors, please refer to $\textrm{A}\pi$ [4], we do not explain any more.

Definition 3.2** (Free variables)**

The free names of a configuration $P$, $fn(P)$, are defined as follows.

$fn(B\langle\widetilde{x};\widetilde{y}\rangle)\subseteq\{\widetilde{x}\}\cup\{\widetilde{y}\}$; 2. 2.

$fn(\textbf{0})=\emptyset$; 3. 3.

$fn(\overline{x}y.P)=fn(P)\cup\{x\}\cup\{y\}$; 4. 4.

$fn(x(y).P)=fn(P)\cup\{x\}-\{y\}$; 5. 5.

$fn((\nu x)P)=fn(P)-\{x\}$; 6. 6.

$fn(\textrm{case }x\textrm{ of }(y_{1}:P_{1},\cdots,y_{n}:P_{n}))=fn(P_{1})\cup\cdots\cup fn(P_{n})$; 7. 7.

$fn(P_{1}\mid P_{2})=fn(P_{1})\cup fn(P_{2})$.

Definition 3.3** (Bound variables)**

Let $n(P)$ be the names of a configuration $P$, then the bound names $bn(P)=n(P)-fn(P)$.

In $\overline{x}y$, $x(y)$ and $\overline{x}(y)$, $x$ is called the subject, $y$ is called the object and it may be free or bound.

Definition 3.4** (Substitutions)**

A substitution is a function $\sigma:\mathcal{N}\rightarrow\mathcal{N}$. For $x_{i}\sigma=y_{i}$ with $1\leq i\leq n$, we write $\{y_{1}/x_{1},\cdots,y_{n}/x_{n}\}$ or $\{\widetilde{y}/\widetilde{x}\}$ for $\sigma$. For a configuration $P\in\mathcal{P}$, $P\sigma$ is defined inductively as follows:

if $P$ is a configuration constant $B\langle\widetilde{x};\widetilde{y}\rangle=B\langle x_{1},\cdots,x_{n};y_{1},\cdots,y_{m}\rangle$, then $P\sigma=B\langle x_{1}\sigma,\cdots,x_{n}\sigma;y_{1}\sigma,\cdots,y_{m}\sigma\rangle$; 2. 2.

if $P=\textbf{0}$, then $P\sigma=\textbf{0}$; 3. 3.

if $P=\overline{x}y.P^{\prime}$, then $P\sigma=\overline{x\sigma}y\sigma.P^{\prime}\sigma$; 4. 4.

if $P=x(y).P^{\prime}$, then $P\sigma=x\sigma(y).P^{\prime}\sigma$; 5. 5.

if $P=(\nu x)P^{\prime}$, then $P\sigma=(\nu x\sigma)P^{\prime}\sigma$; 6. 6.

if $P=\textrm{case }x\textrm{ of }(y_{1}:P_{1},\cdots,y_{n}:P_{n})$, then $P\sigma=\textrm{case }x\sigma\textrm{ of }(y_{1}\sigma:P_{1}\sigma,\cdots,y_{n}\sigma:P_{n}\sigma)$; 7. 7.

if $P=P_{1}\mid P_{2}$, then $P\sigma=P_{1}\sigma\mid P_{2}\sigma$.

3.2 Type System

According to the actor model, as in $\textrm{A}\pi$, actor names have uniqueness and freshness properties, and the persistence property is relaxed by permitting a sink behavior. To assure such properties, as in $\textrm{A}\pi$, a type system is presented as follows.

As in [4], $\bot,*\notin\mathcal{N}$, for $X\subset\mathcal{N}$, $X^{*}=X\cup\{\bot,*\}$; for $f:X\rightarrow X^{*}$, $f^{*}:X^{*}\rightarrow X^{*}$ is defined as $f^{*}(x)=f(x)$ if $x\in X$, and $f^{*}(\bot)=f^{*}(*)=\bot$. $\rho;f\vdash P$ is a typing judgement, where $\rho$ is the receptionist set of $P$, and $f:\rho\rightarrow\rho^{*}$ is a temporary name mapping function that relates actors in $P$ to the temporary names they have currently assumed. $f$, $f^{*}$, $f_{1}\oplus f_{2}$, $f|\rho$, $ch(\widetilde{x})$ have the same definitions and properties as those in [4].

Definition 3.5** (Type system)**

The type system is consist of type rules that is the same as $\textrm{A}\pi$, we retype them in Table 1.

The following theorem still holds, we retype it from $\textrm{A}\pi$.

Theorem 3.6

If $\rho;f\vdash P$ then $\rho\subset fn(P)$, and for all $x,y\in\rho$, $f(x)\neq x$, $f^{*}(f(x))=\bot$, and $f(x)=f(y)\notin\{\bot,*\}$ implies $x=y$. Furthermore, if $\rho^{\prime};f^{\prime}\vdash P$ then $\rho=\rho^{\prime}$ and $f=f^{\prime}$.

Since arbitrary substitution $\sigma$ on a configuration $P$ may destroy the uniqueness, freshness or persistence properties and cause $P$ to be an invalid $\textrm{A}\pi_{tc}$ term, we often assume that $\sigma$ is an one-to-one mapping. The following lemma also holds as in $\textrm{A}\pi$.

The following lemma says that the type system respects $\equiv_{\alpha}$.

Lemma 3.7

If $\rho;f\vdash P$ and $\sigma$ is one-to-one on $\rho$, then $\sigma(\rho);f\sigma\vdash P\sigma$.

3.3 Operational Semantics

The operational semantics is defined by LTSs (labelled transition systems), and it is detailed by the following definition.

Definition 3.8** (Semantics)**

The operational semantics of $\textrm{A}\pi_{tc}$ corresponding to the syntax in Definition 3.1 is defined by a series of transition rules, they are shown in Table 2. Note that, these rules are adjusted to a truly concurrent version.

The intuitions of transition rules in Table 2 for the actor computational model are the same as those of $\textrm{A}\pi$, the differences are that the PAR rule is replaced by four rules $\textbf{PAR}_{1}$–$\textbf{PAR}_{4}$. The rules $\textbf{PAR}_{1}$–$\textbf{PAR}_{4}$ capture the truly concurrent semantics.

The following theorem still hold for transition rules in Table 2, which says the well-typed terms are closed under transitions.

Theorem 3.9

(1)If $P$ is well-typed and $P\xrightarrow{\alpha}P^{\prime}$ then $P^{\prime}$ is well-typed;

(2)If $P$ is well-typed and $P\xrightarrow{\{\alpha_{1},\cdots,\alpha_{n}\}}P^{\prime}$ then $P^{\prime}$ is well-typed.

As in $\textrm{A}\pi$, not every trace produced by the transition system in Table 2 corresponds to an actor computation. We have the following instance,

[TABLE]

by the transition system in Table 2. But the above transition does not correspond to an actor computation, since there cannot be an actor named $x$ in the environment. Similarly, we also need the notation of $\rho$-well-formed trace with $\rho$ as an initial receptionist set, we retype it and adjust it to truly concurrent semantics as follows.

Definition 3.10

For a set of names $\rho$ and trace $s$, $rcp(\rho,s)$ is inductively defined as follows:

$rcp(\rho,\epsilon)=\rho$; 2. 2.

$rcp(\rho,s.(\hat{y_{1}})\cdots(\hat{y_{n}})(x_{1}y_{1}\mid\cdots\mid x_{n}y_{n}))=rcp(\rho,s)$; 3. 3.

$rcp(\rho,s.(\hat{y_{1}})\cdots(\hat{y_{n}})(\overline{x_{1}}y_{1}\mid\cdots\mid\overline{x_{n}}y_{n}))=rcp(\rho,s)\cup\hat{y_{1}}\cup\cdots\cup\hat{y_{n}}$.

We say $s$ is $\rho$-well-formed if $s=s_{1}.(\hat{y_{1}})\cdots(\hat{y_{n}})(\overline{x_{1}}y_{1})\mid\cdots\mid\overline{x_{n}}y_{n}.s_{2}$ implies $x_{1}\notin rcp(\rho,s_{1}),\cdots,x_{n}\notin rcp(\rho,s_{1})$, and $s$ is well-formed if it is $\emptyset$-well-formed.

Let $\Rightarrow$ denote the reflexive transitive closure of $\xrightarrow{\tau}$, $\xRightarrow{\alpha}$ denote $\Rightarrow\xrightarrow{\alpha}\Rightarrow$, and $P\xRightarrow{s}$ denote $P\xRightarrow{s}P^{\prime}$ for some $P^{\prime}$. Then, the following lemma still hold for truly concurrent semantics.

Lemma 3.11

Let $P\mid Q$ be a well-typed $\textrm{A}\pi_{tc}$ term with $rcp(P)=\rho_{1}$ and $rcp(Q)=\rho_{2}$. Then $P\mid Q\Rightarrow$ can be unzipped into $P\xRightarrow{s}$ and $Q\xRightarrow{\overline{s}}$ such that $s$ is $\rho_{1}$-well-formed and $\overline{s}$ is $\rho_{2}$-well-formed.

Similarly, in $\rho$-well-formed traces, we only consider the following traces $s$ such that if $s=s_{1}.(\alpha_{1}\mid\cdots\mid\alpha_{n}).s_{2}$, where $(\rho\cup n(s_{1})\cup fn(\alpha_{1})\cup\cdots\cup fn(\alpha_{n}))\cap bn((\alpha_{1}\mid\cdots\mid\alpha_{n}).s_{2})=\emptyset$.

The transition sequences are also further constrained by a fairness requirement. Different to $\textrm{A}\pi$, the following transition sequences are fair in $\textrm{A}\pi_{tc}$.

[TABLE]

where $Diverge\langle x\rangle\overset{\text{def}}{=}(x)x(u).(\overline{x}u\mid Diverge\langle x\rangle)$. We see that all messages are delivered eventually.

4 A Theory of True Concurrency for $\textrm{A}\pi_{tc}$

4.1 True Concurrency

Firstly, in this subsection, the related concepts on true concurrency are defined based on the following concepts [5] [6] [7].

Definition 4.1** (Prime event structure)**

Let $\Lambda$ be a fixed set of labels, ranged over $a,b,c,\cdots$. A ($\Lambda$-labelled) prime event structure is a tuple $\mathcal{E}=\langle\mathbb{E},\leq,\sharp,\lambda\rangle$, where $\mathbb{E}$ is a denumerable set of events. Let $\lambda:\mathbb{E}\rightarrow\Lambda$ be a labelling function. And $\leq$, $\sharp$ are binary relations on $\mathbb{E}$, called causality and conflict respectively, such that:

$\leq$* is a partial order and $\lceil e\rceil=\{e^{\prime}\in\mathbb{E}|e^{\prime}\leq e\}$ is finite for all $e\in\mathbb{E}$.* 2. 2.

$\sharp$* is irreflexive, symmetric and hereditary with respect to $\leq$, that is, for all $e,e^{\prime},e^{\prime\prime}\in\mathbb{E}$, if $e\sharp e^{\prime}\leq e^{\prime\prime}$, then $e\sharp e^{\prime\prime}$.*

Then, the concepts of consistency and concurrency can be drawn from the above definition:

$e,e^{\prime}\in\mathbb{E}$* are consistent, denoted as $e\frown e^{\prime}$, if $\neg(e\sharp e^{\prime})$. A subset $X\subseteq\mathbb{E}$ is called consistent, if $e\frown e^{\prime}$ for all $e,e^{\prime}\in X$.* 2. 2.

$e,e^{\prime}\in\mathbb{E}$* are concurrent, denoted as $e\parallel e^{\prime}$, if $\neg(e\leq e^{\prime})$, $\neg(e^{\prime}\leq e)$, and $\neg(e\sharp e^{\prime})$.*

Definition 4.2** (Configuration)**

Let $\mathcal{E}$ be a PES. A (finite) configuration in $\mathcal{E}$ is a (finite) consistent subset of events $C\subseteq\mathcal{E}$, closed with respect to causality (i.e. $\lceil C\rceil=C$). The set of finite configurations of $\mathcal{E}$ is denoted by $\mathcal{C}(\mathcal{E})$.

Usually, truly concurrent behavioral equivalences are defined by events $e\in\mathcal{E}$ and prime event structure $\mathcal{E}$, in contrast to interleaving behavioral equivalences by actions $a,b\in\mathcal{P}$ and process (graph) $\mathcal{P}$. Indeed, they have correspondences, in [12], models of concurrency, including Petri nets, transition systems and event structures, are unified in a uniform representation – TSI (Transition System with Independence).

If $x$ is a process, let $C(x)$ denote the corresponding configuration (the already executed part of the process $x$, of course, it is free of conflicts), when $x\xrightarrow{e}x^{\prime}$, the corresponding configuration $C(x)\xrightarrow{e}C(x^{\prime})$ with $C(x^{\prime})=C(x)\cup\{e\}$, where $e$ may be caused by some events in $C(x)$ and concurrent with the other events in $C(x)$, or entirely concurrent with all events in $C(x)$, or entirely caused by all events in $C(x)$. With a little abuse of concepts, in the following of the paper, we will not distinguish actions and events, prime event structures and processes, also concurrent behavior equivalences based on configurations and processes, and use them freely, unless they have specific meanings.

Next, we introduce concepts of truly concurrent bisimilarities, including pomset bisimilarity, step bisimilarity, history-preserving (hp-)bisimilarity and hereditary history-preserving (hhp-)bisimilarity. In contrast to traditional truly concurrent bisimilarities in CTC [17] and APTC [16], these versions in $\textrm{A}\pi_{tc}$ not only must take care of actions with bound objects, but also must suit for the constraints of the type system. That is, the truly concurrent bisimilarities are tagged with a parameter $\rho$. Note that, here, a PES $\mathcal{E}$ is deemed as a configuration.

Definition 4.3** (Pomset transitions and step)**

Let $\mathcal{E}$ be a PES and let $C\in\mathcal{C}(\mathcal{E})$, and $\emptyset\neq X\subseteq\mathbb{E}$, if $C\cap X=\emptyset$ and $C^{\prime}=C\cup X\in\mathcal{C}(\mathcal{E})$, then $C\xrightarrow{X}C^{\prime}$ is called a pomset transition from $C$ to $C^{\prime}$. When the events in $X$ are pairwise concurrent, we say that $C\xrightarrow{X}C^{\prime}$ is a step.

Definition 4.4** (Pomset, step bisimilarity)**

Let $\mathcal{E}_{1}$, $\mathcal{E}_{2}$ be PESs. A pomset bisimulation is a relation $R\subseteq\mathcal{C}(\mathcal{E}_{1})\times\mathcal{C}(\mathcal{E}_{2})$, such that if $(C_{1},C_{2})\in R$ with $rcp(C_{1})=rcp(C_{2})$, and $C_{1}\xrightarrow{X_{1}}C_{1}^{\prime}$ (with $\mathcal{E}_{1}\xrightarrow{X_{1}}\mathcal{E}_{1}^{\prime}$) then $C_{2}\xrightarrow{X_{2}}C_{2}^{\prime}$ (with $\mathcal{E}_{2}\xrightarrow{X_{2}}\mathcal{E}_{2}^{\prime}$), with $X_{1}\subseteq\mathbb{E}_{1}$, $X_{2}\subseteq\mathbb{E}_{2}$, $X_{1}\sim X_{2}$, $rcp(C_{1}^{\prime})=rcp(C_{2}^{\prime})$ and $(C_{1}^{\prime},C_{2}^{\prime})\in R$:

for each fresh action $\alpha\in X_{1}$, if $C_{1}^{\prime\prime}\xrightarrow{\alpha}C_{1}^{\prime\prime\prime}$ (with $\mathcal{E}_{1}^{\prime\prime}\xrightarrow{\alpha}\mathcal{E}_{1}^{\prime\prime\prime}$), then for some $C_{2}^{\prime\prime}$ and $C_{2}^{\prime\prime\prime}$, $C_{2}^{\prime\prime}\xrightarrow{\alpha}C_{2}^{\prime\prime\prime}$ (with $\mathcal{E}_{2}^{\prime\prime}\xrightarrow{\alpha}\mathcal{E}_{2}^{\prime\prime\prime}$), such that if $(C_{1}^{\prime\prime},C_{2}^{\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime})=rcp(C_{2}^{\prime\prime})$ then $(C_{1}^{\prime\prime\prime},C_{2}^{\prime\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime\prime})=rcp(C_{2}^{\prime\prime\prime})$; 2. 2.

for each $x(y)\in X_{1}$ with ($y\notin n(\mathcal{E}_{1},\mathcal{E}_{2})$), if $C_{1}^{\prime\prime}\xrightarrow{x(y)}C_{1}^{\prime\prime\prime}$ (with $\mathcal{E}_{1}^{\prime\prime}\xrightarrow{x(y)}\mathcal{E}_{1}^{\prime\prime\prime}\{w/y\}$) for all $w$, then for some $C_{2}^{\prime\prime}$ and $C_{2}^{\prime\prime\prime}$, $C_{2}^{\prime\prime}\xrightarrow{x(y)}C_{2}^{\prime\prime\prime}$ (with $\mathcal{E}_{2}^{\prime\prime}\xrightarrow{x(y)}\mathcal{E}_{2}^{\prime\prime\prime}\{w/y\}$) for all $w$, such that if $(C_{1}^{\prime\prime},C_{2}^{\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime})=rcp(C_{2}^{\prime\prime})$ then $(C_{1}^{\prime\prime\prime},C_{2}^{\prime\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime\prime})=rcp(C_{2}^{\prime\prime\prime})$; 3. 3.

for each two $x_{1}(y),x_{2}(y)\in X_{1}$ with ($y\notin n(\mathcal{E}_{1},\mathcal{E}_{2})$), if $C_{1}^{\prime\prime}\xrightarrow{\{x_{1}(y),x_{2}(y)\}}C_{1}^{\prime\prime\prime}$ (with $\mathcal{E}_{1}^{\prime\prime}\xrightarrow{\{x_{1}(y),x_{2}(y)\}}\mathcal{E}_{1}^{\prime\prime\prime}\{w/y\}$) for all $w$, then for some $C_{2}^{\prime\prime}$ and $C_{2}^{\prime\prime\prime}$, $C_{2}^{\prime\prime}\xrightarrow{\{x_{1}(y),x_{2}(y)\}}C_{2}^{\prime\prime\prime}$ (with $\mathcal{E}_{2}^{\prime\prime}\xrightarrow{\{x_{1}(y),x_{2}(y)\}}\mathcal{E}_{2}^{\prime\prime\prime}\{w/y\}$) for all $w$, such that if $(C_{1}^{\prime\prime},C_{2}^{\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime})=rcp(C_{2}^{\prime\prime})$ then $(C_{1}^{\prime\prime\prime},C_{2}^{\prime\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime\prime})=rcp(C_{2}^{\prime\prime\prime})$; 4. 4.

for each $\overline{x}(y)\in X_{1}$ with $y\notin n(\mathcal{E}_{1},\mathcal{E}_{2})$ and $x\notin rcp(C_{1}^{\prime\prime})\cup rcp(C_{2}^{\prime\prime})$, if $C_{1}^{\prime\prime}\xrightarrow{\overline{x}(y)}C_{1}^{\prime\prime\prime}$ (with $\mathcal{E}_{1}^{\prime\prime}\xrightarrow{\overline{x}(y)}\mathcal{E}_{1}^{\prime\prime\prime}$), then for some $C_{2}^{\prime\prime}$ and $C_{2}^{\prime\prime\prime}$, $C_{2}^{\prime\prime}\xrightarrow{\overline{x}(y)}C_{2}^{\prime\prime\prime}$ (with $\mathcal{E}_{2}^{\prime\prime}\xrightarrow{\overline{x}(y)}\mathcal{E}_{2}^{\prime\prime\prime}$), such that if $(C_{1}^{\prime\prime},C_{2}^{\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime})=rcp(C_{2}^{\prime\prime})$ then $(C_{1}^{\prime\prime\prime},C_{2}^{\prime\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime\prime})=rcp(C_{2}^{\prime\prime\prime})$; 5. 5.

for each $\overline{x}(y)\in X_{1}$ with $y\notin n(\mathcal{E}_{1},\mathcal{E}_{2})$ and $x\in rcp(C_{1}^{\prime\prime})=rcp(C_{2}^{\prime\prime})$, if $C_{1}^{\prime\prime}\xrightarrow{\overline{x}(y)}C_{1}^{\prime\prime\prime}$ (with $\mathcal{E}_{1}^{\prime\prime}\xrightarrow{\overline{x}(y)}\mathcal{E}_{1}^{\prime\prime\prime}$), then for some $C_{2}^{\prime\prime}$ and $C_{2}^{\prime\prime\prime}$, either $C_{2}^{\prime\prime}\xrightarrow{\overline{x}(y)}C_{2}^{\prime\prime\prime}$ (with $\mathcal{E}_{2}^{\prime\prime}\xrightarrow{\overline{x}(y)}\mathcal{E}_{2}^{\prime\prime\prime}$), or $C_{2}^{\prime\prime}\Rightarrow C_{2}^{\prime\prime\prime}$ (with $\mathcal{E}_{2}^{\prime\prime}\Rightarrow\mathcal{E}_{2}^{\prime\prime\prime}$), such that if $(C_{1}^{\prime\prime},C_{2}^{\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime})=rcp(C_{2}^{\prime\prime})$ then $(C_{1}^{\prime\prime\prime},C_{2}^{\prime\prime\prime})\in R$ with $rcp(C_{1}^{\prime\prime\prime})=rcp(C_{2}^{\prime\prime\prime})$.

and vice-versa.

We say that $\mathcal{E}_{1}$, $\mathcal{E}_{2}$ are pomset bisimilar, written $\mathcal{E}_{1}\sim_{p}\mathcal{E}_{2}$, if there exists a pomset bisimulation $R$, such that $(\emptyset,\emptyset)\in R$. By replacing pomset transitions with steps, we can get the definition of step bisimulation. When PESs $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ are step bisimilar, we write $\mathcal{E}_{1}\sim_{s}\mathcal{E}_{2}$.

Definition 4.5** (Posetal product)**

Given two PESs $\mathcal{E}_{1}$, $\mathcal{E}_{2}$, the posetal product of their configurations, denoted $\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$, is defined as

[TABLE]

A subset $R\subseteq\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$ is called a posetal relation. We say that $R$ is downward closed when for any $(C_{1},f,C_{2}),(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})\in\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$, if $(C_{1},f,C_{2})\subseteq(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})$ pointwise and $(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})\in R$, then $(C_{1},f,C_{2})\in R$.

For $f:X_{1}\rightarrow X_{2}$, we define $f[x_{1}\mapsto x_{2}]:X_{1}\cup\{x_{1}\}\rightarrow X_{2}\cup\{x_{2}\}$, $z\in X_{1}\cup\{x_{1}\}$,(1)$f[x_{1}\mapsto x_{2}](z)=x_{2}$,if $z=x_{1}$;(2)$f[x_{1}\mapsto x_{2}](z)=f(z)$, otherwise. Where $X_{1}\subseteq\mathbb{E}_{1}$, $X_{2}\subseteq\mathbb{E}_{2}$, $x_{1}\in\mathbb{E}_{1}$, $x_{2}\in\mathbb{E}_{2}$.

Definition 4.6** ((Hereditary) history-preserving bisimilarity)**

A history-preserving (hp-) bisimulation is a posetal relation $R\subseteq\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$ such that if $(C_{1},f,C_{2})\in R$ with $rcp(C_{1})=rcp(C_{2})$, and

for $e_{1}=\alpha$ a fresh action, if $C_{1}\xrightarrow{\alpha}C_{1}^{\prime}$ (with $\mathcal{E}_{1}\xrightarrow{\alpha}\mathcal{E}_{1}^{\prime}$), then for some $C_{2}^{\prime}$ and $e_{2}=\alpha$, $C_{2}\xrightarrow{\alpha}C_{2}^{\prime}$ (with $\mathcal{E}_{2}\xrightarrow{\alpha}\mathcal{E}_{2}^{\prime}$), such that $(C_{1}^{\prime},f[e_{1}\mapsto e_{2}],C_{2}^{\prime})\in R$ with $rcp(c_{1}^{\prime})=rcp(C_{2}^{\prime})$; 2. 2.

for $e_{1}=x(y)$ with ($y\notin n(\mathcal{E}_{1},\mathcal{E}_{2})$), if $C_{1}\xrightarrow{x(y)}C_{1}^{\prime}$ (with $\mathcal{E}_{1}\xrightarrow{x(y)}\mathcal{E}_{1}^{\prime}\{w/y\}$) for all $w$, then for some $C_{2}^{\prime}$ and $e_{2}=x(y)$, $C_{2}\xrightarrow{x(y)}C_{2}^{\prime}$ (with $\mathcal{E}_{2}\xrightarrow{x(y)}\mathcal{E}_{2}^{\prime}\{w/y\}$) for all $w$, such that $(C_{1}^{\prime},f[e_{1}\mapsto e_{2}],C_{2}^{\prime})\in R$ with $rcp(C_{1}^{\prime})=rcp(C_{2}^{\prime})$; 3. 3.

for $e_{1}=\overline{x}(y)$ with $y\notin n(\mathcal{E}_{1},\mathcal{E}_{2})$ and $x\notin rcp(C_{1}^{\prime\prime})\cup rcp(C_{2}^{\prime\prime})$, if $C_{1}\xrightarrow{\overline{x}(y)}C_{1}^{\prime}$ (with $\mathcal{E}_{1}\xrightarrow{\overline{x}(y)}\mathcal{E}_{1}^{\prime}$), then for some $C_{2}^{\prime}$ and $e_{2}=\overline{x}(y)$, $C_{2}\xrightarrow{\overline{x}(y)}C_{2}^{\prime}$ (with $\mathcal{E}_{2}\xrightarrow{\overline{x}(y)}\mathcal{E}_{2}^{\prime}$), such that $(C_{1}^{\prime},f[e_{1}\mapsto e_{2}],C_{2}^{\prime})\in R$ with $rcp(C_{1}^{\prime})=rcp(C_{2}^{\prime})$; 4. 4.

for $e_{1}=\overline{x}(y)$ with $y\notin n(\mathcal{E}_{1},\mathcal{E}_{2})$ and $x\in rcp(C_{1}^{\prime\prime})=rcp(C_{2}^{\prime\prime})$, if $C_{1}\xrightarrow{\overline{x}(y)}C_{1}^{\prime}$ (with $\mathcal{E}_{1}\xrightarrow{\overline{x}(y)}\mathcal{E}_{1}^{\prime}$), then for some $C_{2}^{\prime}$ and $e_{2}=\overline{x}(y)$, either $C_{2}\xrightarrow{\overline{x}(y)}C_{2}^{\prime}$ (with $\mathcal{E}_{2}\xrightarrow{\overline{x}(y)}\mathcal{E}_{2}^{\prime}$), such that $(C_{1}^{\prime},f[e_{1}\mapsto e_{2}],C_{2}^{\prime})\in R$ with $rcp(C_{1}^{\prime})=rcp(C_{2}^{\prime})$; or $C_{2}\Rightarrow C_{2}^{\prime}$ (with $\mathcal{E}_{2}\Rightarrow\mathcal{E}_{2}^{\prime}$), such that $(C_{1}^{\prime},f[e_{1}\mapsto\tau],C_{2}^{\prime})\in R$ with $rcp(C_{1}^{\prime})=rcp(C_{2}^{\prime})$;

and vice-versa. $\mathcal{E}_{1},\mathcal{E}_{2}$ are history-preserving (hp-)bisimilar and are written $\mathcal{E}_{1}\sim_{hp}\mathcal{E}_{2}$ if there exists a hp-bisimulation $R$ such that $(\emptyset,\emptyset,\emptyset)\in R$.

A hereditary history-preserving (hhp-)bisimulation is a downward closed hp-bisimulation. $\mathcal{E}_{1},\mathcal{E}_{2}$ are hereditary history-preserving (hhp-)bisimilar and are written $\mathcal{E}_{1}\sim_{hhp}\mathcal{E}_{2}$.

Since the Parallel composition $\mid$ is a fundamental computational pattern in CTC, APTC and $\pi_{tc}$, and also it is fundamental in $\textrm{A}\pi_{tc}$ as defined in Table 2, and cannot be instead of other operators.

4.2 Algebraic Laws

Similarly, for an index set $I=\{1,\cdots,n\}$, we use $\sum_{i\in I}P_{i}$ to denote $(\nu u)(\textrm{case }u\textrm{ of }(u:P_{1},\cdots,u:P_{n}))$ for $u$ fresh if $I\neq\emptyset$; 0 otherwise. If $I$ is a singleton, we write $\sum P$ instead of $\sum_{i\in I}P$. And we also let the variable $G$ range over processes $\sum_{i\in I}P_{i}$. Then we get the following axioms as Table 3 shows.

Then we have the following conclusions.

Theorem 4.7** (Soundness modulo pomset bisimilarity)**

The axioms in Table 3 are sound modulo pomset bisimilarity.

Theorem 4.8** (Soundness modulo step bisimilarity)**

The axioms in Table 3 are sound modulo step bisimilarity.

Theorem 4.9** (Soundness modulo hp-bisimilarity)**

The axioms in Table 3 are sound modulo hp-bisimilarity.

Theorem 4.10** (Soundness modulo hhp-bisimilarity)**

The axioms in Table 3 are sound modulo hhp-bisimilarity.

5 Conclusions

Based on our previous work on process algebra for true concurrency CTC [17], APTC [16] and $\pi_{tc}$ [18], we adjust $\textrm{A}\pi$ [4] to make it have a truly concurrent semantics. Since the actor computational model is a model for true concurrency, $\textrm{A}\pi_{tc}$ makes the algebra of actors truly true concurrency.