名称传递过程演算的三种操作模型以及其共代数模型的研究（20字）

理论计算机科学电子笔记106（2004）91-104www.elsevier.com/locate/entcs名传递过程演算Marcelo Fiore1和Sam Staton计算机实验室剑桥大学英国剑桥摘要我们研究了三个操作模型的名称传递过程演算：（前）层上的余代数，索引标记的过渡系统，和历史相关的自动机。余代数模型既适用于有限集合和注入范畴上的预层，也适用于它的子范畴原子层（称为Schanueltopos）。我们讨论了由共代数模型导出的过渡关系，观察了前两个模型之间的差异。此外，通过对历史相关自动机施加条件，该模型被证明是等价的层理论的共代数模型。保留字：传名过程演算，标号转移系统，余代数。并发计算的操作模型将进程描述为一个状态空间及其通过执行原子操作而可能演化的过程。转移系统的模型已被证明对静态网络的基本过程建模是有用的，如CCS和相关演算所描述的那些过程。然而，它们对于现代系统中存在的重构和移动性是不够的，例如π演算所描述的。因此，命名传递过程演算的操作模型已经被研究。Fiore和Turi [5]提出了一种共代数模型，其相关的互模拟与早期和晚期的强双相似性和同余性相一致Cattani和Sewell [1]引入了所谓的索引标记转换系统来描述早期一致性的名称传递过程。蒙塔纳里和1由EPSRC高级研究奖学金支持的研究。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.02592M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91→ ∈\→.- 是的Σ⊕∅→⊕∅⊕→⊕Pistore [7]提出了一种新的自动机，适合于名字传递行为。本文的主题是比较和联系这些发展。在第一节中，我们将由Fiore和Turi的余代数模型导出的预层上的指标标号转移系统进行了推广，在第二节中，我们将其与Cattani和Sewell的指标标号转移系统进行了比较。随后，在第3节中，我们将共代数模型从预层细化为层，最后，在第4节中，我们将其与Montanari和Pistore的历史相关自动机联系起来。1预层上的余代数模型传递名称进程演算的预置层。Fiore、Moggi和Sangiorgi [4]以及Stark [8]的π演算的完全抽象模型的一个关键组成部分是使用预层来通过它们可能使用的名称索引过程/状态的集合（或cpos）。固定名称N的无限域，合适的索引范畴I是N的所有有限子集和它们之间的注入的范畴。事实上，I等价于在一个生成元上有初始单位的自由对称monoidal范畴，因此具有建模名称生成的适当结构。因此，我们将以这种方式考虑I，将生成元（单例）表示为1，初始单位（空集）表示为，张量积（不相交并）表示为。重要的是，每个有限名称集CfN都配备了规范映射旧C：C→（C1）←1：新CgivenbyyoldC=C=（C）的方式（C） 1）和新的wC=1=（第一章（C） ①的人。这些映射引出了一个内射重命名的概念，如下：对于一个内射，im（n），我们令（d/v C）n：（C第一章D是使下图可换的唯一单射函数。C、1老C 、、C，、、、（d/vC），，n，ewC、、1你，DzJ，sD(As一个记法惯例，每当是一个包含时，我们就删除子索引M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）9193一个预层（=集值函子）P：I→Set可以被认为是将每个名称集CfN映射到一个使用C中某些名称的进程集合PC，并将每个单射重命名函数P：C→D映射到进程上的重命名函数P：PC→PD当我们清楚所指的是哪个P时，我们将P（p）写成早期互模拟的余代数。Fiore和Turi [5]的工作提供了一个使用集合I中的余代数、集合I上的预层范畴和自然变换的名字传递模型。早期和晚期的互模拟是根据特定行为的共代数互模拟来捕获的函子我们回想一下预层上必要的• 一种名称类型N-包含函子I →Set。• 单位类型1-不断1预层（终端在集I）。• 乘积和和，以标准方式逐点定义• Non-empt y powerset+al sogivennpo i ntw iseandactingcovaria nntl y.• 指数PQ，其中PQC由以下集合给出（通过Yoneda引理）：自然变换I（C，−）×Q→。 P. 特别地，PN C=（PC）C×P（C1）• 一个逐点的• 一种动态分配算子δP，由（δP）C=P（C<$1）给出早期互模拟的一个合适的行为函子Be由下式给出：B e P = N~（（N + P）N）输入×N~（N+（N×P））输出×N~（δP+δP）硼输出×1~（π+P）沉默一个Be-余代数由一个载体预层P∈SetI和一个自然的转化为h：P→。 BPinSetI. 一个关于自然过渡的共同点-emationhC（C∈I）将PC中的过程映射到BeP（C）中的行为;即，94M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91∫Σ∫N−→−→−→−→中的元组C~（（n+P C）C×n+P（Cn1））×C~（P+（C×PC ））×C~（n+P（C~1））×1~（π+P C）表示该过程的能力。例如，对于p∈PC，如果hC（p）=（i，o，b，t），那么i是一个部分函数，可以解释如下。对于某个通道名c∈C，如果p能够在通道c上输入，则i定义为c，其中chc为ei（c）是pair（f，pJ）∈（P+PC）C×（P+P（C<$1））. 现在就站起来如果输入一个已知的名字d∈C，则p将继续作为非空集f（d）中的一个过程。对于一个新名字d/∈C，我们使用pJ作为结果过程的模板，继续为[d/νC]pJ∈P（C<${d}）。就像集合中的余代数X→X（Lab×X）导出一个转移关系.我在X给定的状态空间上，一个余代数P→B∈P诱导与由P的元素给出的状态空间的转移关系，即集合P=C∈IPC。 对于一个元素（C，p）∈ P.转换上的标签取自Lab=（N ×N）+（N ×N）+1，输入（写为C？d）、输出（写为c！（d）和沉默（书面τ）分别行动。每个标签l都与一些数据dat（l）和通道ch（l）相关联，我们将其视为集合;在这里，它们将至多具有一个元素。一个函数函数f的一个子集，我们为所有的人写了[f]l重命名Gi venacoalg ebrah：P→. BP，a跃迁r−→P×Lab×Pe被归纳为满足以下条件的最小值：pJ∈ π1（π1（h C p）c）d=<$C<$pJ∈π2 （ π1 （ h C p ） c ） ，d/∈C =<$ Cp（d，pJ）∈ π2（h C p）c=<$C<$ppJ∈π3（h C p）c，d/∈C=C<$ppJ∈π4（hC p）（）=<$C<$pc？Dc？Dc！Dc！D−→CpJC<${d}<$[d/νC]pJC pJC<${d}<$[d/νC]pJC pJFiore和Turi [5]证明了Be-共代数互模拟与诱导跃迁关系上的早期互模拟是一致的。τM. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）9195∫∫I 1. 信道是已知的，并且最多学习传输的数据：Cp−→ Cp=chlC，Cdatl=CLJ JJI 2. Earliness：如果一个名字可以输入，那么任何其他名字也可以输入：对于所有z∈N：Cp−→C {d}pc？DJ=<$$>pJJ∈P（C <${z}）.Cp−→C{z} pc？zJJI3. 双向预存器：对于所有D∈I，其中CCJ=D：σCp− → Cp= <$σC<$[σTC]p−→σCJ <$[σTCJ]pJLJJ[σ]lI 4. 知道新的名字保留了转换：对于所有z∈N\C：Cp−→C {z}pc？zJ=<$C<${z} <$[C<$→（C<${z}）]p−→C<${z} <$pc？zJI5. I包括预存转换：对于所有D∈I，其中D≠l=l：Cp−→ CpLJJ=<$C<$D<$[C<$→（C<$D）]p−→C<$D <$[C<$→（C<$D）]p第六章包含映射反映跃迁：对于所有D∈I，其中chl∈ C：LJJ JJC<$D<$[C<$→（C<$D）]p−→LJJ=pJJ∈ P（C dat l）.CDplJJ[（Cdatl）<$→（CjD）]pJJ=pJ<$Cp−→（Cdatl） <$pI-指标标号转移系统早期行为Be当然不会导出每一个过渡关系。为了理解这个共代数模型，我们推导了由此导出的跃迁关系。定义1.1一个I-指标标号转移系统（I-LTS）是一个预层P∈SetI以及一个满足图1中公理的转移关系−→Lp×Lab×P。Fig. 1. 对I-索引标号转移系统的要求.我们得到了关于余代数和标号变换系的下列结果定理1.2下列等式是等价的。(i) Be-余代数。(ii) I-指标标号迁移系统.96M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91∈−→−→⎧⎨℘+Pı(φc),ifd=ı(c)条件I1对应于我们对标号转移系统的推导.行为函子的结构给出了条件I2，如下所示：N~（（N+P）N）在某个阶段C∈I，我们有一个元素i，C~。. +PC）C×（从而在某个信道C上C必须要么没有通信（因此i在c）或每个名称的通信中被定义（因为幂集不是空的）。条件I3为了清楚起见，我们将注入分为双射和包含。指数的作用产生条件I5. 事实上，假设rapair（φ，π）∈（φ+P）N（C）=（φ+PC）C×φ+P（Cφ1），且nijcφ：C→D. 对于（φJ，πJ）=（φ j+P）N（φ j）（φ，π），我们有φJ（d）=π+P（d/νC）π，或和πJ=π+P（ππ1）π2指数标号变迁系统上面考虑的模型与描述早期互模拟有关。由Cattani和Sewell [1]引入的名称传递模型捕获了更精细的早期一致性。他们的模型由某些索引标记的转移系统组成，称为N-LTS.这些需要满足的公理是根据经验和直觉提出的，而不是像我们的例子那样从数学结构中归纳出来的。然而，他们的公理基本上与我们的一致主要区别突出了早期互模拟和早期一致性之间的Cattani和Sewell [1]的索引范畴是N的有限子集和它们之间的所有函数的范畴F。从这个观点来看，它们自然需要下面的公理，这些公理明确地使用了非内射改名。N2a。 （输入-新）对于任何z /∈CCpc？zC{z} pJ= d∈C. Cpc？DC{d}[d/z]pJM. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）9197−→−→z，t，−→−→−→一一BBCC一12N2b。 （输入C pc？DCpJ=Z/∈C. p∈P（C∈ {z}）.pJJ= [z/d]pjCpc？zC{z}pJJ这些公理在早期双相似性的背景下并不满足例如，考虑过程pi=a（x）. 如果x=a，则na<$a等于ea<$d1+a（x）。如果x=a，则na<$b个元素ea<$d2个元素+a（x）。如果x=a，则n个ac元素eadi（i= 1， 2）这里我们写' a（x）.p '表示'在通道a上输入一个名字，将其绑定到p中的x'; ' a<$x'表示'在c h ann e l a上输出名字x'; d '+ '表示n ondeterministi c s um。的状态图的pi（i= 1， 2），与过渡a？x代表所有转换，其中xa，由下式给出，，o，o·，，oo，，，a？a，a？Xo是吗？aa？x，a？a，a，？x，，，，，·，，o，·，so·Jv·z，，z·，，z·一个！一·J一个！D1·J一个！B·J一个！D2·J一个！C·J一个！Di·J在早期的双相似性中，，，......，a？aa？aa？aa？x，a？x，、、J，，z，，，zpa，t，pb，spcpdpd......、、 、、、、一个！C一个！da！d，，，一个！一个，一个！b、将所述第一一、二，，，无产生I-LTS（根据定义1.1），但不是N-LTS（根据Cattani和Sewell），因为它不满足公理N2b。 如果它满足公理，那么对于C={a，b，c，d1，d2}和z/∈C，我们必须有一些pJ= [z/a]p，pJ= [z/a]p，且pJ= [z/a]p，其中C=p是吗？zC{z}pJ，C p是吗？zC{z}pJb和Cp是吗？zC{z}pJc. 唯一的可能-98M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91∈ {}N对于i，j，k 1，2，关系为（pJa = p di，pJb= p dj，pJc = p dk）。回想一下-LTS允许所有函数重命名。 特别是，我们可以考虑重新-traction [a/z]：（C{z}）→C，充当C上的恒等式，并将z映射到a。M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）9199NNN∈⊆ →∈⊆X∈∈现在我们有了[a/z]pdi=pa[a/z]pdj=pb[a/z]pdk=pc由于i，j，k∈ {1， 2}，因此{pa，pb，pc}中的两个状态相等，但情况并非如此。条件2a和2b要求“如果可以输入一个名字，那么就这样但它们也确保了输入行为是参数化的在输入数据中。这样，它们就加强了我们的条件I2。此外，预层X：F→Set上的N-LTS恰好是满足条件N2a的底层预层I>F−→Set上的I-LTS和N2b除了图1的条件。也就是说，N-LTS上的其他公理等价于我们的公理I1和I3在他们论文的期刊版本中，Cattani和Sewell为I上的预层引入了一个N类指数标记迁移系统的inj-LTS。满足条件I2的注入-LTS就是I-LTS。3从预层到层：完善模型沙努尔地形。考虑一个预层P塞特岛 对于pP（D）和包含物D我们有一个元素[D <$D[J] pP（DJ）。 直观地说，假设一个进程“使用”了比实际更多的名称并没有什么坏处可以这此外，可能D本身包含的名字比p实际我们还可以通过观察注入如何作用于元素p P（D）来识别元素p P（D）使用的名称。例如，如果D的每个固定（即不移动）所有C D的自同构也固定p，那么我们期望p只更一般地说，我们有以下支持的概念。定义3.1一个名称集CD支持一个元素p∈P（D）当且仅当，对于所有的n，J：D→E在I中，只要nTC=JTC，则[n]p=[J]p。根据前面讨论的直觉，我们可以预期如果C支持p∈PD，那么p在这正是原子拓扑的层条件：[Sheaf条件]当C<$D支集p∈P（D）时，存在唯一的q∈P（C），且[C<$→D]q=p.也就是说，声明100M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91Σ∈∈∈ −→ ⊆∫× ×∫层条件要求它在C处有一个 为了我们的目的，这是一个合理的条件。满足这个条件的全子范畴Sh（Iop）称为Schanuel topos。我们简要回顾了Fiore [3]对Schanuel topos的分析 设B是所有有限名集和双射的范畴;即，构成I.对于P∈SetI，定义一个预层<$P<$∈SetB，P0.0000 p∈P（C0）.⎫⎬<$[C0<$→C]p0=p=<$C0=C<$相反，从Q集合B生成预层Q！集合I通过自由地作用于正则包含映射如下：Q！（C）=Q（CJ） ，Q！（n）（CJ，q）=（im（n），Q（nTCJ）（q））CJC这些过程是相互逆的：对于Schanuel topos中的任何层P，我们都有一个P层！ P=P。建设（-）！扩展到一个函子SetB→SetI，左伴随于遗忘函子|−|：SetI→ SetB，Schanuel topos（等价于）Kleisli范畴产生于这个附加。因此，Schanuel topos中的层可以等价地认为是集合B中的预层。B指标标号转移系统早期行为的内函子Be：SetI→SetI限制于Schanuel topos上的内函子，因此在这个子范畴中讨论Be特别地，我们现在要问的是，在集合B中的预层上的哪些转移系统应该被考虑。定义3.2 B-指标标号跃迁系统（B-LTS）是一个预层Q集合B与转移关系Q LabQ满足图2中的公理。我们有以下结果与引入的索引标号转移系统的两个概念有关。定理3.3对于Schanueltopos中的层P，下列是等价的.(i) 环上的B-指标标号转移系统.(ii) 环P上的I-指标标号迁移系.M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91101LLdefine −→！⊆P×实验室×⟨−→⟩ ⊆公司简介B-LTS由下式给出：LB 1. 我们最多可以学习传输的数据：Cp −→ C p=chlC C CdatlLJ JJB 2. 如果一个名字可以输入，那么任何其他名字也可以输入：对于所有z∈ N：C CJJ ∈ B，pJJ ∈ Q（CJJ）. Cp −→ C px？yx？zJJ JJB3. 双向预存流假设：对于所有D∈B，其中σ：C<$CJ<$=D：Cp −→ Cq=<$σC<$[σTC]p−→σC <$[σTC]qL[σ]lJJ图二. 对B-索引标号转移系统的要求.从一个B-LTS到一个I-LTS：let−→P×Lab×PbeaB-LTSanddD<$[C <$→ D] p −→！D<$（datl）<$[CJ<$→（D<$datl）]pJ当Cp−→ CJpJ从一个I-LTS到一个B-LTS：let−→LP×Lab×LPbeanI-LTSanddefine当verD <$q−→D J <$Q J时，C<$p<$−→l <$Cj <$p其中p∈<$P<$（C）且P（C <$→D）p=q，且pJ∈<$P <$（CJ）且P（CJ<$→DJ）pJ=4历史相关自动机Montanari和Pistore的History Dependent Automata[7]提供了另一种名传递进程演算操作模型的方法。历史相关自动机的新颖之处在于它可以在一个“命名集”范畴内工作。具有对称性的命名集。命名集合有多种类别，例如[2，7]。在这里，我们考虑Pistore在他的论文[7，第7章]中引入的具有对称性的命名集合。定义4.1一个具有对称性（X，f）的命名集合由一个集合X给出，该集合X配备有一个映射f：X→SubGrp （Sym （N）），其中SubGrp （Sym（N））是对称群Sym（N）在可数名称集N上的所有子群的集合。JQ。P为I-LTS，由下式给出102M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91一个同构于Q的预层。实际上，考虑X=Q /，其中是[σ]p=pJ。 对于ρ：X→设置⎫⎬从这样一个命名集合（X，f）中可以恢复一个支集的概念。假设CN支持x∈X，如果每当一个置换σ固定C时，它就在f（x）中。也就是说，C支持x∈X，如果<$σ ∈ Sym（N）. （c ∈ C. σ（c）= c）=<$σ ∈ f（x）我们将写supp（x）为x∈X的最小支集，只要它存在。 我们把注意力限制在每个元素都有有限支集的命名集合上。定义4.2范畴fsNSet具有有限支持的具有对称性的命名集作为对象。态射m：（X，f）→（XJ，fJ）由函数m：X→XJ以及对于每个x∈X的等价类[] x给出，使得−1·f（x）·f j（mx），关于等价X，该等价x对所有σ∈Sym（N）和τ∈f J（mx）标识σ和σ · τ。以下结果是将模型关联起来的主要步骤。定理4.3有限支撑对称命名集范畴fsNSet等价于Schanuel topos Sh（Iop）。回想一下第3节，在Sh（Iop）中给出一个层就是在集合B中给出一个预层。因此，对于（X，f）∈fsNSet，我们将预层Q：B→Set关联如下：QC={（x，σ）|x∈X，σ：sup（x）→∞其中，由下式给出等价关系：（x，σ）x，σ·（τTsupp（x））C}/N对所有的τ∈f（x），其中im（τTsupp（x））=supp（x）.对于任意[x，σ]∈QC且σJ：C→CJ，设QσJ[x，σ] = [x，σJ·σ].这个映射本质上是满射的，在通常的意义上，对于任何预层fQ∈SetB，存在som_em_n-set（X，.f）milling（asabove）等价关系<$h（C，p）<$（CJ，PJ）i <$<$存在σ：C→Cj使得f（x）=σ∈Sym（N）im（σTπ1（ρx））=π1（ρx）和对于所有x∈X。Q商映射的固定收缩，定义f为⎩M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91103Q（σTπ1（ρx））（π2（ρx））=π2（ρx）104M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91H 1。我们最多可以学习传输的数据：对于任何C∈I，t∈T（C）：chC（ labC（t））_ supp（ srcC（t）），supp（ tarC（t）） supp（ srcC（t）） suppatC（ labC（t））H 2。 如果一个名字可以输入，那么任何其他名字也可以输入：对于所有C∈I，t∈T（C），c，d，z∈ N：实验室C（t）= c？D=tJ∈T（C{z}）. labC<${z}（tJ）=c？z[C<$→C<${z}]（srcC（t））=srcC<${z}（tJ）H 3。 每个源、标签和目标只有一个转换：（src，lab，tar）：T→P×L×P是monicH 4。 过渡得到的支持最少：supp（t）= supp（ srcC（t）） supp（ labC（t）） supp（ tarC（t））上面从有限支撑的具有对称性的命名集到B上的预层的映射扩展到一个完全且忠实的函子fsNSet →Sh（Iop）。(An最佳观测值是一个自然变换α：P→。PJ在Sh（Iop）中，如果CJ支持p∈P（C），则CJ也支持αC（p）∈PJ（C）。作为B-指标标号变迁系统的历史相关自动机回想一下，一个历史依赖自动机是由一个命名的状态集P、一个命名的转换集T、一个命名的标签集L给出的，这些标签集在fsNSet中分别配备了映射src、tar：T→P和lab：T→L，从而我们为当前场景固定一组命名的标签L，自然转换ch，dat：L→N。根据定理4.3，我们可以把这些命名集和映射看作层和自然变换。我们对历史依赖自动机施加了一些限制（图3），以便考虑那些特别适合π演算早期语义的条件H1和H2类似于I-LTS上的条件I1和I2（图1）以及B-LTS上的条件B1和B2（图2）。条件H3相当于考虑转换系统而不是转换图，而条件H4根据转换的源、目标和标签来固定转换的支持。图三. 对历史相关自动机的要求。定理4.4对于Schanueltopos中的层P，下列等式是等价的.M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91105∫∫L∫∫(i) 一个历史相关的自动机，状态P满足图3的条件。(ii) 一个B-indexed的标号迁移系统.从这样一个历史依赖自动机，我们可以得到一个过渡关系− →P×Lab×P，Cp−→CJpJ当存在D∈I和t∈T（D）且srcD（t）=P（C <$→D）p时，tarD（t）=P（CJ<→D）pJ，以及labD（t）=l。条件H3和H4确保跃迁关系由下式导出：最多一个历史依赖自动机。 src，tar，lab的自然性将确保转换关系满足条件B3。条件H1和H2确保转移关系满足条件B1和B2。从一个B-LTS−→LLP<$×Lab× LLP<$，我们得到一个依赖于历史设T（C）为集合，。（D，p），l，（DJ，pJ）<$∈−→|DDjC，然后src，tar，lab是相应的投影，然后是包裹体。自然性由条件B3给出。5总结发言相关工作。 其中一个参考 文献引起了我们对Gadducci 、 Miculan 和Montanari [6]工作的注意，他们独立地建立了一个类似于我们定理4.3的结果，用于类似于Ferrari、Montanari和Pistore [2]所考虑的命名集的变体。命名集合的这个变体中的一个重要区别是，具有有限支持成为一种属性而不是要求。最小化。Final coalgebra semantics（最终余代数语义）产生了与划分细化技术密切相关的最小化技术（通过找到一系列通向最终余代数的余代数）。这已经研究了与历史相关自动机相关的名字传递系统[2]。对于这里考虑的余代数，实现的主要障碍之一是集合I中预层的元素集合通常是无限的。但这些被认为是在，例如，在，taryπ-calculus，arefinitely presentable.在这种情况下，一个合适的介绍106M. Fiore，S.Staton/Electronic Notes in Theoretical Computer Science 106（2004）91通过Schanuel topos与具有对称性的命名集范畴之间的等价性给出了一个新的定义。规则格式。在本书中，我们没有考虑余代数、转移系统或自动机最初是如何定义的。在实践中，转换关系通常使用规则上的结构归纳来定义。我们有初步的结果（按照[5]的方法）的语法规则，诱导转换系统满足公理，如图1和图2，以及对GSOS规则格式的推广名称传递过程演算，保证双相似是一个同余。引用[1] Cattani，G. L. Sewell，Model for name-passing processes：Interleaving and causal，Information and Computation190（2004），pp. 136-178.（在Proc中的扩展摘要。LICS'00 .）[2] 法拉利，G.，联合Montanari和M. Pistore，Minimising transition systems for name passingcalculi：A co-algebraic formulation，in：Proc. FoSSaCS129比158[3] Fiore，M.P.，Notes on combinatorial functors，Draft（January 2001）.[4] Fiore，M.P.，E. Moggi和D.Sangiorgi，π演算的完全抽象模型，信息与计算179（2002），pp.76-117.（在Proc中的扩展摘要。 LICS'96 .）[5] Fiore，M. P.和D. Turi，Semantics of name and value passing，in：Proc. LICS93-104.[6] Gadducci，F.，M. Miculan和U.关于置换代数和层（以及命名集合！）2003年，乌迪内大学研究报告UNODC/26/2003/RR[7] Pistore，M.，“历史依赖自动机”，博士论文，比萨大学（1999年）。[8] 斯塔克岛， 一个完全抽象的领域模型的π演算，在：Proc. LICS '96（1996），pp. 36比42