理论计算机科学电子札记192（2007）13-28www.elsevier.com/locate/entcs模拟高达和规范前序（扩展摘要）David de Frutos Escrig大卫·德·弗鲁托斯·埃斯克里格1，3DepartamentodeSistema sInform'ticosyComputacio'nUniversidad Complutense de Madrid西班牙马德里CarlosGregorioRodr'ıguez2，4DepartamentodeSistema sInform'ticosyComputacio'nUniversidad Complutense de Madrid西班牙马德里摘要在本文中，我们定义了模拟到一个前序，并展示了我们如何使用它们来提供一个共归纳的，类似模拟的，过程的语义前序的表征。结果适用于广泛的一类前序，特别是所有的语义前序粗糙比准备好的模拟前序的线性时间分支时间谱。一个有趣但意想不到的结果是，当从等价关系构建时，模拟到是一个典型的前序，其内核是给定的等价关系。这些正则前序有几个很好的性质，主要是因为它们都是以齐次的方式定义的，所以它们的性质可以用一般的方式证明。特别是，我们提出了一个公理化的特征，这些典型的前序，这是通过添加一个单一的公理化的原始等价关系。这给了我们线性时间分支时间谱中每一个可公理化的前序的另一种公理化，它的正确性和完备性可以被一劳永逸地证明。关键词：过程，语义前序，模拟，线性时间分支时间谱。1介绍及相关工作每当引入一个语义框架来定义某种形式语言的含义时，也会引入一个等价关系，如果两个术语具有相同的语义，则将它们等同起来反过来，等价关系提供了一种1由西班牙微额信贷项目DESAFIOS TIN 2006 -15660-C 02 -02和项目PROMESAS-CAM S-0505/TIC/0407提供部分支助。2 由西班牙MEC项目WEST/FAST TIN 2006 -15578-C 02提供部分支助。3电子邮件：defrutos@sip.ucm.es4电子邮件：cgr@sip.ucm.es1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.01414D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）13定义一个抽象的语义，将每个术语与它所属的等价类联系起来。进程代数已被广泛用于描述和研究反应系统的行为，并产生了著名的语言，如CSP，CCS或ACP。许多不同的语义和他们各自的等价关系已经提出了反应系统。其中大部分是在Van Glabbeek [9]深入研究的线性时间分支时间谱（简称ltbt）中收集的。在那里，他提出了一个几乎详尽的语义集合，每个语义的特征是一个自然的测试场景，一个模态逻辑来识别等价过程的集合，以及一个有限公理化来比较任何一对有限过程。互模拟语义是谱中最强的等价语义，也是最重要的等价语义之一。互模拟等价可以很容易地定义，因为它的共归纳性，因此可以应用共代数技术，这为基于归纳和连续性论证的经典方法提供了一个富有成效的替代方案。此外，可以很容易地建立一个有效的算法，在此基础上，几个工具，可以有效地检查过程的双向相似性[5]。尽管自David Park [21]提出以来，互模拟已经得到了深入的研究（参见[24]最近关于该主题的历史介绍），但它仍然是最近许多论文的主题，如[17]。但有时互模拟等价性太强，许多其他有趣的语义弱于双相似性已被提出，其中大多数出现在ltbt频谱。例如，跟踪是流程最弱的合理语义。然而，非确定性行为并没有通过跟踪的方式得到正确的描述，因为死锁信息没有被准确地捕获。[12]中提出了故障语义来解决这个问题。一个更精确的语义是由就绪性定义的。故障和就绪集可以与跟踪组合，从而获得更强的语义，如[9]所述。不幸的是，一般来说，这些等价不能像互模拟语义那样容易地研究，主要是因为它们缺乏直接的共代数定义。然而，它是可能的互模拟和其余的语义，使这些coalgebraic技术可以用于他们的研究。在文献[6]中，我们证明了ltbt谱中的所有语义都可以被刻画为互模拟的子。这是通过放松互模拟的证明义务来实现的，这样在玩新游戏时，防守者可以在他移动时修改过程的后续转换，从而更容易证明相应的等价性。前序和等价关系密切相关，后者只是前序的一个特殊（对称）情况，而任何前序都通过其核定义了一个导出等价关系。虽然过程的语义是由等价关系定义的，但我们还需要顺序关系来比较对应于几个顺序关系的非等价过程，例如D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）1315此外，还需要一个序关系来规定语义域中的连续性要求这些顺序已经被彻底研究，特别是它们也出现在[9]中，其中它们使用经典的测试方法引入：本文主要研究过程的语义前序及其余代数刻画。我们可以在[19，4]中找到测试语义的递归定义，这可以被认为是朝着所需方向迈出的第一步，但在这两种情况下，作者在他们的特征描述中使用了after相反，我们想要一个更局部的表征，其中互模拟步骤解决了比较过程中的选择。人们可能会认为这不是一个困难的任务，因为[6]中的结果是过程等价的，但事实并非如此：互模拟是语义等价中最强的，因此放松互模拟要求的想法原则上允许得到较弱的等价。 然而，不存在以互模拟等价为核心的适当的前序;事实上，模拟前序（最自然的共归纳定义的前序）并不比ltbt谱中的许多语义前序更强，它诱导的等价关系比互模拟等价弱得多。幸运的是，我们可以通过加强模拟来克服这个障碍，也就是说，通过施加一些额外的条件来满足相关过程对。特别地，就绪模拟[15，2]是受过程的初始动作集应该相同的条件约束的模拟;就绪模拟前序比ltbt谱中任何其他有限可公理化的前序都要精细。正如我们将在本文的其余部分看到的那样，我们确实得到了前序的共代数特征，以及与等价和前序有关的有趣结果其中一个结果非常出乎意料，但也非常好：对于任何等价关系（在合理的假设下），存在一个典型的前序（非平凡的，即不同于等价本身），其内核是原始等价关系。这是许多令人愉快的性质背后的原因，特别是，我们可以系统地从相应等价的公理化中获得任何这些典型预序的有限过程的完整公理化，从而可以一劳永逸地证明这些公理化的完整性和正确性。此外，对于所有比Van Glabbeek谱中的现成模拟更粗糙的等价令人惊讶的是，在[1]中，作者发现了建立前序公理化之间的相反关系的方法，[5]我们要特别感谢Wan Fokkink提供的一些有用的提示，包括在讨论本文的前一版本时提供的提示，[1]中对该版本进行了第二次评论。事实上，根据那里的建议，我们在这个最终版本中稍微改进了一些结果，这样你就可以在他们的评论和这里的印刷文本之间找到一些不一致之处。16D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）13−→−→−→}弱于准备好的模拟和相应的等价物，在Van Glabbeek的频谱的语义。 我们同意他们的意见，事实上，从一个前序出发寻找诱导等价的公理化比反过来寻找诱导等价的公理化更自然。尽管如此，像我们已经做的那样，有一个规范的方法来获得一个核是给定等价关系的非平凡预序也是很好的本文其余部分的结构如下。在第2节中，我们介绍了过程和预序的基本定义和符号，并回顾了[6]中的一些结果。在第3节中，我们定义了模拟直到，并证明了一些结果，这些结果表征了模拟直到前序和模拟直到等价的行为前序这些结果分两步给出，首先是比模拟前序粗糙的前序，然后是比准备好的模拟粗糙的前序，这需要更详细的证明（尽管出现了很好的辅助结果）。在第4节中，我们将重点从前序转移到等价，并展示了一些结果，这些结果使我们能够将等价描述为模拟的内核。在此基础上，我们刻画了一个典型的共归纳前序，其内核是一个给定的等价关系。 在第5节中，作为本文中所发展的理论的应用的一个例子，我们提供了线性时间分支时间谱中的前序的另一种公理化定义。证明其完整性是容易和简单的，使用的模拟的想法，以发展的文件。最后，在第6节中，我们提出了一些结论和未来工作的路线。2个房间描述过程行为的通常方法是通过操作描述。像往常一样，我们通过使用Plotkin（转载于[22]）引入的标记迁移系统（定义2.1一个标号转移系统是一个结构T =（P，Act，→），其中P是一组过程、主体或状态; Act是一组动作; → P ×Act×P是一个转移关系。一个有根LTS是一个对（T，p0），其中p0∈ P.集合Act表示进程可以执行的操作的字母表，关系→描述了在执行操作之后的进程转换。 任何过渡关系→中的三元组p，a，q由p表示一q，表明进程P执行动作A并演变成进程Q。一个有根LTS描述了一个具体进程的语义：对应于它的初始状态p0。通常情况下，L TS不会在纸张上使用。我们写p−a→ifhere存在一个过程q使得paq。 函数I计算初始一个过程的动作，I（p）={a|a ∈ Act和pa.D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）1317一−→我有限过程的LTS如果扩大。这些有限树可以用基本进程代数BCCSP在语法上描述，例如，在[9，6]中也使用了它定义2.2给定一组动作Act，BCCSP过程的集合由以下BNF-文法定义：p：：= 0|AP|p + Q其中a ∈ Act。 0表示不执行任何操作的进程;对于Act中的每个操作，都有一个前缀运算符;+是一个选择运算符。我们在论文中提出的所有定义对任意过程都是有效的，也就是说，对任意有根的LTS，无论是有限的还是无限的。我们在第3节和第4节中提供的证明广泛地使用了归纳推理，因此它们只对BCCSP过程有效，即对有限过程有效。 然而，正如我们在[6]中所做的那样，通过使用标准的近似归纳原理[8]，我们可以首先将我们的所有结果扩展到无限深度的无限分支树过程，然后扩展到任意的有限分支转移系统，因为通过展开它们中的任何一个，我们都可以得到等价的无限树过程。图1中定义了BCCSP术语的操作语义。BCCSP进程的深度是它所表示的树的深度ap−a→pp−a→pJp+q−a→pJq−a→qJp+q−a→qJFig. 1. BCCSP术语后面的常量0被省略了：我们写a而不是0。 像往常一样（例如参见[9]），因为选择的操作语义定义了它，作为一个交换和结合运算符，以及任何其他语义，我们Σ基于此，我们可以使用n元选择运算符来写Σ Σ任何进程作为APi。这对应于每个进程的转换树，而我们使用集合作为索引的事实使得该算子根据定义是可交换的和可结合的。一个过程aqJ是过程q的a-被加数当且仅当qaqJ. 我们定义p|a作为（子）过程，我们通过将p的所有a-被加数相加得到。也就是说，Σ Σ Σ如果p =ap i，则p|=ap i.阿一阿阿一阿前序是自反的和传递的关系，我们用±表示。为了简单起见，我们使用符号±来表示前序关系±−1。每一个预序都导出一个等价关系，我们用表示，即p<$q当且仅当p±q和q±p。定义2.3过程上的前序关系±是行为前序，如果6 我们得到一棵树，如果我们在树上生成状态，则为生成的每个转换引入新状态 通过应用定义操作语义的规则，例如参见[18]。18D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）13BRsPW RTFTRFCSCTS不（x+y）+z=x+（y+z）+++++++++++x+y=y+x+++++++++++x+ 0 =x+++++++++++x+x=x·· ··· · ··· ··· · ·· · ·· ·· · ·· · ·· · ··· ··· · ··· ··+···+···+···+···+···+···+···+···+···+···+···ax±ax+ay++++++vvvva（bx+by+z）=a（bx+z）+a（by+z）I（x）=I（y）ax+ay=a（x+y）ax+ay±a（x+y）a（bx+u）+a（by+v）±a（bx+by+u）ax+a（y+z）±a（x+y）·· ··· · ··· ··· · ·· · ·· ·· · ·· · ·· · ··· ··· · ··· ········+···v+···VV+···VV+···vvvv+······vvvvv······vvvvv···ax±ax+y++vva（bx+u）+a（cy+v）=a（bx+cy+u+v）·· ··· · ··· ··· · ·· · ·· ·· · ·· · ·· · ··· ··· · ··· ··························+······v···x±x+y++ax+ay=a（x+y）+表1线性时支时间谱中前序的公理化I [9]• 它比互模拟等价性弱，即， p = B q <$p ± q，• 它是一个关于前缀和选择运算符的预同余，即如果p±q则ap±aq和p + r±q + r。从[9]中借用的表1显示了ltbt谱中一些语义的完整公理化，每个前序（列）的相应公理都标有“+"。标有“v”的公理是满足的，但不是必需的。列顶部的简写表示不同的语义，B表示互模拟等价，对于线性时间分支时间谱上出现的其余前序也是如此。表1左上方的前四个公理描述了互模拟等价性。它们也属于任何其他公理化特征，因此在讨论其他具有较少区分能力的语义时被例如，我们可以看到，准备好的模拟前序由互模拟等价的四个公理加上公理（RS）ax±ax+ay来表征。类似地，互模拟公理与公理（S）x±x+y一起表征模拟前序。让我们用一些关于语义等价的结果来结束这一初步部分在[6]中，我们引入了直到前序的互模拟，以削弱互模拟的定义，使得更弱的等价可以通过共归纳定义来定义2.4设±是一个行为预序。则过程上的二元关系S是直到±的互模拟，如果pSq意味着：• 对于a，如果p−a→pJ，则x为tqJ和qj，q±qJ−a→qJ和pJSqJ;a a a a a• 对于a，如果q−a→qJ，则x是tpJ和dpJ，p±pJ−a→pj和dpJSqJ。a a a a a如果存在互模拟，则两个过程在±以下是互相似的，记为p±D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）1319上至±，S，使得pSq.由±约简引入的附加能力推广了互模拟的原始定义，因此我们现在有更多的机会证明进程之间的等价性为了理解下面定理2.6中的条件，我们需要下面的定义。定义2.5当p±q蕴涵I（p）<$I（q）时，行为预序±是保持初始值的。当p ± q蕴涵p时，它是作用因式分解的（或仅仅是因式分解的）|a±q|a∈ I（p）.初始值保持和因式分解是任何“自然”进程语义都满足的属性定理2.6（[6]）设±是一个行为预序，它是保持初始值的，作用分解的，满足公理（RS），而λ是诱导等价，我们得到±和λ是相同的关系。这个结果是相当普遍的，适用于广泛的过程语义类。特别地，表1中的任何前序满足定理的条件。因此，对于这些语义前序中的任何一个，对应的互模拟直到表征了诱导等价。推论2.7（[6]）对于每个行为前序±，它是保持初始值的，作用分解的，并且满足公理（RS），我们有= ±=。虽然我们在[6]中的结果是很有希望的，但它们并没有为寻找过程语义的共归纳特征提供一个完整的答案。为什么？为什么？正如我们上面提到的，对于定义进程代数的语义，前序比等价更重要，因此获得它们的共归纳特征也很3模拟直至预订当我们第一次解决寻找过程等价的共归纳特征的问题时，我们有一个明确的起点：互模拟等价。双模拟是最强的等价，因此通过削弱它的定义（定义2.4），我们可以得到更弱的语义（定理2.6）。找出如何定义语义前序的共归纳刻画并不是一件容易的事。我们首先修改模拟的经典定义，得到以下模拟的定义，直到前序。定义3.1对于±a行为预序，我们说过程上的二元关系S是直到±的模拟，如果pSq意味着：• 对于rya，ifp−a→pJ，re存在qj和qJ，q±qJ−a→qJ和pJSqJ。a a a a a我们说过程p被过程 q模拟到±，或者 q模拟 p到±。20D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）13∼±∼±∼±∼±∼±∼≡∼±±，书面pиq，如果存在高达±，S的模拟，使得pSq.为了简单起见，我们经常只写<$而不写<$当行为从上下文来看，前序是清楚的。∼ ∼±例3.2让我们考虑过程s = a（b（d + e）+cd）和t = abf + a（be + bd + cd）。 很明显，对于模拟前序，我们有s/±St，因为在s中执行ab之后，我们到达了一个可能选择d + e的状态，但是在t中执行ab之后，它就不可能了。相比之下，对于迹预序，我们显然有s ±Tt，因为s的迹集{abd，abe，acd}包含在t的迹集{abf，abe，abd，acd}）中。让我们看看我们如何检查S不 t，通过构造相应的模拟达到± T。如果进程s执行动作 a并到达SJ=b（d+e）+cd，则进程 t不需要应用任何前序约简，它只需通过执行动作a，并演化为tJ= be + bd + cd。 现在我们必须检查sJи不 tJ：如果SJ执行动作C，则TJ可以简单地模拟到达相同状态移动。唯一需要检查的非平凡情况发生在SJ执行动作b并演化为d + e的时候。 在这种情况下，tJ应该利用迹减少的可能性，tJ±Tb（e + d）+cd，然后执行动作b也到达d + e，从而完成对模拟的验证。当然，如果我们事先知道s±T t，我们可以直接将 t简化为 s当检查s时，不 t，但我们想在这里说明的是我们如何使用在实践中，我们共代数特征：我们不想使用任何复杂的关于相应阶的信息，在这种情况下是±T，但只有一些更容易获得的关系对，就像我们在上面减少t J时所做的那样。下一个结果表明，到的模拟对于相应的基前序是正确的。命题3.3对于每个前序±，如果p ± q则p <$q。下一个定理陈述了关于满足公理（S）的任何前序的直到前序的模拟的定义的完备性，即，对于任何弱于模拟前序的前序，±S。定理3.4对于满足公理（S）的每个行为预序±当且仅当p± q。注意给定的预序必须满足公理（S），因为我们有±S=。∼∅∼ ±定理3.4以语义前序的相同方式刻画了语义等价性在定理2.6中得到了刻画，尽管在这两种情况下我们都使用了up-to关系的预序。最好有一个对偶刻画，其中等价被用来刻画语义前序。这确实是可能的，正如以下提议所述命题3.5对于满足公理（S）的每个行为预序±，我们有p±q<$p<$q。pD. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）1321∼±∼≡∼±∼±∼≡∼≡∼∼±∼±推论3.6对于满足公理（S）的每个行为预序±，我们有关系±，和，是相同的。考虑到互模拟和模拟，我们可以在下面的推论中画出等价图。推论3.7对于满足公理（S）的每个行为预序±，下列等价成立：pq优惠p±q优惠pqp±q惠pиqpиq惠p我qpиq考虑到ltbt谱中的语义，（仅）跟踪和模拟前序（参见表1）满足公理（S），从而满足Corol-1ary3.7的假设。因此，在这两种情况下，相互模拟上至和互模拟上至定义了相同的等价关系作为前序的核。因此，我们提供了两个可选的这些前序和四个可选的特征的诱导等价刻画。这些结果虽然很有趣，但没有达到我们在[6]中得到的一般性。 这种局限性来自于这样一个事实，即i的定义是基于 模拟语义，具有相当弱的区分能力。为了为了得到更一般的结果，类似于定理3.4中的那些，对于其他更强的语义，例如失败或准备，我们需要向我们开始的模拟添加更多的鉴别能力。准备好的模拟语义比[9]中的任何其他公理化语义都要强。 它将作为定义更强的模拟概念的基础。从现在开始，我们将考虑由pIq惠I（p）=I（q）定义的过程对上的二元关系I。定义3.8对于±行为预序，我们说过程上的二元关系S是直到±的I-模拟，如果S<$I（即pSq<$pIq），并且S是直到±的模拟。或者，等价地，以共归纳的方式，每当我们有pSq时，我们也有：• 对于每个a，如果pa存在qJ，qJ使得q±qjqJ和pJSqJ;• pIq.−→a a−→a a a我们说过程p是由过程q模拟到±的，或者过程 qI-模拟过程 p到±，写作p<$Iq，如果存在 I-模拟过程p到±±，S，使得pSq.为了简单起见，我们有时只写<$I而不写<$I当∼ ∼±行为前序从上下文中是清楚的。下面的命题将一个行为前序与相应I-模拟到。命题3.9对于每个前序±使得± <$I，如果p ± q那么p <$I q。⇔⇔⇔22D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）13∼±∼±∼±∼≡∼±∼≡现在我们可以使用I-模拟来证明一个类似于Theo-rem3.4中的结果，对于具有更大区分能力的语义前序。注意，在ltbt谱中，由从失败前序到就绪模拟前序的任何前序关系（见表1）相关的一对进程满足I条件。定理3.10对于满足公理（RS）的每个行为预序±，我们有p我q当且仅当p± q。注意给定的前序必须满足公理（RS），因为±RS=<$I<$<$I，∼∅∼ ±其中±RS是就绪模拟前序。我们还需要第二个但书因为我们一直都有我在Milner和San- giorgi [18，23]的作品中，互模拟的原始技术旨在减少证明两个过程是双相似的关系的大小在不深入细节的情况下，可以使用双相似关系的一小部分（已知）来生成其他不太明显的双相似对。我们的（bi）模拟可以完全以相同的方式使用：通过使用关系±我们可以通过<$I生成关系中的其他对。接下来我们将看到，我们也可以用模拟来刻画一个前序，直到它的核等价，这样，刻画的前序就从刻画的前序的定义中消失了我们首先给出一个关于预序与诱导等价关系的辅助结果。在我们看来，这个结果，即使相当简单，本身也很有趣引理3.11对于满足公理（RS）且保持首字母或弱于I的每个行为预序±，我们有p ±q <$q <$q + p。所有定义ltbt谱中语义的前序都比现成的模拟更粗糙，满足这个引理的假设，因为它们都是动作分解的。我们也考虑了其他的但书，以便得到一个更一般的结果。此外，有趣的是，前面结果的逆一般不成立。为了得到它，我们需要附加一个条件。命题3.12对于满足公理（RS）和±I的每个行为预序±，我们有p±q惠q <$q+p<$pIq。虽然我们在本节中不会使用前面的结果，但它显然是对第4节中的一个主要结果，即推论4.7的启发。通过使用引理3.11，我们现在可以很容易地证明下面的结果。命题3.13对于满足公理（RS）的每个行为预序±和±I，我们有p±q<$p<$I q。下面的推论总结了以前的结果。推论3.14对于满足公理（RS）的每个行为预序±，我们有关系和我是一样的推论3.15对于满足公理（RS）的每个行为预序±，D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）1323∼±∼±∼≡∼≡∼±±I，则下列等式成立：pq优惠p±q优惠pqp±qp±q惠pиIqpиIq惠pиIqpиIq推论3.14和3.15适用于一个广泛的过程前序类。考虑到ltbt谱，故障和就绪模拟之间的任何行为前序满足条件，因此我们可以将这些结果应用于它们。因此，推论3.15提供了故障和就绪模拟之间的任何前序，以及相应的等价性，这是一种根据类互模拟关系和类互模拟关系的表征事实上，从我们的模拟结果到现在，我们可以间接地证明定理2.6，这是我们在[6]中的主要结果。• 推论3.7对任何满足公理（S）的前序都成立，特别是对ltbt谱中的迹和模拟前序• 推论3.15可以应用于满足（RS）且使得p±q<$I（p）=I（q）的任何行为预序，特别地，这是在 ltbt频谱之间的故障前序和准备好的模拟前序，因为人们可以立即得出结论，看看表1中的定义公理。• 在线性时间分支时间谱中只有两种语义，完全迹和完全模拟，它们的前序既不满足推论3.7的条件，也不满足推论3.15的条件。然而，对于这些预序，相应的结果可以很容易地证明，通过由I（p）=负I（q）=负给出的关系CI来限制模拟，并定义CI-模拟直到±，从而导出序关系<$CI。事实上，在在这种情况下，对于满足（CS）公理ap±ap+q的任何行为前序，结果都是真的。定理2.6给预序加上了保持初始值和作用因式分解的条件，并且该结果对满足公理（RS）的任何行为预序都成立。 相比之下，当使用到的模拟时，我们不需要要求动作分解，而在推论3.15中，只有当我们施加±I时才假设初始值保持。因此，为了获得我们的结果，我们将ltbt谱中的语义前序分类为三个不同的切片。这些切片在表1中由虚线分开。每个切片分别对应于公理（S）、（CS）和（RS）中的任一个。4模拟达到等效我们在前几节中给出的所有结果都是基于满足某些性质的语义前序的存在在许多情况下，这些结果⇔⇔⇔24D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）13∼≡∼≡∼≡∼≡∼≡∼≡∼≡给出一个前序和它的导出等价关系。然而，正如我们将在本节中展示的那样，即使我们没有这样的前序，模拟技术也会产生一些有趣的结果。正如我们在第3节末尾所讨论的那样，模拟的结果将以切片的形式出现，这取决于我们在每种情况下考虑的基本模拟类别在本节中，我们只陈述和证明最困难的情况，即对应于由就绪模拟语义确定的切片。首先，我们以一种自然的方式将行为前序的定义扩展到等价关系。定义4.1过 程 上 的等价关系是一个行为等价，当它弱于互模拟等价时，即 p = B q<$p<$q，它是关于前缀和选择算子的同余，即。 如果p ≠ q，则ap ≠ aq且p + r<$q + r。我们将特别感兴趣的所有行为等价粗糙比现成的模拟等价。它们是满足以下公理的那些：（RS）I（x）=I（y）<$a（x+y）<$a（x+y）+ay在表2中，可以找到ltbt谱中语义等价的完整公理化。我们提出的第一个结果涉及I-模拟和等价性，以及选择对相关过程的应用。引理4.2对于每个满足（RS）和（RS）的行为等价，我们有那个PIq<$q<$q+ p。现在我们可以通过相应的模拟来陈述和证明给定等价关系的特征。定理4.3对于每个满足（RS）和（RS）的行为等价，我们havepq惠pиI 我问你。作为结果，我们也得到了一个表征的等价性方面的互模拟高达。推论4.4对于每个满足（RS<$）和（RS <$I）的行为等价，我们havepq惠pиIqpиIq惠pq.定理4.3中的特征描述告诉我们，任何行为等价都可以通过到的模拟来定义除此之外，这是更重要的，以这种方式定义了一个预序，其核是原始等价。此外，这个前序满足一些有趣的性质。命题4.5对于每个满足（RS）和（RS）I的行为等价，我们知道，<$I是满足（RS）的行为前序，<$I是满足（RS）的行为前序，Kernel是一个因此，给定一个等价，我们有一种方法来刻画一个核是该等价的特殊预序。D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）1325∼≡∼≡∼≡∼и∼≡定理4.6对于每个满足（RS）和（RS）的行为等价，预订我是唯一满足（RS）的行为前序，并包含在我的内核是这意味着我是通过完全填充所有以上条件。这个典型的预序可以用一个简单的方法来刻画，即对应的等价性和它们都满足的条件I推论4.7对于每个满足（RS<$）和<$I的行为等价<$i，定义为p ± q惠q <$q + p <$I（p）= I（q）的预序是由<$i生成的规范预序的另一个特征。很高兴地发现，在线性时间分支时间谱中不同语义的文献中出现的推论4.8对于失败等价和准备好的模拟等价之间的ltbt谱中的每个语义等价，对应的前序±是由给定的等价生成的规范前序。相当多的结果遵循从以前的命题，并宣布了丰富的基本代数理论。我们想指出以下几点：推论4.9对于满足性质（RS）的和I，我们有=<$I，和<$I II.∼≡∼≡为了结束本节，我们想对Corol- laries4.7和4.8中的结果进行评论。有几个前序的核是一个给定的行为等价。在它们之中，我们有上面定义的典范预序，等价本身，或者在格理论中所谓的典范预序，即p±Jq惠q<$q+p。可以看出，±J与对于满足定理4.6的假设的所有行为等价，我们的典型预序，这里我们将仅用±表示。例如，对于由准备好的模拟等价诱导的前序，我们对任何过程p都有0±Jp，但如果pi=0，则有0/±p。应用推论4.7，我们得到p±q惠p±Jq<$I（p）= I（q），因此± jq之间的唯一区别是：和±J在过程的初始作用集中，但这对于得到推论4.8中相应前序的特征是至关重要的。5关于公理化刻画作为一个例子的可能性，最多的技术observers，在本节中，我们证明了一些结果的公理化表征的行为前序。推论3.14指出一个行为前序（在某些条件下）可以由I-模拟直到该前序的核± =<$I来刻画。这一结果向我们暗示了从等价公理化中找到前序公理化的可能性。 更具体地说，如果A E是一组公理，它表征了一个给定的等价命题，我们可以很容易地定义一个公理化，26D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）13∼≡∼≡canonical preorder<$I.新的公理集可以通过将（RS）公理添加到等价公理中得到：AP=AE<${ax±ax+ay}。我们在下面的定理中将其形式化。定理5.1对于满足（RS）和I的每一个行为等价，我们有一个公理化A E，我们有A P=A E<${ax ± ax + ay}是关系I的一个公理化。BRsPW RT FT RFCSCT S不（x+y）+z=x+（y+z）+++++++++++x+y=y+x+++++++++++x+ 0 =x+++++++++++x+x=xI（x）=I（y）<$a（x+y）=a（x+y）+ay++++v+v+v+v+v+v+v+v+va（bx+by+z）=a（bx+z）+a（by+z）I（x）=I（y）ax+ay=a（x+y）+v+v+vvvvvvvvax+ay=ax+ay+a（x+y）+vvva（bx+u）+a（by+v）=a（bx+by+u）+a（by+v）++vvax+a（y+z）=ax+a（x+y）+a（y+z）+vva（x+by+z）=a（x+by+z）+a（by+z）+vvva（bx+u）+a（cy+v）=a（bx+cy+u+v）+va（x+y）=a（x+y）+ay+vax+ay=a（x+y）+表2线性时支时间谱等价性的公理化I [9]我们可以直接将定理5.1应用于满足正确条件的ltbt谱中的那些等价。在表2中给出了ltbt谱的等价性的公理化。从这些公理我们可以定义表1中前序的另一个公理化。推论5.2假设O ∈ {F，R，FT，RT，PW，RS}，只要将公理（RS）添加到以下公理中，我们就有了前序±O的有限我的天值得注意的是，在[9]中，为了证明表1中公理化的完备性，需要详细的证明，而在这里，我们基于相应等价公理化的完备性一次性地得到所有这些完备性结果。6结论和今后的工作本文引入了模拟的概念，并利用它得到了语义前序的余代数刻画。特别地，我们已经表征了与线性时间分支时间谱中的语义相关联的所有前序，以类似于使用互模拟的语义等价的相应表征的方式。此外，我们还得到了几个关于语义前序与等价关系的新结果，以及一些关于互模拟的新结果D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in Theoretical Computer Science 192（2007）1327相互模拟达到。事实上，对于语义的大家庭，包括那些在ltbt频谱粗糙比现成的模拟，互模拟的结果上升到作为一个推论相应的模拟高达（见推论3.7和3.15）。一个相当出乎意料的结果是，给定一个等价关系，我们可以得到一个典型的预序，其核正是等价关系，通过对它的模拟，很明显，我们可以得到与许多不同预序的核相同的等价，但是现在我们可以在它们之间区分一个典型的预序，它可以用一种系统的方式定义，并且具有一些有趣的性质，这些性质来自于它被定义的齐次方式。很高兴地发现，对于ltbt谱中的所有语义，这样获得的规范前序与我们已经从文献中知道的规范前序相同由于我们的表征，我们发现了新的属性，为我们提供了新的证明技术，以产生通用的证明有效的所有这些规范的前序。特别地，我们从相应等价的公理化中得到了典范前序的公理化。此外，我们计划继续我们的工作有关的互模拟和模拟，我们特别感兴趣的是将我们的结果翻译到纯共代数世界，比较他们的Hughes和Jacobs在[13]和Hasuo在[10]。在这个方向上的一些相关步骤已经出现在[7]中，在那里我们为分布式系统提出了几个类似于双模拟的语义，这些语义可以形式化为分类模拟，因此继承了它们所有的好的共代数属性。确认我们感谢米格尔·帕洛米诺对本文件前一稿引用[1] 我是说，我是说，我是说。 Re adytoopre orrder：gettyourBCCSPaxiomatizationfor free！ 在proc 第二届计算机科学代数和余代数会议-CALCO'07，卷出现在计算机科学讲义。Springer，2007年。[2] Bard Bloom，Sorin Istrail，and Albert R.迈耶互模拟是无法追踪的。Journal of the ACM，42（1）：232[3] E.布林克斯玛一种推导测试的理论。在方案规范、测试和验证VIII中，第63-74页。北荷兰，1988年。[4] 兰斯·克里夫兰和马修·轩尼诗作为互模拟等价的测试等价。Formal Aspects of Computing，3：1[5] Rance Cleaveland，Joachim Parrow，and Bernhard Ste Einstein.并发工作台：用于并发系统验证的基于语义的工具。ACM翻译计划。Lang.系统，15（1）：36-72，1993.[6] DavideFrutos-E s criganddCarlo s Gregorio-Rodrguez.对于线性非分支时间谱，采用了双相似性方法。CONCUR2005 - Concurrency Theory，第16届国际会议，计算机科学讲义第3653卷，第278施普林格，2005年。28D. de Frutos Escrig，C.G.Rodríguez/Electronic Notes in
我的内容管理
展开
