理论计算机科学电子笔记175（2007）77-88www.elsevier.com/locate/entcs关于生成概率互模拟的注记Simone Tini西蒙娜·蒂尼1，2Dipartimento di Scienze della Cultura，Politiche e e dellVia Carloni 78，22100，Como（科莫），意大利摘要在本注记中，我们考虑生成概率转移系统的模型，以及Baier和Her- manns的弱互模拟概念在它们之上的定义。我们证明了，如果我们考虑任何进程代数产生的概率转移系统满足正则性的条件，并且满足预固定，交织和保护递归，那么包含在弱互模拟中的粗同余是强互模拟。关键词：进程代数，生成概率，行为等价，互模拟，弱互模拟，同余1介绍概率过程代数已经在文献中被引入（参见[1，2，3，7，10，11，12，16，18，21，31]），以开发处理系统行为的功能和非功能方面的技术，例如性能和可靠性。概率过程的模型在[18]中被分类为生成的、反应的和分层的。 在生成模型中，一个单一的概率分布归因于一个给定的进程的所有动作，独立于他们的动作标签。在反应式模型中，给定进程执行的动作类型是以非确定性的方式选择的，并且概率分布归因于该进程的所有动作在分层模型中，一个给定的过程要么有概率移动，它有一个单一的概率分布，并且没有动作标签，要么有一个单一的动作移动，有一个动作标签，因此意味着动作和概率的明确分离概率模型1作者部分由PRIN Project“Analisi di sistemi di Riduzione mediante sistemi di Tran- sizione”（ART）支持2电子邮件：simone.tini@ uninsubria.it1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.01678S. Tini/Electronic Notes in Theoretical Computer Science 175（2007）77自动机[29]被引入来捕获概率和经典的非确定性过程代数概念。在这里，自动机的状态可以有几个以非确定性方式选择的转换，每个转换都会导致标记动作的概率分布。通常，[29]的模型被称为非交替模型，与[19]的交替模型相反，其中在非确定性状态和概率状态之间存在明显的区别，非确定性状态允许导致唯一状态的转换并且以非确定性方式选择，概率状态允许导致状态概率分布的唯一转换。概率转移系统（ProbabilityTransitionSystems，简称PTS）是对经典的标号转移系统进行扩展以表示概率的一种机制，已被广泛应用于概率过程的基本语义模型。当然，考虑到所考虑的概率模型，已经引入了PTS为了从概率过程计算的方式中抽象出不相关的信息，在PTS模型中定义了几个概率等价和前序的概念[2，8，9，11，12，19，20，22，23，25，30，32]。为了将一个给定的等价物放入一个公理框架中，要求它是关于所有进程代数运算的一个同余概率互模拟，它将两个过程联系起来，如果它们的PTS具有相同的概率分支结构，并且最初在[25]中为反应模型定义，在上面提到的论文中提出的过程代数中享有同余性质，并且是最常用的等价定义之一。在非概率情况下，Milner [26]成功地提出了弱互模拟，将其作为从内部计算步骤中抽象出来的等价关系。在[2，11，12，30]中已经考虑了非交替模型的弱互模拟的概念。Baier和Hermanns [5]在[26]的启发下为生成模型提出了弱互模拟的概念。关于概率弱互模拟的有趣动机和结果，我们参考[5在非概率背景下，弱互模拟不是关于非确定性选择操作的同余，而这是大多数已知进程代数所具有的.由于具有同余性质的重要性，关于比弱互模拟更精细的非确定性选择的粗同余已经被描述，并被Milner称为观测同余[26]。这样的同余也被称为有根τ-互模拟[4]和有根弱互模拟[6]。同样在非交替模型中，关于比弱互模拟更精细的非确定性选择的粗同余已经被表征[2，11，12]。遵循生成模型的进程代数不允许任何非确定性选择的操作。更确切地说，这些过程代数不允许任何引入非确定性的操作。然而，在一般情况下，也在生成模型弱互模拟不是一个同余。 事实上，许多过程代数交织操作的参数版本，其中参数决定了两个组成过程中的每一个的移动概率，并且我们通过一个简单的例子表明，弱互模拟不是关于S. Tini/Electronic Notes in Theoretical Computer Science 175（2007）7779Σ∈S≤ ≤−−−→α，p−−→这种交织操作。此外，[10，7]的类CCS并行合成操作和[10]的类CSP并行合成操作不保持弱互模拟。我们的目标是在生成模型中研究问题，以给出粗等价概念的特征化，该概念比概率弱互模拟更精细，并且是关于任何合理操作核的同余。 为了这个目的，我们假设prefixing，交织，和保护递归因为它们被广泛使用。我们证明了，如果我们只考虑过程代数产生的PTS满足正则性条件，那么我们的目标是刻画的同余是概率互模拟。从某种意义上说，这一结果具有负面影响。 事实上，在非概率情况下，已经对弱于互模拟和强于弱互模拟的同余做了大量工作[6，13，14，15，17]，而在生成情况下，这样的工作不能重复，因为我们的结果意味着没有严格位于互模拟和弱互模拟之间的同余。注意，我们的结果还强调了生成模型和非交替模型之间的差异，其中弱互模拟中包含的粗同余比强互模拟严格粗。这种差异取决于这样一个事实，即非交替模型的并行合成操作没有参数，引入了非确定性，并且可以被视为[26]的经典交织操作2概率双模拟给定任意集合S，设M（S）表示S上所有多重集的集合。 让我们使用“{|“和“|}“作为多集的括号。下面的定义来源于[3，5，7]。定义2.1生成概率转移系统（简称GPTS）是一个三元组（S，Act，T），其中S是一组状态，Act是一组可数的动作，T∈ M（S ×Act×（0，1]× S）是一个多重转移集，使得对于所有状态s∈ S：{|p |<$α ∈ Act，sJ∈ S：（s，α，p，sJ）∈ T|} ∈ {0，1} 3定义2.1要求每个国家是半随机的，也就是说，它的输出转移的概率，如果有任何，总和为1。让我们回想一下，在[18，31]中考虑的GPTS具有较弱的要求，因为它们承认，对于每个状态s，其传出转移的概率之和（如果有的话）是值0q 1，解释为s死锁的概率为1q。本文证明的结果也适用于[18，31]的GPTS模型，因为它们不依赖于对从s出发的跃迁概率的任何约束。设sα，p sj表示（s，α，p，SJ）∈T，s−→表示sα，p sJ为一些α，p和SJ，和s→/−表示s−−→SJ保持f或不保持α，p和SJ。[3]请注意，需要多重集来处理从状态s到状态s j的几个具有相同标签α和概率p的转移的情况。80S. Tini/Electronic Notes in Theoretical Computer Science 175（2007）77α，p−−→ΣΣ∈∈ΣG设s=SJ表示SJ从s可达，即存在一个序列过渡Sα0，p0s ... Sαn−1，pn−1S使得s=s和s=sJ.0−→1n−1−−→n0n在下文中，我们假设“正则性”条件，即对于每个状态，s∈ S，只有有限个向外的转移s sJ，并且从s只有通过一个ny（po−s−s→iblyin finite）序列，可以得到其他无限多的状态的过渡。让我们回忆一下累积概率分布函数μG[18]，它计算了从状态s通过标记为动作α的跃迁到达状态SJ的总概率。采用概率的空和为0的惯例，μG定义如下。定义2.2μG：S×Act×S →[0，1]是由下式给出的函数：sJ∈S：μ（s，α，sJ）={|p|sα，psJ∈T|}函数μG可以扩展到目标状态的集合。 s∈S，μG（s，α，S）=μG（s，α，SJ）sJ∈S在[5]之后，函数μG可以被扩展到动作A中的动作序列。让表示空的动作序列。对 于 每个α Act和λAct，令αλ 表示Act中的序列，通过用α前缀λ获得。那么，<$s∈S，<$α∈Act，<$λ∈Act<$，<$S<$S：μG（s，n，S）=1 ifs∈SμG（s，n，S）=0 ifs/∈SμG（s，αλ，S）=μG（s，α，sJ）·μG（sJ，λ，S）sJ∈S最后，将[5]中的μG函数推广到动作序列的集合。 设Λ表示Act_n的任意子集，Λ/α表示集合{λ∈Act_n|αλ∈Λ}。那么，s∈ S，<$ΛAct<$，<$S<$S：μG（s，Λ，S）=1，若ε∈Λ且s∈SμG（s，Λ，S）=（α，SJ）∈Act×SμG（s，α，sJ）·μG（sJ，Λ/α，S）否则我们现在可以回忆一下GPTS的互模拟概念[18]。 对于状态集S上的任何等价关系R，设S/R表示由R导出的等价类集。定义2.3等价关系R <$S × S是（强）互模拟，如果（s1，s2）∈R蕴涵：<$C∈S/R，<$α∈Act：μG（s1，α，C）=μG（s2，α，C）S. Tini/Electronic Notes in Theoretical Computer Science 175（2007）7781∼ǁ--ǁ所有互模拟的并集又是一个互模拟，用表示。关系将具有相同概率分支结构的状态等同起来让我们假设Act包含特殊的沉默行动τ。我们现在可以回想起Baier和Hermanns让我们用正则表达式来表示动作序列的集合定 义 2.4 等 价 关 系 R<$S × S 是 弱 互 模 拟 ， 如 果 （ s1 ， s2 ） ∈R 蕴 涵 ：<$C∈S/R，<$a∈Act\{τ}：μG（s1，τaτ，C）=μG（s2，τaτ，C）μG（s1，τ，C）=μG（s2，τ，C）所有弱互模拟的并集又是一个弱互模拟，表示为- 是的关系式R1比R2更粗糙，因为它从无声的计算步骤中抽象出来3弱互模拟不是同余像往常一样，让我们假设一种过程描述语言，其抽象语法由签名给出，由一组操作符号和一个arity映射组成，该arity映射为每个f∈f指定一个自然ar（f）对于一组变量Var，范围为x，y，. ，则在λ和Var上的（开）项的 集 合 是最小集合，使得：• 每个变量x∈Var是一个项;• f（t1，.，tar（f））是一项，只要f∈f且t1，.，tar（f）是术语。在Var中不包含变量的项称为封闭项或过程。语言的语义由GPTS给出，其状态是进程，其转换由一组SOS规则推断[27，28]。像往常一样，让我们假设R2包含操作符号0（有时表示为nil），ar（0）= 0，其中0表示没有移动的空闲过程。让我们回顾一下全等性的概念定义3.1过程上的等价关系R称为同余i ∈ R，对于每个f∈R，如果关系（ti，tJi）∈R对所有1 ≤i≤ar（f）成立，则（f（t1， . ，tar（f））， f（tJ1， . ，tJar（f））∈R.现在，互模拟是关于文献[1，3，7，10，16，18，21，24，31]中使用的众所周知的过程代数的让我们考虑[3]的概率交织p的操作，其SOS风格的语义在表1中给出。直观地说，如果过程t1和t2都可以移动，那么过程t1pt2以概率p作为t1移动，以概率1p作为t2移动。如果只有t1（相应地，t2）可以移动，则t1pt2随着t1（resp. （2）概率为1。通过一个例子，我们可以证明弱互模拟不是关于运算BFP的同余。82S. Tini/Electronic Notes in Theoretical Computer Science 175（2007）77α，p−−→1 1−−−→122pppp·ǁ··Qǁ·ǁ·ǁ·ǁ·ǁ·ǁ·∈\{ }≡····{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}{\fnarialblack\fs12\bord1\shad0\4aH00\fscy110}一12−−−→112−−−→1x[re c] x/X]−−→yα，1α·x−−→xrecX. xα，p yα，px1−→y1 x2→/−x→/−xα2，p2 yxxα1，p1 y阿克斯xxα2，p2 X埃什基xα1，p1α2，p21−→y1 x2−→x1−→x2−→y2xxα1，p1·pyxxx pα2，p2·（1−p） X射线p12−−−−→12表112−−−−−−−→12一些概率运算;x，x1，x2，y1，y2是过程变量，α，α1，α2在Act上的范围，p，p1，p2是区间[0， 1]上的变量，X是递归变量。例3.2假设a法τ，t1和t2是过程t1τ一0和t2τ τa0，其中是表1中描述的预固定操作。这是直接的t1t2，但是，对于每个 p.一0- 互模拟就是互模拟。给定一个进程t，让actions（t）表示出现在GPTS中以t为根的部分的转换标签中的动作集合。GPTS上的正则性条件确保actions（t）是有限集。假设有两个过程t和tJ。 由于动作（t）和动作（tJ）是有限集合，并且由于Act是可数集合，我们可以取两个动作b，c∈Act\（动作（t）<$动作（tJ）<${τ}）。我们可以证明，给定任意值0 p2。现在，p1=μG（s，a，C）意味着μG（s，τaτ，C）p1。由于s sJ，我们推断μG（sJ，τ∈aτ∈，C）p1。由于p1>p2=μG（SJ，a，C），我们推出μG（SJ，τ+aτ，C）+ μG（SJ，aτ+，C）≥（p1−p2），其中τ+表示所有n≥1个τ-作用序列的集合。由于a b和a/=c，C中的进程可以通过序列从sJ到达τ+aτ和aτ+仅通过至少两次t2的移动。 这意味着84S. Tini/Electronic Notes in Theoretical Computer Science 175（2007）77·−·≈- -·ǁ··−·−·−联系我们−/∈·/∈·≤··≥ −|−|·/−−−→μG（sJ，τ+aτ，C）+ μG（sJ，aτ +，C）p2 q2. 综上所述，p2q2p1p2，证明了本文的结论.(ii) α=b。因为bactions（t）actions（tJ），所以唯一的b移动s是由于recX。b X并导致s本身，类似地，唯一的b被sJ移动是由于rec X。b X，并导致sJ本身。因此，要么C既不包含s也不包含SJ，并且命题是直接的，因为μG（s，b，C）= 0 =μG（SJ，b，C），要么C既包含s又包含SJ。让我们集中讨论第二种情况。自t1qrecX. c X移动，b移动的概率不可能是rec X。b X为1，我们确信b移动的概率为1p，因此μG（s，b，C）= 1p。基于同样的理由，我们推出μG（SJ，b，C）= 1p。综上所述，μG（s，b，C）=μG（SJ，b，C），证明了本文的结论.(iii) α=c。设p1和p2为满足p1=μG（s，c，C）和p2=μG（ SJ，c，C）的值。因为cactions（t）actions（tJ），所以唯一的c移动s是由于recX。并且导致s本身，类似地，唯一的c被SJ移动是由于recX。 cX并导致sJ本身。因此，要么C既不包含s也不包含SJ，并且命题是直接的，因为μG（s，c，C）= 0 =μG（SJ，c，C），要么C既包含s又包含SJ。让我们集中讨论第二种情况。如果t1有移动，则p1= p（1 q）;如果t1没有移动，则p1= p。此外，如果t2有一些移动，则p2=p（1q），或者如果t2没有移动，则p2=p因此，证明了t1移动而t2不移动的情况不可能发生，也就不可能推出p1= p（1q）=p2或p1= p= p2，从而蕴涵了这一命题。通过矛盾，让我们假设t1移动而t2不移动。由于t2不移动，SJ只有一次b移动，概率为1p，只有一次c移动，概率为p 由于s，S，J，我们推断s只有进步b，c，τ，这意味着t1有τ次移动。 这意味着序列τ<$bτ <$bys的总概率严格大于1−p，这与s<$sJ相矛盾。(iv) α=τ。首先，让我们注意到，由于SsJ，或者C同时包含s和sJ，或者C既不包含s也不包含sJ。如果C既不包含s也不包含SJ，我们可以像情形（i）那样推理。假设C包含s和SJ。 在这种情况下，设p1和p2是使得p1=μG（s，τ，C）和p2=μG（SJ，τ，C）的值。我们要证明p1p2p2q2。如果p1=p2，命题是直接的.如果p1=p2，则w.l.o.g. 我们可以假设p1>p2。首先，让我们注意到，由于每个国家都在努力，可从s或sJ中读取的内容可以在cmove中执行，它可以不执行该操作，1因此，因此，我们可以肯定s∈b，1−ps。Sinceboths−→和C从s通过一次τ移动可到达的（总概率为p1）可以以1−p的概率执行b，同时保持在C中，则μG（s，τ，C）≥（1−p）+p1·（1−p）成立。由于s<$sJ，所以μG（sJ，τ<$bτ<$，C）≥（1−p）+p1·（1−p）成立。由于C中的状态不能以概率1执行b，我们S. Tini/Electronic Notes in Theoretical Computer Science 175（2007）7785··− ≥ −·−·≥ −Jmn2 2mnμ（s， τbτ，C）≤p ·q·（1−p），因为τbτ满足m+n≥2Gm+n≥2·<$μ s，b，C−pμ s， τbτ，Cp·−p2GGm+n=1Σp·qX.C··ǁ··ǁ·ǁ··|≤·|−|≤·ǁ·|ǁ·ǁ·−ǁ·ǁJPQ一一知道（J））=（1）和（ JMn） = 的（一））.因此，m+n≥2μG（SJ，τmbτn，C）≥（p1−p2）（1 −p）。此外，我们知道，需要至少两次t2移动和一次从rec X移动。b X. 总结，第2页Q2（一）p）的范围内 （p1） p2） （一） p），这意味着p2 Q2 p1p2，而 论文被证明。Q引理4.4暗示存在一个（p2·q2）-互模拟，它与从（t=qrec）X可达的过程有关.c·X）X. b·X和（tJqrecX. c·X）X. b·X，并且包含由（t<$qrecX）形成的对。c·X）X. b·X和（tJqrecX. c·X）X. b·X。 L∈p2·q2表示一个（p2·q2）-二进制.设一个等价类C∈S /S/p2·q2.我们给出了一组过程C={s}，使得（s）={x}。c·X）X. b·X∈C}是a（p·q）-互模拟的一个等价类，它涉及从t和TJ可达的过程. 设φp·q表示这样的（p·q）-互模拟。关系式<$p·q使t和tJ相等，因为（t<$q rec X. c·X）X. b·X和（tJq rec X. c·X）X. b·X等于y=p2·q2。 本文的研究思路是：因此，对于某些（p · q）-双模拟<$p· q，C∈S/<$p·q 仍 有 待 证 明. 给定任意处理st1，t2∈C，任意等价类D， 以及任意动作α∈动作（t1）和动作（t2），则p和q的语义意味着：μG（t1，α，D）=1·μG（（t1qrecX. c·X）X. b·X，α，D），μG（t2，α，D）=1·μG（（t2qrecX. c·X）qrecX. b·X，α，D）。自（t1qrecp·q·X）记录X。 b·Xp2·q2（t2X. c·X）X. b·X，我们确定μG（（ t1qrecX. c X） precX. b X，α，D）μG（（t2qrecX. c X） precX.bX ），α，D）p2q2. 因此， T，μG（t1，α，D）μG（t2，α，D）pq，as必需的。Q乍一看，我们选择使用引理4.3中交织算子出现两次的上下文可能令人惊讶。人们可以预期，一个上下文只有一个这样的发生表面。关键是，如果我们考虑上下文，引理4.4precX. BX而不是（qrecX. c X）precX. bX. 事实上，在α=b的证明和α=τ的证明中，我们都利用了b的概率移动recX的事实。bX不能为1。 这是由recX. CX可以执行C移动。没有进程记录X。cX，p左边的进程可以是没有任何移动的进程，b通过recX移动。bX的概率为1。注意，如果我们替换交织操作，上面的引理4.3也成立使用类似CCS的并行组合操作BLP和BLP 和， [10][7]条件是t和tJ除了既不执行b也不执行c之外，也不执行b也不执行c。此外，如果我们用类似CSP的平行线替换Bqp和Bqq，引理4.3也成立[10]的关系式的合成，其中A=α。现在让我们证明，对于所有0
0，R是对无限多δ > δ>0的一个互模拟。我们可以证明R是一个强互模拟。通过矛盾，让我们假设R不是强互模拟。则存在一对状态（s，SJ）∈ R，一个作用量α∈Act，以及一个等价的R上的价类C使得μG（s，α，C）μG（SJ，α，C）. 设d为值|.|.因此，R对任何d都不是n-互模拟，这与R对无限多d > n>0是n-互模拟相矛盾。现在，由于R是互模拟，且（t，TJ）∈ R，本文成立.Q现在我们可以给出主要结果。定理4.6给定任意过程t和TJ，如果对所有p<，q 1和作用，b，c∈Ac t\（{τ}<$action s（t）<$action s（tJ））它保持t hat（t<$qrecX. c·X）X. b·XX. c·X）X. b·X则t <$tJ。是的。根据引理4.3，对于each0p，q1，对于某些（p·q），t∈p·qt∈J成立二分法给定一个0d1，我们可以选择p=q=d，以推断，tdtJ。 由于tdtJ对于所有0< d<1，我们可以应用引理4.5来推断ttJ，以及 证据就完整了Q让我们假设，是一个等价关系的过程是一个同余w.r.t交织，prefixing和递归，并且比弱互模拟（即R互模拟）更精细。给定过程t和 TJ使得（t， TJ）∈R，由于R是同余，我们推论，对所有的0
下载后可阅读完整内容，剩余1页未读，立即下载
