互动空间：理论与实现的中间模型

理论计算机科学电子笔记154（2006）63-82www.elsevier.com/locate/entcs交互空间弗雷德里克·佩尚斯基皮埃尔和玛丽·居里大学-巴黎6-LIP 6摘要移动代理系统的推理和实现是一个既困难又安全的问题。理论工作，特别是进程演算，为移动系统提供了坚实的语义。然而，理论往往过于抽象，无法与实际实现的要求相匹配。为了填补这一空白，必须提出中间模型。在本文中，我们提出了这样一个模型命名为互动空间，几何空间中的代理人通过简单的变换进行交互的隐喻。该框架捕捉高层次的分布式语义，最显着的异步，FIFO通道上的多播通信。 它还改进和实现了pi演算的通道传递功能，以及代理本身的移动性。在交互空间之上，我们提出了一个全边代理演算及其相关的操作语义.保留字：移动Agent，过程演算，几何空间1介绍代理系统涵盖了大量的研究领域，从系统级方面到人工智能，语言语义学中的重要问题。从技术的角度来看，代理系统很难推理和有效安全地实现。首先，代理演变在大规模的并发和分布式环境。它们还支持各种动态特性。我们在本文中集中讨论流动性这一重要议题。 一方面，诸如π演算[10]或移动环境等理论[3]建立流动性的基础。另一方面，许多实际的实验和原型平台说明了移动代理系统在现实世界中的兴趣和可行性，但也存在困难[6]。尽管在该领域有大量的贡献，但还需要更多的贡献来填补理论和实践之间的差距。抽象演算的应用变体构成了一些分布式实现的基础（包括Nomadic1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.03364F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）63[14]和Jocaml [5]）。这些为在分布式环境中正确、高效地执行移动系统提供了坚实的基础。但这些工作大多只支持相当有限的交互语义。第一个限制是，大规模系统的基本要求是通过不允许输出预置来提供的。这意味着一个进程可能不会在本地执行因果相关的输出序列，这与大多数现实世界的通信协议（如TCP）相矛盾。关于移动性的另一个重要限制是局部性[9]，它避免了在运行时传输通道的输入容量。在某种程度上，这将π演算的传统减半，只保留了移动性的“写”方面。我们还发现大多数相关工作的点对点通信模型相当令人沮丧，并且有利于多播语义，这在理论和实践中都取得了重大进展[4]。为了同时利用所有这些限制，我们引入了互动空间模型.所提出的语义在FIFO通道上实现多播通信，同时具有缓存和输出预处理。还支持通道末端的非本地移动性（即虚拟移动性）和通道状态的非本地移动性（即物理移动性）以及整个代理的移动（即迁移）。该模型的独创之处在于它使用了几何空间的隐喻，在几何空间中，智能体通过简单的变换（扩展、平移等）进行交互，这为我们提供了对智能体特征的直观而又具有教育意义的解释。在直觉之外，这使我们能够依赖于一组简化的基本概念和公理，我们可以用几何术语来说明和证明。当然，如果与更抽象的演算相比，这使得语义更加复杂。例如，一个智能体可以表示不同的行为，这取决于它在其中演化的特定交互空间。一个技术上的贡献，我们也认为原来是展示如何将这种上下文信息集成在相当标准的操作语义标记的过渡系统（LTS）和互模拟的基础上。论文的提纲如下。作为第一步（第2节），我们定义了交互空间的基本模型，提供了几何隐喻及其语义。几何学和它的相关演算之间的一个重要步骤是空间组成，这在第二节3. 然后，我们在第4节中介绍代理演算本身。 介绍是相当经典的一个变种的π演算。主要的结果是一组行为等价物和相关的属性，支持组合推理代理的行为。F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）6365定义中，n =C是C的幂集，N和Z是通常的整数集。位置Fig. 1. 相互作用空间2相互作用空间如图1所示，交互空间由位置（或代理身份）的维度L、通道（或通道身份）的维度C以及位置和通道的每一对l，c，行为（或通道状态）的维度A它们的内容由两种信息组成：• 集合V中的值，其填充动作A的维度，反映代理之间传输的数据的内容• C=^{read，write，lfalil，cfalil}，其可用于装饰信道或位置参考来维护控制级信息，渠道的所有权颜色lfail和cf ail分别处理位置和通道故障。我们没有提出完整的故障语义的文件。然而，我们注意避免在故障信道上通信和在故障位置上移动.正式定义如下：定义2.1相互作用空间，通常记为Δ，是一个多维空间。在E=^中分配包含值和颜色的集合N2→NC×（ Z→ V）。在这2.1变换和投影相互作用空间及其内容通过展开ED（在每个可能的维度D中）和初等变换来操纵，这些初等变换被归类为单位平移TD（在维度D中）、颜料Pc和反演Pcb（颜色c）以及填充Fv（值v）。变换可以使用符号θΘJΔ来组成，其中Δ首先被Θ j变换，然后被Θ变换。定义2.2我们定义相互作用空间Δ的各种投影：行渠道L1L2L3EDC66F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）63^ ^您的位置：^ ^您的位置：• Δ（L<$LΔ，C<$CΔ）<$C×（Z→V）• Δ（l∈ LΔ，c∈ CΔ）∈<$C×（Z →V）• fst（Δ（l∈L，c∈C））∈CΔ Δ• snd（Δ（l∈ LΔ，c∈ CΔ））（a∈ AΔ（l，c））<$V.最简单的一个是在给定位置l和通道c上的投影，其中Δ（l，c）。一个特定交集的行为的颜色和维数分别记为fst（Δ（l，c））和snd（Δ（l，c））。行为的维度的域记为AΔ（l，c）。 投影子空间可以用作对变换，记为（T，δ）Δ，其中空间Δ被变换只在它的子空间δ中。最后，空间Δ的位置和信道恒等式的集合分别记为LΔ和CΔ定义2.3相互作用空间Δ∈E的维数为：• LΔ=^fst（dom（Δ）），l〇caion的尺寸• CΔ=^snd（dom（Δ）），其中，• AΔ（l∈LΔ，c∈CΔ）=^dom（snd（Δ（l，c）adimensionsofacts2.2新鲜度新鲜度的概念在进程演算中讨论私有名称时至关重要。在流动性的存在下，新鲜感的实现是一个困难的方面，有些人为的公理的干预，例如，用于内窥镜挤出[10]。我们的目标是以纯粹的几何术语来解决新鲜度问题。 两个不同的要求与新鲜度有关：(1)新频道的创建，以及（2）新位置的创建。为了创建一个新的位置，我们必须在维度中扩展一个给定的空间L的位置。新创建的位置的标识是基数在原始空间中的维度。我们定义了以下用于新鲜创作的复合变换：newloc（Δ）=ELΔlocref（Δ）=card（LΔ）−1newchan（Δ）=ECΔchanref（Δ）=card（CΔ）−1必须建立的新鲜度属性是：（fresh-location）locref（newloc（Δ））∈ LΔ（fresh-channel）chanref（newchan（Δ））/∈ CΔ2.3动态示波器交互系统的结构通常在非正式的层面上使用图来描述[10]。图2（a）示出了一个流程图及其对应的-F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）6367L3CL1CL2L3L2^L1→(a) 初始流速图(b) 更新的流程图图二. 图表示法互动空间。代理（或位置）使用圆圈和箭头通道表示。通道端点使用点和箭头描述。在该图中，通道c对接到代理l2，代理l 2因此可以执行发射。通道c还链接到代理l1和l3。它们都可以接收c上的信息，这表示多播交互。在π演算中，交互空间支持动态的通道图，其中通道端动态地从代理移动到代理。在图2（b）中，c的dock和link属性被修改。为了模拟这种修改，我们使用颜色和油漆变换。使用颜色写入绘制停靠到位置l的通道c的交叉点。这在图中显示为黑色路面。链接的位置由颜色表示，由蓝色路面表示。我们定义函数来获取和设置通道和位置的特定交叉点处的颜色，如下所示：cget（Δ，l，c）=^fst（Δ（l，c））cset（Δ，l，c，c〇l〇r）=^（Pc〇l〇r，Δ（l，c））Δcunset（Δ，l，c，c〇l〇r）=（Pc^ol〇r，Δ（l，c））Δ预期属性为：（cset-安全）color∈cget（cset（Δ，l，c，color），l，c）（cunset-safety）color/∈cget（cunset（Δ，l，c，color），l，c）2.4通信一旦使用对接和链接操作建立了正确的流程图，就可以执行代理之间的通信。我们在图3（b）中说明了表示为白色立方体的信息的发射。多维数据集由代理l2发出并在通道c（停靠到l2）上传输。立方体的副本被放置在通道c链接到的每个位置（即，l1和l3）。为此L1L2L3CL1CL2L368F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）63L1L2L1L2CL1L2C^^^L3C→(a) 初始空间L3(b) l2在c(c) L2L3在C上发射→(d) L3L3在C上接收图三. 交互空间中的通信模型我们首先需要扩大有联系的代理人的行为范围，包括：link ed（Δ，c）=^{l∈LΔ|read∈cget（Δ，l，c）}newact（Δ，c）=^l∈linked（Δ，c）EAΔ（l，c）一旦空间被扩展，我们可以通过填充通道的链接代理的子空间来为此，我们写道：mcast（Δ，c，v）=^[Fv，snd（Δ（l，c））（max（AΔ（l，c）] Δl∈linked（Δ，c）然后，我们必须结合前面的两个转换来执行完整的发射，如下所示：send（Δ，c，v）=mcast（newact（Δ，c），c，v）在图3（c）中，我们描述了由同一个代理l2发送另一个表示为黑色立方体的信息的效果。这就好像立方体堆叠在前一个立方体上，引入了一个顺序关系。接收过程如图3（d）所示。在这里，代理l3正在执行接收。要接收的值是坐标snd（Δ（l3，c））（0）处的空间中的点，其对应于通道c位置l3。 下面的投影通常会得到这个值：fetch（Δ，l，c）=snd（Δ（l，c））（0）为了用几何术语进行接收，我们必须在行为的维度上平移一个单位，我们写为：receive（Δ，l，c）=（TA，snd（Δ（l，c）Δ请注意，值一旦被获取，就不会从交互空间中消失。行为维度中负坐L1L2CF. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）6369标的子空间精确地表征了相互作用的历史。主要要求是实施者--70F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）63L1L2^FIFO的语义：（send-fifo）<$l ∈linked（Δ，c），令Δ使得AΔ（l，c）=<$，令ΔJ=send（send（Δ，c，v1），c，v2），然后fetch（ΔJ，l，c）=v1并且fetch（receive（ΔJ，l，c），l，c）=v22.5移动性交互空间模型支持两种最常见的移动性形式：代理移动性（所谓的迁移）和通道移动性。我们已经讨论了动态图的实现，类似于pi演算中实现的移动性。如我们在[8]中所讨论的，可以有效实现的通道状态的孤立运动在实践中也具有很大的意义。在语义学中，这对应于定义如下的简单翻译：xfer（Δ，c，l1，l2）=（TL，Δ（{l1，l2}，c））Δ，其中l1 λ−1<$σλ<$（Δ<$λ，γΓ）<$<$Δ<$P <$ Γ <$Q <$Δ <$λ，γΓ<$P<$（Q）<$◦γ−1◦ σγ（Δλ，γ r）（SC4）ΔP+QΔQ+P，ΔP+0ΔP（SC5）如果D（x）=P（SC6），则ΔD（y）ΔP{y/x}表2结构同余LTS转换由代理执行的可观察动作标记可观察的动作是语法中的动作（见表1），除了init和new，它们是不可观察的，并且与内部步骤τ一致。通过可观察，我们的意思是在语言中可观察的，因为new和init修改了交互空间，因此具有可观察的效果。一个动作α位于L中的标记为α@L。动作的位置在语法中是可选的，但在语义中是必需的[12]。公理A1、A2和A3描述了所有无声和可观察动作的基本语义。如规则A3所述，一个项的相互作用空间部分通过观察是显著不变的。只有内部操作可能涉及上下文转换。基本公理A1、A2和A3必须是⎢⎣78F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）63Δφinit（l）{Q}@l.P−τ@→l2new loc（Δ）φ（Pφ[Q]@l）{locref（Δ）/l}（A1）1 2 1 1Δλnew（c）@l.P−τ→@l（A2）newchan（Δ）P{chanref（Δ）/c}Δα。P−α→ΔΔPΔP−α→ΔJ<$PJ（A3）对任意作用α/∈ {init，new}ΔP−α→ΔJ<$PJΔ<$P<$Q−α→ΔJ<$PJ<$Q（O1）Δ<$P+Q−α→ΔJ<$PJ（O2）P<$PJΔ<$P−α→ΔJ <$QQ<$QJΔ<$PJ−α→ΔJ<$QJ（O3）表3运营商由语言的基本运算符规则组合：并行（规则O1）和选择（规则O2）组合。我们可以通过专用规则O3注意到与结构全等的联系。这些定义是过程代数的经典定义。4.3减小规则表4的规则告诉我们，在特定的交互空间环境中，如何从可观察到的动作的发生中推断出无声的步骤或减少规则可以用附加条件修饰。例如，规则S1规定不能在链接的通道上执行停靠。只允许在已停靠到同一位置的情况下取消停靠（规则S2）规则S3及用于链接的S4以类似的方式操作此外，代理可以执行发射（规则C1）在给定的通道，只有当它是对接到该位置。规则C2描述了代理在正确链接的信道上的接收。这些限制强制执行一个不干涉的纪律，其中代理人不得在通信发生时干涉其他代理。通过规则M1和M2在语义上实现了代理和通道状态的移动.跳跃动作仅适用于既未停靠也未链接到任何位置的通道。基本原理是，跳跃动作的潜在竞争条件也不应该干扰通信。go动作不需要这样的约束，因为新的位置被用作目标。F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）6379−→−→−→−→ΔPdock（c）@lΔPJcget（Δ，l，c）/={read}（S1）ΔφP−τ@→lcset（Δ，l，c，write）φPJΔPundock（c）@lΔPJcget（Δ，l，c）={write}（S二）ΔφP−τ→@lcunset（Δ，l，c，write）φPJΔPlink（c）@lΔPJcget（Δ，l，c）/={write}（S3）ΔP−τ→@lcset（Δ，l，c，read）PJΔPunlink（c）@lΔPJcget（Δ，l）={read}（S4）ΔφP−τ@→lcunset（Δ，l，c，read）φPJΔPc−！v→@lΔPJcget（Δ，l，c）={write}（C1）ΔP−τ→@lc？（x）@lΔPΔsend（Δ，c，v）PJJ−→ΔPcget（Δ，l，c）={read}（C2）ΔP−τ→@lreceive（Δ，l，c）{fetch（Δ，l，c）/x}go（l2）@l1ΔP−→Δ ► PJ（M1）ΔφP−τ@→l1move（Δ， l）φP{locref（Δ）/l}1 2leap（c，l2）@l1ΔPΔJ−→ΔPcget（Δ，l2，c）=Δ（M2）ΔφP−τ@→l1xfer（Δ，c， l， l）φPJ1 2表4.裁减规则4.4行为等价代理演算的LTS特征表示项上的行为等价性。这样的数学结构是比较和推理代理行为的基础。我们首先将互模拟的共同概念与交互空间的特定设置联系起来：80F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）63定义4.1相互作用空间中的A（强）互模拟是两个主体的LTS之间的对称关系ΔA和ΓB，使得：• Δ =Δr，以及F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）6381⊗• 如果Δ<$A−α→ΔJ<$AJ，则nΓ<$B−α→ΓJ<$BJ且ΔJ=ΓJS tr ong bisim ula tioneq uivalen c eΔA.在代理人A和代理人B之间。ΓB是最大的互模拟直觉是，两个代理人在相同的行为下，（1）执行相同的可观察和无声动作序列，（2）具有相同的分支结构，（3）如果放在相同的空间中，它们通过空间等价的归约产生相同的变换空间。一个众所周知的结果是，由于沟道迁移率的原因，互模拟等价性并不总是由输入前缀保持。然而，代理演算，我们提出了一个干净的分离之间的并行组成，仅在代理级别，并在进程级别的总和组成。由此，我们可以引入单独的代理和过程上下文和一致性。定义4.2一个主体上下文C[X]是一个主体X与其他主体平行放置。语法是C[X]：：=X|其中S是一个平行代理系统。过程上下文C[X]是其中X是过程的一部分的上下文。它由以下语法给出：C[X]：：=X|其中P是过程表达式。我们写C[X|A]中的上下文C[X]。过程一致性是保留所有过程上下文的等价性。代理一致性是保持所有代理上下文的等价性这是比较容易证明强互模拟等价是两个代理一致性和过程一致性。我们只概述了证明中专门处理输入前缀的部分。在纯π演算中，很容易证明以下性质成立：c！vd？（x） c！v.d？（x）+d？（x）.c！v然而，结果在绑定c或d的输入前缀的上下文中不再成立，因此：b？（d）. [c！vd？（x）]b？（d）. [c！v.d？（x）+d？（x）.c！v]的在左手侧，如果例如通过b接收信道c，则可以发生通信。这种通信可能不会发生在右手边，因为进程可能只在π演算中的并行组合中交互。让我们在相互作用空间的框架中翻译这一点，82F. Peschanski/Electronic Notes in Theoretical Computer Science 154（2006）63−→ −→−→.一个空间Δ，其中对于某个l2/=l1：.你说什么？（x）@l2.c！v@l1mmΔt [init{d？（x）}.c！v]@ l1Δ τ @ l1。⎣+c！v@l1.d？（x）@ l2m我们可能会问，这个结果是否被输入前缀保留，例如，验证以下性质对于某些Γ和l2/=l1成立：.你说什么？（x）@ l2.c！v@ l1mm[b]？（d）. [init{d？（x）}.c！[v]]@l1rb？（d）@ l1.τ@ l1. ⎣+c！v@l1.d？（x）@ l2m事实上，这在交互空间的框架中确实成立，因为代理人不直接交互。例如，如果我们考虑以下内部步骤：[b]？（d）. [init{d？（x）}.c！v]]@l1−→ ΓJ <$[init {c？（x）}.c！v]@l1−→ΓJJ<$[c？（x）]@l2[c！v]@l1−→Γ3<$[c？（x）]@l2 [0]@l1−→Γ4 <$[0]@l2<$[0]@l1然后，这可以通过没有并行的等效步骤来匹配：你说什么？（d）@l1.τ@l1[d？（x）@l2.c！v @ l1+ c！v@l1.d？(x)@l 2]−→ I1处的ΓJ <$τ。[c？（x）@l2.c！v@l1+ c！v @ l 1.c？（x）@ l 2]−→Γjj c？（x）@l2.c！v@l1+ c！v @ l 1.c？（x）@ l 23−→Γ c？（x）@l2−→Γ40@l2这些结果当然是双相似的结构等价。强语义的一个问题是，它们暴露了代理行为的所有细节。一个有用的变体是弱语义方法，.相关弱互模拟等价性，记为Δ1<$P<$Δ2<$Q。 这个想法是从语义学中纯粹的内部步骤中抽象出来。第四章. 3对于可观测的α，Aweaktransition=α-围绕一个转换的无声转换的可传递和可传递α，即，=α=^τ∗ατ∗. 弱互模拟等价是最大代理A和B之间的对称关系ΔA<$A <$T <$B，例如：