π演算的概率变种的交错和真正并发语义

理论计算机科学电子笔记190（2007）147-166www.elsevier.com/locate/entcs概率π-演算和事件结构1Daniele VaraccaaaPPS-U iversit′eParis7CNRS，Franceb英国伦敦帝国理工学院摘要本文提出了π演算的概率变体的两种语义：Segala自动机方面的交织语义和概率事件结构方面的真正并发语义。关键的技术点是使用类型来识别一类良好的非确定性概率行为，其可以在事件结构和演算中保持并行运算符的组合性。我们展示了两个语义之间的操作对应关系。这允许我们证明一个保留字：事件结构，概率过程，π演算，线性类型1导言和动机并发的概率模型有大量的文献：大多数研究涉及交织模型[21，27，10]，但最近，真正的并发模型也被研究[20，14，1，30，33]。本文提出了一个交错和真正的并发语义的概率变种的π演算。我们考虑的变体类似于[16，7]中提出的变体，但包含重要的差异。最主要的区别是类型的存在，这也是所有其他类型的动机所在。已经开发了用于移动过程的各种类型系统，以便提供静态和compo- sitionally控制非确定性行为的学科在概率并发中，对非确定性的限制变得更加重要，例如，为了保持并行组合的结合性或保证不受任何特定调度策略的约束[30]。本文执行了一个“好”的概率分类纪律的第一步，1由EPSRC赠款GR/T04724/01和ANR项目ParSec ANR-06-SETI-010- 02部分支持的工作。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.07.009148D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）147名称传递，它可以保持表达能力，并可以与现有的概率并发语义和编程语言协调[24，11，8]。我们提出了一个概率π演算的类型系统，灵感来自π演算的线性类型系统[4，37]。线性型π-演算可以完全抽象地嵌入一族λ-演算。线性类型进程有几个有趣的特性。特别地，它们保证是连续的，也就是说，它们执行的计算是确定的。在真正的并发设置中，并发可以被视为没有冲突或无冲突。在无冲突系统中，可以有不同的部分运行，例如因为选择执行不同的子系统。然而，在一些基本的公平性假设下，如果我们从并发事件发生的顺序中抽象出来，系统将总是产生相同的运行。在[32]中，我们通过增加一个非确定性选择来扩展线性π演算。打字系统不再保证无冲突性，而是保证更一般的无混淆性。这个属性已经以自由选择Petri网的形式进行了研究[25，9]。无混淆事件结构也被称为具体数据结构[5]，它们的域理论对应物是具体域[19]。在一个无混淆的系统中，所有的非确定性选择都是局部的，并且独立于系统中的任何其他事件。在概率论背景下，直觉认为局部选择可以通过局部硬币解决，或者死亡。文[30]的结果表明概率无混淆系统是概率连续的。我们已经论证了，并发性包含只有一个最大计算的性质，直到并发事件的顺序。因此，将概率连续性定义为只有一个最大概率计算的属性是合理的，其中概率计算被定义为计算集合上的概率度量。我们提供了一个交错和真正的并发语义，这个概率π演算。交织语义被给出为Segala自动机[27]，其是结合概率和非确定性的操作模型。不确定性是考虑系统中独立部分的不同可能的分布所必需的真正的并发语义是作为概率事件结构给出的[30]。在这个模型中，我们不需要考虑不同的随机数，这就导致了概率连续性结果（定理6.2），这是本论文的主要贡献之一。为了将这两种语义联系起来，我们展示了概率事件结构如何这使我们能够显示两种语义之间的操作对应性。类型在组合语义中扮演着重要的角色，这是作为温斯克尔CCS [ 34 ]的原始事件结构语义到π演算的干净概括而给出的在这个意义上，这项工作将概率事件结构的具体语法表示作为名称传递过程，关闭了[30，32]中的一个开放问题。这项工作为概率λ-演算和编程语言的事件结构语义打开了一扇门，使用概率线性π-演算作为中间形式主义。D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）147149→在初始状态x0中，有三个可能的跃迁群，对应于它的三个空心子群。最左边的过渡群是x0{a我 x}pii i∈I其中I={ 1， 2}，a1=a，a2=b，p1=p2= 1/ 2。最右边的过渡群是x{ajx}0pjjj∈J其中J={ 0， 5}，a0=a，a5=b，p0=ε，p5= 1−ε。Fig. 1. 塞加拉自动机证明和关键的定义可以在附录中找到;一些非概率性的材料留给[32，31]。2塞加拉自动机为了给概率π演算一个操作语义，我们使用Segala au-tomata，一个结合概率和非确定性的模型。Segala自动机可以看作是马尔可夫链和标记转移系统的扩展。它们是由Segala和Lynch介绍的[28，27]。Segala自动机的最新介绍可以在[29]中找到。“Segala自动机”这个名字最早它在文献中是非标准的，但我们更喜欢它，而不是更常见的，但模棱两可的，2.1符号在有限或可数集合X上的概率分布是一个函数：X[0， 1]Σ使得x∈X<$（x）= 1。X上的概率分布集表示为：V（X）。用P（X）表示X的幂集。一个标记集A上的Segala自动机由一个有限或可数的状态集X和一个转移函数t：X→P（V（A×X））给出。这个模型表示一个过程，当它处于状态x时，非确定性地选择t（x）中的概率分布，然后执行动作a，并以概率<$（a，y）进入状态y我们使用的符号来自[16]。考虑一个过渡函数t。当一个状态x∈X的概率分布f属于t（x）时，我们将写为：x{aix}（一）pii i∈I当r exi∈X，i/=j=<$（ai，xi）=（aj ，xj），nd<$（ai，xi）=pi. T（x）中的P_（o_b）b_i_d_i_i_u也称为x的过渡群。可视化概率自动机的一个好方法是使用交替图[15]。在图1中，黑色节点表示状态，空心节点表示转换组。x0的ε一一BCa二分之X11/21/ 3X2B2/31−εx3x 4x 5150D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）1472.2电子邮件初始化的Segala自动机，是一个Segala自动机连同一个初始状态x0。初始化的Segala自动机的有限路径是（X ×V（X ×A）×A） <$X中的元素，写作x0<$1a1x1. n a n x n ， 使得n i+1∈ t （ x i） 。 无限路径的 定义与（ X×V（X×A）×A）ω的元素类似。有限路径的概率τ：= x01a1x1. n a n x n定义为（τ）=1≤i≤ni（a i，x i）.有限路径τ的最后一个状态记为l（τ）。一条路τ是最大的，如果它是无限的或如果t（l（τ））= π。具有转移函数t的Segala自动机的调度器是部分函数，问题S：（X×V（X×A）×A）<$X→V（X×A）使得如果t（l（τ））<$则S（τ）故，有一个定义，S（τ）∈t（l（τ））。调度程序选择下一个概率分布，知道进程的历史。使用交替图的表示，我们可以说，对于每个以黑色节点结束的路径，调度器选择他的空心子之一。给定一个（初始）状态x0∈X和一个调度器S，我们考虑由S的作用从t得到的极大路集B（t，x0，S）。这些是路径x01a1x1. n a n x n使得n i+1 = S（x0n1a1x1.（i）a i x i）。 极大路集被赋予由有限路生成的σ-代数调度程序在这样的σ-代数上导出一个概率测度如下：对于每个有限路τ，设K（τ）是扩展τ的最大路的集合。定义<$S（K（τ））：=<$（τ），如果τ∈B（t，x0，S），否则为0。可以证明[27]，在由有限条路径生成的σ-代数上，σ-S扩展为唯一的概率测度给定一个标签集B<$A，我们定义<$S（B）为<$S（Z），其中Z是包含来自B的某个标签的所有极大路的集合。3概率π演算3.1语义和操作语义我们假设读者熟悉π演算的基本定义[23]。我们考虑π演算的一个限制版本，其中只有绑定名称在交互中传递。这种变体被称为πI演算[26]。在类型化设置中，它具有与完整演算相同的表达能力[36]。πI-演算的标号变迁语义比全演算的标号变迁语义简单，它的标号更自然地对应于事件结构的标号从句法上讲，π I-演算是通过将输出重新构造为m（νy ）xνy的形式而得到的.P（whereenamesinynyamasapallisedistinct），whichichwewritexx（yth）. P.我们扩展这个框架的概率版本的演算，输出被赋予概率。在非概率的情况下，输入类似于微积分的形式语法定义如下，其中pi∈[0， 1]。D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）147151pii i i∈IP{Q}我xpin（y）. P{xiniyjP}xΦin（yΦ）。P{xinjyjP}i∈Ii i i i i ipii i∈Ii∈I i i i1j！x（y）。P{xyP|！x（y）。P}x（y）。P{xyP}1P{βiP}subj（β）/=x1P{βiP}pii i∈Iipii i∈I（vx）P{βi（νx）P}P|Q{βiP|Q}第一节i∈I第一节i∈IP{αiP}Q{βi Q}obj（α）=y我PPJP{βiQ}第一节i∈I1iαpii i∈IP|Q{αi·βi（νyθ）（P|（Q）}Jβ ipii i∈I图二. 概率πI演算P：：=xΦi∈Ii ni（yi）.Pi|xi∈Ipiini（y<$i）.Pi|P|Q|（νx）P|0|！x（y）.P过程xΦi∈Iini（y<$i）.Pi是分支输入，不附带概率它的事件。 过程Xi∈Ipiini（y<$i）.Pi是一个概率选择输出，事件的概率用p表示，条件是Σi∈Ipi= 1. 最后，P|Q是一个平行复合，（νx）P是一个限制，！x（y）。P是一个可编程的输入。当输入或输出的索引数据集是一个简单的方法来使用非整数x（y）时。P或x（y）。P;whhenthe ntexingsetite，wecnw ritex（in1（y n1）.P1&. & inn（y <$n）. Pn）或x（p1in1（y <$1）.P1<$. 在n（y<$n）.Pn）中。我们省略空向量和0：例如，a代表a（）。0的情况。绑定/自由名称已定义为通用名称。 我们认为，在一个向量空间中，节点的数量是有限的。我们用α和α来表示标准α和结构等价[23，17]。操作语义是根据Segala自动机给出的，使用第2节（1）中定义的我们使用的标签形式如下α，β：：=xini y|xi ni| xy|xy|τ（分支）（选择）（选择器）（请求）（同步）根据上面的符号，我们说x是标记β的主题，表示为assubj（β），而y=y1， . . . ，而在一个块节点中，不存在一个对象（β）。 F或R分支/选择标签，索引i是标签的分支。 符号图2给出了导出转换的规则。标签上的部分操作·是双标签的标准合成。也就是说，一个输入与它的双重输出同步，并产生一个无声的动作。形式上，·被定义为如下公式：xi ni2特别地，选择输出与分支输入同步，并且同步步骤以由输出过程选择的概率2更准确地说，为了进行校样，同步标签应跟踪它们代表的同步。这只会使本已困难的演示变得复杂，我们在这152D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）147里省略它-更多解释请参见[32]D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）1471533.2概率π-演算本小节概述了概率π-演算的线性类型的基本思想线性类型规程[4，37]以两种方式控制进程的组合：首先，对于每个线性名称，都有一个唯一的分支输入和一个唯一的选择输出;其次，对于每个复制名称，都有一个唯一的无状态复制名称。输入（或服务器）与零个或多个双输出（请求或客户端）。让我们考虑下面的例子，其中分支和选择提供概率行为，保持线性：年q1d=efa. （pin1.b<$（1 −p）in2.c）|a. （在1.d中，在2.e中）Q是可类型的，我们有Qτ（b|d）或Qτ（c|e）。 以下1过程也是可类型化的：Q2d=efp1−pa. （pin1.b<$（1 −p）in2.b）|a. （在1.d中，在2.e中）因为无论选择哪个分支，b都被使用一次。 然而，a.b |a.c |a是不可键入的，因为线性输出a出现两次。作为请求者-请求约束的一个例子，让我们考虑以下过程：Q3d=ef！ a（x）。X. （pin1<$（1−p）i n2）|a（x）x. （1. D&在2。e）、|a（x）x.（i n1. f&i n2. g）的Q3是可类型化的，因为当a处的输出出现两次时，a处的复制输入只出现一次。请注意，复制下的x在每次调用后都保持线性。另一方面，！b.a|！b. c是不可分型的，因为b与两个复制子相通道类型由类型变量和操作模式归纳组成：输入模式↓，！和双输出模式↑，？.类型的语法如下：τ：：=Φ （τ）↓|（τ）↑|（τ）！|(τ˜)? |‡i∈I ii∈Ii（分支）（选择）（选择器）（请求）（关闭）其中τ是类型的元组。分支类型代表了“环境选择”的概念选择类型代表了“过程选择”的概念：一些选择是由过程做出的，可能是概率性的。在这两种情况下，选择是可选择的：一个排除所有其他的。对象类型代表“可用资源”的概念：无论发生什么，我都向环境提供可用的东西。请求类型代表了“并发客户端”的概念：我想使用一个可用的资源。封闭类型用于表示无法进一步组合的通道我们将τ的最外模写成MD（τ）。 τ的对偶，记作τ，是递归对偶化所有作用模式的结果，其中τ是自对偶。一种154D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）147环境Γ是从通道到通道类型的有限映射。有时我们会写x∈Γ来表示x∈Dom（Γ）。类型限制进程的可组合性：如果P在环境Γ 1下类型化，Q在环境Γ 2下类型化，并且如果Γ 1，Γ 2是“兼容的”，则定义一个新的环境Γ 1 <$Γ 2，使得P|Q在Γ 1 <$Γ 2下有类型。 如果环境不兼容，则不定义Γ1<$Γ2形式上，我们在类型上引入了一个部分交换运算，定义如下3：(i)Φ（τ）↓（τ）↑=i∈Iii∈Ii（ii）（τ）？ （τ）！ =（τ）！(iii) （τ）？ （τ）？ =（τ）？然后，同态地定义环境Γ1< $Γ2直觉，规则(i)说，一旦我们组成输入-输出线性通道，通道就变得不可组合。规则（ii）说服务器应该是唯一的，而规则（iii）说任意数量的客户端可以请求交互。其他的组合物是不确定的。定义类型判断P dΓ的规则（其中Γ是将通道映射到类型的环境）与aeronneπ-演算[4]相同，除了处理生成输出的直接修改，生成输出由[32]中的无混淆过程的相同规则定义，没有任何额外的复杂性。规则如图3所示。在（Par）中，Γ 1 <$Γ 2保证了一致的信道使用，如线性输入仅与线性输出组成等。或↓-信道被限制，因为它们携带期望其双重作用存在于环境中的作用。（WeakOut）和（WeakCl）减弱与？-names或-names，因为这些模式不需要进一步的交互。(LIn)和（LOut）确保x恰好出现一次。(RIn)与（LIn）相同，只是没有抑制自由线性通道。这是因为复制下的线性通道可以使用多次。（ROut）与（LOut）类似。请注意，我们需要在第一次应用（ROut）之前应用（WeakOut）。然后，我们通过限制类型环境不允许的操作来获得操作语义的类型化版本。非正式地，如果操作的主题具有分支、选择或服务器类型，则环境允许操作。形式上，对于标签β，谓词Γ允许β定义如下：• 对于所有的Γ，Γ允许τ;• 如果MD（Γ（x））=↓，则在i∈Y中，所有x都是Γ;• 如果MD（Γ（x））=↑，则在i∈Y中所有x都是Γ;• i f MD（r（x））=！，则nr都是xy;• ifMD（r（x））=？这一切都是X的。作为示例，|a. 不允许0，因为a是线性的[3]为了简化符号，我们省略了表示多子性的符号“n”。D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）147155Ci∈I我 我我11Pd Γ，a：τa/∈ Γ MD（τ）=！，（νa）P dΓRes0d<$ZeroP dΓx/∈ ΓP dΓ，x：<$WeakClPidΓ，yi：τia/∈ΓPdΓx/∈Γapin（y）.Pdr，a：（τ）↑LOutP dr，x：（τ）？WeakOuti∈Ii i i iii∈IiPidΓ，yi：τia/∈ΓPidΓi（i= 1，2）aΦin（y）.PdΓ，a：Φ（τ）↓LinP|PdΓ ⓈΓParPdr，yr：τra/∈Γ（x：τ）∈ Γ. MD（τ）=？！a（y）。PdΓ， a：（τ）！RInPdr， a：（τ）？，y：τa（y）。Pdr， a：（τ）？ROut图三. 线性打字规则从而假设A仅与A相互作用。0，不与外部观察者。类型化自动机P d Γ {βi Pdr}”于是，他又补充道。ing约束：第一节i i∈I如果P{βi P}且Γ允许β对所有i ∈ I ，则PdΓ {βi Pdr}第一节i∈I i第一节i i∈I类型系统的本质是这样的，对于每个转换组，要么所有动作都被允许，要么所有动作都不被允许，因此上面的语义被很好地定义。3.3一个概率过程我们考虑[24]中的交通灯模型。设a是一个驱动程序，并让输入red，输入yell，输入grenreprentcolsofhetr a raccl ght。 该概率sainred（y）表示交通灯向驾驶员发出信号，它是红色的，同时传达交叉口的名称y。驾驶员在交叉路口的行为是减速、静止或减速（制动、静止、行驶）。一个谨慎的司机是代表的过程：Da=aΦi∈{red，yell，greenn}ini（y）.Pi 其中hPred=y（0. 2在制动器上，8instill）Pyell=y（0. 9在制动器上。1个驱动器）Pgreen=y（indrive）我i∈I22156D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）147谨慎的驾驶员会观察灯的颜色，并据此采取行动。如果它是红色的，她保持不动，或者完成刹车。如果是黄色的，她很可能会刹车。如果它是绿色的，她开车。D. Varacca，N.Yoshida/Electronic Notes in Theoretical Computer Science 190（2007）147157HCH一个匆忙的司机是由过程表示的Da=aΦi∈{red，yell，greenn}ini（y）. QIWITHQred=y（0. 3在制动器上。6我仍然是100。1个驱动器）Qyell = y（0. 制动器100中的1。9在驱动器）Qgreen=y（indrive）这类似于谨慎的司机，但他更有可能在红灯和黄灯时继续开车。事实上，两者都有相同的类型，它们检查光线，并选择一种行为：01-02（）↑）↓chi∈{red，yell，green}j∈{brake，still，drive}其中Φi∈I （τi）↓是输入类型τi的值的分支类型且i∈I（τi）↑是选择类型，其选择具有类型τi的值的分支i。注意到类型实际上表明驾驶员在看到灯光后选择了行为。我们可以代表两个独立的驱动程序：D2=（νa，AJ）（ainred（y）。R|Da|亚真格林（y）.R |D aJ）当R=yΦi∈{brakee，stilll，drivee}ini（）表示驾驶员的我们知道D2有两个过渡群，两个司机。请注意，打字系统保证每个司机只能执行三个动作中的一个，即在任何一个时间刹车，静止或驾驶4概率事件结构现在我们提出概率事件结构的模型，我们使用它来给概率π演算提供另一种语义。概率事件结构首先由Katoen [20]引入，作为所谓的bundle事件结构的扩展。在[30]中引入了一个概率版本的素事件结构。在本文中，我们使用素事件结构，因为我们认为它们是最简单和最容易理解的事件结构的所有变体。此外，同余定理使用[30]的结果。下面我们从没有概率的基本定义开始。4.1基本定义一个事件结构是一个三元组E=E，≤，×，使得(i) E是可数事件集;(ii)是偏序，称为因果序;(iii)对于每个e∈E，集合[e]：={eJ|eJ j，对应于c的过渡群被启用，但它不是由S选择的。定理6.2设E是一个概率事件结构，并考虑相应的Segala自动机.对于所有的标签集B，以及所有的公平竞争者S，T，我们有S（B）=T（B）。在一个非概率性的连续系统中，非决定性选择的所有（公平）解决方案都会产生一组相同的事件，可能顺序不同。在这个意义上，我们可以把定理6.2看作是表达概率连续性。图6示出了（部分）概率事件结构的示例。生成单元为{αJ，αJJ}，{βJJ，γJJ}，概率用上标