余代数的弱互模拟

理论计算机科学电子笔记122（2005）211-228www.elsevier.com/locate/entcsn-型余代数的弱互模拟（延伸摘要）Ana Sokolova安娜·索科洛娃1，2荷兰埃因霍温理工大学数学与计算机科学系Erik de Vink3埃因霍温理工大学数学与计算机科学系LIACS莱顿大学埃因霍温，莱顿，荷兰Harald Woracek4维也纳工业大学分析与科学计算系奥地利维也纳摘要本文对由范畴Set上的双函子得到的一类余代数给出了弱互模拟的余代数定义。 将系统的弱双相似性转化为变换后系统的强双相似性。 转换包括两个步骤：首先，行为上的行为扩展到有限词上的行为。其次，有限词的行为取模隐藏不可见的动作，产生在无声步骤下关闭的词的等价类上的行为。共代数定义由两个对应结果证明，一个对应于Milner的弱互模拟的经典概念，另一个对应于Baier和Hermanns倡导的生成概率转移系统的弱互模拟概念。关键词：余代数，互模拟，弱互模拟，标号迁移系统，生成概率迁移系统1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.06.050212A. Sokolova等人/理论计算机科学电子笔记122（2005）2111介绍本文给出了作用型系统弱互模拟的定义。动作类型系统的典型示例是熟悉的标记转换系统（LTS）（参见，例如，[20，18]），而且许多类型的概率系统（参见，例如，[16，27，11，3，26]）属于这一类。为了强调作用的作用，我们认为余代数产生于范畴集上的双函子。在验证一个系统的属性时，强双相似性往往是太强的等价性。弱双相似性[17，18]是一个松散的等价系统，抽象出无形的步骤。 众所周知，在标记转移系统S的弱双相似性的具体情况下，相当于在'双箭头'系统S jj诱导的强双相似性由S.我们利用这一思想，在制定一个一般的弱biimilation的coalgebrical定义。给定系统S，我们的方法包括两个阶段：(i) 首先，我们定义一系统SJ在有限迹上捕获S(ii) 接下来，我们固定一组不可见的动作τA，并将SJ转换为从τ步抽象出来的然后我们定义S上的弱双相似性为弱-τ-扩张SJJ上的强双相似性。在具体的概率转移系统的背景下，已经有几个建议弱互模拟的概念，往往依赖于所考虑的特定模型。Segala [27，26]为他的简单概率自动机模型提出了四个弱关系的概念。Baier和Her- manns [3，2，4]对生成概率系统的弱互模拟给出了一个相当吸引人的定义Philippou，Lee和Sokolsky [21]研究了交替模型 [14] 中 的 弱 互 模 拟 。 这 项 工 作 由 Desharnais ， Gupta ， Jagadeesan 和Panangelan扩展到无限系统[9]。Desharnais等人还提供了弱互模拟的度量模拟[8]。在这里，我们在一个共代数框架中工作，并使用互模拟的一般coalge-coalge装置[1，15，25]。对于这种情况下的弱互模拟，Rutten对while程序[24]的弱互模拟进行了早期工作，Rothe [23]对弱互模拟进行了语法方法。在后一篇文章中，对一类特殊的1 由PROGRESS项目ESS.5202支持的研究，（a）MaPAoTS2电子邮件：a. tue.nl3电子邮件地址：evink@win.tue.nl4Email：harald.woracek@ tu wie n. 梭的tA. Sokolova等人/理论计算机科学电子笔记122（2005）211213通过将余代数转化为LTS，并利用Milner在LTS中的弱互模拟，得到了余代数.这种方法还允许定义弱同态和弱模拟关系。后来，在Rothe和Masulovic[22]的工作中，发展了一个复杂的算法理论他们还考虑了一个选择的“观察者”和一个函子的隐藏部分。然而，在概率系统和相似系统的情况下，弱互模拟的定义不会导致直观的结果，也不能与上面提到的弱互模拟的具体概念联系[22]中使用的所谓跳跃关系似乎是主要障碍，因为尚不清楚如何将定量信息纳入其框架。本论文中提出的定义弱双相似性的两阶段方法，放大了米尔纳的原始想法，是相当自然的。在范畴论的背景下，在[10]中，它已经在预层模型上弱互模拟的开映射处理的上下文中然而，在本文中采取的方法产生了一个相当基本和直观的概念弱互模拟。此外，不仅对于标号转移系统的情况，而且对于概率系统，本共代数建议对应于具体的定义。尽管弱互模拟的共代数定义很有吸引力，但对应结果的证明可能会从直接到技术上有所不同例如，在技术报告[29]中，标记转移系统的相关定理不到一页，而证明生成概率系统的对应结果需要大约20页（包括额外的机器）。本文的组织如下：在第2节中，我们提供了所考虑的系统的基本定义和性质第3节给出了弱互模拟的共代数定义。我们表明，我们的弱双相似性的概念导致米尔纳第5节致力于生成系统类关于Baier和Hermanns的弱双相似性定义以及我们的共代数定义的对应结果。最后，第6节以一些结论性意见结束。2系统与双相似性从余代数的观点[15，12，25]，一个系统是一个给定的内函子的余代数，通常在范畴Set上。然而，对于我们定义弱双相似性的方法，显式指定可执行操作的集合至关重要。因此，我们将从双函子而不是内函子开始214A. Sokolova等人/理论计算机科学电子笔记122（2005）211SF→ F.∃在Set上，cf. [5]的文件。双函子是任何函子F：Set×Set→Set。如果F是双函子且A是一个固定的集合，那么集合内函子FA定义为：FAS=F（A，S）和FAf=FidA，f，（1）对集合S和映射f：S→T.为了进一步参考，我们陈述以下简单性质。命题2.1设F是双函子，A1，A2是两个集合，f：A1→A2a映射. 则f诱导自然变换η f：F A <$F A，由下式给出：2η f= Ff，idS.Q对于双函子F，集合S和A以及映射α：S→FA（S），三元组αS，A，αR称为F-A余代数.两个F-A共轭代数<$S，A，α<$与<$T，A，β<$之间的同态是满足F-Ah<$α=β<$h的函数h：S→T.A余代数与它们的同态一起形成一个范畴，我们用CoalgA表示。F定义2.2设λS，A，αλ和λT，A，βλ是两个F-A余代数. A，α∈S和β ∈T，A，β∈ T之间的双模拟是关系R ∈ S × T，使得存在一个映射γ：R A R，使得投影π1和π2在各自的余代数之间同态，S，π1Rπ2 Tαγ。βJ.JJS，FAπ1名法、阿、俄FAπ2FAT也就是说，使上图中的两个正方形交换。两个状态s∈S和t∈T是双相似的，记为s<$t，如果它们通过在<$S，A，α<$和<$T，A，β<$之间的某种互模拟而相关。设FA和GA是两个Set函子，η：FA<$GA是一个自然变换.自然变换η诱导函子T：CoalgA→CoalgA由FG给出T（ηS，A，α）= ηS，A，η S<$α且T（f）= f。（二）由自然变换导出的函子保持同态（参见。[25]因此保持互模拟关系和双相似性。接下来，我们介绍两种基本类型的系统，标记为过渡系统和生成系统，这将是续集中的主要例子。 我们首先给出它们的具体定义，以及它们对应的互模拟关系的具体定义，参见。[17、18、16、11]。1FAA. Sokolova等人/理论计算机科学电子笔记122（2005）211215∞{|∈}i∈Ii∈J一个标号跃迁系统，简称LTS，是一个三重的S，A，→ A，其中S是状态的集合，A是动作的集合，→S×A×S是过渡区通常，当ver∈s，a，sJ∈→时，w e表示s → a s j。定义2.3设S，A，→ S是LTS。一个等价关系R<$S×S是关于<$S，A，→<$S的强互模拟当且仅当，对于每个对<$s，t<$∈R和所有a∈A，它成立，s→a sJ=tJ∈S：t→atJ∈ R.两个状态s和t被称为双相似的，当且仅当它们通过某种互模拟关系相关联。符号：slt。将LTS的转移关系替换为定义2.4生成概率系统是一个三元组S，A，P，其中S和A是集合，映射P：：S×A×S→[0， 1]具有这样的性质，即对所有s∈S，它保持：a∈A∈，sJ∈SP（s，a，SJ）∈ {0，1}.（三）同样，我们将S称为系统的状态集，将A称为系统的动作集。P称为概率转移关系。条件（3）指出，对于所有s∈S，P（s，，）要么是A×S上的概率分布，要么是P（s，，）≠0，即s是一个终止状态。 像往常一样，我们写sa[p]sJ，无论何时P（s，a，sJ）=p，ands→asJ，其中P（s，a，sJ）>0。−→为了澄清条件（3），让我们回顾一下，任意的家庭{x i|非负实数的i ∈ I}定义为x i= sup {|JI，Jfinite}.注意，如果i∈Ixi<，那么我们也有集合xi i I，xi= 0是有限的或可数无限的。定义2.5设A，P，S是一个生成系统。 一个等价关系R<$S×S是S <$S，A，P<$S上的（强）互模拟当且仅当，对每一对s，t∈R，所有a∈A，所有等价类C∈S/R，则有P（s，a，C）= P（t，a，C）.216A. Sokolova等人/理论计算机科学电子笔记122（2005）211ΣL×这里我们设P（s，a，C）=SJ∈CP（s，a，SJ）.两个状态s和t是双相似的当且仅当它们通过某种互模拟关系相关联。表示法：斯韦格湖现在让我们转向共代数的观点。LTS可以看作是对应于双函子的余代数L= P（Id×Id）。也就是说，如果αS，A，→ α是LTS，则αS，A，αα，其中α：S→ LA（S）由下式给出：a，sJ<$∈α（s） ⇐⇒s→asJ，是A余代数，反之亦然。生成系统也可以看作是双函子G=D（Id×Id） +1。这里，D表示Set上的分布函子，即，DX ={µ：X → [0，1] |µ（x）= 1}和（Df）（µ）（y）=x∈Xf（x）=y对于一个集合X和一个映射f：X→Y（且μ∈ DX，y∈Y）。如果αS，A，Pα是生成系统，则αS，A，αα是GA余代数，其中α：S→ GA（S）由下式给出：α（s）（a，sJ）=P（s，a，sJ），反之亦然这里，单例集合1被解释为包含A上的零函数的集合S. 注意，α（s）是零函数，当且仅当 % s是终止状态。LTS和生成系统的双相似性的具体概念和各自的共代数定义是一致的。例如，对于LTS的情况，可以在[25]中找到直接证明。对于生成系统，这一事实可以追溯到[30]，其中考虑了马尔可夫链，并在[6]中处理了具有有限支持的生成系统。在这里，我们描述了一个一般的程序，以获得这种符合结果它适用于LTS以及生成系统在其充分的一般性。此外，我们将应用第5节中讨论的函子的双相似性的具体刻画（引理2.12）的方法。A. Sokolova等人/理论计算机科学电子笔记122（2005）211217⟨ ⟩ ∈ ⇒≡F→FF日本语简体中文⊆× ⟨⟩你好 |{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy110}定义2.6设R∈S×T是一个关系，F是一个集合函子。关系式F，R<$FS×FT，定义为：x<$F，Ry<$z∈ FR：Fπ1（z）=x，Fπ2（z）=y，对x∈S，y∈T，称为R关于F的提升.下面的引理直接来自定义2.2。引理2.7关系RS×T是FA系统的互模拟<$S，A，α<$和<$T，A，β<$当且仅当<$s，t<$∈R =<$α（s）<$FA，R β（t）.Q注意蕴涵式s，t R=α（s）FA，R在具体情况下，β（t）通常称为传递条件。在本节的剩余部分，我们收集了一些与回调弱保持相关的结果。如果一个函子将任意带外延分支的回调图变换为弱回调图，则称它弱保持总回调。对带外延分支的回调的限制，而不是任意的回调，是一个新的技术性问题，这在下面需要。引理2.8如果函子F弱保持总拉回，且R是S上的等价则R关于的提升F，R是余跨距的集合FSFcF（S/R），FcFS（四）其中c：S S/R是将每个元素映射到其等价类的规范态射。Q假设函子F弱保持总拉回，并假设R是S上的等价互模拟，即，R是S上的等价关系和互模拟，使得S，t∈R。 cospan（4）的集合中的回调是集合{x，y，|Fc（x）=Fc（y）}。通过引理2.8，这个集合与提升关系一致F、R.因此，xF，Ry c（x）=c（y）。因此，如果我们成功地用α（s）和α（t）的表示来具体表示（c<$α）（s）=（c<$α）（t），我们就得到了互模拟这一特殊概念的转移条件。例如，考虑LTS函子LA，其保持弱回调。对X∈ LA（S），即X<$A×S，有LA（c）（X）= P <$idA，c <$（X）= idA，c（X）= a，c（s）a，sX. 利用引理2.7，我们得到等价R S S是LTSS，A，α的共代数互模拟当且仅当s，t|⟨a, sJ⟩ ∈α (s)}={⟨a, c (tJ) ⟩ |<$a，tJ<$∈α（t）}218A. Sokolova等人/理论计算机科学电子笔记122（2005）211LG→→x∈Cy∈Dy∈Dx∈C或者等效地，s，t∈R=s→sJ=tJ∈S：t→atJ<$sJ，tJ<$∈R）。因此，我们得到等价关系R是定义2.2意义下关于A的余代数互模拟当且仅当它是定义2.3意义下的具体互模拟。通常，为了使函子是“良好的”，需要保持弱回调 可以很容易地看出，弱保持总回调的较弱条件使得双相似性已经是等价的。我们需要放松弱回调保持的条件，因为我们需要弱保持总回调但不保持弱回调的函子的互模拟的特征。接下来，我们关注函子A的弱拉回保持。对于定义有限支撑生成系统的函子，De Vink和Rutten [30]使用图论最大最小割定理证明了弱拉回保持，Moss[19]使用初等矩阵填充性质证明了弱拉回保持。我们遵循后一种方法来处理任意的无限矩阵。引理2.9函子D保持弱拉回。Q引理2.9的证明依赖于下面的引理2.10设C和D是集合，且设φ：C[0，1]和n：D[0， 1]使得φ（x）= φ（y）<∞。（五）则存在函数μ：C×D→[0，1]，使得µ（x0，y）=φ（x0） 和对任意x0∈C和任意y0∈ D.Q利用引理2.8，可以证明，集合S上的等价关系R是生成系统S，A，α关于函子GA的共代数互模拟，当且仅当它是根据定义2.5的具体互模拟。对于弱概率互模拟的处理，我们需要考虑一A. Sokolova等人/理论计算机科学电子笔记122（2005）211219G G G P×P → → G∗ ∗∗FG⎨⎨∈⊆联系我们P→另一种系统。 设G是双函子，定义为G（A，S）=P（A）×P（S）→[0，1]对于集合S和A，并且，Gf（ν）=νf1−1，f2−1.对态射f=<$f1，f2<$：A×S→B×T（其中ν∈ G<$（A，S））.考虑对应于的集合函子A。显然，A（S）=（A）（S） [0，1]且对映射f：ST，有<$Af（ν）=ν<$ idA， f−1. 我们是一家人来刻画这个函子的等价互模拟。为了应用引理2.8，我们需要以下性质。引理2.11函数G_A可以表示总的pul_ack。Q值得注意的是，GAdostpreserverveeeakpullbacks：Choosea setXwithth|X|≥3. 固定x0∈X。 设Z ={1，2，3}，并考虑cosspan XZ， X对于由下式给出的映射f，g：X→Z，f（x）=12x=x001否则且g（x）=x003否则该cospan的集合拉回是{x0，x0x}，并且它没有被G_A转换为we ak pullback。设R是集合S上的等价关系。一个子集MS是一个R-饱和集，如果对所有的s M，s的整个等价类包含在M中。我们用Sat（R）表示S的所有R-饱和子 集 的 集 合 . 实 际 上 ， M 是 饱 和 集 当 且 仅 当 对 S/R 中 的 集 合 Cii∈I ，M=i∈ICi。因此，在R-饱和集和P（S/R）的元素之间存在一一对应现在，考虑到C_spanG_SG_A_cG_s（S/R）G_A_cG_S的拉力P。我们有μ，νA A，A⇐⇒µ◦⟨idA, c−1⟩=ν◦⟨idA,c−1⟩⇐⇒ ∀AJ⊆A,∀M⊆S/R:µ(AJ, c−1(M)) =ν(AJ, c−1(M))⇐⇒ ∀AJ⊆A,∀M∈Sat(R):µ(AJ,M) =ν(AJ,M)因为c−1：（S/R）Sat（R）是双射。因此，我们展示了以下特征。220A. Sokolova等人/理论计算机科学电子笔记122（2005）211J∗∗F GGF引理2.12A等价关系R是G-A系统的互模拟<$S，A，α<$当且仅当<$s，t<$∈R=<$$>AJ<$A，<$M∈ Sat（R）：α（s）（AJ，M）=α（t）（A，M）.3弱互模拟在本节中，我们给出了动作类型系统的弱互模拟的一般定义。我们的定义受到了具体系统弱互模拟定义的启发。出发点是这样的想法，即给定系统的弱互模拟产生为从原始系统获得的系统的强互模拟。弱互模拟的定义包括两个阶段。首先，我们定义一个所谓的扩展系统，它捕获了原始系统中A中的单词的行为，而不仅仅是A中的动作。- 扩展应该以忠实的方式从原始系统中第二阶段考虑的是隐形。给定一个不可见行为的子集τA，我们通过定义一个所谓的弱τ-扩展系统，将τ-扩展限制为仅可见行为。在这个系统中，标签是词的等价类。然后一个弱原系统上的互模拟关系是弱-τ-扩张上的互模拟关系。定义3.1设F和G是两个双函子。设Φ是一个映射，它赋给每个A余代数S，A，α，一个具有相同状态集的A余代数系统S，A余代数，αJ，使得满足下列条件：(i) Φ是单射的，即Φ（λS，A，αλ）= Φ（λS，A，βλ）λα=β;(ii) Φ保持并反映双相似性，即系统εS，A，αε中的sεt当且仅当系统Φ（εS，A，αε）中的sεt。nΦ是从F到G的代数变换，nΦ：F→G证明了Φ（αS，A，α<$）是αS，A，α<$的α-扩张.G，我们说定义3.1中的条件（i）和（ii）保证原始系统[6，28]。初看起来，这似乎是违反直觉的，即双转译产生了另一种类型的系统，即双函子而不是双函子。然而，这种额外的自由是至关重要的情况下，开始函子是不够的表达，以允许一个双扩展（参见。第5节生成系统）。以前的工作[6，定理3.9]提供了一种获得n-平移的方法也就是说，如果λ：FA <$GA<$是具有内射分量的自然变换，并且函子FA保持弱拉回，则诱导函子是a翻译（cf.等式（2））。然而，考虑到新出现的A. Sokolova等人/理论计算机科学电子笔记122（2005）211221∗τS≈≈⊆≈⟨⟩⊆ ⇒≈⊆≈⊆τ仅仅从自然的转变中，是不够的。实际上，第4节和第5节中的反翻译不是从自然转换中产生的接下来，我们讨论如何处理不可见动作的子集τA隐藏函数hτ：A→（A\τ）是同态，使得hτ（a）=a，如果a/∈τ，并且hτ（a）=ε，对于a∈τ（其中ε表示空字）。考虑集合Aτ=（A\τ）。 根据命题2.1，隐藏函数hτ：Aτ→Aτ确定自然变换，使得η：GAGAτ 和ηS= Gh τ，idS.设函子π τ：CoalgAπ →CoalgAτ由自然转化而来τG Gmationη，即<$τ（<$S，A<$，αJ<$）=<$S，A τ，αJJ<$其中αJJ= η τ<$αJ且<$τf = f(see等式（2））。弱τ-平移Φ和集合的弱τ-平移因此，不可见作用的集合τ被定义为组合Wτ= ττ Φ。定义3.2LetF，Gbtwo双函子s，Φ：F→Ga-translationandA. 关系R<$S×T是两个F-系统<$S，A，α<$的弱互模拟以及R_T，A，β_r关于Φ和τ的互模拟当且仅当R是余代数Wτ（R_S，A，α_r）和Wτ（R_T，A，β_r）的互模拟两个态s∈S和t∈T关于Φ和τ是弱互相似的，记作sτ t，如果它们通过关于Φ和τ的某种弱互模拟而相关。下一个命题指出，定义3.2意义下的弱双相似关系τ满足弱双相似关系的基本性质命题3.3LetF，Ge两个双函子，Φ：F→G，S，A，α→F A余代数A且让τ表示S，A，α上的弱双相似性，关于Φ和τ。然后，下面的保持：(i) 对于任何τ A，即强双相似性意味着弱。(ii) = 强双相似性是在没有不可见动作的情况下的弱双相似性。(iii) τ1τ2τ1τ2 对于任何τ1，τ2A，即当更多的动作不可见时，弱双相似关系变得更粗糙。Q应该注意的是，在[29]中给出的上述命题的证明中，定义3.1中引入的所有要求都已被利用。因此，这些要求似乎是自然的。对定义3.2的进一步解释将在以下两节中收集，在这两节中，我们将探讨标记变迁系统和生成概率变迁系统中的共代数弱互模拟的具体情况。222A. Sokolova等人/理论计算机科学电子笔记122（2005）211∗K为了进一步参考，我们引入一些更多的符号。对任意w∈Aτ=（A\τ） <$ ，wedenoeBw=h−τ1（{w}）<$A<$. 我们把其他的设置都当作块。 注意，对于w= a 1.，Bw=τa1τ· ·τakτ。 . ak∈（A\τ）<$.传统上，不可见动作的子集仅仅是由无声步骤τ组成的单例。然而，除了可以处理多个不可见动作的一般定义的数学吸引力之外，这种可伸缩性也是有利的，例如在处理Segala系统的弱互模拟时（参见。[27，26]）。4标号迁移系统在本节中，我们重新定义了Mil- ner弱互模拟的标准定义[17，18]。我们提供了一个弱互模拟的共代数公式与具体的一个相吻合的一个定义4.1设S，A，→ S是LTS。设τ∈A是一个不可见作用。等价关系R <$S ×S是关于<$S，A，→ S的弱互模拟当且仅当每当<$s，t <$∈R，则s→a sJ=tJ∈S：t→τ∗◦→a◦→<$tJ<$$>sJ，tJ<$∈R，对于所有a∈A\ {τ}，且s→τ sJ=tJ∈S：t→τtJ∈ R.两个态s和t被称为弱双相似的，当且仅当它们通过某种弱互模拟关系（记作s<$lt）相关联。设L，LA是具有标签集A的LTS的函子，如第2节所介绍的。下面的-translationΦ捕捉了从动作到有限动作串的转换关系的自然扩展。定义4.2设Φ赋给任何LTS，即一个LA余代数S，A，α∈，则LA∈ 余代数αS，Aα，αJα，其中，对于w = a1. a k∈ A，w，sJ∈αJ（s） 如果 和 只 如果有 存在国 s1，.，s k−1∈S等的s−a→1s1−→ s2···sk−1−→sJ。我们有以下对应结果。定理4.3(i) 由定义4.2给出的赋值Φ是一个双平移。τ一个2A. Sokolova等人/理论计算机科学电子笔记122（2005）211223∗一个k1.Σ2我 一期+1一期+1(ii) 设αS，A，αS为LTS。 设τ ∈ A是一个不可见作用量，s，t ∈ S是任意两个状态. 则s根据定义3.2关于Φ和{τ}使{ τ } t变小当且仅当s根据定义4.1使t变小。Q定理4.3的证明很简单，可以在[29]中找到。5生成系统在本节中，我们将讨论生成概率转移系统及其弱双相似性。Baier和Hermanns[3，2，4]的工作的启发，我们提供了一个翻译，我们基于生成概率系统的弱互模拟的概念。我们表明，我们的定义与Baier和Hermanns的定义一致。与LTS的情况不同，在这里，我们的设置的一般性是必要的，因为双平移确实产生了生成系统类设A，P， S是一个生成系统。一个有限的路径π的S，A，P是一个的1一个2alternatinggsequenceπs0−→s1−→ s2···sk−1−→ sk使得k∈N0，si∈S，aj∈A且P（si，ai+1，si+1）>0. Weputlength（π） =k，first（π） =s0，最后（π） = sk，迹（π） = a1a2···ak.我们用ε表示从s开始的空路径。S，A，P的无穷路π是交错序列一个2πs−a→1 slong→s· ··其中r对所有i≥1，P（s， a， s ）>0. 第一次非空路径的元素由first（π）表示。一个完整的路径是一个无限路径或一个以终止状态结束的有限路径所有（有限或无限）路的集合、所有有限路的集合和所有完全路的集合此外，对于s∈S，我们写路径= π∈路径|第一个（π）= s类似地，我们使用FPaths（s）和CPaths（s）。 集合路径部分地由预定关系“排序。对于所 有 π ∈ P a t h s （ s ） ， Noth a tε“π.我们强调，对于任意状态s ∈ S，集合FPaths（s）至多是可数的. 对于有限路径π∈FPaths（s），我们将π↑ ={π ∈ CPaths（s）|π“π}。我们称π↑为π的完全路锥。让r={π ↑ |π ∈ FPaths（s）}表示从s开始的所有圆锥的集合。注意，任何两个锥π1↑和π2↑要么不相交，要么一个是另一个的子集，反之亦然。从这个224A. Sokolova等人/理论计算机科学电子笔记122（2005）211联系我们一个2一个k{的元素Xn∈Γ π{π}，则Prob（X）=nProb（Xn）.不加性;我们只有Prob（n）≤π∈<$Prob（{π}）. 然而，对于集概率（%）=π∈Prob（π↑）. 每一个集合都可以由一个极小的而FPaths（s）至多是可数的，我们看到Γ具有以下性质：– 它包含空集，– 它相对于交叉点是封闭的，– 对于任意两个元素X，Y∈Γ{}，差X\Y可以写成Γ{}中元素的可数并。我们定义一个函数Prob：Γε {ε} →R，使Prob（ε）= 0，Prob（ε↑）= 1，概率（π↑）= P（s，a1，s1）·P（s1，a2，s2）P（sk−1，ak，sk），对于π=s-a→1 s−→s· · ·s−→s。让我们注意到，函数Prob是1 2k1k确是善报。此函数具有以下属性：– Prob(– Prob（X）≤Prob（Y）当X<$Y对X，Y∈Γ <${<$}，– 如果X∈Γ π{π}可以写成一个最小连表，则连接并X=πnXn从[31]5可以得出，Prob可以唯一地扩张到由Γ生成的σ-代数上的测度。因为根据定义，Prob（ε）= 1，这是一个概率测度。如果f= F路径，则我们用f↑ f = CP路径表示集合Π ↑ =π ↑。π∈Π注意，↑属于由Γ{}生成的σ-代数。导出测度通过将P rob（f）定义为卷积的平均值而产生函数Prob：P（FPaths（s））→R。一般来说，其功能是，在某种意义上说，这是最小的，平等仍然成立。这里，我们称一个集合为FPaths（s）minimal，记作min（n），当且仅当对于任意两个di，ntπ1，nπ2∈ nΠw既不是raveπ1“π 2，也不是π 2“π 1。Ifmin（），then集 对于多个FPaths，令↓ ={π ∈ |<$πJ∈ <$：πJ/<$π}[5]参考[31]而不是更流行的文本，如Halmos [13]的要点是，[31]中的扩张定理的版本适用于半环，其中集合的集合可以表示为半环元素的可数并而不是有限并。A. Sokolova等人/理论计算机科学电子笔记122（2005）211225J JJ→一个k∪∪1K1K一个2w∈Xw∈Xi∈Ij∈Ji∈Ij∈J则↑=（↓）↑。 最后，设s∈S，SJ<$S和W<$A<$。 我们把s→WS J={π∈F P aths（s）|first（π）=s，last（π）∈S J<$S，trace（π）∈W<$A<$}↓，并且writProb（s，W，SJ）=Prob（s→WSj）.我们继续提出的生成概率系统的双函子G捕获的-翻译。定义5.1设Φ g赋给每个生成系统，即，对于任意G_A_c_e_b_S，A，α_j，G_A_c_e_b_S，A_c_d，α_J，其中W_c_a_ s和S_j_S，α（s）（W，S）= Prob（s，W，S）.定理5.2赋值Φ g是一个π-平移。Q[29]这是一个证明。主要困难是保持双模拟。为此，对路径集合进行了详细的分析f→a1C· · ·→C，其中hC， . . ， Cequiv a lenceclassesofstates模互模拟关系。在Φg的上下文中，弱-τ-系统具有以下形式：<$τ<$Φg（<$S，A，α<$）=<$τ（<$S，A<$，αJ<$）=<$S，Aτ，αJJ<$其中αJJ（s）：P（Aτ）×P（S）→[0，1]由下式给出：αJJ（s）= η τ（αJ（s））= Gh τ，idS（αJ（s））= αJ（s）h−1，idS。S τ因此，对于X<$Aτ=（A\τ）<$且SJ<$S，我们有：αJJ（s）（X，S J）=αJ（s）（h−τ1（X），S J）=αJ（s）（Bw，S J）=Prob（s，Bw，S J）.因此，从引理2.12我们得到，等价关系R是生成系统S，A，α上关于Φg和τ的弱-τ-互模拟当且仅当S，t∈R意味着，对于任何块集合{Bi}i∈I，任何集合{Cj}j∈J的类，它认为，概率， B i，C j）= Prob（t，B i，C j）。（七）注意，i∈IBi是ker（hτ）-饱和集，j∈JCj是R-饱和集.接下来，我们回顾Baier和Hermanns [3，2，4]对生成系统的弱互模拟的最初定226A. Sokolova等人/理论计算机科学电子笔记122（2005）211义。A. Sokolova等人/理论计算机科学电子笔记122（2005）211227≈≈∈\ {}定义5.3设S，A，P是生成概率系统。 设τ∈ A是一种无形的行为.一个等价关系R<$S×S是在<$S，A，P<$S上的弱互模拟当且仅当对于每个对<$s，t<$∈R，所有作用a∈A和对于所有等价类C∈S/R，它成立Prob（s，τα<$τα，C）=Prob（t，τα<$τα，C），（8）当对αAτ，τα=ε，e α <$= α时，则为空. 两个国家的s和t是弱互相似的，当且仅当它们通过某种弱互模拟关系相关联。记法是“t”。我们有以下对应结果。定理5.4设αS，A，αS是生成系统. 设τ ∈ A是一个不可见作用量，s，t ∈ S是任意两个状态. 则根据定义3.2关于Φ g和{τ} s∈{τ}t，当且仅当根据定义5.3s∈gt。该定理的充分性部分很容易成立，记住定义5.3和方程（7），因为对于任何a∈A\ {τ}，τ和τ aτ都是ker（h{τ}）-饱和集。此外，每个R-等价类都是R-饱和集.因此，{τ}至少和g一样强。必要性证明更加投入。在[29]中，一系列引理表明（8）蕴涵（7）。困难在于，表达式Prob（s，W，M）在其第二个或第三个参数中不是加法的证明利用组合参数需要详细分析的几何路径。请注意，在LTS的定性设置中不会出现6总结发言在本文中，我们提出了一个弱互模拟的行动型系统的共代数定义为了证明它的正确性，我们考虑了熟悉的标号转移系统和生成概率系统的情况，并论证了余代数概念与具体定义一致此外，本文还包括一些其他较小的贡献。本文建立在与Falk Bartels [6，7]合作的早期工作基础上。在第2节中，我们讨论了一个通用的方法，以获得对应的结果，共代数与具体的互模拟。我们的介绍概括了直接的方法与明确的证据中提到的主要想法是根据提升的互模拟关系F，R和特定cosspan的拉回来捆绑共代数互模拟的重新表述（参见引理2.8）。 该方法适用于任何弱保持全回撤，即具有epi腿的回撤，比弱回撤保留更弱的条件。228A. Sokolova等人/理论计算机科学电子笔记122（2005）211D我们对概率分布的处理避免了限制支持集的基数，这是一个有技术意义的事实。 结果适用于第2节的函子捕获的任意离散分布。虽然我们没有对所考虑的状态空间施加基数限制，但生成概率系统本质上是离散的。Baier和Hermanns的工作只处理有限系统，也是因为[3，4]中的算法考虑。由于我们在这里不涉及这类问题，因此，对于任意大小的系统，给出了具体的和余代数的定义。致谢我们感谢福尔克·巴特尔对互模拟的具体概念和共代数概念的对应关系进行了各种讨论，这些讨论进入了本文。我们感谢匿名推荐人的宝贵意见和建议。引用[1] Peter Aczel和Nax Mendler 一个最终余代数定理 在DH Pitt，D.E. 莱德希尔P. 今天上午，我和你一起去。 Pittts，anddA. Poign'e，editors，Proc. CTC S第3版，LNC S第389卷，第357-365页。Springer，1989年。[2] C.拜尔概率系统的数学验证方法Habilitationsschrift，Un iver sitüatMannheim，1998.[3] C. Baier 和 H. 赫尔曼弱 互模拟 为 全概率过程。在O. Grumberg，编辑，Proc. CAVLNCS 1254，1997年。[4] C. Baier和H.赫尔曼全概率过程的弱互模拟。 Technical Report[5] F.博塞 分类代数手册。剑桥大学出版社，1994年。[6] F. Bartels，A. Sokolova，and E.P. de Vink.概率系统类型的层次结构。在H.P.Gumm，编辑，Proc.CMCS 2003中。ENTCS 82，2003年。19页。[7] F. Bartels，A. Sokolova，and E.P. de Vink.概率系统类型的层次结构。计算机科学，2004年。在出版社。[8] J. Desharnais，V. Gupta，R. Jagadeesan和P. Panangelan.概率过程弱互模拟的度量模拟 在procLICS 2002，第413-422页。IEEE，2002年。[9] J. 德沙尔奈河谷古普塔河，巴西-地Jagadeesan和P.帕南加。 弱互模拟对于PCTL是合理的和可实现的。 因湖 Brim，P. 是的，M。你知道的，还有A。 Kuer a，e d it or s，P roc.CONCUR2002，第355-370页。LNCS 2421，2002年。[10] M. Fiore，G.L. Cattani和G.温斯克弱互模拟与开映射。在Proc. LICSIEEE，1999年。[11] R.J. van Glabbeek，S.A. Smolka和B. Ste daughen. 概率过程的反应、生成和分层模型。信息与计算，121：59[12] 惠普口香糖余代数的一般理论基础技术报告LUATS[13] P.R.哈莫斯 测量理论范诺斯特兰德1950年A. Sokolova等人/理论计算机科学电子笔记122（2005）211229[14] H. A.汉森分布式系统形式化设计中的时间和概率。乌普萨拉大学博士论文，1991年。[15] B.P.F.雅各布斯和J.J.M.M.拉顿关于（余）代数和（余）归纳法的教程。EATCS公报，62：222-259，1996年。[16] K.G. Larsen和A. Skou.通过概率测试进行互模拟。信息与计算，94：1[17] R.米尔纳通信系统的微积分。LCNS 92，1980年。[18] R.米尔纳并发进程的操作和代数语义。在J. van Leeuwen，编辑，Handbook of TheoreticalComputer Science，第1201-1242页。Elsevier and MIT Press，1990.[19] L.S.莫斯 共代数逻辑 Annals of Pure and Applied Logic，96：277[20] G.D.普洛特金操作语义学的结构化方法。技术报告DAIMI FN- 19，奥胡斯大学计算机科学系，1981年。[21] A. 菲利普 I. 李， 和O. 索科尔斯基弱互模拟 用于概率 系统. 在C. Palamidessi，编辑，Proc. CONCUR 2000，第334-349页。 LNCS 1877，2000。[22] J. R o和D。 我是你的朋友。对于煤炭企业来说，这是一个很大的挑战。 InA. 库尔茨，编辑，Proc. 并发、交