网址：http://www.elsevier.nl/locate/entcs/volume51.html17页关于异步演算罗贝托·M. AmadioCharlesMeyssonnier1;2Materialatoire d'Informatique Fondamentale deMarseille，CMI，39 rue Joliot-Curie，13453，Marseille，France.摘要我们研究了异步演算的各种片段的可达性问题的判定性.我们考虑三个主要特征的组合：名称生成，名称移动性和无界控制。 我们表明，名称生成与名称移动性或无界控制的组合导致一个不可判定的片段。另一方面，我们证明了没有名字移动和有界控制的名称生成是可判定的，通过减少Petri网的覆盖性问题。1引言我们感兴趣的属性约简关系，如可达性，死锁，活性，：基于异步演算的进程演算[2，7，1]。我们回想一下，这里的“异步”指的是一种通信机制，在这种机制中，消息被放在一个无界的、无序的缓冲器中，在过程演算的行话中，这相当于不允许输出pre x。通过对立，同步演算强制发送者和接收者之间的同步.我们对异步演算的兴趣源于这样的观察，即并发编程语言的核心，如Pict[13]，Join[4]或Tyco[17]都是基于异步演算的，以及面向对象编程语言在这些形式主义中享有相当直接的表示。在本文中，我们将主要考虑不包括外部选择的最小异步，多元，简单排序演算，我们将集中于这个最小演算的三个主要“特征”：1 famadio，meyssonn g @cmi.univ-mrs. fr.2 作者得到RNRT MARVEL的部分支持。c2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2名称生成，即生成新名称的可能性（值，通道，：）。名称移动性，即传递姓名的可能性无限控制，即动态添加新控制线程的可能性。在没有名字生成的情况下，我们的形式主义可以映射到Petri网（参见[15]）。这种编码基本上可以追溯到早期将ccs[11]转换为Petri网的工作[5]，解决了没有名称生成的片段的最有趣的决策问题。因此，在我们看来，仍然需要澄清的主要问题是是否存在包含某种形式的名称生成的可判定片段。到目前为止，我们所知道的大多数可判定性结果都涉及同步- 具有有界控制的微积分（参见，例如，[3，12]）。在异步情况下，我们的主要结果如下：名称生成和名称移动性的组合导致不可识别的片段，即使假设控制节点。名称生成和无界控制的组合导致不可判定的片段，即使假设没有名称被传输（这是ccs的一个众所周知的不可判定性结果）。无名称移动和有界控制的名称生成可通过Petri网约简来描述。这是我们的主要技术成果，它基于对生成名称使用的分析。分析，这似乎是原始的，区分“持久”和“临时”的名称，并提供了一种方法来重用相同的名称生成的临时名称是活在不同的时间。我们认为这些结果作为第一步，系统地介绍近似决策方法的语言，包括名称生成。我们期望，一个富有成效的方法是理解这些方法的因素，通过翻译成Petri网的近似。一旦将行为映射到Petri网，则可以使用进一步的标准近似技术，例如，在半线性集合上（参见，例如，[16]，以获取最新的调查结果）。2异步演算像往常一样，我们假设给定一个可数的名称集合，我们表示a; b;：名称的向量（可能是emp ty）表示为~a;~b; ：We表示[~b =~a]名称上的替换。如果~aa1; ：;an，则我们使用（~a）作为简写for（a 1）：（a n）.我们假设每个名字a都有一个相关联的排序st（a），并且名字的使用与它们的排序一致。我们将只依赖于简单的排序，3由以下语法定义（一）其中o是某种接地类型。s：：= o j Ch（s;：; s）我们考虑一个多元的、简单排序的、异步演算，它具有消息创建a~b、输入pre x a（~b）：P、并行组合P j Q、名称生成（a）P和参数递归定义等标准操作后者优于迭代，因为它允许更好地控制并行线程的创建和终止。我们用A; B;：参数过程标识符表示。由参数方程A（~a）=P和一个初始构形构成的有限系统E表示一个过程，其中我们假定：（i）每个过程标识符都由一个方程定义，（ii）在P中自由出现的名字都包含在f~ag中.假设每个方程具有以下归一化形状将是方便的：（2）A（~a）=a（a~0）：（a~00）（i2Iai~aijj2JAj（~aj））：这样一个等式指定了一个过程，输入一个消息，然后生成新的名称，发送一些消息，并运行一些延续。假设集合I和J是nite（可能是空的，在这种情况下，并行组合简化为终止过程0）。 我们注意到，在方程中（2）~a，a~0，a~00是有界的。我们将假设它们被重命名为所以它们都是不同的。给定如上所述的递归方程的nite系统，构造是形状的归一化过程：（~a）（i2Iai（~ai）jj2JAj（~aj））其中，“”通常代表平行组合。设P，Q是两个Cong- urations.我们写PQ，如果P是语法上等于Q的重命名的绑定名称，置换的名称代，结合性和可交换性的并行组成。我们用fn（P）表示在P中自由出现的名字的集合。其次，我们介绍了Congurations上的约化关系。 我们所要捕捉的只是通常的归约规则a~bj a（~c）：P！[~b=~c]P允许在名称生成和并行组合下进行，直到合适的结构等价。我们的归约定义有点技术性，因为它必须评估实际参数，展开递归定义以找到匹配消息的输入前缀，然后将名称生成、消息和延续置于顶层的输入前缀之下。这种方法的优点是，我们可以将结构规则限制为上述规则，为配置提供一个紧凑的范式，并提供一个简单的Petri网翻译。定义2.1如果与过程标识符A相关联的等式是（2），4和（i）P（b~0）（A（~b）jc（~c） jQ），（ii）集合f~a;a~0;a~00g和f~b0g [fn（P）]互不相交，（iii）[~b=~a;~c=a~0]，(iv)且（a）= c，则（3）P！（b~0;a~00）（i2I（ai~ai）jj2JAj（~aj） jQ）：我们可能会怀疑，我们正常化的集会是否能代表所有人，通常的过程- 微积分，说：p：：= a~ b j a（~b）：p j！(a(~b）：p）j（a）p j（pj p）：事实上，这很容易检查。我们注意到，直到结构等价，过程p总是可以写为：p（~a）（i2Iai~ai j2Jaj（~aj）：pjj k2K！（ak（~ak）：pk））：我们声称我们可以建立一个配置P和一组方程E，其行为与p的等价。我们通过对p的结构进行归纳来产生方程组。对于每一 个过 程aj（~aj）：pj，我们引入一个新的过程定义层Aj（ ：）和方程Aj（：）=aj（~aj）：，并且我们将该变换归纳地应用于p j。同样，对于每个过程，！（ak（~ak）：pk）），我们引入了一个新的过程，在层Ak（：）和方程Ak（：）=ak（~ak）：（Ak（：）j： ），并且我们将变换归纳地应用于pk。放心我们的形式主义的表达能力，我们现在可以正式声明的可达性问题，我们在本文中解决定义2.2给定一个包含进程标识符A和相关初始配置P的方程组E，可达性问题询问是否P还原为包含过程标识符A的构型，即P！ （~a）（：j A（~b）j： ），对于某些~a;~b。在3.4节中，我们将把这个问题与众所周知的Petri网的可覆盖性问题联系起来。3没有名字生成的片段归结为Petri网我们考虑其中等式（2）被限制为具有以下形状的片段：（4）A（~a）=a（~b）：（i2Icid~ijj2JAj（~ej））：在这个片段中，不允许生成名称。给定这样一个方程组和一个初始配置P，我们将回想起下面的模拟过程约简的Petri网5一3.1无参数方程首先，我们回顾无参数方程组的概念（使用的符号，例如，在ccs的范围内[11]）。在这种情况下，所有名称都具有sort Ch（），并且方程具有以下形状（5）A=k2Kak：（i2Ikaijj2JkAj）其中K是夜晚设置和代表外部选择（外部选择在这里只是用来表示向Petri网转换的中间步骤）。如果K是空的，我们通常把左边作为终止进程0。不允许重命名，进程标识符实际上被定义它的等式的右侧替换3.2从无参数方程组到Petri网我们x的方程组没有参数的形状（5）。 设P为初始构形。不失一般性，我们可以假设P不包含名称生成器;否则我们将由新鲜的名字。设N是P中自由名的集合。 由于没有生成名称，因此这些名称都可以出现在可访问的配置中。(1) 我们将一个不同的位置与每个名称a2N和每个进程标识符A相关联。预期的解释是，位置a处的标记对应于当一个令牌位于位置A时，意味着线程的控制权是在A. 根据这种解释，我们确定初始标记。(2) 对于每个方程，我们将一组与位置相连的转换如果A = a1：+ +an：那么我们引入n个变迁t1;：; tn，并且对于k = 1;：;n，从位置A到变迁tk的边和从位置ak到变迁tk的边。此外，如果k的延拓具有以下形状（i2 I）Jj2J A j）然后我们添加一条边，从转变tk到i 2I的 位 置，从转变tk到j2 j的位置。3.3从无名称生成系统到无参数系统我们x一个系统的参数方程没有名称生成的形状（4）。为了符号简单起见，我们假设所有通道都有递归排序s = Ch（s），并且所有进程标识符都依赖于k个参数。然后又道：对于每对通道名a; b 2 N，我们引入一个新的通道名a b，其排序为Ch（）。对于每一个形状为e（4）的方程和每一个名为a~02N k的向量，a我6我们得到一个方程Aa~0 =b02N（（a）b0：（i2I（ci）（di）j j2JAj;（~ej）：其中[a~0=~a;b0=b]。总之，我们把一个参数系统转化为一个没有参数但有外部选择的系统，反过来，我们把后者转化为一个Petri网。3.4从可达性到可覆盖性，然后返回在Petri网方面，我们在定义2.2中阐述的可达性问题相当于检查与给定进程标识符将包含一个令牌。这是Lipton [10]提供的2O（pn）空间下界的可覆盖性问题的一个实例，拉茨科 [14]时间复杂度为2O（nlogn）另一方面，很容易看出，Petri网的可覆盖性问题可以归结为可达性问题2.2。 给定一个Petri网，对于每个转移t，比如说，从位置a1;：; an取一个标记，并将一个标记放在位置b1;：; bm，我们引入方程（我们省略参数）：At = a1：A1 A1 = a2：A2：An1 = an：（b1 jj bm j At）t t tt因此，现在通过序列化令牌的读取来模拟Petri网的转换。如果我们想知道，比如说，地点a是否会包含一个记号，我们就加上等式A = a：B。然后，初始配置包含每个转换t的进程标识符At、对应于初始标记的消息的数量以及进程标识符A。要确定位置a是否包含令牌，只需检查初始配置是否达到包含进程标识符B的配置这种减少是多项式，它表明，即使没有移动性和没有名称生成的可达性问题2.2，我们考虑需要指数空间。我们希望我们的可达性问题可以模仿Petri网[18]所做的那样一般化。另一方面，对等价问题（迹，互模拟，：）的可判定性结果的追求被Petri网[6，9]已知的否定结果所阻碍。4控制有界的片段是不可判定的如果存在一个自然数来限制在任何可访问的配置中并行运行的活动线程的数量，则我们说配置具有有界控制。我们可以想象出各种各样的句法条件，它们隐含着这个属性，并且是有效可检验的。为了显示我们的否定结果，考虑方程（2）被限制为具有的片段就足够了。7不形状：A（~a）=a（~b）：（d~）（i2Iai~bijA0（~c））A（~a）=A1（~a1）A2（~a2）：其中表示内部选择。这意味着，直到内部选择，每个控制点只有一个延续，因此控制基本上由初始配置中存在的并行线程数限制。注4.1众所周知，内部选择是由并行组合和名称生成定义的。在我们的案例中，t是归一化方程（2）的形状。因此，我们将方程A（：）= A1（：）A2（：）替换为以下方程：A（ ：） =t：（c） （ A01 （ c; ： ） jA02（c; ：） jc jt）A0i（：）=c：Ai（：）对于i=1;2其中T是在初始配置中提供的具有消息的“全局”信道（T信道扮演CCS动作的角色）。类似的技巧也适用于我们想定义内部二选一的情况消息.然后我们引入一个标识符A和方程：A（：）=t：（c）（A01（c; ：）jA02（c; ：）jcjt）A0i（：）=c：aifori=1;2：命题4.2有界控制的片段的可达性问题是不可判定的。证据证明是松散的启发编码的计算机制的图灵机到一个演绎系统的霍恩条款与-出功能symbols，也称为数据库。 熟悉后者的读者可能会觉得它启发我们把 Horn子句8~x（a（~x）9~yb（~x;~y））看作一个递归过程A=a（~x）：（~y）（b（~x;~y）ja（~x）jA）.现在我们来谈谈技术发展。我们模拟一个2计数器机器（参见，例如，[8]）并将停机问题简化为可达性问题2.2. 我们假设2计数器机器包含如下形式的指令(1) q：Ck：= Ck + 1; goto q0(2) q：（Ck=0）！gotoq0;Ck：=Ck1;gotoq00其中C1和C2表示两个计数器。类型（1）的指令递增计数器k并跳转到控制的另一点。类型（2）的指令测试计数器Ck是否为0，如果是，则跳转到一个控制点q0，否则它递减计数器并跳转到控制点p i ntq00.计数器表示为一堆单元格，其中底部单元格包含的1一个280 其他的都是1。因此，值2由堆栈表示9的1a0级C1a0级如果通道a指向底部单元格，则我们引入消息a0，011.对于每个状态，我们假设信道q的排序为Ch（）。此外，对于每个计数器Ck，我们假设通道前k 类型为Ch（Ch（Ch（）; Ch（）; Ch（），调整k 类型Ch（Ch（Ch（）; Ch（）; Ch（））; Ch（））：堆栈中的每个单元格都被分配了一个不同的通道a，其排序为Ch（Ch（）; Ch（）; Ch（））。我们将三个不同的通道a0; a1; at和消息a（a0; a1; at）与每个这样的通道相关联。此外：否则我们引入一个信息。如果通道a引用堆栈顶部的单元格，则引入消息Top k a。如果信道a和b指的是两个相邻的小区（第一个在第二个之下），那么我们引入消息Adj k（a; b t）。例如，堆栈011可以由以下消息表示a（a0; a1; at）j j Adjk（a; bt）j（底部单元格）b（b0; b1; bt）j b1 j Adjk（b; ct）j（第二小区）c（c0; c1; ct）j j Topk c（top cell）我们现在考虑在这个数据结构上实现2-反机器操作。类型（1）的指令被翻译为：A=q：Topk（a）：（a0;a00;a01;a0t）（q0jAdjk（a;at0）jTopk（a0）ja0（a00;a01;a0t）ja01jA）;并且类型（2）的指令变为：A=q：Topk（a）：a（a0; a1; at）：（a0：（q0jTopk（a）ja（a0;a1;at）j jA）（如果Ck=0）a1：Adjk（b;bt）：（atjbt：（q00jTopk（b）jA）（如果Ck>0）：注意，在上面的等式中，我们省略了参数（其可以容易地推断）以及中间过程标识符。情况（Ck> 0）揭示了信道at的作用：它用于通过通信模拟at和bt之间的相等性测试，以确保接收到的信道b对应于a之前的小区24.1具有生成值和条件的上述编码依赖于信道移动性，而且过程可以输入接收到的信道名称。微积分的一个常用的扩展包括名称相等的条件。为了形式化这个扩展，我们可以将方程的形状如下：10（6）A（~a）=[a=a0]A0（a~0）;A00（a~00）11预期的意思是，如果a为0，则我们选择A0，否则选择A00。现在，如果我们允许一个基本排序为o的名字的条件，那么一个更简单的编码是可能的，其中所有传输的名字都是排序为o的。我们假设附加通道Contk指示单元格的内容（值0或1）。现在的分类如下：排序Ch（o）的Topk;排序Ch（o; o）的Adjk;以及排序Ch（o; o）的Cont k：类型（1）的指令被翻译为：A=q：Topk（a）：（a0）（q0jAdjk（a;a0）jContk（a0;1）jTopk（a0）jA）;并且类型（2）的指令被翻译为：A=q：Topk（a）：Contk（a0;v）：[a0=a]（[v=0]（q0jTopk（a）jContk（a;0）jA）;Adjk（a0;a00）：[a00=a]（q0jTopk（a0）jA））：5没有名称移动性的片段是不可判定的我们考虑所有名称都具有sort Ch（）的片段，即，不允许名称移动性。那么等式（2）被限制为具有以下形状：（7）A（~a）=a：（d~）（i2Iaijj2JAj（~cj））：在没有名称移动性的情况下，生成的名称不能被挤出，因此名称生成本质上是ccs限制。米尔纳[11]表明，具有限制、重新标记和外部选择的同步CCS我们将证明，这种模拟仍然可以进行，而放弃外部选择和重新标记，只使用异步通信。示意性地，我们将（i）同步通信替换为异步通信加上确认，(ii)内部选择的外部选择（当然，这是可能的，因为我们只是看一个可达性属性），和（iii）重新标记的参数方程。命题5.1有名字生成和没有名字移动的片段的可达性问题是不可判定的。证据我们再一次以命题4.2的证明中描述的形式模拟一个2计数器机器，并将停机问题简化为可达性问题2.2。基本问题是表示堆栈。为此，我们定义了以下方程组（受[11]的启发）。通道i代表增量，z代表计数器为零，d代表减量。这些通道中的每一个都带有相应的“确认”通道ia、za和da，12我一一一在下面保持隐式。B（i; z; d）=Bi（i; z; d）Bz（i; z; d）B（i; z; d）=i：（iajCB（i; z; d））Bz（i; z; d）=z：（zajB（i; z; d））C（i;z;d;z0;d0）=Ci（i;z;d;z0;d0）Cd（i;z;d;z0;d0）Ci（i;z;d;z0;d0）=i：（ijCC（i;z;d;z0;d0））Cd（i;z;d;z0;d0）=d：（（d0z0）jD（i;z;d;z0;d0））D（i;z;d;z0;d0）=Dd（i;z;d;z0;d0）Dz（i;z;d;z0;d0）Dd（i;z;d;z0;d0）=（d0a：（djC（i;z;d;z0;d0）Dz（i;z;d;z0;d0）=（z0a：（djB（i;z;d）CB（i;z;d）（i00;z00;d00）（C（i;z;d;z00;d00）jB（i00;z00;d00））CC（i;z;d;z0;d0）（i00;z00;d00）（C（i;z;d;z00;d00）jC（i00;z00;d00;z0;d0））：进程C在i;d上接收，并在z0;d0上发送。 A过程B在i; z上接收。当递减时，进程C向其邻居发送消息。如果邻居是C，则消息在d上，如果邻居是B，则消息在z上。下面是一个直观的示意图：DCCCBB！DDCCBB！DDDCBB！DDDDBB！DDDBBB！DDCBBB！DCCBBB！CCCBBB：D向右传播，直到它遇到B，当这发生时，它变成B，并缩短了最后一个B。注意我们使用内部选择的特殊方式。如果一个“服务器”可以在两个通道上接收请求，那么它会不确定地猜测下一个消息将来自哪个通道。对称地，具有两个请求的“客户端”在内部猜测哪个请求将被服务。如果客户端和服务器端的猜测一致，我们就可以获得所需的行为。否则客户端和服务器会卡住。我们将一个2计数器机器的程序翻译为一个“nite”控制进程，它充当两个计数器进程的客户端，初始化如下：13B（i1; z1; d1）j B（i2; z2; d2）：14K(2)Aq = Az AdAz=q：（zkjza：（q0jAq））Ad=q：（dkjda：（q00jAq））：类型（1）和（2）的指令被模拟如下：(1) Aq=q：（ikjia：（q0 jAq））;Q QQ KQ K很明显，通过适当地选择内部选择，我们可以模拟2计数器机器的行为。另一方面，假设一次尝试的沟通由于错误的内部选择而陷入困境这可能发生在（i）当控制向计数器发送请求时，或者（ii）当递减指令在计数器中向右传播时。在这两种情况下，控制都被卡住了。在第一种情况下，这是清楚的，在第二种情况下，这发生是因为控制等待仅在传播完成之后才递送的确认2备注5.2在上述所有方程中，输入之后，直到内部选择，正好有一个输出。这意味着可达配置中存在的消息数量是有界的。6无移动性且有界控制的片段是可判定的我们考虑片段，其中所有名称都具有排序Ch（），并且等式(2) 被限制在形状上：（八）A（~a）=a：（d~）（i2IjB（~b））：为了简单起见，我们假设给定系统中的所有方程都依赖于k个参数。我们注意到，在系统中没有名字的流动性和有界控制有一个约束的数量上的“活”的名字出现在任何可达的配置。事实上，在这些系统中允许的唯一形式的名称传输是通过递归参数：一旦名称从递归参数中消失，就不能再对该名称执行输入。因此，在不失一般性的情况下，我们假设，方程（8）a bovefd~gf~b g.其基本思想是将第3节中提出的Petri网简化，并通过重用“死”名称来取代名称生成。我们将首先将系统转换为一个等价的无参数方程系统，该方程系统具有重置（并且没有名称生成），然后我们将其转换为具有重置弧的Petri网。后者可以减少到一个标准的Petri网，提供的令牌的数量在复位的地方是有界的（在一般的Petri网与复位弧是不可判定的）。a我15我在下文中，具有重置的无参数方程组是在第3.1节中呈现的无参数系统的变体。在这样的系统中，方程具有以下形状：（九）A=a：resetd~：（i2I（j B）;而reset操作符的语义是擦除所有在属于其参数的名称上发送的消息。6.1姓名寿命分析为了将带重置弧的Petri网约简为标准Petri网，我们需要对任意可重置位置上的令牌数量进行限制。 这导致我们区分原始系统中的两种名称：持久名称，没有绑定，但永远不需要重置，以及临时名称。我们将对任何临时名称上发送的消息数量进行绑定。为此，我们引入系统的参数流图，其定义如下。定义6.1系统E的参数流图是有向图G =（L; 7！），其中：节点集合L由参数位置fA i[1; k]g给出。j E和i 2一个7！BJ是图的一条边，如果如果在图中与A相关联的方程系统E是A（~a）=a：（d~）（：jB（~b））;并且~ a的第i个分量等于~ b的第j个分量。导致G中的循环的位置将被称为持久位置，而其他位置将被称为临时位置。相应地，当名称在A（~a）中发生时，如果该名称在至少一个持久位置中使用，则我们将调用该名称persistent_t，并且如果该名称仅在临时位置中使用，则调用该名称temporary。请注意G的特殊结构：如果我们考虑与一个进程标识符相关联的位置类，则由于我们对nite控制的语法定义，该类中顶点的所有边都会导致唯一类中的顶点。此外，由于f~ag中的所有名字都是不同的，所以we不能有av e，因为i6=j，Ai7！ Bl和A j7！Bl.从这些观察可以得出，从临时位置可到达的顶点集是夜树如果e是方程的个数在E中，那么树的大小由e k限定，e k是参数位置的数量。此外，如果m是E的任何方程中任何参数的最大输出数，则对任何临时名称执行的输出数以e k m为界，这是E的大小的多项式。a我16一 一A2B2C2A1 B1 C1Fig. 1. 参数 E的ow图例6.2让我们考虑由下列方程A（a; b）= b：（a j B（a; a））B（a; b）= a：C（a; b）C（a; b）= b：（c）（c jA（c; a））;以及初始构型P j j b j A（a; b）：在这个系统中，所有新生成的名称都是在位置A1中使用的临时名称.由于以A1为根的树有6个节点，并且E中的方程在其任何参数上都不会执行超过1个输出，因此我们可以将6作为任何临时名称上发送的消息数量的6.2从无移动有界控制系统到无参数重置我们x一个方程组E的类型（8），和一个初始配置P，它不包含任何生成的名称。设N0是P中的自由名称集，n是P中的进程标识符的数目。不失一般性，我们可以假设E中的每个进程标识符都与初始配置的唯一线程相关（如果进程标识符在不同线程之间共享，那么我们总是可以重命名它们以满足此条件）。我们将构造一个方程组E0的形状（9），并表明，对于E和P的可达性问题归结为对于E0和适当的初始配置P0的有限数量的可达性问题。我们假设，对于每个j 2[1; n]，分别具有基数k和2k的成对不相交集合Pj和Tj，它们将表示第j个线程的私有名称空间（Pj用于持久名称，Tj用于临时名称的）。无参数系统 e0级 将被定义为 超过 名称空间N=N0[（[j2[1;n]Pj[Tj）.17第j层的第n层A thread（written（a; ：; a）#A;j）iffor alla2定义6.3名称的向量（a1;：; ak）与pro-k相容。1K18Sfa1; ：;akg一个28N0[Pj]如果9i（ai=a且ai是一个永久posit ion）：N0[ T]，否则。接下来我们定义与（P; E）相关联的系统E0定义6.4确定E中形状（8）的方程，例如与螺纹j有关。然后又道：(i) 对于每个a~0，(ii) 对于每一个内射代换[d~0=d~]，fd~0gPj[Tj，fd~0g \fa~0g=;，=[a~0=~a;d~0=d~]，以及~b #B;j我们引入一个方程Aa~0 =（a）：reset~r：（i2I 0aijB~b）其中f~rg =Tjnf~bg且I0=fi2Ij ai2=f~rgg。粗略地说，我们考虑线程j的层A中的进程的所有兼容实例a~0，我们替换生成的名称d~byun使用Pj[Tj]中的名称（一个简单的基数参数表明它们存在），并且我们重置所有的在continuation中不使用的临时名称上的通道其次，我们引入了一个二元关系R的congurations和param-eterlesscongurations。定义6.5设Q（d~0）（d~）（i2Iaijj2[1;n]Aj（~aj））是一个构形，其中我们假设：日(ii) 标识符Aj与第j个线程相关，并且(iii) 如果d2fd~ g，则d0恰好发生在一个参数集fa~jg中。 则QR（i2I 0aij j2[1;n]Aj;~aj），其中：I0=fi2Ijai2N0[（Sj2[1;n]f~aj g） g，是从d~到j2[1：：n]（Tj[Pj]）的内射置换，对j2[1; n]，在这里，我们遵循与前面的定义6.4相同的方法：我们将恰好一个进程标识符的参数中出现的生成名称为集合Tj[ Pj]中的兼容名称，同时删除无用的限制和消息。给定一个初始配置P，我们可以很容易地计算出 使得PRP0. 然后，我们证明关系R是充分一般的，使两个国家步调一致。引理6.6如果QRQ0，我们有：（i）fd~0g \（Sj2[1;n]f~ajg）=;，19如果Q！ 则re是R0，使得RRR0和Q0！ R0。20一如果Q0！ 则re是R，使得RR RR0和Q！ R.这个引理的证明是对定义2.1、6.4和6.5的简单而费力的操作。然后，我们可以减少可达性问题，（P;E）是（P0;E0）的可达性问题的一个新的概念。命题6.7（P; E）中过程标识符A的可达性等价于（为数不多的）无参数标识符之一的可达性Aa~0 in（P0;E0）.证据我们将引理6.6归纳地应用于所考虑的约简链的长度，并利用关系R的定义。26.3从带重置的无参数系统到带重置弧的在本节中，我们将展示如何将3.2节中描述的从无参数系统到Petri网的约简扩展到从带重置的无参数系统到带重置弧的Petri网的约简。我们假设给出了一个无参数方程组，其中E0为零，一个初始配置P0没有名称生成。 设N为 别名系统被定义的空间（注意，这可能严格大于P 0中的自由名称集合）。像在3.2节中一样，我们构建一个Petri网，在E0中为每个无参数的过程IDn层提供一个位置，在N中为每个名称提供一个位置（rememberber我们不考虑流动性）。预期的解释仍然是，在位置a中的令牌对应于消息，而在位置A中的令牌对应于响应于当前配置中无参数过程标识符A的存在转换的设置与3.2节一样，除了我们不再需要关心外部选择（即每个方程只有一个转换），并且如果与A相关的方程是A=：reset~r： ，则对于ea cha2f~r g，我们添加一个从转换t A到位置a的重置弧。注意，由于6.1小节中的分析，我们可以保证重置弧指向的所有位置都是有界的。命题6.8A在（P0;E0）中的可检索性等价于上述带复位弧的Petri网中的库所A对1个标记的可超越6.4从带重置弧的Petri网到Petri网最后，我们回顾了如何模拟一个Petri网与复位弧N与标准Petri网N0，提供了所有可复位的地方是有界的（这是一个标准的结果Petri网）。对于每个可复位位置p，我们添加一个互补位置p0。如果b是在所有可达标记M中，以位置p上的标记数为界，我们将保持不变式M（p） +M（p0）=b。
我的内容管理
展开
