理论计算机科学电子笔记156（2006）3-25www.elsevier.com/locate/entcsSOS规则的层次结构1穆罕默德·礼萨·穆萨维2米歇尔·A.Reniers3埃因霍温理工大学计算机科学系（TU/e），P.O. Box 513，NL-5600 MB埃因霍温，荷兰摘要1981年，结构操作语义学（SOS）被引入，作为一种系统的方法，通过一组特定形状的规则来定义编程语言的操作语义[62]。随后，SOS规则的格式成为研究对象。使用所谓的转换系统规范（TSS这导致了一系列的研究，提出了几种语法规则格式和相关的元定理。由这种规则格式保证的属性范围从操作语义的良好定义和行为等价的组合性到安全性和概率相关问题。在本文中，我们提供了一个初始层次的SOS规则格式和元定理制定围绕他们。关键词：形式语义，结构操作语义，规则集，框架。1引言结构操作语义学已成为定义操作语义的常用方法。操作语义定义了一段语法在其“执行”过程中可能发生的转换。每个转变可以由要传达给外部世界的消息来标记一个组合的语法片段的转换这构成了结构操作语义学（SOS）背后的核心思想。1 电子邮件：J.F. tue.nl2 电子邮件：M.R. tue.nl3 电子邮件：M.A. tue.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.0774J.F. Groote等人/理论计算机科学电子笔记156（2006）3Groote和Vaandrager在[ 36 ]中引入的转换系统规范（TSS通过对TSS的句法限制，可以推导出关于TSS的操作语义的一些有趣的性质。这些属性的范围从操作语义的良好定义[35，15，32]到安全性[70，71]和概率相关问题[10，41]。这些元定理所施加的句法限制通常表明特定形式的演绎规则对于特定目的是安全的，因此这些元定理通常定义了所谓的规则格式。优秀的概述[3]提供了到其出版日期（2001年）的现有规则格式。从那时起，更多的格式被提出，我们认为为了保持跟踪，这个格式领域需要一些结构。因此，我们试图概述文献中定义的所有SOS规则格式，以及围绕它们制定的元定理。所有结果都放在一个网格中，以便轻松找到最适合某个应用程序的格式。为了做到这一点，我们定义了TSS的概念，比[36]更一般，包括多排序签名和变量绑定的概念，灵感来自[24]的定义。TSS的这个一般定义作为一个统一的框架，为研究SOS的语义元定理和比较它们的底层框架铺平了道路。本文的其余部分组织如下。 在第2节中给出了格式的层次结构在第3节中，我们列出了SOS规则可以具有的不同语法特征。在第4节中，我们回顾了不同SOS框架的语义元定理。免责声明。本文件是迈向全面调查的一步。这意味着，尽管本文的其余部分提到了大多数格式和结果，但仍可能缺少一些规则格式和元结果。如蒙告知此等遗漏，我们将不胜感激。致谢。Peter Mosses、Simone Tini和Irek Ulidowski对本文的草稿提出了有益的意见2操作格式由于TSS规则定义了第一种格式，因此添加了许多格式为了跟踪它们，我们在图1中概述了现有的规则格式。这里提出的格有SOS框架作为节点，按句法包含（主要基于句法特征）排序。最通用的格式可以在顶部找到，更具体的格式在较低的位置。箭头表示语法包含。一种包含，它不是句法的，但可能需要对句法结构进行某种翻译J.F. Groote等人/理论计算机科学电子笔记156（2006）35福金克费尔霍夫VB，TL，CPY、LA、Pred、Neg.提升PANTH[24]第二十四话广义PANTH、、、、、、、、加长型轮胎有限非决定论SS、CPY、LA、Pred、Neg.BNd [25]∗SS、TL、CPY、LA、Pred、Neg.C（Partics，h，o），[53] 、、、MS，VB，CPY，LAC（参与者）[45]，[46]第四十六话MS、TL、CPY、LAC（Participatory），Ind.E，q。[，26]、、、、PanthSS、CPY、LA、Pred、Neg.C（Particles）[81]，、、、晋升TyftSS、CPY、LA、TLC（参与者）[1，1]，，OC[8，0，8，2]NTyft/Ntyxt（NTree）、、、、、、、路径、、、、、、、、、、SS、CPY、LA、阴性C（Participate）[21，35]、、SS、CPY、LA、PredC（参与）[8]、、、、、、. 你好， ，，s，. . . .，，，，，，，，，. . . .、、COMM-Tyft. ..GSOSSS、CPY、阴性，就绪模拟，SS，阴性蒂夫特SS，CPY，LASS、CPY、LA、Pred、Neg.Comm. [56]C（Particips）[14]你好，[31]第31话：我的世界PC（≤C（Particips）[36]Axiom，. [，2]，、、、、、、[13]第二届世界贸易组织部长级会议PC（≤，nn）[13]CccCc可能的GSOSSS，阴性C（Participp）[10]x-酷语言SSC（ParticipR+（η，WB，BB，D））阿克西奥山，[12，，33]SBSNNISS、、、、、、、、、、、、、、、、、、PB格式LA，LAC（参与）Stoch，[41，]de SimoneSSCcc公司简介CccCCCCCNINTf [71]、、、、、¸C6J.F. Groote等人/理论计算机科学电子笔记156（2006）3C（Particips）[17]PC（≤tr，f）[79]Fig. 1.现有SOS格式用虚线表示。这个格中的一个节点具有下面左手边所示的结构在右边显示了一个例子，取自网格。J.F. Groote等人/理论计算机科学电子笔记156（2006）37格式名句法特征语义元定理[参考文献]NTyft/NTyxt（NTree）SS、CPY、LA、阴性C（参与者）[21，35]每种格式的句法特征在第3节中描述。缩略语见表1。在第4节中描述了每种格式的TSS的定理3TSS的句法特征在本节中，我们列出了不同规则格式的独特语法特征。表1列出了每种格式的典型特性。速记句法特征SS与MS单-与多排序术语VB变量绑定TL与TLA术语与作为标签CPY变量LALookaheadPred谓词Neg个否定的前提表1规则格式的语法特征（参见图1）3.1标签标签是可能作为演绎规则中的转换关系和谓词的参数出现的术语。SOS框架可以根据它们所使用的标签类型进行分类，如下所示。开放式标签。许多SOS框架假设标签的特殊排序，并且只允许这种类型的常量（或者封闭项）显示为标签。因此，这种SOS框架禁止任何相关性，8J.F. Groote等人/理论计算机科学电子笔记156（2006）3通过使用共同变量对术语和标签进行估值。[24，26，11，53]中定义的框架允许任意项作为标签。本文中回顾的所有其他SOS框架都只允许常量标签。在过渡系统规范的许多情况下，开放术语被用作标签。高阶过程演算[16，69，66]是利用此功能的形式主义的例子。另外两个使用带有某种结构的标签的框架是[51，52]的模块化SOS框架和[18]的增强操作语义。前者假设标签是一个类别的箭头，因此配备了组成和身份。后一种方法在它们的标签上编码转换的派生树术语列表作为标签。大多数SOS框架只允许使用单个术语作为标签。唯一存在的例外是[24，53]。3.2签名名称和绑定器。在许多当代进程代数和演算中，名称、（实际的和形式的）变量和名称抽象（绑定）的概念都存在，甚至作为一个基本成分。例如，在π演算[48，49，50]中，名字是第一级公民，整个演算都是围绕在并发代理之间传递名字的概念构建的。这些概念的不太中心但却很重要的例子，以递归算子、无穷和算子和时间积分算子的形式出现在不同的过程代数中（参见，例如，[48]，[44，63]和[7]，分别）。因此，在技术支助服务框架中容纳名称的概念是有意义的。在这方面已经有一些尝试。在[83，24，45，46，39，65]中制定了建模名称和绑定器的建议。除了引入参数化变量外，[83，45，46，39，65]的TSS框架比[24]的限制更多，因为它们不允许开放项作为标签。此外，[83，39，65]的框架不支持负前提。除了上面提到的格式，我们在本文后面提到的所有其他规则格式都不支持名称和绑定器。多分类状态。根据签名中允许的排序数量，SOS框架可以分为以下三类：(i) 多排序的TSSJ.F. Groote等人/理论计算机科学电子笔记156（2006）39(ii) N-sortedTSS's：框架可能只允许固定数量的排序参与签名。这种框架的一个例子是[55]的过程类型除了这两种用于定义语义状态的排序之外，还有一种用于常量标签的排序。(iii) 单排序：这是文献中最常见的框架。它对操作状态有一个单一的排序，通常称为过程排序（来自这种排序的项是过程项）。在这个框架中，通常也有一个常量标签的排序[26]的TSS在其允许的签名方面具有特殊的地位也就是说，它需要一个特殊的进程排序和至少一个（必然不同的）标签排序。此外，它要求进程排序不应该参与以标签排序为目标的函数符号。3.3肯定前提与结论看前面如果框架中的演绎规则可以具有两个前提，其中一个前提的目标中的变量存在于另一个前提的源中，则框架允许前瞻。下面是一个带有前瞻的演绎规则的示例x→τy y→l zLx→z[28]中的上述规则用于组合无声（τ）和普通转换，以便在强语义框架内实现弱语义（通过忽略无声步骤）。基础良好。演绎规则的变量依赖图是以变量为节点的图，如果演绎规则中一个变量出现在（同一）正前提的源中，另一个变量出现在（同一）正前提的目标中，则两个变量之间存在边。当变量依赖图中所有变量的反向链都是有限的时，演绎规则是有根据的。当TSS的所有演绎规则都是有根据的时，TSS是有根据的。SOS规范的所有实际实例都是有根据的。在SOS框架的语义元结果的证明中，有根据性也非常方便。一个框架是否允许无充分根据的演绎规则是理论上的兴趣。- 是的如果框架允许变量在不同的前提和结论的目标中重复，并且在前提的源和结论的目标之间共享变量，10J.F. Groote等人/理论计算机科学电子笔记156（2006）3谢谢~B>a（在[72]中分别称为分支前提、显式复制和隐式复制复制的一个简单例子是下面TSS中的第二条规则，它定义了while构造的语义<$保持[b，M]当（b）做Pod时，M↓保持[b，M]当（b）做Pod时，M→P;当（b）做Pod时，M在有限的前提下。一个框架是否允许无限多个前提，这是一个有趣的理论问题。此外，实际上，当处理无限域时（例如，在有限的基本动作、数据或时间域中），有时具有有限前提的演绎规则是有用的。下面[58]中的例子说明了在无限前提下演绎规则的可能用途：x→a ya∈/H一a∈A\H一CH2OH（x）→CH2OH （xJ）χδH（x）→δ上述演绎规则定义了封装运算符的语义，禁止其参数在H中执行操作。如果参数不能执行任何普通的动作，那么它会转换到死锁进程δ。如果基本行动的集合是无限的，那么对于某个有限H，右边的演绎规则具有无限（否定）前提。3.4个否定的前提消极前提是SOS框架中的一个复杂因素。他们造成了几个复杂的语义方面的TSS的，这是相当困难的解决。换句话说，目前还不清楚什么可以被认为是否定公式的据我们所知，在实践中，SOS中负前提的第一个例子出现在[6]中，具体说明了以下优先级运算符θ（）的语义。x→axJ<$x~b一θ（x）→θ（xJ）上面的演绎规则指出，如果不能执行具有更高优先级的标签b的转换，则参数θ（）可以执行具有标签a的转换（根据给定的排序>）。除了消极的J.F. Groote等人/理论计算机科学电子笔记156（2006）311y→x;yx;y→y前提，上述演绎规则可能有无限前提，如果有一个具有无限多（不同）基本动作的优先级3.5谓词谓词是一种有用的句法特征，它用来说明诸如终止或分歧等现象。3.6其他句法特征制定扣除规则。避免使用否定前提（有时是谓词）的一种方法是在演绎规则中定义一个顺序。然后，仅当不存在可应用的高阶的演绎规则时，可以应用低阶的演绎规则来证明公式。例如，在3.4节中定义的优先级运算符的语义可以用以下形式的许多规则来表示：（ra）x→a一θ（x）XJ（xJ）→θ一个由ra<1）<$l∈L0<$L1tss0<$tss1<$p→l pJ惠tssp→l pJ（和similarl y，tss tssP（l）p惠tssP（l）p），0 1 0则TSS0-TSS1是TSS0的操作上保守的扩展。接下来，我们制定充分的条件来证明操作保守性。但在此之前，我们需要一些辅助定义。定义4.14[来源依赖]所有出现在演绎规则结论来源中的变量都被称为来源依赖。演绎规则的变量是源相关的，如果它出现在前提的目标中，其中源的所有变量都是源相关的。当一个前提中出现的所有变量都是源依赖的时，它就是源依赖的。 当一个规则的所有变量都依赖于源时，该规则就是源依赖的当TSS的所有规则都依赖于源时，TSS是源依赖的定义4.15[简化规则]对于演绎规则d=（H，c），关于签名的导出规则定义为ρ（d，.HJ，c）其中）=（HJ是H的所有前提的集合，这些前提以一个项作为源。文[24]中的下列结果给出了TSS扩张为操作保守的充分条件20J.F. Groote等人/理论计算机科学电子笔记156（2006）3定理4.16（运算保守性元定理[24]）给定两个TSS(i) tss0是源相关的;(ii) 对于所有d∈D1，至少有以下之一成立：(a) 结论的来源有一个函数符号，或(b) ρ（d，n）有一个依赖于源的正前提lJsuchthatl∈/0或tJ∈/T（t0）。t→t在[57]中，引入了运算保守性的稍微自由的概念，称为正交性，并提出了一个关于它的元定理。Or- thogonality允许在旧语法上添加新的转换和谓词，只要这些新的转换和谓词不改变旧术语之间的行为等式。4.4生成方程理论方程理论是处理代数的中心概念[5，38，47]。它们捕捉了代数背后的基本直觉，并且代数的模型被期望尊重这种直觉（例如，由操作语义模双相似性导出的模型）。拥有等式理论的附加价值之一是，它们能够在语法层面上进行推理，而无需承诺特定的语义模型。当行为的语义模型（例如，与术语相关联的转换系统）是有限的，这些技术可能会非常方便。为了在操作模型和代数的等式理论之间建立合理的联系，应该固定行为等式的概念。理想情况下，行为等价的概念应该与等式理论的封闭推导相一致。这种巧合的一个方面被可靠性定理所捕获，该定理指出，等式理论的所有闭导子对于特定的非线性等式概念确实有效。巧合的另一面，称为完全性，所有诱导的行为等式都可以从等式理论推导出来。这些概念在其余部分中被形式化。定义4.17[等式理论]一个等式理论或公理化（E，E）是一组等式E在一个形式为t=tJ的签名上，其中t，tJ∈ T。对于某个p，PJ∈ C，一个闭实例p=pj可从E导出，记为Ep=PJ当且仅当它在由E的等式导出的闭项上的最小同余关系中.一个方程理论（E，E）对于TSStss是合理的（也是在J.F. Groote等人/理论计算机科学电子笔记156（2006）321签名（签名）和行为等式的一个特殊概念（签名）当且仅当对所有p，pJ∈C，如果E<$p=pJ，则它保持tss<$p<$pJ。如果蕴涵在另一个方向上成立，则它是完备的在[2，1]中，提出了一种从GSOS这种技术在[9]中得到了扩展，以满足进程的显式终止。这种方法虽然本质上更复杂，但与[2]的原始方法相比，产生了更直观和更紧凑的方程组。公理系统的预购已经产生，太，例如见[73]。沿着同样的思路，[74]为TSS生成优先重写系统4.5其他元结果不干涉。保密性是安全性的一个重要方面，而非干扰[34]是保证端到端保密性的一种经过充分研究的方法。非干扰性意味着具有较低机密级别的用户不能通过与系统交互（使用其手头的较低级别方法）来推断有关较高级别信息的任何内容。在[70，71]中，提出了一种基于Cool语言格式的非干扰规则格式（为了保证非干扰的组合性），并施加了进一步的限制，以确保系统的低级别行为不会因执行高级别转换而改变逻 辑 公 式 的 分 解 在 [37] 中 ， 提 出 了 一 个 逻 辑 框 架 ， 现 在 被 称 为Hennessy-Milner逻辑Hennessy-Milner逻辑可以用来推理过程并描述它们的等式。在[42，43]中，开发了一种元理论，允许通过检查DeSimone格式的过程语言的演绎规则，以通用的方式使用项的结构来分解Hennessy-Milner公式。该结果在[22]中得到了改进，并扩展到就绪模拟格式（无前瞻的ntyft/ntyxt格式）。在[23]中，分解技术被用于导出用于eta互模拟概念的同余格式Simpson在[68]中介绍了一个组合证明系统，用于检查GSOS格式中指定过程的Hennessy-Milner公式随机性。对于概率转移系统，必须确保属于同一分布的所有概率之和等于1（或零）。这叫做（半）随机性。在[41]中，提出了De Simone格式的限制形式，保证了半随机性。22J.F. Groote等人/理论计算机科学电子笔记156（2006）3为了避免处理否定前提，[41]的格式支持规则排序。有限的非决定论在[78]中，通过对De Simone格式施加限制，提出了一种规则格式，该格式保证了所导出的语义只包含有界非确定性，即，每一个闭项只有有限数量的输出转换。Fokkink和Duong Vu在[25]中将[78]的结果推广到更一般的SOS框架。定时特性。在[77]中，定义了一组句法条件来保证时间系统的属性，例如时间决定论，持久性，最大进度和耐心。引用[1] L. Aceto.为一类产生规则行为的GSOS语言导出完整的推理系统。芽孢杆菌中Jonsson和J.Parrow编 辑 ， Proceedingsofthe5thInternationalConferenceonConcurrencyTheory（CONCURSpringer-Verlag，1994.[2] L.阿塞托湾Bloom和F.W.凡德拉格把SOS规则变成等式。信息与计算，111：1-52，1994。[3] L. Aceto、W.J. Fokkink和C.维尔霍夫 结构操作语义学。 在J.A. 伯格斯特拉，A. Ponse和S.A.Smolka，编辑，Handbook of Process Algebra，第3，第197Elsevier Science，2001年。[4] E.A. Astesiano，A. Giovini和G.瑞吉欧关系规范中的广义互模拟。In R.Cori和M.Wirsing，编辑 ， Proceedings of the 5th Annual Symposium on Theoretical Aspects of ComputerScience（STACSSpringer-Verlag，1988.[5] JCM Baeten和J.A.伯格斯特拉实时处理代数。Formal Aspects of Computing，3：142[6] JCM Baeten和R.J. van Glabbeek。进程代数中的归并与终止。在K. V.Nori，编辑，Proceedingof the Seventh Conference on Foundations of Software Technology andTheoretical ComputerScience（FST TCSSpringer-Verlag，1987.[7] JCM Baeten和C.A.米德尔堡带定时的进程代数。EATCS各论。Springer-Verlag，2002.[8] JCM Baeten和C.维尔霍夫带谓词的结构化操作语义的一个同余定理。Eike Best，编辑，International Conference on Concurrency Theory（CONCURSpringer-Verlag，1993.[9] JCM Baeten和E.P.德·温克将全球安全保障与终止一起公理化。Journal of Logic and AlgebraicProgramming，60-61：323[10] F. 巴 特 尔 斯 概 率 转 移 系 统 的 GSOS 在 Proceedings of the 5th International Workshop onCoalgebraic Methods in Computer Science（CMCS[11] K.L.伯恩斯坦高阶语言结构化操作语义的一个同余定理。在IEEE Symposium
我的内容管理
展开
