基于结构操作语义的同余方法与η-互模拟等价的研究

理论计算机科学电子笔记156（2006）97-113www.elsevier.com/locate/entcs除同余法在η-互模拟Wan Fokkink1阿姆斯特丹自由大学，计算机科学系，阿姆斯特丹CWI，软件工程系，阿姆斯特丹Rob van Glabbeek2National ICT Australia，Sydney北京大学计算机科学与工程学院新南威尔士州，悉尼Paulien de Wind3阿姆斯特丹自由大学计算机科学系摘要给出了η-互模拟等价和有根η-互模拟等价的同余格式。这些格式是使用过程代数中分解模态公式的方法导出的。为了确定一个过程代数项是否满足模态公式，可以检查它的子项是否满足通过分解原始公式得到的公式。分解使用了作为进程代数基础的结构化操作语义。保留字：结构操作语义学，模态逻辑，分解，同余，η互模拟1介绍结构操作语义[16]为进程代数和规范语言提供了解释。它会产生一个标记转换1 电子邮件地址：wanf@cs.vu.nl2电子邮件：rvg@cs.stanford.edu3 电子邮件地址：pdwind@cs.vu.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.02998W. Fokkink等人理论计算机科学电子笔记156（2006）97系统，其中状态是（单排序，一阶）签名上的封闭项，状态之间的状态之间的转换是从转换系统规范中获得的，该规范由一组称为转换规则的证明规则组成标记的转换系统可以通过广泛的语义等价来彼此区分，例如基于执行序列的分支结构或装饰版本。VAN GLABBEEK[8]对考虑内部作用量τ的过程进行了等价分类。在这里，我们专注于一个这样的等价，称为η-互模拟[1]。一 般 来 说 ， 由转 移 系 统 指 定 所 诱 导 的 语义 等 价 不 是 同 余 ， 即 项f（p1，.. .. ，pn.作为一个全等是一个重要的属性，例如，为了适应将等价性转化为公理化框架。转换规则的句法格式已经相对于几个语义等价物被开发，以确保这样的等价物是一致的。 这些格式有助于避免重复的全等证明。为了互模拟，引入了几种同余格式，例如De Simone格式[17]，GSOS格式[4]，tyft/tyxt格式[13]和ntyft/ntyxt格式[12]。 B织机[2]介绍弱和分支互模拟和有根弱和分支互模拟的同余格式。这些格式包括函数符号f的参数i的所谓耐心规则，这意味着项f（p1，.，pn）继承了它的辐角pi的τ -跃迁. 此外，包含正在运行的进程的函数符号的参数被标记，并且使用该标记以限制转换规则中变量的出现最近，范·G·拉贝克[11]大大简化了[2]的格式，并为延迟和η-互模拟以及根延迟和η-互模拟提供了类似的格式。V和 GLABBEEK[9，8]根据实验者在一个过程中所能观察到的结果给出了等价性的特征。模态逻辑捕捉到了这样的观察。一个等价的模态刻画由一类C模态公式组成，使得两个过程等价当且仅当它们使C中的相同公式为真。例如，Hennessy-Milner逻辑[14]是互模拟的模态表征LARSEN和LIU[15]介绍了一种方法，用于从具体过程的Hennessy-Milner逻辑中分解公式，关于来自具有De Simone格式的结构操作语义的过程代数的为了确定一个过程代数项是否满足模态公式，可以检查它的子项是否满足某 些 其 他 公 式 ， 这 些 公 式 是 通 过 分 解 原 始 公 式 得 到 的 。 B LOOM ，FOKKINK&VANG LABBEEK[3]将该方法扩展到不带前瞻的ntyft/ntyxt格式，W. Fokkink等人理论计算机科学电子笔记156（2006）9799VANGLABBEEKDE WIND转换为tyft/tyxt格式的完整版[7]。 在[3]中，应用分解方法从[9]中获得了行为等价的同余格式其思想是，给定一个等价和它的模态特征C，这个等价的同余格式必须确保在C中分解一个公式总是在C中产生公式。在一篇未发表的论文中，我们将[3]的工作推广到具有τ-跃迁的过程给出了一种从模态逻辑中分解具有τ-变迁过程的公式的方法，并利用这种分解方法得到了分支互模拟和根分支互模拟的同余格式本文利用这种分解方法得到了η-互模拟和有根η-互模拟的同余格式因此，我们开车回家的一点是，在从过去的一致格式的特设建设相反，我们现在可以系统地从语义等价的模态特征推导表达一致格式。我们的格式在函数符号的参数上使用了两个谓词，以标记两个正在运行的进程以及可能已经开始运行的进程2预赛2.1标号迁移系统标号迁移系统（LTS）是一个具有一组过程的对（，→）和→ <$×（A<${τ}）×，其中τ是内部作用量，A是不含τ的作用量集。 我们用α，β，γ表示A的元素<${τ}，用a，b表示A的元素。我们记p−α→q，对于（p，α，q）∈→和p−α→，对于q∈：p−α→q，annd=对于 f−→τ的transitive-rexexiveclosuree， .定义2.1 [1]对称关系B×是η-互模拟，如果pBq和p−α→pJ意味着存在rα=τ和pJBq，或rq=qJ−α→qJJ=QJJJ对于一些QJ，QJJ，QJJJ具有PBQJ和PJBQJJJ。过程p，q是η-互相似的，记为pParticipateηq，如果存在一个具有pBq的η-互模拟B.η-互模拟对于文献中的大多数进程代数不是同余，这意味着f（p1，.，pn）并不总是由其自变量p1，. ，pn.生根条件弥补了这种缺陷。定义2.2 [1]一个对称关系R×是一个有根η-互模拟如果pRq和p−α→pJ隐含sthatq−α→qJ=πqJJ对于某个qJ，qJJ有pJ参与qJJ。过程p，q是根η-双相似的，记为pParticipirηq，如果存在一个根η-互模拟R与pRq。100W. Fokkink等人理论计算机科学电子笔记156（2006）972.2模态逻辑模态逻辑的目的是在LTS中制定过程的属性。在[8]之后，我们用模态连接词Hennessy-Milner扩展了Hennessy-Milner逻辑[14]。定义2.3阶级 模态公式的定义如下，其中，所有索引集的范围：：=i∈I|¬ϕ| ⟨α⟩ϕ|⟨ϵ⟩ϕp|=表示thatpsatis fies。 根据定义，p|=ifp−α→pJwithPJ|=，andp|=如果p=pJ有hpJ|=0。 我们使用缩写sT表示空合取，1∧ϕ2 对于i∈{1，2} i，我们如果p，则写|=优惠p|对于任何LTS中的任何进程p，定义2.4的子类η和rη定义如下：η：=i∈Ii|¬ϕ| ⟨ϵ⟩ϕ|⟨ϵ⟩(ϕ⟨a⟩⟨ϵ⟩ϕ)(a∈ A)rη：：=i∈Ii|¬ϕ|⟨α⟩⟨ϵ⟩ϕˆ|ϕˆ（α∈A<${τ}）类和分别是η，rη，在下的闭包。η rηrη的定义中的最后一个子句保证了我们在命题3.7的证明中所需要的η∈rη。同样，如果没有这一条款，≡⊆ 使用结构归纳法和结构归纳法。η rη对于L，如果p和q满足L中的相同公式，则我们写作p<$Lq。请注意，简单地说， q惠pq和prη q惠pq.η rη定理2.5p参与q惠pη qandp参与者ηq惠prη q，对所有p，q∈.这个定理的证明在附录中给出2.3结构操作语义学设V是一个无穷多个变量的集合，具有典型的元素x，y，z。如果一个语法对象不包含任何变量，那么它就是封闭的一个签名是一个函数符号f的集合，其元数为ar（f）。我们始终以|Σ|、|一|≤|V|. 集合（2）项在V和V上的定义与通常一样。t，u表示项，p，q表示闭项。var（t）是在t中出现的变量的集合。置换是从V到（V）的部分函数。闭代换σ是从V到闭项的全函数。定义2.6A（positive或negative）iteral是t−α→tJ上的一个exprssi，或t−α→。一个（转换）规则是由一组称为tαJ−→t我的朋友。 t−α→tJ是余弦函数，t是规则的根。规则W. Fokkink等人理论计算机科学电子笔记156（2006）97101μνκ∅isalsowrittent−α→tJ. 设置了一个转换系统性能（TSS）tαJ−→t过渡规则。定义2.7设P=（R，R）是一个TSS。规则H的一个来自P的无冗余证明是一个良基树，其节点由文字标记，tαJ−→t在标记为“h y p o th e s is s“的Leaves中，假设的标签集合，并且如果μ是不假设，K是该节点的子节点的标签集合，则μ是阳性和K是R中规则的替换实例。H的证明称为非冗余，因为H必须等于（而不是tαJ−→t包括）假设的标签集合这种不冗余将是至关重要的为保存我们的一致性格式节。3.1（见图）3.4）。TSS是指指定一个LTS，其中的转换是封闭的正文字。只有正前提的TSS以直接的方式指定LTS，但是将LTS与具有正前提的TSS相关联并不那么容易。负前提。 从[10]中，我们采用了封闭文字的支持良好的证明的概念。 L迭代t−α→tJ和t−α→是用来否定e的。定义2.8设P=（R，R）是一个TSS。一个来自P的关于闭文字μ的有充分支持的证明是一个良基树，其中节点被闭文字标记，使得根被μ标记，并且如果ν是节点的标签，K是该节点的子节点的标签的集合，则：(i) v是正数，K是R中规则的闭替换实例;(ii) 或者ν是负的，并且对于每个闭负文字的集合N，其中N可从P无冗余地证明，并且κ是否定ν的闭正文字，K中的文字否定N中的文字。Pwsμ表示存在一个来自P的μ的有充分支持的证明。P是完全的，如果对eachp和α，eiterPwsp−α→或Pwsp−α→pJ对somepJ。一个完备的TSS指定了一个LTS，由ws-可证明的闭正文字组成2.4关于过渡规则的在本节中，我们介绍了规则的语法限制术语，起源于[3，12，13]。定义2.9ntytt规则是这样一个规则，在这个规则中，正前提的右边是变量，它们都是不同的，并且不在源中出现如果ntytt规则的源是变量，则它是ntyxt规则，如果它的源是变量，则它是ntyft规则。102W. Fokkink等人理论计算机科学电子笔记156（2006）97我−→τ只包含一个函数符号，不包含多次出现的变量，如果其前提的左侧是变量，则包含nxytt规则。定义2.10规则中的变量是自由的，如果它既不出现在源中，也不出现在前提的右侧。如果某个变量出现在前提的右侧和左侧，则规则具有前瞻性。如果一个规则没有前瞻性，并且不包含自由变量，那么它是合适的最初引入ntyft/ntyxt和就绪模拟格式[12，3]是为了保证互模拟和就绪模拟的一致性。定义2.11如果TSS由ntyft和ntyxt规则组成，则TSS为ntyft/ntyxt格式;如果TSS的规则没有前瞻，则TSS为就绪模拟格式谓词标记包含正在运行的进程的函数符号的参数（参见。[3]）。通常情况下，在进程代数中，对于合并函数的参数，则不成立，但对于可选复合函数+的参数，则不定义2.12设f是{（f，i）}上的一元谓词|1 ≤i≤ar（f），f∈φ}. 如果f（f，i），则f的参数i是liquid;否则它是冻结的。如果t = x，或t = f（t1，... ，tar（f）），并且对于f的liquid变元i，出现在t i中的非流动位置处。函数符号f的参数i的耐心规则表示项f（p1，.，pn）继承了自变量pi的τ-跃迁（参见[2，5]）。我们将需要耐心的存在规则的流动参数。定义2.13ntyft规则是（f，i）的耐心规则，其中1≤i≤ar（f），如果它的形式f（x，...，x，.得双曲余切值.x−τ→y）−τ→f（x， . .得 双曲余切值. ，y，x... （x）1名iar（f）1i−1一期+1ar（f）如果f（f，i）满足，则这是一个双耐心规则一个ntytt规则对于n是耐心的，如果它是从tτ忍耐规则。这些规则具有以下形式：−→y其中C[]是一种液体，C[t]τC[y]上下文，意味着上下文符号[]出现在液体位置。定义2.14如果TSS包含所有的双耐心规则，则它是双耐心的是抽象自由的如果只有无耐心规则有t−→u形式的结论。2.5模态公式为了分解模态公式，我们使用[3]的结果，其中对于任何TSSP在现成模拟格式中，一组合适的nxytt规则，称为P-ruloids，W. Fokkink等人理论计算机科学电子笔记156（2006）97103tα构造了我们在一个相当肤浅的层面上解释这个构造;精确的变换可以在[3]中找到。首先，P被转换为体面的ntyft格式的TSS。在[ 13 ]的这种转换中，规则中的自由变量被封闭项取代，如果源是x的形式，则这个变量被f（x1，. ，xn），其中f∈ N. 然后，使用[6]中的构造，posi的左侧，主动前提被简化为变量。大致的想法是，给定一个前提f（t， . . ， t）−α→yinaruler，anddaruleH，以将r转换为re-1nf（x，.，x）α t1n−→把前面提到的前提用H，y用t，xi用ti;这是重复（transfinitely），直到所有具有不变左边的都消失。 在最后的转换步骤中，引入了在t−α→上具有负约束的规则。我们的动机是在定义2.8中，我们需要一个更有建设性的概念，比如定义2.82.7，通过使否定前提与结论是肯定的。 一个关于f（x， . . ， x）−α→，1N通过从具有结论f（x， . . ， x）−α→t，1N并且包括拒绝每个所选择的前提作为R的前提。对于最后一种转换，规则不具有前瞻性是至关重要所产生的TSS由P+确定，其在图中未示出。 In[3]证明了P+μ惠P对所有闭文字μ都是μ。无冗余可证明性的概念以一种简单的方式进行了调整，接受带有否定结论的规则P-规则集是从P+中可得到的不冗余的适当的nxitt规则.文[3]中TSS与其规则集之间的下列对应关系在本文所用的分解方法中起着决定性的作用。 它说有一个很好的支持，从P到p−→aq的跃迁，其中p是一个闭合的子空间，一个项t，当且仅当有一个证明这个转换，使用在根P-ruloid与源t。命题2.15设P是一个可用模拟格式的TSS。 然后是P.P.σ（t）−α→p当且仅当r是P-类鲁维H−→u 和一个σJ，σJ（μ）对μ∈H，σJ（t）= σ（t），σJ（u）= p.我们现在展示如何从。对于每一项t和公式，我们赋予一个分解映射：V→的集合t−1（）。每个映射<$∈t−1（<$）保证σ（t）|如果σ（x），则= σ|（x）= x∈var（t）。反之亦然，当σ（t）|=，有分解映射<$∈t−1（<$）与σ（x）|（x）= x∈var（t）。这在Thm中是正式的。两点十七分为了最小化模态分解和内部作用量τ相结合所固有的复杂性，我们应用分解方法104W. Fokkink等人理论计算机科学电子笔记156（2006）97tαβ抽象的自由TSS，并扩展我们的派生同余结果的一般情况下，使用众所周知的组合的抽象操作。定义2.16设P是一个无病人的、无抽象的TSS，采用现成的模拟格式。我们定义·−1：（）×→P（V→）如下。设t表示单变量项，即而不需要多次出现相同的变量。(i)01-0i∈I（i）i∈V（x）=i（x）其中，对于i∈I，<$i∈t−1（<$i）。i∈I(ii) <$∈t−1（<$α<$$>）i <$$>存在一个P-规则型H和一个χ∈u−1（<$），其中−→u⎧⎪⎨χ(x)∧β<$<$γ<$Tifx∈var（t）（x）=γx y∈Hx H⎪−→−→∈如果x/∈var（t）(iii) 有一个函数h：t−1（<$）→var（t），其中n（x）=<$x（x），x∈Vx∈ h−1（ x）(iv) <$∈t−1（<$$><$$>）i <$<$有一个χ∈t−1（<$），⎧如果x出现在t中，则为液体，t为液体，x（x）否则(v) <$∈ρ（t）−1（<$）对于ρ：var（t）→V不是单射i <$$>有一个χ∈t−1（<$）与（x）=y∈ ρ−1（ x）x（y）forx∈V不难看出，如果n∈t−1（n），则n（x）<$T对于x/∈var（t）。为了解释Def.2.16，我们扩展它的两个案例。考虑t−1（），设σ是任何闭代换。问题是在什么条件下，当x∈var（t）时，σ（t）−α→q有一个hq的转移|=0。一个抄送给我。2.15，这里t是一个转移当且仅当存在一个闭置换σJ，其中σJ（t）=σ（t），且有一个P-拟序W. Fokkink等人理论计算机科学电子笔记156（2006）97105tαH使得（1）满足σJ（H）中的前提，且（2）σJ（u）|= 0。的−→u第一个条件被覆盖，如果对于x∈var（t），（x）包含合取βT，β γx−→y∈H和对x−→ ∈H的合取<$$> γ<$T。 通过添加一个连接词106W. Fokkink等人理论计算机科学电子笔记156（2006）97ηrηχ（x），并将每个合取<$β<$T替换为<$β <$χ（y），对于某些χ∈u−1（<$），第二个条件也被覆盖。考虑t−1（<$），设σ是任何闭代换。我们有σ（t）|当且仅当不存在χ∈t−1（χ）使得σ（x）|= χ（x）对于所有x∈var（t）。换句话说，对于每个x∈t−1（t），对于某个x∈var（t），x（x）必须包含一个合取<$x（x）。下面的定理，其证明在这里省略，将是即将到来的同余结果的关键定理2.17给定一个完整的、无病人的、无抽象的、现成的模拟格式的TSS。对于任意项t，闭代换σ和ε∈：σ（t）|= ⇔ <$x∈var（t）：σ（x）|= x（x）作为同余的3η我们继续应用前一节的分解方法来推导η-和有根η-互模拟等价的同余格式这个想法是，η-互模拟格式必须保证来自η总是从η（见第3.6条）。同样地，根η互模拟格式必须保证来自rη的公式总是分解成公式，（见第3.7条）。 这意味期望的全等结果（参见Thm. 3.9和Thm.3.11）。在推导同余格式时，我们将使用抽象算子的组合性来规避对无抽象TSS的限制3.1同余格式我们假设函数符号的参数上有第二个谓词Λ，表示它们包含的进程可能已经开始运行，但可能正在休息，在这种情况下，这些参数不需要耐心规则一直都是。通常，在进程代数中，对于顺序复合的第一个参数，Λ成立，而对于第二个参数，只有Λ成立，而对于交替复合的参数，Λ不成立。W. Fokkink等人理论计算机科学电子笔记156（2006）97107tα定义3.1设 安提特规则H−→u 根η-互模拟安全关于λ和Λ，如果：(i) 它没有前瞻性，(ii) 前提的右侧仅出现在u中的非流动位置，并且(iii) 如果x在t中恰好出现一次4，在Λ-液体位置，则：(a) 规则中x的所有出现都在Λ-液体位置，(b) x在负前提的左手边没有非线性流体出现(c) x在一个正前提的左手边至多有一个正流出现，并且这个前提有来自A的标号，并且(d) 如果x出现在t中的冻结位置，则x不出现在持仓─位于处所左手边的流动头寸。当Λ是泛谓词时，我们称该规则是η-互模拟安全的关于。定义3.2一个准备好的模拟格式的TSS是根η-互模拟格式，如果对于某个εΛ，它由ε-耐心规则和根η-互模拟安全的规则组成。一个准备好的模拟格式的TSS是η-互模拟格式的，如果对于某个随机数，它由η-耐心规则和相对于随机数是η-互模拟安全的规则组成。[3]的运算符初始优先级（参数冻结）和二元Kleene星（两个参数都冻结）符合根η-互模拟格式。在这些应用中，以及为了捕获CCS和类似语言的运算符，它需要取Λ = λ。在下面的例子中，这是不可能的。例3.3设f是一个二元运算符，它将动作α∈A <${τ}与其参数交错，直到它的第一个参数产生动作崩溃。然后f执行警报和防止熔毁的动作，中间没有任何τ步骤，随后继续作为其第二个参数。x−α→xJf（x，y）−α→f（xJ，y）y−α→yJf（x，y）−α→f（x，yJ）xc−ra→shxJf（x，y）−ale→rtpm. y防止下午. y−m−e−lt−d−ow→nypm是一个CCS动作预处理操作符。要使这个TSS成为（有根的）η-互模拟格式，必须将pm的变元标记为"冻结“（因此不伴随耐心规则），而标记为”流动“，因为它包含一个已经开始但当前未运行的过程。[4]只有对t是单变量的规则的要求才重要。 定义3.1中一般术语t的现行表述为提议3.4铺平了道路。108W. Fokkink等人理论计算机科学电子笔记156（2006）97ηηηηηη在模态分解的定义中，我们没有使用原始TSSP中的规则，而是使用P-ruloids。因此，我们必须证明，如果P是（有根的）η-互模拟格式，那么P-规则胚也是。命题3.4如果一个TSS P相对于某个π是（有根的）η-互模拟格式，那么每个P-规则体相对于π是患者安全的或（有根的）η-互模拟安全的。这里省略了Prop.3.4的证明证明的关键部分是证明在无冗余可证性下保持体面（有根）η-互模拟格式。(The形容词irredundant在这里是必不可少的。）3.2模态特征从现在开始，我们将提到患者和（根）分支安全规则，而不涉及伴随的谓词和Λ。引理3.5给定一个可用模拟格式的TSS。 对于任意项t，而 变 量 x 只出 现 在 t 中 ， 则 为 液体，<$∈ t−1 （ <$$><$$> ） <$$> （ x ）<$$><$<$（x）。证据设t ∈ t−1（<$$><$$>）且x在t中只出现<$-liquid。然后是Def.2.16.iv和2.16.v，n（x）的形式为i∈I <$$><$<$i。 所以是（x）（x）。Q命题3.6设P是根η-互模拟格式的无抽象TSS。对于任何项t和变量x，仅在t中出现Λ-液体：ϕ∈η⇒ ∀ψ∈t−1(ϕ) : ψ (x) ∈≡证据我们将结构归纳法应用于结构分析。 设ε∈η。 设t∈（n）且n∈t−1（n），且x在t中只出现Λ-液体。首先，我们处理t是单变量的情况 如果x/∈ var（t），则<$（x）<$T ∈ <$。假设x在t中出现一次。• =i∈I<$i，其中对于i∈I，<$i ∈η。 根据定义2.16.i，（x）=i∈I<$i（x），其中i∈t−1（ 通过归纳， 对于i∈I，则<$（x）∈- 是的η η• =<$<$J，其中<$J∈η。 由定义2.16.iii，有一个函数h：t−1（J）→var（t），使得χ∈h−1（x），所以<$（x）∈<$。χ∈h−1 （十）<$x（x）. 通过归纳法，χ（x）∈为•=η。 由定义式2.16.iv，要么<$（x）=<$$><$$> x（x），要么<$（x）=对于某个χ∈t−1（J），有Χ（X）。 通过对公式大小的归纳，得到χ（x）∈χ。 所以n（x）∈n。• =η。 根据定义2.16.iv，或者是：W. Fokkink等人理论计算机科学电子笔记156（2006）97109η对于某个x ∈ t − 1（2），x（x）或（x）= x（x）。由Def. 2.16.i，χ（x）= χ1（x）2）。通过对公式大小的归纳，得到χ1（x）∈θ.根据定义2.16.ii，110W. Fokkink等人理论计算机科学电子笔记156（2006）97不不是ηrηrηχ2（x）=（x）βx−→ y∈Hβγx−→∈H¬⟨γ ⟩T对于某个ε∈u−1（ε）和某个P-ruloidH. 由于，而prop。3.4，一−→uH一−→u 是根η-互模拟安全的因为x在t中的出现是Λ-液体，x在u中只出现Λ-液体。此外，右侧的变量在H中的前提只在u中出现Λ-liquid（因此是Λ-liquid）。 所以在前-在上述情况下，我们证明了， 对于β，. 我们η区分两种情况。ηx−→y∈H例1：x在t中的出现是双液性的。 则n（x）= nnnx（x）。 以来H是根η-互模拟安全的，并且是一个nxytt规则，x不出现在−→u在H中的负前提的左手边，最多一次在左边-在H中保留一个位置的边，其中fx−→by具有hb∈A。这样一个前提的右边，y，只在u中出现，所以Lem。3.5，（y）（y）.因此，要么χ2（x）=（x）要么χ2（x）=（x）b（y）≡ （x）以来 ψ（x） = ⟨ϵ⟩(χ1(x)∧χ2(x)),either（x）=η η例2：x在t中的出现被冻结。 则n（x）= x（x）。 以来H一−→u 是根η-互模拟安全的，并且是nxytt规则，x不发生在H的房屋的左手边。所以χ2（x）=（x），因此（x）=χ1（x）<$χ2（x）= χ1（x）<$$>（x）∈<$。最后，这不是一个统一的姿势。对于somuuivaterm，nt=ρ（u）u和ρ：var（u）→V不是内射的。 根据定义2.16.v，对于某些χ∈u−1（n）。由于u是单变量的，并且对于每个y∈ρ−1（x），在u中是Λ-液体，对于y∈ρ−1（x），χ（y）∈π 因此，<$（x）∈<$。Qη η命题3.7设P是根η-互模拟格式的无抽象TSS。对于任意项t和变量x：ϕ∈rη⇒ ∀ψ∈t−1(ϕ) : ψ (x) ∈≡证据我们将结构归纳法应用于结构分析。 设r∈rη，t∈ （）和∈t−1（）。我们把注意力限制在t是单变量的情况上;一般情况就像在3.6节的证明的结尾一样。如果x/∈var（t），则<$（x）<$T ∈<$。假设x在t中只出现一次。• 案例=i∈Ii和<$i=<$<$J的证明过程与Prop.3.6的证明过程相同。• <$=<$α<$$><$$><$J，其中<$J∈η。 由Def. 2.16.二，（x）=χ（x）βx−→ y∈Hβγx−→∈H¬⟨γ⟩T不不2W. Fokkink等人理论计算机科学电子笔记156（2006）97111tαtαrηrηrηηηηη对于某些χ∈u−1（J）和某些P-ruloid H.通过归纳法，χ（x）∈rη。−→u（可以应用归纳法，因为J∈ηrη和J是严格的子公式） 根据提案3.4，H−→u 是根η-互模拟安全的或者说病人。因此，H中前提右侧的变量出现β在U中只有水-液体。通过Prop。3.6，对于x−→y∈H，χ（y）∈η.此外，委员会认为，根据引理3.5，χ（y）≠χ（y）。 因此，<$β <$χ（y）<$$>β <$$><$$>χ（y）∈< $。 也<$$>γ T <$$><$γT∈。 因此，n（x）∈rη。• ϕ∈η。 如果x在t中的出现是Λ-liquid，则<$（x）∈≡如下从prop。三点六 所以我们可以假设这个事件是Λ-冻结的。的情况<$i=i∈I <$i和<$i=<$<$J如前所述进行。我们专注于另外两个案子。∗ϕ= ⟨ϵ⟩ϕJwithϕJ∈η⊆rη.由 于 x 在 t 中 的 出 现 是 Λ- 冻 结 的 ， 通 过 Def 。2.16.iv，对于某个χ∈t−1（<$j），<$（x）=χ（X）通过对公式大小的归纳，得到χ（x）∈rη。所以<$r（x）∈rη。∗ϕ= ⟨ϵ⟩(ϕ1⟨a⟩⟨ϵ ⟩ϕ2) withϕ1, ϕ2∈η⊆rη. 由于x在t中的出现是Λ-冻结的，根据定义2.16.iv，对于某些χ∈t−1（<$1 <$a <$$><$<$2），<$0（x）=χ（x根据定义式2.16.i，χ（x）=χ1（x）<$χ2（x），其中χ1∈t−1（<$1），χ2∈t−1（<$a<$$><$<$2）。通过对公式大小的归纳，得到χ1（x），χ2（x）∈rη.因此，n（x）∈rη。Q3.3同余结果最后，我们能够证明承诺的一致性结果。引理3.8给出一个完全无抽象的TSS，η-互模拟格式。若σ（x）ParticipinσJ（x），其中x∈var（t），则σ（t）Participin σJ（t）。证据 通过Thm。 2.5，σ（x）ParticipinσJ（x）implies σ（x） σJ（x），其中x∈var（t）。令σ（t）|= ∈η。 通过Thm。2.17存在一个具有σ（x）的ε∈t−1（ε）|= x（x）对于x∈var（t）.由于Λ是泛在的，根据Prop. 3.6，对于x∈var（t），<$（x）∈ <$。由于σ（x）σJ（x），σJ（x）|（x）= x ∈ var（t）。通过Thm。 2.17，σJ（t）|= 0。同样，σJ（t）|= ∈η 隐含σ（t）|= 0。 所以σ（t）<$σJ（t）。因此，我们认为，σ（t）参与σJ（t）。Q定理3.9给定η-互模拟形式的完备TSSP =（R，R）.若σ（x）ParticipinσJ（x），其中x∈var（t），则σ（t）Participin σJ（t）。112W. Fokkink等人理论计算机科学电子笔记156（2006）97证据 设PJ是由P得到的，通过改变所有的规则，期望Pj-耐心规则是ft−τ→uin到t−→iu的一个约束条件，对于自由交换i/∈A{τ}。通过构造，PJ是无抽象的并且是η互模拟格式。所以根据引理3.8，Participin是PJ的所有算子的同余。设PJJ是由PJ加上一个新的算子τi得到的，W. Fokkink等人理论计算机科学电子笔记156（2006）97113x−α→yα（αi）x−→iyττi（x）−→τi（y）τi（x）−→τi（y）这个算子将所有的i-标签转化为τ-标签。这是众所周知的[1]和平凡的检查参与是一个同余τi以及。如果平凡地得出，对于任何算子f ∈ f，τi<$f在P JJ中的行为与f在P中的行为相同。 所以当Participiη是τi<$f在P中的同余时，它一定是f在P中的同余。 Q引理3.10给定一个完全无抽象的TSS，采用有根η-互模拟格式。若σ（x）参与ησJ（x），其中x∈var（t），则σ（t）参与η σJ（t）。定理3.11给定一个完全TSS的根η-互模拟格式。如果对于x ∈ var（t），σ（x）参与ησJ（x），则σ（t）参与η σJ（t）.引理3.10的证明与引理3.8的证明相似，只是用了3.7而不是3.6。同样，Thm的证明。3.11与Thm相似。三点九4相关工作我们所知道的η-和有根η-互模拟的唯一其他格式出现在[11]中。这些格式包含在GSOS格式中[4]。[ 11 ]的格式区分了所谓的“主”运算符和“缩写”。后者可以被看作是句法糖，没有添加任何不能用主算子表达的东西。我们的故事，是一部经典的经典。然而，我们的格式通过要求所有算子都是主算子来推广[11]的简化格式的结果对于η-互模拟格式，我们的推广在于允许GSOS格式之外的转换规则;[11]的简化格式正是我们的η-互模拟格式和GSOS格式的交集然而，我们的根η-互模拟格式和GSOS格式的交集仍然是[ 11 ]的根η -互模拟的简化格式的适当推广。后者可以被描述为我们的根η-互模拟格式和GSOS格式的交集，在GSOS格式中，出现在转移规则结论右侧的所有算子的所有参数都必须是Λ-liquid。[11]的格式对于有根η-互模拟，在[2]之后，区分在我们的方法中，野生算子只有Λ-冻结参数，驯服算子只有Λ-流动参数。允许运算符同时具有两种参数的想法源于[5]。114W. Fokkink等人理论计算机科学电子笔记156（2006）97引用[1] JCM B AETEN&R.J.VANG LABBEEK（1987）：进程代数中抽象的另一种观点。在Proc.ICALP84比94[2] B. B LOOM（1995）：弱互模拟的结构操作语义。 理论计算机科学146（1/2），pp. 25比68[3] B. B LOOM，W.J.F OKKINK&R.J.VANG LABBEEK（2004）：Precongruence formatsfordecorated trace semantics. ACM Transactions on Computational Logic 5（1），pp.26比78[4] B. BLOOM、S.我是A.R. MEYER（1995）：互模拟不能被追踪。ACM杂志42（1），pp.232-268。[5] W.J. Fokkink（2000）：有根分支互模拟作为一个同余。 Journal of Computer and SystemSciences 60（1），pp. 13-37[6] W. J. F OKKINK&R. J.VANG LABBEEK（1996）：Ntyft/ntyxt规则简化为ntree规则。信息和计算126（1），pp.1-10.[7] W.J.去你妈的，R.J.VANG·拉贝克&P.DEW IND（2005 ）： 结构操作语 义学的Hennessy-Milner 逻辑的组合 性。可查阅http://theory.stanford.edu/。 出现在理论计算机科学。扩展摘要见：Proc. FCT412-422.[8] R.J. VANG LABBEEK（1993）：线性时间分支时间谱II：顺序系统的无声移动。 在proc CONCUR'9 3 ，LN CS 715 ，Springer ，pp . 66比81[9] R.J.VANG LABBEEK（2001 ）：线性时间分支时间谱I：具体的顺序过程的语义.在J.A.Bergstra ， A.Ponse S.A.Smolka ， editors ： Handbook of Process Algebra ， chapter 1 ，Elsevier，pp.3-99[10] R.J.VANG LABBEEK （ 2004 ） ： The meaning of negative premises in transition systemspecifications II. Journal of Logic and Algebraic Programming 60/61，pp. 229-258[11] R.J. VANG LABBEEK（2005）：On cool congruence formats for weak bisimulations. 可查阅http://theory.stanford.edu/。在Proc. ICTAC331-346[12] J.F. Groote（1993）：带负前提的变迁系统规范。 理论计算机科学118（2），pp. 263-299。[13] J.F.G鲁特&F.V AANDRAGER（1992）： 结构化操作语义和互模拟是一种一致性。 信息与计算100页202-260[14] M. 亨尼西河 Milner（1985）：非决定论和并发性的代数定律。ACM杂志32（1），pp. 137-161。[15] K.G. 拉森&X. LIU（1991）：通过操作语义学的组合性contexts. Journal of Logic and Computation1（6），pp. 761-795.[16] G.D. Plotkin（2004）：A structural approach to operational semantics. Journal ofLogic and Algebraic Programming 60/61，pp. 17-139.最初出现于1981年。[17] R. 03 The Dog（1985） 更高级别的同步装置，计算机科学37（3），pp. 245-267我的-SCCS。理论一η-互模拟的模态特征我们来看看第一部分。2.5，它指出η是η-互模拟等价的模态特征。我们需要证明，给定一个LTS（，→），pParticipateηq惠p<$ηq对所有p，q∈。证据 （1）设p参与q，且p|对于某个<$∈η， 我们证明q| = 0，通过结构归纳，相反的含义遵循对称性。W. Fokkink等人理论计算机科学电子笔记156（2006）971151ηηηη• =i∈Ii。 则p |= i，对于i ∈ I。 通过归纳q |i ∈ I，所以Q|=i∈ I<$i.• =<$ 则p =0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000