移动环境中的可达性问题的研究

理论计算机科学电子笔记239（2009）5-15www.elsevier.com/locate/entcs移动环境中具有名字限制的可Giorgio Delzanno和Roberto MontagnaDipartimento di Informatica e Scienze delldisi.unige.it摘要我们调查的可达性问题的片段的移动环境，一个强大的模型，分布式和移动计算。通过使用一个连接与联想交换项重写，我们证明了可达性是可判定的开放自由片段的纯移动环境的名称限制和弱约简语义。这个模型中的过程有三个无限性的来源：环境的深度、平行组合的宽度和限制名称的数量。 我们的工作扩展了移动环境的公共片段保留字：移动环境，可达性，术语重写1引言Cardelli和Gordon的Mobile Ambients（MA）[4]是一个强大的分布式移动计算模型。这个模型的基本模块是环境的概念。环境由表达式n[P]表示，其中n是名称，P是本地代理和子环境的集合。本地代理对环境中可能发生的计算进行建模。该形式主义基于进程代数的经典操作，如action prefix act.P，并行组合P|Q和复制！P.复制！P表示并行的P的任意数量的副本。 它的语义是通过公理定义的！P！P|P. 除了这些操作之外，纯（即没有通信）版本的演算提供了像in n（out n）这样的移动能力，允许环境A（具有任何标签）进入（退出）具有标签n的环境B。作为示例，过程m [in n.P|Q] |n [R]在一个步骤中减少到n [m [P|Q] |R]，而n [m][out n.P|Q] |R]在一个步骤中减少到n [R] |m [P|Q]。开放功能可用于溶解环境光的边界。名称限制vx.P（其中x是可以在P中自由出现的名称）可以用于向动态生成的环境分配唯一标识。例如，复制的进程P=！vx.x [in n. [0]相等1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.05.0276G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）5WWWW过程v x1... . vxn.x1 [in n. 0个字符]|......这是什么？| xn [in n. 0个字符] |P，即，到具有新名称和能力的任意数量的环境的集合n（0表示空进程）。移动能力可以生成具有任意嵌套结构的环境因此，MA是一个无限状态模型，它有几个无限性的来源：平行组合的宽度、限制名称的数量和环境的深度。MA的可达性MA方言的表达问题和证实问题在[2，10，1，3，5，7，8]中已经在本文中，我们把注意力集中在可达性问题：是否有一个计算从进程P到进程Q？这个问题已经在[6，1，3]中针对MA的公共（即没有名称限制）片段进行了研究。具体而言，在[6] Charatonik和Talbot证明了纯公共MA中可达性的不可判定性。在[1]中，Boneva和Talbot通过证明可达性在公共MA的开放-自由（即没有开放能力）片段中是不可判定的来细化这个结果。他们还通过展示两个计数器机器的编码证明了同一片段的图灵完备性。在该编码中，复制的标准语义（即，！P！P|P）用于收集执行计数器机器的模拟的进程所留下的垃圾。事实上，在同一篇论文中，作者表明，只要复制操作仅用于生成新进程（即！P！P|P转化为有向归约规则！P→！P|P）。 这种语义限制称为弱归约。 在[3] Busi和Zavattaro证明了在具有标准归约语义的开放自由公共MA中，只要每次复制都由移动能力保护，可达性是可判定的。(i.e.他们承认使用！只有在这样的过程中！M.P，其中M是in n或out n）。有趣的是，具有保护复制的开放自由公共MA片段仍然是图灵完备的[3，10]。新贡献本文推广了Boneva和Talbot在文献[1]中的可判定性结果，证明了在弱约化的MA的开自由片段上加上名字限制时，可达性仍然是可判定的，即，当第三个无限的来源添加到片段考虑[1]。我们将得到的片段称为pMA−o。 为了证明这一结果，我们利用MA和AC项重写之间的联系。具体来说，我们证明了pMA−o中的可达性问题可以简化为一个可达性问题的地面条款和重写规则与多集变量。由此产生的重写规则满足[9]（结构保持重写）中提出的句法限制，在此条件下可达性是可判定的。这种简化需要对pMA−o语义进行一些初步的转换。更详细地说，我们首先介绍了一个新的约简关系，它以一种特殊的语法形式（称为前束形式）作用于pMA−o过程。一个进程处于前束当复制范围之外发生的所有名称限制都已在复制级别上删除时（即， ithatheformv→x. PherePhasnorrestrictionnsG. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）57WWWW外部复制）。这种转换需要一些工作，因为MA的聚集关系不提供通过移动能力移动限制的直接方式，例如，x.inp对于x/= n不是n的公理。作为第二步，我们展示了如何在新的pMA − o约简语义中将可达性问题约简为基础项的可达性问题。 术语通过映射环境n [P1|......这是什么？ |......这是什么？|... | tn⟩,其中ti是与P i相关联的项，并且|是一个结合-交换项构造器。当地代理人喜欢！P是由像q这样的常数编码的！P.编码中的关键点在于表明，考虑一组有限的节点构造函数和常数来建模pMA−o中的可达性问题就足够了。因为我们是在AC项重写中工作的，所以常数集的有限性并不意味着我们必须处理的基项集的有限性。作为一个例子，如果q0是表示零过程0的常数，那么我们必须处理q 0形式的基项的无限集合|......这是什么？ | q0. 这使得编码从pMA−oto term术语rewriting重写non平凡.如前所述，我们的结果推广了Boneva和Talbot在[1]中针对pMA−o的公共片段所做的结果。据我们所知，这是第一个积极的结果，可达性的非平凡片段的MA名称限制。相关工作在[9]中，我们研究了MA的公共片段与结合和交换（AC）项重写片段（我们称之为TUC）之间的关系。事实上，公共MA的计算机制可以很自然地用重写系统来表达，重写系统工作在多集变量项上。在[9]中，我们已经证明了基项之间的可达性（但对于具有多集变量的规则集）对于TUC的结构保持片段（称为TUCSP）是可判定的。结构保留规则不能删除树项的内部节点 然而，在这方面，它们仍然可以生产和消费树叶。在同一篇论文中，我们已经证明了TUCSP中可达性的可判定性推广了[1，3]中针对移动环境片段所获得的结果。事实上，[1，3]中研究的MA的语义和句法限制可以使用一组结构保留TUC重写规则以统一的方式重新表述。有趣的是，TUCSP具有与AC重写的其他片段（如PRS [12]和AC接地重写[11]）不同的性质。事实上，为了表达MA的移动操作，我们需要重写规则（如前一个例子中的规则），使树项与多集变量同步。这种同步规则仅限于PRS中的接地项和接地AC项重写（感兴趣的读者可以参考[9]以获得关于这一点的更详细的讨论）。8G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）51 .一、 P|0元二、 P|QQ|P3 .第三章。 （P|Q）|RP|（Q|右）4. 若P<$αQ则P<$Q5. vn. （νm.P）νm. （v n.P）第六章 vx. 0 ≡07. vx. （P |Q）可持续发展|对于x/∈ fn（P），νx.Q8. vx. （n[P]）<$n[νx.P]f或x/=nFig. 1. 同余关系m [在n.P中]|Q] |n [R] → n [m [P|Q] |R]（in）n.外，外，外|Q] |R] → m [P|Q] |n [R]（输出）开放式|n [Q] →P |Q（打开）P|！P→！P（绝对值）！P → P|！P（gen）P→QC[P]→C[Q]（context）PJ<$P P→Q Q<$QJPJ→QJ（r）图二. 还原关系：C [·]是·|R、n [·]或νx。·2Pure Mobile Ambients（MA）给定环境名称Amb的可数集合，MA过程项的集合是由以下语法生成的最小集合。P，Q ：：=0| P|Q| ! P| v x.P| n [P ] | 在N.P中| 输出| open n.P术语n [P]表示名称为n的环境。本地代理是以下形式之一的进程：0、！P，进N.P，出N.P，开N.P。在本文的其余部分中，我们使用P <$αQ表示P和Q是等价的模α-转换，fn（P）表示P中的自由名集合（所有出现在P中的不受名称限制约束的名称）。结构同余关系是满足图1所列方程的最小同余关系1.一、 注意，对于任何P和x/∈fn（P），我们有νx.P<$P。我们称这种限制是无用的。此外，我们将任何出现在范围之外的术语/操作符称为active。复制品该语言的操作语义是通过一个归约关系给出的，它被定义为满足图1中公理和规则的最小关系。2. 与Mobile Ambients的标准表示不同，！P！P|P被分成两个归约公理，即gen（生成）和abs（吸收）。这一介绍简化了下一节所研究的碎片的定义。我们用→闭包来表示→的自反传递闭包。定义2.1给定过程P和Q，可达性问题RP（P，Q）包含决定P是否→→ RP（Q）。G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）59WWWW2.1开放式移动环境如在引言中所提到的，在[1]中，Boneva和Talbot提出了一个没有开放和没有名称限制的片段的弱约简语义。根据[1]的弱约化，在这个片段中的复制只能用来产生新的过程。[1]中的结果基于以下属性：如果在这个片段中P→<$Q，那么Q的树结构给了我们一个上界在从P到Q的推导中出现的过程中可能出现的环境（发生在复制之外）的数量。事实上，如果没有开和弱归约，就不可能在推导中消费环境本文我们研究的可达性问题的一个扩展，命名为pMA−o，片段Boneva-Talbot的弱约化定义如下。定义2.2片段pMA−o是通过禁止在过程的定义中使用开放能力（open-free），并从图2的规则中删除abs和open（弱约简）而获得的。为了将[1]的结果推广到pMA−o，我们需要考虑限制和运动的语义。 考虑一个过程νn.PJ，从P到Q的推导，并假设我们使用α转换来避免与P中出现的其他限制冲突。那么，我们有三种可能的情况。（1）若n不出现在PJ中，则νn.PJ等价于PJ.（2）如果n出现在子项中n[Q]的PJ，则n发生在所有连续的配置（弱约化不允许活动环境的消耗（3）最后，更微妙的情况是当n出现在P j的子项in/out n.Q中，而它不出现在P j的子项n [QJ]中。潜在地，我们可以通过执行相应的功能来消耗名称n但是，in n和out n需要存在名为n被处决因此，在后一种情况下，进程in n.Q和out n.Q永远不会被执行（它们被死锁）。前面的性质告诉我们，如果P→nQin pMA−o，那么Q包含每个新生成的环境名的至少一次出现（或者在项n[Q]中，或者在n.P或out n.P中的死锁过程中）。因此，Q的树结构连同在复制范围之外出现在Q中的环境名称的集合可以用于具有关于树结构的大小和关于我们必须考虑以求解RP（P，Q）的名称的数量的上界。为了使这种观察成为一个正式的论点，我们引入了一类特殊的术语，我们称之为前束形式，其中所有的限制都被移动到顶层（即前束形式）。我们尽可能地挤出它们的作用域），并且我们只保留绑定在过程中某个地方出现的名称的限制。2.2前束型项P的前ex形式是项PJ（结构上等价于P），其中所有名称限制都已尽可能地在P为了找到前束形式，我们使用重写关系-定义为满足图3中规则的最小关系。前束形式的减少定义如下。10G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）5νx.P-P若x/∈fn（P）（v x.P）|Q-νx。（P |Q）如果x ∈ fn（P）且x/∈ fn（P）n[νx.P]-νx.n[P]若x∈fn（P）且xi=n在n.（νx.P）-νx. （在n.P）如果x∈fn（P）且xn出去;（νx.P）-νx. （out n.P）如果x∈fn（P）且x/=nP- QC[P]-C[Q]（context）P<$1− 5PJ-QJ<$1− 5QP-Q（r）图3.第三章。 关系~：C [·]是·|R，n [·]，M. ·，或νx。·m [在n.P中]|Q] |n [R] →n [m [P]|Q] |R]n.不，不P|Q] |R] →λm[P|Q] |n[R]P$v→yDPJ！P →→y ！P|P JP→→yQP|R→→yP|Rif→yfn（R）=P→→yQn[P]→→yn[Q]ifn/∈→yP→→yQP<$1−5PJ→→yQJ<$1−5QP→→yQif→y→x=ν→xDP→ν→xy→DQ见图4。限制约简关系定义2. 3P$PJifP-1PJ。P的前束形式PJ使得P$PJ。在前束形式的过程中，所有活动的限制都在顶层移动。为了研究前束形式的过程的性质，我们把过程P的树结构称为ts（P），它是通过去掉P中所有活动的限制出现而得到的。形式上，ts（！Q）=！Q，ts（0）= 0，ts（νx.Q）= ts（Q），ts（n [Q]）= n [ts（Q）]，ts（Q|R）= ts（Q）|ts（R），ts（M.Q）= M.ts（Q）.以下属性保持不变。命题2.4关系$modulo 1 − 5是终止的。支持2. 5如果P1$P2，则重新定义为Nam→y，因此P2=ν→y。P3、P3对检索词的生成没有任何影响，everynamemin→yoccursfrein存在Pj <$αP1使得ts（PJ）= ts（P2）.1 1命题2.6如果P1$P2和P1$P3，则P2<$1 - 5P3。在下面的表格中，我们将不会看到任何信息，也不会看到任何信息。Pin，其中P不包含限制的活动出现，例如，以隔离前束形式的顶层限制块。在图4G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）511中，我们定义了一个新的归约关系12G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）5WDerN（0）={0}DerN（n[P]）=DerN（P）DerN（M.P）={M.P}<$DerN（P）DerN（νx.P）=n∈NDerN（P[n/x]）DerN（P|Q）= DerN（P）<$DerN（Q）DerN（！P）={！P}如果P$PJ，则N（PJ）图五、过程的衍生物在前束形式的项上工作，并且其中α-重命名仅局部应用于生成规则（表示空向量）。以下属性将新的折减与标准折减相关联。命题2.7对任何P，Q，P → Q i <$P$P J−→ QJ和Q $QJ。让我们最后考虑一下pMA−o的语义。让我们首先注意到，我们可以使用仅适用于不同上下文的同余关系！P（对于归约语义）。此外，让我们重新表述公理P|0P作为以下两个归约规则P → P2P|0P| 0 →PARP由于在MA中，空环境是n[0]而不是n[ ]，因此当使用0的归约规则时，我们需要如下改进out规则的归约规则n.外，外，外|R] |Q]→m [P|R] |n [Q| 0个字符]在所得到的约简中的几个计算步骤可以对应于原始语义中的一个然而，可达性可以安全地检查在新的语义。从这里开始，我们仍然使用›→来表示修改后的归约关系。最后，给定一个过程项P和一个有限的在图5中，我们定义了在计算（导数）过程中可能变为主动的局部代理DerN（P）的集合，并且其中受限名称被N中的名称替换。对于有限集合N，DerN（P）也是有限的。 此外，我们还具有以下性质。支持2. 8IfP0›→P1.. . <$→Pn=→xnDQn，nDer→xn（P0）<${0}包含在P i中活动的局部代理的集合，其中i：0，.，n.3从移动环境到AC术语重写为了证明上一节定义的纯移动环境片段的可达性问题是可判定的，我们在AC项重写的一个特殊片段中使用了可达性的约简，称为结构保持。后一个问题是可判定的[9]。我们将在下一节介绍结构保持重写规则的语法。G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）513i=11M我04保持结构的AC项重写我们考虑一类受限的重写规则，定义在TR项上，变量范围在多项集上。为此，我们首先需要定义分别出现在规则RTL和RTR的左侧和右侧的限制项的形状。给定可枚举的变量集合V ={X，Y，. . }：在MS项上的范围：RTL是满足以下条件的项的最小集合：Q <$RTL;如果t1，.，tn∈RTL，且X∈ V，则n<$t1|......这是什么？|X∈ RT L，其中n ≥ 0。|X⟩ ∈ RTLfor n ≥ 0.此外，RTR是满足以下条件的项的最小集合：Q <$RTR;如果t1，. ，tn∈ RTR，且X∈ V，则n<$t1|......这是什么？|X∈ RT R且n ≠1|......这是什么？|... | tn⟩ ∈ RTR.给定项t，让IntNds（t）表示在t中N（内部节点/环境）中标签的出现次数。 形式上，IntNds（t）由t上的归纳法定义如下：IntNds（x）=IntNds（X）=IntNds（q）= 0对于X∈ V和q∈ Q，IntNds（t1|......这是什么？|......这是什么？|... |X）=k|X) = Σ kIntNds（ti）和IntNds（nm）=IntNds（m）+1。结构保持规则l→r是这样的，(i) l = t1|......这是什么？ | tn, and ti∈ RTLfor i : 1,...，n，(ii) r=tJ| ... | tJ且tJ∈RTR，其中i：1，.，m;(iii) l和r具有相同的变量集合V;(iv) V中的每个变量在l中出现一次，在r中出现一次;(v) IntNds（l）≤IntNds（r）。5编码可达性问题可以确定P0=→xDPJ，其中h→x=1x1， . . ，xkndP1=→x→yDPJwith0 1→y=y1， . . ，yp. 对于更多的人来说，在Pjoccurin中，→x。本文提出了一种新的可重写规则集RP（P0，P1）的可重写性算法，该算法可以对两个基本项和一个有限的项重写规则集R进行可重写性编程，该规则集R具有变量和一个关联-交换构造函数。为了处理名字，我们考虑一个连续的集合N1与n→x中的名字相关联，并且考虑一个集合N2，d与N1相关联，与n→y→x中的名字相关联。 我们定义N=N1<$N2。使用新的设计将过程编码为术语。用于表示进程的术语集TR是基于具有以下构造函数和常量符号的签名构建的：• 对于任何n ∈ N，环境n[·]由构造函数n·表示。• 并行组合由一个结合和交换的构造器表示|.常数是的单位元素|. A项t1|......这是什么？|tncan be viewed as a multiset of terms.•P0的每一个导数R都用一个常数qR表示.• 为了跟踪未使用的名字，我们将一个常数qn与每个n∈N2相关联。14G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）5W1vT（0）=q0 T（！Q1）= q！Q1T（M.Q1）= qM.Q1T（n [Q1]）= n<$T（Q1）<$T（Q1|Q2）= T（Q1）|T（Q2）见图6。 将过程编码为基本术语。从P0导出的过程P通过图6所示的归纳法定义的映射T映射到TR中的基项T（P）（即具有变量的项）。 注意，映射T不产生常数qn，其中n∈N2.我们将它们添加到初始配置中，如下一节所述。现在我们准备定义规则集R，它对DerN（P0）中的过程行为进行建模在下面的X，Y，…表示在多项集上变化的变量。• 对任意n，m∈ N，in n.Q，out n.Q∈DerN（P0），R包含：mqinn.Q|X轴|n⟨Y⟩ −→ nmT（Q）|X轴|Yn.出，出|X轴|Y −→ mT（Q）|X轴|nq0|Y这些规则是pMA−o运动运算的自然重新表述。延拓Q是常数qM中的一个标号。Q出现在左边。它变成了右手边的基项T（Q）• 为了生成一个新的副本进程！Q，我们首先把它放在它的前束形式QJ=ν→YDQ1中。这个，我们一直都很清楚， . ，q表示与q并行的未使用的名称。Q. 规则消耗这些叶子（即，N 2中的每个名称只能使用一次），并生成Q 1的实例，其中自由名称y1，.，y，v被替换为1，.，av.形式上，对于每一个q！Q∈ Q和a1，.，av∈N2，R包含：qa1|......这是什么？ | q！|q! Q−→q！Q|T（R）其中，Q$v→yDQ1 ， →y=y1 ， .. . ， yv ， ai/∈fn（ Q1 ） ，其中i：1， . . ，v ，anddR=Q1 [a1/y1，. ，av/yv]。• 为了使前面的规则起作用，表示未使用的名称的常量必须在需要时在任何环境中可用为了让常数qa（a∈N2）在环境中移动，对于任何m∈ N \ {a}，我们向R添加以下规则Qa|m <$X <$−→ m <$qa|X轴如果与N2相关的常数在初始配置中处于顶层，那么移动规则允许我们将它们分布在术语的树结构中，以便准备与生成规则同步• 最后，对于任何R∈DerN（P0）和n∈ N，我们将规则添加到RqR→ qR|q0nX → X |q0qR|q0→ qRn <$X <$|q0→n <$X <$G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）51501WWW这些规则自然地模拟了同余P|0P独立于P的结构（环境氮）。. 代理商或本地代理商qR）。由于DerN（P0）是一个有限集，并且$是终止的，那么我们总是可以预先计算定义R所需的所有项。因此，对于固定的P0和N，R是重写规则的有限集合。现在，让t表示基项的标准重写关系，即t <$tJ，如果存在R中规则的基实例l→r，使得l是t的子项，并且tJ通过在t中用r替换l而获得。 设是的自反传递闭包。然后，以下属性成立。第五点。1给定RP（P0，P1），其中P0=ν→xdPj，P1=ν→XD PJ，l∈tN1 ={n1，.，nk}，N2 ={a1，.，ap}，N = N1<$N2，设R为重写集，与DerN（P0）相关联的规则。 那么，我们有那个→xDPJ→→x→yDPJiQa|..... . 你 好 。 . |Qa| T (Q0) ⇒∗T (Q1)011p其中Q0=PJ[n1/x1， .. . ，nk/xk]，Q1=P J[n1/x1， . . ，nk/xk，a1/y1， . . ，ap/yp]。0 1从prop。5.1由此得出，pMA−o化小两个基项和有限个AC项重写规则的变量范围涵盖多个术语集。在这种简化中使用的所有重写规则都满足在[9]中引入的结构保持语法限制。该限制确保结构保留重写规则的应用永远不会从当前项中删除内部节点（构造函数的出现次数）。对于这类规则，在[9]中，我们证明了可达性可以通过进一步编码到Petri网可达性中来确定。因此，以下结果成立。定理5.2可达性在pMA − o中可判定。证据然后，它遵循的可达性的判定地面条款和结构保持AC项重写证明在[9]。Q6结论具有弱约化的MA的开放自由片段是一个具有不同无限性来源的模型：本地代理/环境的数量，环境的嵌套和名称的数量在本文中，我们证明了在这个无限状态模型中可达性是可判定这一结果推广了文[1]对于pMA−o，没有名称限制。引用[1] I. Boneva和J. - M.当环境无法打开时，塔尔博特！ TCS 333（1-2）：127-169，2005年。[2] N. Busi和G.萨瓦塔罗论纯移动环境中移动与限制的表现力。TCS 322（3）：477-515，2004年。16G. 德尔扎诺河Montagna/Electronic Notes in Theoretical Computer Science 239（2009）5[3] N. Busi和G.萨瓦塔罗决定移动环境中的可达性。在ESOP '05：248-262中[4] L. Cardelli和A.D. 戈登移动环境。TCS 240（1）：177-213，2000年。[5] L. Cardelli和A. D.戈登随时随地：移动环境的模态逻辑。在POPL[6] W. Charatonik，J. M.塔伯特移动环境模型检测的可判定性。CSL 2001：339-354。[7] W. Charatonik，S. Dal Zilio，A. D. Gordon，S. Mukhopadhyay和J.M.塔伯特移动环境模型检测的复杂性。FoSSaCS 2001：152-167。[8] W. Charatonik，S. Dal Zilio，A. D. Gordon，S. Mukhopadhyay，J-M.塔伯特模型检查移动环境。TCS 308（1-3）：277-331，2003年。[9] G. Delzanno和R.蒙塔格娜AC术语重写片段中移动环境的可达性分析。正式ASP. Comput. 20（4-5）：407-428（2008）[10] S. 妈妈和我。菲利浦纯环境结石的计算强度TCS 330（3）：501-551（2005）[11]R. Mayr和M. Rusinowitch。地面交流重写系统的可达性是可判定的。在INFINITY[12] R. 迈尔过程重写系统。INF. Comput. 156（1-2）：264-286，2000.