异步π演算中的输出前缀编码对测试语义的影响

理论计算机科学电子笔记154（2006）95-108www.elsevier.com/locate/entcs通过测试Diletta Cacciagrano1，Flavio Corradini2Dipartimento di Matematica e InformaticaUniversita`degliStudidiCamerino，ItalyCatuscia Palamidessi3INRIA Futurs Saclay andLIXE′colePolytechniquee，Frannce摘要异步π演算的早期结果之一是能够以自然和优雅的方式编码（无选择的）π演算的输出前缀，这对它的流行有很大的贡献这种编码由Honda和Tokoro，Nestmann和Boudol（独立）提出我们调查是否上述编码保存德尼古拉和轩尼诗的测试语义。从这个意义上说，事实证明，在某些一般条件下，没有输出前缀的编码能够保留必须测试。 这个否定的结果是由于（a）步骤序列的非原子性，在异步π演算中模仿同步通信是必要的，以及（b）测试语义关键词：π演算，通信，同步，异步，测试语义。1介绍近年来，异步通信范式在进程演算社区中变得越来越流行。原因包括它很容易在分布式系统中实现，并且它自然地代表了大多数Internet和Web应用程序的基本通信机制。最流行的异步演算之一可能是异步π演算[16，4]。这是π演算的一个真子集[19]，主要的困难是缺少输出前缀和选择算子。特别地1电子邮件：diletta. unicam.it2电子邮件：flavio. unicam.it3电子邮件地址：catuscia@lix.polytechnique.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.00996D. Cacciagrano等人理论计算机科学电子笔记154（2006）95[[x（y）. P]]=（νv）（x<$v|v（y）。[[P]]）[[x<$z.P]]=x（v）. （v<$z|其中，v是一个新的名字。[[x（y）. P]]=x（u）。（vv）（u<$v|v（y）。[[P]]）[[x<$z.P]]=（νu）（x<$u|u（v）.（v<$z|[[P]]），其中u，v/f∈n（P）.表1Boudol编码的输入输出规则表2Honda和Tokoro编码的输入输出规则与同步相关的输出前缀（不存在）事实上，这个结构允许我们直接表达，当一个进程执行一个输出时，它会挂起，直到伙伴执行补充输入。自然，这两种结石表现力之间的关系引起了许多研究者的关注。因为π-演算包含了异步π-演算，所以它显然至少是同样有表现力的。至于另一个方向，第三作者已经展示了一个分离结果，基于这样一个事实，即选择算子与同步通信相结合，允许我们解决异步π演算无法解决的分布式协议的某些问题[23]。然而，如果我们考虑无选择的π-演算，情况就完全不同了。[23]中的结果并没有单独说明输出前缀是否存在。事实上，Honda和Tokoro [16]以及独立的Boudol [4]已经提出了异步π演算中输出前缀的（不同的）编码，从而证明了同步通信可以通过异步通信“实现”的主张。 在这两种情况下，经由执行“相互包含”协议的一系列异步步骤的同步，该协议涉及确认消息的交换。这两种编码都是合成w.r.t.输入输出前缀和同态w.r.t.所有其他运营商。用[ ]表示Boudol提出的编码和Honda和Tokoro提出的编码，前者根据表1中的规则映射输入和输出前缀，而后者根据表2中的规则映射它们。我们在表1中给出了规则背后的直觉，表2中的规则可以类似地解释。Sup ppos e tha tww wish to builldasytembehavinglik e（xz. S|x（y）。R）。如果是同步时钟，则需要执行以下过程：写入（x<$z|S），但我们必须根据实际接收到的消息来提供子过程S。然后一个想法是通过接收一个D. Cacciagrano等人理论计算机科学电子笔记154（2006）9597确认，这是一个显式的延续，将发送方写为：SJ=（x<$z|u（v）. S）假设v在S中不是自由的。对称地，接收器将在沿着x接收到z之后立即发送确认，即：RJ=x（y）。（u¯v|R），假设u在R中不是自由的。不幸的是，我们不能独立地应用这个简单的转换，上下文，因为在该同步协议中，不存在将通信信道x与同步信道u链接的特定关系。最后一个名字应该只有发送者和接收者知道，而在这里它也可以被环境用来干扰SJ和RJ之间的通信（例如，SJ可以从环境接受u为了实现无干扰的同步，我们必须使用更复杂的协议，其中发送方和接收方在执行实际通信之前首先交换私有链接关键的观察是，由于限制，在发送者中，（vu）（x<$u|u（v）. （v<$z|（S））这是一个非常重要的问题。（v<$z|S）无法执行由某些预处理器接收的数据存储，并且此过程已通过新的数据存储器进行存储。 此外，作为发送方的私有名称的信道名称u只能在发送方和接收方之间使用。后来，在[22]中，Nestmann证明了即使是单独的选择也可以在异步π演算中编码。这比Honda- Tokoro和Boudol的结果更强，因为单独选择指的是一种保护选择的构造，其中保护可以是输入或输出前缀（但不是一起）。上述编码对异步π演算的流行做出了重大贡献，但只有一些弱正确性结果：Boudol证明了他的编码的可靠性w.r.t.莫里斯Nest-mann证明了他的编码是无死锁和无发散的[22]。在本文中，我们考虑一种语义，在我们看来，作为比较语言表达能力的基础是相当我们的选择是出于这样一个事实，即在这种语义中，当两个过程在相同的实验下给出相同的结果时，它们被认为是等价的。实验，根据并发框架，包括与给定的测试过程的相互作用。我们的主要结果是，没有上述编码保留德尼古拉和轩尼诗的测试语义。更准确地说，如果P和Q是π-演算过程，[[·]是上述映射之一，R是测试语义生成的等价，则(1)PRQ当且仅当[[P]]R[[Q]]98D. Cacciagrano等人理论计算机科学电子笔记154（2006）95坐可以公平可以公平并不普遍。为了更好地解释我们的贡献，让我们简要回顾一下De Nicola和Hennessy的测试语义学背后的一些概念。让我们假设一组测试环境，即能够执行特殊操作以报告成功的流程。进程P通过并行组合嵌入到测试环境o中。 然后，我们说，如果存在一个成功的计算，如果P和o的每一次计算都是成功的，并且P公平，（在[6，21，2]中提出），如果P和o的每次计算的每个状态在有限次相互作用后都导致成功。每一个准则都导出一个关于processes：对于任何过程P和Q，P±OQ当且仅当对于每个测试o∈ O，Psato意味着Qsato，其中sat代表可能，必须或公平。前两位作者开始研究Boudol编码的性质w.r.t.各种测试理论[8]。他们特别感兴趣的是在[·]]和R上建立条件，以使（1）成立。然而，他们意识到（1）的唯一如果部分不能用于测试理论，因为编码过程是异步π演算的严格子集。因此，用一个不是π演算中任何过程的编码的测试来测试一个过程[P]意味着用一组比P“更强大”的测试来测试[P事实上，不是编码结果的测试通常不遵循w.r.t.的“游戏规则”。通信协议，并能以奇怪的方式与之交互。在[8]中，前两位作者提出了一种改进的测试理论，只考虑右边的编码测试，并证明了Boudol(i) P±O(ii) P±OQi[P]]±[[O]]Qi[P]]±[[O]][[Q]];[[Q]]。事实上，[8]的作者证明了以下更强的结果Psatoi[P]]sat[[o]]SAT是May或Fair。本文研究了must预序。我们关注的条件，这将意味着必须版本的性质（i）和（ii），即：我们把这个条件称为必须测试。我们考虑（无选择）π演算到异步π演算的一般编码[·]。我们证明，在某些一般条件下，即组合w.r.t.前缀和发散编码项的存在，[·]不能保留必须测试。请注意，上面提到的Boudol、Honda和Tokoro以及Nestmann的所有编码都满足这些条件。问题的根源在于（原子）同步通信是-D. Cacciagrano等人理论计算机科学电子笔记154（2006）9599可以在异步世界中模拟发送器和接收器之间的通信，但是没有办法保证发送器和接收器将同时恢复（在通信之后）。更准确地说，可能是这样的情况，当发送方准备继续时，接收方仍然参与协议的某些部分因此，存在不公平的计算，其中一个合作伙伴永远不会恢复，并且在通信之后，基于与该合作伙伴的交互的测试不会成功。在通信伙伴同时恢复的同步世界中，这当然不是问题事实上，我们的结果适用于一般类的编码指出，我们的意见，异步通信的同步一个固有的缺点。本文的其余部分组织如下。第二节介绍了π-演算和异步π-演算。第3节正式定义了必须测试。第4节回顾了一些关于编码的基本定义。第5节证明了我们的主要结果，第6节研究了它的一些结果。由于篇幅所限，本文省略了证明的细节。感兴趣的读者可以在本文的完整版中找到它们[10]。2π演算与异步π演算在这一节中，我们简单地回顾了（无选择）π-演算和异步π-演算的基本概念。2.1π演算令N（由x，y，z，.. . ）是一组名称。 集合Ps（范围为P，Q，R，... . ）由以下语法生成：P：：=0x（y）.Pτ.Px'y.PP|P（v x）P ！P输入前缀y（x）.P和限制（νx）P充当P中名称x的名称绑定器。P的自由名fn（P）和束缚名bn（P）的定义与通常一样。P的名称集合被定义为n（P）=fn（P）bn（P）。当fn（P）= 0时，称P是闭的。进程的操作语义是通过一个标记的变迁系统给出的标签（以μ、γ、.. . ）cor-respond to oprefixes，输入x-ray，输出x-ray 和taut，并通过bounded d o t-putx-ray（其中model s可执行x-ray）。 如果μ=xy，则定义了sub（μ）= x和obj（μ）= y。函数fn、bn和n被扩展以处理如下标签：bn（x<$y<$）={y}bn（x<$$>y <$）={y}bn（x<$y）=<$ bn（τ）=<$fn（x<$y<$）={x}fn（x<$y<$）={x}fn（x<$y）={x，y}fn（τ）=<$100D. Cacciagrano等人理论计算机科学电子笔记154（2006）95−→Pμ（P=P），我们写P= −→输入x（y）.P−→P{z/y}其中x，y∈ NOutput/Taua。P−α→P，其中rα=x<$y或rα=τxzx′yμ开放P−→PJ（νy）xyx/=yResP−→PJ（νy）P−→μy/n∈（μ）ParP−→PJP|Q −→ P J|Qμμbn（μ）fn（Q）=xyxyxy网P −→ PJ，Q −→QJP |Q − τ → PJ|QJP−→PJx′yP−→PJ，Q −→QJ密切P|Q −τ→（νy）（PμPPJμBangμ聪PJ−→QJQJ<$QP−→Qμa1）PQiQ可以通过α重命名从Pa2）（Ps/s，|，0）是交换幺半群a3）（（νx）P|Q）（νx）（P|Q），ifx/f∈n（Q）a4）（νx）P<$P，ifx/f∈n（P）a5）（νx）（νy）P<$（νy）（νx）P表3中给出了过渡关系。“从律”中的符号“从”代表结构一致性。这是由表4中的公理导出的集合Ps上的最小同余。表3P s术语的早期操作语义。表4结构一致性。定义2.1（弱转移）设P和Q是Ps过程。然后又道：- P=εQ当且仅当存在P0，P1，.，Pn∈Ps，n≥0，使得P= P0−τ→ P1−τ→. −τ→ Pn= Q;μ- P=<$Q当且仅当存在P1，P2∈ Ps使得P=εPμP=εQ .1−→记法2.1有时我们写Pμ2μ）表示存在PJ使得PJμJ−→（P= 0εμ意味着有PJD. Cacciagrano等人理论计算机科学电子笔记154（2006）95101−→Outputx<$y−→0x′yτ.P−→Pτ和Q满足P=εPJ和PJμQ. 我们有一个P驱动器，旋转P↑，如果存在从P到τ跃迁的无限序列，即P=P0−τ→P1−τ→. . . Pi−τ→Pi+1−τ→. . . 对于P0，P1， . . . Pi，Pi+1， . ..我不想坐在这里，我。e.If我们说P收敛，记作P ↓。2.2异步π演算异步π演算的进程集合PaP：：=0x（y）.Pτ.Px′yP|P（v x）P ！PP a的操作语义由表3中的规则给出，其中规则Output/Tau由表5中的规则Output和Tau替换。定义结构全等的公理与表4中的公理相同。表5P a中的输出和Tau的规则。同步设置中给出的定义和符号也适用于异步设置。注意，异步π演算是π演算的子集。我认为，我们的put-actionprocesssy不能作为我们put-prefixy的特殊情况。0.3必须预订在本节中，我们简要总结了π-演算测试方法背后的基本定义。在下文中，P将表示Ps或Pa。定义3.1（观察员）- 设N J =N <${ω}是名称的集合。 按照惯例，我们让fn（ω）={ω}，bn（ω）=ω，sub（ω）=ω。 动作ω用于报告成功。- 集合O（由o，oJ，oJJ，. . ）的定义类似于P，其中文法被扩展为产生式P：：=ω.P。- P的操作语义通过定义该规则ω来实现。o−ω→o 。在下文中，我们将用P来表示P的某种限制形式，即任何形式为（νx1）（νx2）.的过程。（v xn）P，对于某个x1，.，xn∈fn（P）.定义3.2（最大计算）给定P∈ P和o∈ O，|或者是无穷序列P|o= 0.0000|o0π−τ→πP1|o1π−τ→πP2|o2π−τ→. . .102D. Cacciagrano等人理论计算机科学电子笔记154（2006）95或有限序列P|o= 0.0000|o0π−τ→πP1|o1π−τ→. . −τ→πPn|on−/τ→。我们现在准备好呈现必须测试语义的定义。定义3.3（必须语义给定一个过程P∈ P和一个观察者o ∈ O，定义P必须o当且仅当对于每个最大计算P |o = 0.0000|o0−τ→CIP1|o1π−τ→. . Pn|on[−τ→. . . ]theexisi≥0 suchhatpi|oi−ω→。注意，对于每个P∈ P和o∈ O，P必须是ω.o。4将pi演算编码为异步pi演算在本节中，我们回顾一些关于编码的概念。一般来说，编码只是语言之间的语法转换。我们将关注π演算到异步π演算的编码，我们将使用符号[[·]]：Ps→ Pa来表示一个这样的变换。一般来说，一个“好”的编码满足了一些额外的属性，但是对于“好”编码的一般概念还没有达成一致。也许确实不应该有一个独特的概念，而应该有几个，这取决于目的。无论如何，在本文中，我们专注于最常见的要求，这是组合性w.r.t.某些运算符，和正确性w.r.t.给定的语义。为了描述组合性，我们使用上下文C[ ]，它是Pa中具有一个或多个给定P1，...，Pn∈Pa和具有n个洞的上下文C [ ]，C [P1，.，Pn]表示通过将[ ]的出现替换为P1，.，Pn。定义4.1（相对于设op是Ps的n元算子。我说：“我们的故事，是一部经典。op当且仅当在Pa中存在上下文Cop[]，使得[[op（P1，. ，Pn）]]= Cop [P1]]，. ，[[Pn]]。请注意，组合性的一个特殊情况是同态，其中源语言上的运算符映射到目标语言上的运算符，即Cop[ ] =opJ。通常，同态仅对某些运算符是必需的（通常，在分布式语言中，它对并行构造是必需的），对于其他的，我们只需要一个合成翻译。关于语义正确性，我们考虑保留必须测试：定义4.2（可靠性、完整性和必须保持性）设[·]]是从Ps到Pa的编码，我们说[·]]是：- 声音w.r.t.必须 i <$$>P∈Ps，<$o∈ O，[[P]]must[[o]蕴涵Pmusto;- 完全w.r.t.必须 i <$$>P∈Ps，<$o∈ O，Pmusto蕴涵[P]]must[[o]];D. Cacciagrano等人理论计算机科学电子笔记154（2006）95103- 必须-保存 i[·]]是健全和完整的w.r.t. 必须的5不存在必须保持和输入输出前缀组合编码这一部分是论文的核心部分。我们证明了一个一般的负面结果的一大类编码的π演算到异步π演算，其中包括Boudol的，本田和Tokoro，和Nestmann。我们的主要结果表明，任何编码[·]，即组合w.r.t.输入和输出预置并产生至少一个发散项，不能是必保的。这个否定的结果是（a）异步π演算中模仿同步通信所必需的步骤序列的非原子性，以及（b）测试语义我们注意到，我们只需要很少的假设就可以得到这个不可能的结果。特别是，我们不需要同态，也不w.r.t.并行运算符，也不是w.r.t.任何其他运营商。定理5.1设[·]是一个编码，满足：1. 相对组合性 输入和输出预置，2. P是P，P是P，P是P。[1][2][3][4][5][6][7][8][9][9][10][11][10][11][12][12][13][14][15][16][17][18][19][19][10][19][10][19][19]为了澄清这个结果背后的直觉，我们可以展示当[·]]是Boudol的编码时会发生什么，C n s i d e e P p p p p d e d e d a s P = a a n e d e d e d e d e e。 ！τ。0，且观察者0 = a. 0. 那么唯一的一个最大的计算，|o可以执行P|o=a<$。 ！τ。0|a. ω。0-τ→！τ。0|ω。0−τ→. . . −τ→0 |0|.... . . 你 好 。 . |！τ。0|ω。0−τ→. . .当然，P必须是O。 现在，考虑[P|o]]=[[P]]|[注]。考虑以下最大计算：[[P|o]]=[[ a <$. ！τ。0]]|[[a. ω。0]]=（νu）（a<$u|u（v）. （v<$|[[！τ。0]]））|a（h）。（vk）（h<$k|K. [[ω. 0]]）（vu）（vk）（a<$u|u（v）. （v<$|[[！τ。0]]）|a（h）。（hk|K. [[ω. 0]]））−τ→（νu）（νk）（0|u（v）. （v<$|[[！τ。0]]）|乌克|K. [[ω. 0]]）−τ→（vk）（k<$|[[！τ。0]]|K. [[ω. 0]]）=（νk）（k<$|！ [[τ。0]]|K. [[ω. 0]]）−τ→（vk）（k<$|0|！ [[τ。0]]|K. [[ω. 0]]）−τ→（vk）（k<$|0 |0|！ [[τ。0]]|K. [[ω. 0]]）−τ→... ... − τ →（vk）（k<$|0 |0|.... . . 你 好 。 . |0|！ [[τ。0]]|K. [[ω. 0]]）−τ→104D. Cacciagrano等人理论计算机科学电子笔记154（2006）95... ... − τ →注意，计算的每个中间状态不能执行任何ω操作。Hence，[P]]m/ust[[o]].6其他不可能的结果编码的目标语言中的发散过程的存在，这是定理5.1的假设之一，可以通过对编码本身的适当假设和必须测试的保留来保证本节研究的条件尽可能弱的编码下，必须保存的输入和输出前缀意味着不存在必须保持的编码。下面的定理指出，源语言中存在一个发散项和一个收敛项，其编码不与上下文相互作用，这是一个充分条件。定理6.1设[·]是一个编码，满足：1. 相对组合性 输入和输出预置，2. Q∈ Ps使得Q ↑和fn（[[Q]]）=3. R ∈ Ps使得R ↓且fn（[[R]]）= fn。[1][2][3][4][5][6][7][8][9][9][10][11][10][11][12][12][13][14][15][16][17][18][19][19][10][19][10][19][19]下面的定理指出，对于不可能结果，具有同态w.r.t.τ-前缀。注意，我们w.r.t.爆破操作员。同态w.r.t. τ前缀和bang都直接暗示目标语言中存在发散过程。定理6.2设[·]是一个编码，满足：1. 相对组合性 输入和输出预置，2. 关于同态τ-prefix，则[·]]不是必保的。在我们看来，下一个结果是最令人惊讶的。它指出，如果τ的编码是保必的，则压缩编码不能是保必的。[ ]和0不与环境交互。定理6.3设[·]是一个编码，满足：1.相对组合性输入、输出和τ前缀，2。fn（[τ. []]）=fn（[[0]]）= 0。[1][2][3][4][5][6][7][8][9][9][10][11][10][11][12][12][13][14][15][16][17][18][19][19][10][19][10][19][19]D. Cacciagrano等人理论计算机科学电子笔记154（2006）951057相关工作许多论文研究了几种通信机制的表达能力文献中的标准方法是定义配备两种通信机制的语言之间的编码，并验证是否存在完全抽象结果w.r.t.意图的语义。 如果我们特别考虑同步和异步通信，几种语言和演算器运算符可以实现第一种或第二种机制。最流行的演算是用于同步通信的π演算及其变体和用于异步通信的异步π演算及其变体[23]中比较了混合选择π演算和异步π证明了在保持合理语义的前提下，不可能将π演算映射为具有统一编码的异步π演算我们注意到，Boudol然而，我们的负面结果w.r.t.这不是[23]中的结果的结果。事实上，后者是相对于混合选择的存在，而我们不考虑选择在我们的源语言。[23]中的分离结果不适用于我们在这里考虑的两种语言。试图证明一个完整的抽象结果的编码，介绍了一个通信协议（如Boudol，本田和Tokoro，和Nest- mann）涉及一个一般的困难：存在，在目标语言中，不遵循协议的规则的条款。因此，例如，这些编码不能完全抽象w.r.t.倒钩同余下面的例子，由洪德和Y提供，显示了[17]，例如： Cniderh e process e sP=xy. x'y. 0和Q=x<$y。0|x'y. 0的情况。 这是一个干净的、有弹性的结构。 [P]]和[Q]]（其中[[·]是例如Boudol的编码，参见表1）是不全等的，因为如果我们考虑R=x（y）。0，R| [[P]简化为一个过程，它不具有一个x′ barb，而这不是R的情况|[[Q]]。 No thatR是一个不“遵循协议规则”的进程，因为它不向[ P ]]发送u上的确认（参见表1），这就是[ P ]]卡住的原因。在文献中，我们找到了解决上述问题的各种方法。通常，可以限制目标语言的上下文，或者对其语义施加某些限制。其中一篇使用上下文限制的论文是[24]。作者认为多元π演算和一元π演算的异步版本分别作为源语言和目标语言，Boudol式编码和异步倒钩同余作为要保留的语义。他们考虑了一个类型系统，允许他们消除不尊重编码的“同步协议”的上下文w.r.t.源中的任意上下文和目标中的可输入上下文。 前两位作者在[8]中探讨了类似的问题。测试语义主要区别是w.r.t.[24]在[8]中，对上下文的限制更为激烈：事实上106D. Cacciagrano等人理论计算机科学电子笔记154（2006）95由于测试语义的定义，唯一相关的上下文是并行测试过程。Fuelman [8]只考虑源语言编码过程中产生的测试。文[8]证明了Boudol编码是完全抽象的可以和公平的测试，但不是w.r.t.必须测试。值得注意的是，对编码上下文的限制足以证明Boudol的编码w.r.t.莫里斯异步倒钩同余（这可以通过查看[24]中引理17的证明来轻松检查）。 另一方面，对于[24]的上下文，完整性结果，即另一个类似的问题是[15]。本文主要研究ν-演算，它是异步π-演算的一个子集，其中只有输入保护项可以在bang算子的作用域中。请注意，这不是一个真正的限制，因为这种复制子与全爆炸算子一样具有表达力[20]。考虑了两种操作语义：第一种称为第二种称为本文考虑了具有同步和异步语义的ν-演算的两种编码，每种编码对应一个方向.然后证明第一个编码是完全抽象的w.r.t.。弱互模拟的异步语义的一些限制。更确切地说，它只考虑那些由原始过程的“编码”痕迹产生的编码过程的痕迹。第二种编码是完全抽象的w.r.t.弱互模拟，这是由于编码通过将术语与称为身份受体的特殊过程并行来削弱术语。在[16]中，作者考虑了[15]中的两个操作语义，用于v-演算的变体，通过用递归替换bang获得。除了[15]的结果外，[16]还证明了异步演算中的弱互模拟严格弱于同步演算中的弱互模拟，并且可以通过削弱同步演算来消除这个差距，如[15]中所提出的。还有其他几种演算实现了特定的通信机制例如，逻辑和物理局部性，远程通信，高阶通信，等等。作为一个例子，我们提到Klaim，一个异步语言与编程原语的全球计算，通过结合的特点，从进程代数和协调语言。在[12]中，作者研究了Klaim及其一些子语言的表达能力。通常，这是通过定义从一种语言到另一种语言的编码，并通过研究每个编码的完全抽象结果来完成的。倒钩双相似性和倒钩同余。特别值得注意的是，存在一种将异步π演算编码为Klaim变体的编码。后者是通过从克莱姆那里去除准备的基本行动、逻辑和物理场所之间的区别以及更高秩序和多元交流的可能性而获得的。D. Cacciagrano等人理论计算机科学电子笔记154（2006）95107是的。此编码的完整抽象结果w.r.t.由于对目标语言中的编码上下文的限制，再次获得倒钩等价8结论和今后的工作在本文中，我们研究了输出前缀在π演算w.r.t.的异步版本中的可编码性。必须测试语义。我们的主要结果是，如果编码满足一些一般要求，即组合性，w.r.t.前缀和发散编码项的存在，则它不能保留必须测试。这个否定的结果是（a）异步π演算中模仿同步通信所必需的步骤序列的非原子性，以及（b）测试语义作为未来的工作，我们计划调查的可能性，积极的结果下，一些尝试公平性假设的想法来自于这样一种观察，即必须测试的负面结果本质上是当然，如果我们对计算的所有部分都施加公平性，那么我们必须对源语言和目标语言都施加公平性，以便编码保持语义。这将削弱预期的结果。为了避免这个问题，我们计划只对异步计算施加公平性，更具体地说，只对那些属于模拟的动作施加公平性。我们还计划研究本文的结果是否适用于广播与点对点通信。引用[1] M. 博雷阿莱河德·尼古拉。移动过程、信息和计算的等价性测试120页。279-303，1995年。[2] M.博雷阿莱河德尼科拉河普利亚人 过程的基本可观测性，LNCS1256，pp。 482-492，1997.[3] M. 博雷阿莱河德尼科拉河普利亚人异步进程中的跟踪和测试等价性信息与计算172页139-164，学术出版社，2002年。[4] G. 布多异步和π演算，技术报告1702，INRIA，Sophia-Antipolis，1992年。[5] F.S. de Boer，J.W.克洛普角Palamidessi。进程代数中的异步通信，Proc. of LICS137-147，1992年。[6] E. Brinksma，A. Rensink，W.沃格勒公平测试，CONCUR313-327，1995年。[7] D.卡恰格拉诺Comunicazione Sincrona ed Asincrona in Sistemi Concorrenti e Distribuiti，MasterThesys，University of[8] D. Cacciagrano，F.科拉迪尼On Synchronous and Asynchronous Communication Paradigms，Proc.of ICTCS256-268，2001。[9] D.卡恰格拉诺On Synchronous and Asynchronous Communication：Some Expressiveness Results，PhD Thesys，University La Sapienza of Rome，2004.[10] D. Cacciagrano，F.科拉迪尼角Palamidessi。同步和分离通过测试实现异步通信，技术报告，在线http://portalcs.unicam.it/flavio.corradini，Camerino大学，2005年。108D. Cacciagrano等人理论计算机科学电子笔记154（2006）95[11] I. 卡斯特拉尼湾轩尼诗异步语言的测试理论。FSTTCS1530年，第1530页。90-101，1998年。[12] R. De Nicola，D.戈尔拉河普利亚人基于KLAIM的演算的表达能力，Proc. of EXPRESS[13] R. De Nicola，M.轩尼诗测试过程的等效性，理论计算机科学34，pp。83-133，1984年。[14] M.轩尼诗 过程的代数理论，麻省理工学院出版社，剑桥，1988年。[15] K. 本田关于ν-演算的两个双相似性，庆应义塾大学计算机科学系，1992年。[16] K.本田，M.时郎异步通信的对象演算，Proc. of ECOOP133-147，1991年。[17] K. 本田，N.吉田个人通信，2005年。[18] R. 米尔纳通信与并发，Prentice-Hall International，1989。[19] R. Milner ， J. Parrow ， D. 沃 克 A Calculus of Mobile Processes ， Part I and II ， Information andComputation100，pp. 1-78，1992年。[20] M. Merro，D.桑吉奥吉关于名字传递演算中的隐式结构，Proc.of ICALP[21] 诉纳塔拉扬河克里夫兰 分歧和公平测试，Proc. ICALP '95，LNCS 944，pp. 648-659，1995。[22] 联合内斯特曼什么是保护选择的“好”编码？信息与计算156页287-319，2000。[23] C. Palamidessi。比较同步和异步π演算的表达能力，计算机科学中的数学结构13（5），pp。685-719，2003。1997年《人民权利公约》会议记录中载有初步文本[24] P. 夸利亚D。沃克 在同步和异步移动进程，Proc. FOSSACS 2000，LNCS 1784，pp. 283-296，2000。