GETGRATS项目的主要科学贡献及参考书目

网址：http://www.elsevier.nl/locate/entcs/volume51.html64页GETGRATS：科学结果总结（带注释的参考书目）编辑：Andrea Corradini1比萨大学信息学院意大利比萨摘要本文总结了GETGRATS项目在网络生命周期内（从1996年9月1日至2001年8月31日）开展的研究活动的主要科学贡献参考书目列出了大约300种出版物，其中大部分发表在国际期刊或会议上。从参考书目项目到文档主体的反向链接允许将其用作注释参考书目。内容1介绍22图重写的基本方法理论52.1代数方法：单和双推出52.2回调重写62.3超边替换和顶点替换62.4高级替换系统72.5代数变换系统82.6采油树传感器92.72-结构102.8确定性下推自动机102.9基于图变换的编程构造languages语言112.10 图-理论结果113规格113.1开放和反应系统的规范与图转换和视图111电子邮件：andrea@di.unipi.itc 2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。23.2使用Tiles3.3图的一元二阶13逻辑143.4图变换163.5数据和行为规范形式的整合173.6其他方法：耦合图文法和图形SOS。174结构方面184.1分布式图转换184.2软件架构204.3层次图214.4模块化概念：GRACE和转换单元224.5类型化图转换系统的模块联系方式234.6 Colimit结构24第五章语义245.1代数图文法245.2局部行动系统：过程语义学和Petri网265.3术语图的分类表示及其应用285.4图变换305.5结构化变迁系统305.6（上下文）Petri网316应用程序326.1术语图重写和术语图缩窄326.2 DNA计算336.3拼贴语法和图片生成346.4移动环境356.5基于Agent的系统356.6控制访问策略366.7半结构化数据和超媒体的建模366.8图形匹配367种基于图重标记系统的378手册、教程和会议记录39引用401介绍GETGRATS（General Theory of Graph Transformation Systems）是一个由欧 盟 委 员 会 资 助 的 研 究 TMR 网 络 ， 从 1996 年 9 月 1 日 到 2001 年 8 月GETGRATS由七个3研究小组，连同相应的团队负责人一起列出：(i) 安特卫普大学（比利时）：教授、博士德克·詹森斯(ii) 柏林工业大学（德国）：Hartmut Ehrig(iii) Bordelais de Recherche en Informatique教授（法国）：Prof. 博士米歇尔·鲍德龙(iv) 不来梅大学（德国）：教授、博士汉斯-约尔格·克廖夫斯基(v) 莱顿大学（荷兰）：教授博士。格热戈日·罗森贝格(vi) 比萨大学（意大利）[主要承包人]：Ugo Montanari(vii) 罗马大学（意大利）：教授博士 弗朗切斯科·帕里西·普雷西切网络协调员是Andrea Corradini（意大利比萨本文件介绍了GETGRATS项目在其生命周期内开展的研究活动的主要科学贡献它包括GETGRATS成员发表的约300份出版物的书目，其中大部分发表在国际期刊和会议上。根据GETGRATS的项目计划，该项目的目的是通过巩固数学在其研究中的应用并将其视为话语和兴趣的对象来开发图形转换系统的一般理论。“该项目涉及的研究主题分为以下七个重点领域”：(a) 基础、统一、组合和比较，涉及到图形重写的不同方法的比较和统一，或这些方法的特定方面。(b) 分类和表达能力，包括识别影响表达能力的GTS的各种结构特性。(c) 分析与验证技术，是指通过对GTS句法描述的考察，研究GTS的哪些语义性质可以被推断或决定的分析与验证技术的发展(d) 抽象语义学，包括基于派生序列（抽象或具体），过程和事件结构的语义研究，特别是根据对模块化和并发性的研究。(e) 并发方面，关于并发和分布式GTS概念的发展，包括适当的语义，以及它们与其他并发模型的比较。(f)模块化方面，包括模块概念的定义，从其他领域（如抽象数据类型）借用技术。(g) 态射、变换和运算，包括图过程、事件结构和其他抽象域的适当类别的定义，并通过函子将它们与语法类别联系起来，4或者，更好的，通过预防。这一划分的目的是便于集中（从而加强）各伙伴之间的合作。然而，为了向该领域的非专家描述在网络中进行的研究活动，根据主要研究主题来组织演示文稿会更方便。特别是，各种贡献可以（松散地）归类在以下标题下：(i) 图重写基本方法的理论，涉及各种方法的定义和性质的研究，包括代数方法、拉回重写、超边和顶点替换、高级替换系统、代数变换系统、树转换器和2-结构等。(ii) 基于图形转换系统的规范技术，包括开放式和反应式系统与图形转换，视图和瓦片的规范;一元二阶逻辑的图形属性的规范; GTS的模态和时序逻辑;以及数据和行为规范形式的整合。(iii) 结构化方面，包括空间维度上的系统结构（如分布式图变换和分层图变换），以及从软件工程角度来看的系统逻辑结构（如基于GTS的软件架构，模块化和重新配置方法）。(iv) 图变换系统的语义，包括代数图文法和局部动作系统的基于过程的（并行）语义;代数图文法的展开、基于事件和抽象语义（使用双模拟）;类项结构的范畴表示及其在项图重写中的应用; GTS的归纳定义;结构化转换系统的共代数语义;（上下文）Petri网的代数语义。(v) 应用程序，关于使用一个或多个基本方法的主要案例研究，如图形表示的条款和重写规则（术语图重写和缩小）;在DNA计算纤毛虫基因组装建模;图形应用程序，如拼贴语法和图片生成;建模的移动环境和基于代理的系统;访问控制策略的规范;和其他。(vi) 基于图重标记系统的分布式算法，用于模拟图上的局部计算;其中，三个经典的问题，lems解决：识别问题，选举问题和终止检测问题。(vii) 手册、教程和会议记录。在这个标题下，我们将列出一些出版物，无论是教程介绍-5对图形转换系统的各种方法的评论，或对特定研究领域的结果的综述。这些捐款证明了网络成员在培训活动中的努力在下面的章节中，我们将简要介绍GETGRATS期间的主要主题和贡献2图重写2.1代数方法：单次和双次推出在[HMP 00]中，通过考虑规则中的内射匹配和/或任意右手态射，得到了图变换的经典双推出方法（[CMR+97]）的三个变体结果表明，与传统的任意匹配方法相比，内射匹配不仅为无非终结符文法生成图语言提供了灵活的表达方式此外，对于具有内射匹配和任意右射的最一般变体，通过加强序列和并行独立性，建立了序列和并行交换性.此外，在[HMP01]中，关于并行性和并发性的经典定理适用于具有内射匹配的设置在[Plu98]中，它表明终止是图重写系统的不可判定属性证明是通过简化的邮政对应问题。它还认为，无论是图灵机的停机问题，也没有字符串重写系统的终止问题，可以减少到图重写的终止问题，在一个简单的方式。在[BMRV 99]中，单推出方法（[EHK+97]）被推广到部分多序一元代数的代数变换.主要结果是在给定签名上的一元部分代数的所有保形、所有闭准同态和所有闭域闭准同态范畴中的单推出变换的代数刻画，以及相应的运算刻画.另一个重要的结果是定义了合并的高级替换条件，并证明了上述三个范畴满足所有的并行和合并的高级替换条件。在[Gru00b]中，类型化的SPO方法已经被元类型化设施扩展。主要结果是，所提出的元类型的概念是兼容的SPO理论，并可以实现到基于SPO的图形语法环境AGG不破坏其形式基础。这种基于SPO的元类型化方法与PROGRES中遵循的元类型化算法方法进行了比较。62.2拉回重写拉回重写[BJ01b]是最近提出的一个描述图中顶点替换的范畴从那时起，它已经出现了一个相当强大的机制来描述大量的图重写系统。特别是，它显示在[BJ01a]如何可以用来提供一个统一的重写机制下的名称“结构化图”下统一描述的广泛的一类图Pullback重写在[Kle98]中被用来描述Petri网单元，在[JK00]中被用来实现超图中NCE节点的重写拉回重写也可以被认为是一种合成机制。在这种方法中，在[BC00]中示出了如何将某些类型的图分解为两个正交分量，其拉回是原始图。迭代该过程，这些图可以被写为一些基本构建块的组合这个结果给出了一个简单的描述几种类型的图谁看起来非常规则（如网格），虽然没有这样，在任何语言理论的意义。为回调重写制定一个完整而充分的框架的工作一直在继续，导致了Hel ene Jacquet博士的介绍1999年1月的论文。在[BJK 02]关于图重写的拉回方法的综述中，描述了扩展到并行重写的基本机制以及在NLC重写和Petri网恢复中的应用。2.3超边替换和顶点替换文献[Dre97，Dre98a]研究了由（超）树构成的超边置换（HR）图语言的结构.结果表明，这些语言可以生成的产生式的右手边是自己的超树。然而，对于这一点，派生树的集合必须由nite复制自顶向下树转换器产生。因此，nite复制补偿了由于只允许超树作为右侧而导致的功率损失在[Man 98]中，从语法系统领域已知的合作和分布的概念被引入到图语法，更准确地说，引入到超边替换语法。两个不同的推导模式被认为是所谓的t模式和=k模式。对于t-模式，它表明，超图语言类是等于类的ET 0 L HR语言，这是一个自然的推广的ET 0 L语言超图。在[CM00]中，基于由数量自由公式定义的超图运算以及具有相同标号的所有顶点关于基于定义VR文法的图操作的图分解，相应的复杂性度量是7称为cn-width。在nite图的情况下提出了具体的问题。在[HK98]中引入了超图中的原子置换，它结合并统一了节点置换和超边置换的概念在[DK01b]中，超边替换语言被看作是语法图。通过读取沿着路径的边的标签，获得单词。本文研究了字符串语言的这种规范方法，特别是关于其生成能力。一致节点重写图文法，在文献中被称为C-edNCE考虑到超图而不是图的上下文无关重写，在[Kle99]中表明，并发节点重写允许指定所有超边重写和分离的超边重写语言，甚至超越该并集的语言。尽管如此，这些C-hNCE语法仍然存在一些范式，这些范式允许推断生成的图形语言已经可以由C-edNCE语法指定[Kle 01]。Klempien-Hinrichs的博士论文[Kle 00]对具有节点和超边重写的上下文无关超图文法进行了全面的研究，包括在Petri网中的应用。文[Kle02]中简要地总结了本文的一些主要结果。[MV98]介绍了属性上下文无关超图文法（acfhg文法）。 Acfhg文法和属性文法密切相关：属性文法可以用来计算acfhg文法的属性值。一些已知的形式主义，如兼容函数和属性树文法可以嵌入到acfhg文法。acfhg语法可以用于以这样的方式来定义编程语言P的语义，使得P的非上下文无关约束已经在语法阶段中被检查，即，通过底层的图形语法。2.4高级替换系统高级替换系统是一个公理化范畴框架，它将图变换系统和图文法的概念从图推广到计算机科学和数学中在图变换的代数方法中，这是可能的，通过将图、图态射和图的推出（胶合）替换为适当类别中的对象、态射和推出。特别感兴趣的是各种标记和类型的图，超图，代数speci阳离子和Petri网的类别。在[Tae97]中，引入并行高级替换系统以在该框架内形成并行重写的概念。一方面，这一概念通过允许图以外的其他结构，推广和扩展了迄今为止在代数方法中提出的并行图文法，另一方面，为高级替换系统引入的替换类型通过不同类型的并行替换来扩展，8在不同的定理中相互比较。一个抽象版本的基于窗口的图形编辑器和描述对象的运动在配置空间的并行高级替换系统的例子。高级替换系统的主要理论概念和结果在[EGP99]中进行了调查，其中显示了代数双推出方法中图变换系统的一些基本结果如何在这个更一般的框架中重新表述。关于局部Church-Rosser性质和水平结构的结果的具体选择是由本文研究的应用领域所需的结果所激励的，这些应用领域包括代数规范和Petri网，其中变换分别对应于规范或网的结构的基于规则的变化[EHP 02]中介绍了高水平置换系统理论的最新综述。在[Pad 99]中，给出了高阶置换系统的几个结果，这些结果围绕着一个称为Q-变换的置换范畴概念高级置换系统的几个概念和结果被推广到Q变换 这些是顺序和并行转换，联合，和融合，基于不同的colimit结构。这些结果在[Pad99]，[PGE98]和[PG98]中应用到Petri网。广义上的系统验证是指通过分析系统的语法描述来确定或推断系统的语义属性。在[KV00]中，冗余和包容的语义属性从基于规则的系统转移到高级替换系统，高级替换系统又概括了图和超图语法。主要结果是包含的一个特征和包含的一个充分条件，其中包含合成产生式。2.5代数变换系统代数变换系统是[Gro98]中作为开放分布式系统组件的形式化模型而引入的。它们由模拟控制流的转换图和模拟数据状态及其变换的部分代数和方法表达式给出。 根据这两层结构，它们涵盖了标记迁移系统和基于规则的规范方法，分别对应于信息、计算和工程观点模型。研究了代数变换系统的不同复合运算.极限和共极限模型组件的并行和顺序组合，签名态射产生适当的语法支持这样的组合。从代数规范中已知的最重要的组合性属性，如签名的共同极限在部分代数的情况下构造推出补的相关技术问题在[LR 00]中得到了解决。9在[Gro02]中，定义了复合运算和关系，为代数变换系统定义了一个语义层，从而定义了系统组件的组合。同样在语义层面上，元素关系的定义支持从更抽象的设计或需求规范迭代开发更具体的设计规范。复合操作和关系都被抽象为模式，可以通过不同的实例化分别得到具体的复合操作和关系。这些方案是明确定义的。2.6采油树传感器在[DE 98]中，证明了一个大类的树变换的值域的有穷性是可判定的。结果表明，这产生了一个推广的已知的判定结果有关的有界性问题的功能图和其他领域。可以处理的函数可以通过图的导出树上的递归来定义。在[EV98]中，表明自下而上和自上而下的树到图转换器定义了同一类树转换（与经典的自下而上和自上而下的树转换器相反）。在[BE 00]和[EM 99]中，在MSO可定义树转换之间进行比较，即，可以在一元二阶逻辑中指定的树转换，以及经典的、面向实现的树转换：属性语法和函数编程。在[BE 00]中表明，MSO可定义树转换对应于“一次性”专用语法，在[EM 99]中它们对应于“节点复制”宏树转换器。这些结果可以看作是Bu的树平移chi的经典结果：MSO可定义的字符串语言对应于nite自动机。文[EM00b]给出了由上下文无关的超边置换文法生成的树语言类的一个特征：它是宏树转换器的输出树语言类，它是纯拷贝的，参数是特殊的（即线性的和非删除的）。图文法和树转换器之间有着密切的关系在[Man99]中，考虑了可以由宏树转换器（MTT）生成的字符串语言的类别。通过一个“桥定理”，它表明，总的确定性MTTs不能产生特定的语言产生的更简单，不确定性的设备（即ET0L系统）。在[MN99]中，可扩展样式表语言XSL，通常用于将XML代码转换为HTML代码，可以通过某些自顶向下的树转换器进行建模。重要的新的一点是，这些传感器上的unranked树。利用一元二阶逻辑给出了该类的另一个刻画，并证明了各种复杂性结果。10众所周知，上下文无关图语言可以通过MSO可定义的树到图转换从正则树语言获得。在[EM00a，EM01]中，MSO可定义的树到树转换由宏树转换器表征，宏树转换器的输出树的大小与输入树的大小成线性关系。此外，它示出，它是可判定的宏树转导是否是MSO-可确定的。树转换器是一种有用的工具，用于层次可分解图的转换。然后，可以通过查看所使用的树换能器的特性来研究图形变换的特性。在[Dre99，Dre01a]中，研究了决定自上而下或自下而上树换能器是否产生指数大输出树的复杂性。原来对于总的自上而下的树换能器，输出为LOGSPACE-完全，但一般为DEXPTIME-完全，而在自下而上的情况下为P-完全2.72-结构动态标记2-结构形成了面向网络的并发和分布模型。它们在图论中也起着重要的作用，被称为增益图的切换类。其中一个核心问题是确定在系统演化过程中是否会出现具有某些性质的全局态。这一问题已被调查的模式和congurations。得到了一些关于模式和构形之间关系的结果。2-结构理论的完整介绍已在书[EHR 97]中发表。[HH 00]中给出了关于切换类大小的结果。文献[EHHR 00a]研究了几个关于增益图的判定问题的复杂性及其与一般图的类似问题的关系。增益图的隶属度问题的研究，即，两个增益图是否属于相同的切换类的问题在[Hag99]中解决，而[EHHR00b]主要关注泛循环性，[HH98]研究切换类的非循环性。工作正在进行中的一些纯粹的组合问题，使用禁止子图;第一结果出现在[HH01]。所有这些结果，加上一些额外的材料，可以在Ph.D. J. Hage的论文[Hag01]。2.8确定性下推自动机[Sen98b]完全解决了所谓的“确定性下推自动机（dpda's）的等价问题这个问题可以重新表述如下：给定两个方程根，确定图G1;G2，是否有可能决定他们是否是双相似的？这种可判定性证明可以被看作是一种验证技术，其行为可以通过方程图来描述[Sen97]， [Sen98a]将上述工作扩展到非确定性情况，而[Sen98c]将其扩展到具有阿贝尔群中的输出的dpda（等价于11图的标号属于阿贝尔群）。 本文[Sen99]将[Sen98 a]关于方程根确定图的双相似性的可判定性的结果推广到输出取在有理数域上的任意矩阵群中2.9基于图变换的语言的编程结构在[HP01]中，确定了一组编程结构，可确保基于图变换的编程语言在计算上是完整的。这些构造是（1）一组图转换规则的非确定性应用，（2）顺序组合，以及（3）迭代。这种语言是最小的，因为省略顺序组合或迭代会导致计算不完整的语言。通过计算完备性，我们指的是在标记图上计算每个可计算部分函数的能力。2.10图论结果最后，我们提到对图论的一些贡献。的博士thesis [Pel97]提供了各种类型的Inite图的自同构群的详细结构，按照复杂性的顺序：上下文无关，等式和自动。在文献[BE 97c]中研究了树宽的一个新概念，它与顶点图文法密切3规范2.03.1具有图变换和视图的开放反应系统的规范反应式系统通过与用户或其他系统（作为更大系统的一部分）的交互来执行任务。 对这种系统建模的一个基本要求是能够表达这种交互。经典的基于规则的方法，如Petri网和图变换不适合这个目的，因为它们假设对系统的状态及其变换具有完全的控制为了提高图形转换系统对开放式反应系统建模的表达能力，在[HEWC 01]中引入了图形转换。基于给定图产生的图转换是重写步骤，其中不仅执行由产生规定的效果（即，特定图项的删除、保存和创建），而且还可以执行附加改变，即添加或删除其他项，就好像这些是由环境引起的一样。从概念上讲，这种图形操作没有隐含的框架条件：图形生成被认为是要执行的转换的不完整描述。从技术上讲，图形转换是12使用双拉回构造，与基于双推出的经典图推导相反本文给出了图变迁分别与经典的双推出导子和混合导子相联系的两个刻画结果此外，一个松散的语义图转换系统的定义，它与每个系统的一类模型（确定性转移系统）定义为一个合适的函子上的余代数。这样的范畴有一个nal对象，它包括所有夜间和夜间转换序列。在这些结果的基础上，[HEWC 97]的目的是通过引入图变换的约束来丰富这种建模形式主义的表达能力，以限制上述图变换系统的松散语义共代数框架使得去-需要一个行为约束逻辑的一般概念。包括，因为例如，开始图，应用和一致性条件，以及时序逻辑约束。结果表明，所考虑的语义可以被限制到一个最终的余代数语义系统的行为约束。在[EHL+00]中给出了图变迁的几种构造方法，如图变迁存在的充要条件最后，将该概念框架应用于Petri网，得到了开步的概念。该方法在[ERP98]中得到了进一步推广，其中提出了一个框架，用于扩展图转换和其他基于规则的形式主义，以便可以处理不完整信息的转换。这种扩展的动机是需要模型的开放系统在不同的应用领域，使用图形变换和Petri网的代理。DNA计算和其他基于规则的形式主义的问题也进行了讨论最近在软件工程界提出了一种结合参考模型和基于视图的规范方法的思想。在[EHTE97]和[EEHT97]中，提出了一种基于图变换的规范技术，该技术支持这样的开发方法。图形和图形转换的使用在此背景下，视图和视图关系的形式化概念被提出，视图的行为被松散的语义描述。定义了一种视图自动集成的结构，它假定不同视图之间的依赖关系由一个参考模型来描述。视图和参考模型手动保持一致，这是模型管理员的任务。所有的概念和结果都说明了一个银行- ING系统的例子。[HEET99]中调查的总体方法。此外，它在[Hec98a]中被用于规格的组成验证。这个想法是，视图提供了一个不完整的规范，只描述了整个系统的某个方面视图预期（潜在）行为13整个系统的松散语义。 这确保了视图的属性被整个系统继承。 通过利用这一事实，可以通过将规范分解为若干视图、分别分析它们并从针对视图示出的属性导出期望的属性来验证时间属性。Reiko Heckel[Hec98b]的论文将刚刚回顾的概念（图转换和视图）带入了一个一致的，统一的概念框架，该框架基于开放图转换系统，为并发和反应式系统的组合建模而设计。为了验证时间特性，一个大规格分解成几个视图，分别进行分析。然后，从视图的性质导出原始规格的性质。基于开放图变换系统的松散语义，提出了开放图变换系统的函子语义。这种语义是作为一个基础的组合验证的时间属性的系统的正确性。在[BCEH01]中，为了模拟开放反应系统的行为，通过Petri网的方法，引入了开放Petri网作为一种推广，普通模型的一些地方，指定为开放，代表反应系统对环境的接口。由于与环境的相互作用，代币可以在网络的开放位置自由出现和消失。开放网被赋予了一个真正的并发语义的基础上开放的进程，这是一个扩展的Goltz-Reisig（确定性）的过程。3.2使用Tiles当考虑抽象等价时，例如，双相似性是组合性的一个关键点，它保证等价组件可以在任何系统中安全地相互替换。SOS格式的定义，确保闭项上的双相似性是一个一致性，在过去的二十年里受到了广泛的关注。为了处理开项，通常通过以所有可能的方式实例化自由变量来从闭项中提取论文[BdMM00a，BdMM00b]提出了一种基于tilel ogic（t1）[GM00]的方法，其中封闭项和开放项被统一管理，并研究了几种tile格式的同余属性，实现了开放系统的不同概念，其中，例如，配置是由项图而不是普通项来定义的。事实上，瓦片是重写规则，其具有处理非常一般的配置和观察的副作用，其仅需要具有合适的顺序和并行组合。在[Bru99，BMM98c，BMM01]中，根据对称monoidal和cartesian双范畴的原始概念，研究了几种图块格式的范畴基础，这些图块格式的构形和观测具有类似的附加结构（例如对称性，笛卡尔性）。当配置和观察配备了相同的基本14代数运算，瓦片逻辑也适合于建模开放式系统，其中动态重构是通过观察合适的上下文嵌入来获得的。特别是，该方法可以扩展到处理congurations的结构公理，仍然保证了重要的属性，即“双相似性是一个同余”[BMS00]。在全文（[BMS01]）中，将该方法应用于微积分的实例研究，证明了开放双相似性和瓦片双相似性是一致的。上下文和实例化闭包之间的二元性，在瓦片的分类模型中很明显，在逻辑编程[BMR 01]的应用中得到了很好的例证，其中采用了自由生成的双重拉回类别来建模union。最简单的瓦片类，其中congurations和观察是基本元素的多集，已被证明提供并发事务的概念的Petri网。由此产生的瓦片模型被称为零安全网，并已在[BM 97，BM 98 c，BM 00 b]中进行了研究，以及对几个案例研究的应用。在[BM00a]中，定义了一个用于零安全网的分布式解释器，这让人想起普通的网展开，而在[BM01a]中，该方法已扩展到处理读弧（允许在读取同一令牌时进行多路访问在[BM01b]中给出了带读弧的零安全网在Linda事务并发建模中的应用零安全网络的教程介绍在[BM99 b]中给出。介绍高阶版本的TL的自动治疗的名称传递和名称创建在移动结石被认为是在[BM 99A]，与应用程序的演算。相应地，利用最初的范畴闭双范畴的概念，定义了高阶tl虽然目前还没有直接基于tl的自动验证工具，但通过重写逻辑中的保守编码，已经使一些原型能够用于合适的tl规范类，如[BMM 98 c，BMM 98 b，BMM 99，BMM 98 a]中所报道的。特别地，tl的实现利用重写逻辑中的反射来定义用于控制重写的合适的内部策略，并且是用Maude语言编写的[CDE +99]。3.3一元二阶逻辑对图性质的描述一般代数的等式子集和可识别子集的基本性质在[Cou 96 a]中进行了综述;这些集合可以分别被看作是上下文无关语言和正则语言的推广这种方法以Uni-代数为基础，促进了形式语言理论的发展，使其包括了对nite树、nite图、nite超图、词元组、部分可交换词（也称为迹）和其他类似nite对象的描述。描述性复杂性关注的是复杂性的表征-15用逻辑公式分类。特别感兴趣的是一元二阶逻辑（MSOL）的公式，从存在集量化开始，然后是一阶量化。在[Cou97b]中，从用这些公式表示的角度对图的主要基本性质进行了评述。特别是，它认为建设性的表达的平面性的公式描述了一个平面嵌入。这应该与库拉托夫斯基定理的经典否定刻画形成对比，库拉托夫斯基定理没有提到被认为是平面的图的平面嵌入。在[Cou96b]中，对以下一般问题给出了一些答案：对于哪些类的图C，可以用一个固定的一元二阶公式来指定C的每个图的顶点集的线性序还研究了C的子类的可识别性和一元二阶可确定性是否相同，以及C的图的层次代数结构是否可以在一元二阶逻辑的扩展中定义.文献[BE 97 b，BE 97 a]证明了树结点的一元二阶逻辑性质只能用布尔值的属性文法来实现，而树结点间的MSO关系可以用带有MSO测试的树行走自动机来实现。这些特征可用于通过属性文法实现MSO可定义树转换，如[BE 00]所示。众所周知，语言是上下文无关的，它是可识别集合的树的边界的集合，其中（标记的）树的边界是由从左到右读取的叶子标签组成的单词。在[CL 98]中，给出了这个结果在有界树宽的平面图中的推广。在这里，平面图的边界是一条路径的边标签的词，该路径与某个平面嵌入的面邻接。本文证明了一种语言是上下文无关的，它是一组有界树宽的（标号）平面图的图的边的集合，这是由一元二阶逻辑公式定义的。在[Lap98]中，示出了对于每个k，存在一元二阶转换，其与每个树宽度至多为k的图关联其宽度至多为k的树分解之一。与Courcelle的一个已知结果一起，得出了每一组有界树宽的图是CMSO-可确定的当且仅当它是可识别的。某些图，如余图，有一个独特的层次分解。人们自然会问，这种分解是否可以用一元二阶逻辑的公式来定义（在精确的意义上）。对于上图来说，这是可能的，只要给图一个辅助线性序。在[Cou99]中，Tutte定义了连通图的唯一分解，并证明了它可以用MSO公式来定义。论文[Cou00b，Cou00c]考虑了图的关系结构的形式化，有或没有边交叉，其中图形的属性用一元二阶逻辑形式化。关于Kuratowski16定理，非平面图可以用一个存在的MSO公式来刻画。当所考虑的图是平面图时，这个公式的无效性并没有给出关于其平面图的信息：用MSO公式来定义一个可能的平面图下面的组合映射（一个有限的逻辑结构）是很有意义的。文[Cou00b]证明了线性序平面图的平面映射是MSO可定义的。在一元二阶逻辑中，图的性质有两种表示方式：有边集量化和无边集量化。改进了文献[Cou01c]中的结果，证明了边数线性有界的图的边集量化可以被去除在[CMR99，CMR00，CO00]中研究了图的层次分解。它们对于有效的图算法是重要的，并且它们是由文法生成图的基础特别是，图分解相关的宽度产生线性算法的问题，制定了一元二阶逻辑没有边缘量化。文[CMR01]进一步研究了基于MSO逻辑问题的逻辑描述的多项式图构造算法，而文[Cou01b，CM01]则研究和比较了不同类型的图构造算法的图运算。在[EHvB99，EH99]中研究了树行走自动机对鹅卵石的使用在[EHvB 99]中证明了树上的trip可以用一元二阶逻辑来定义，它们可以由树行走的大理石/卵石自动机来执行。在[EH99]中，它表明，所有的一阶可定义的树语言可以识别的树行走自动机与卵石，有嵌套的生命期，这样的自动机只识别正规树语言。二叉树上的一元二阶逻辑（S2S）是非常强大的，它包含了并发中使用的各种逻辑，如分支时间时序逻辑或μ演算。在[JL99]中表明，S2S不会塌缩到其级别2，甚至不会塌缩到2的布尔组合。第一个断言的一个例子是S2S公式，它说，对于二叉树的某个固定子集S，有一条路径经常与S论文[Cou00a，Cou01a]是本小节中讨论的一些研究主题的综述。3.4图变换在[GHK00]中，图解释时序逻辑被引入作为与基于图变换的基于规则的规范结合使用的规范逻辑。它通过解释状态是图的转换系统上的公式来专门化命题时态逻辑，即，图转移系统证明了图迁移系统具有与一般迁移系统相同的判别力。因此，命题时态逻辑的任何可靠和完备的演绎演算对于图解释的变体也是可靠和状态的性质表示为：17解释时态公式中的命题变量的图形约束对于任何一种解释，都构造了一个典型的、完全抽象的图转换系统。这里的典型性意味着所构造的系统满足时间公式当且仅当该公式对所有具有这种解释的过渡系统都为真。完全抽象是指系统中任何两个不能用图形约束区分的状态都是相等的。因此，对于一组有限的约束，我们最终得到一个适合于模型检查的有限转换系统。Manuel Koch（[Koc 99]）的论文将图解释时态逻辑推广到分布式图变换。类似于[Hec98b]，从子系统中局部公式的局部满足进行推理，支持分布式系统以在完全分布式系统中全局满足全局公式。3.5数据和行为规范形式化在[EO01]中，给出了数据类型和过程规范技术的一般分类。此外，提出了一个系统规范的集成范式，它提供了一个统一的方法在概念层面上。其核心思想是考虑四个不同的层次，对应于系统规范的不同类型的集成视图。这四个层的形式化模型分别称为数据类型层、数据状态和转换层、过程层和系统体系结构层，它是基于抽象数据类型和结构化转换系统的集成。这种形式化模型可以通过各种基本的和集成的建模技术来实现。大量的数据类型和过程驱动的规范方法，包括Al-george高级网，属性图转换，Z与状态图的集成，以及UML的一些图表技术，作为集成范例的实例进行了简要的讨论。在[EPO01]中，Ehrig，Padberg和Orejas区分了主要涉及系统的一个视图或方面的基本规范形式主义和照顾不同视图和方面的集成形式主义。基本视图被认为是数据类型和过程视图和时间约束作为一个重要的附加方面。概述了相应的基本规格形式主义，并进一步讨论了如何将它们组合或集成，以处理不同视图和方面的组合和集成。3.6其他方法：耦合图文法和图形SOS。在[Gru00a]中，提出了一种基于耦合图文法的分布式数据建模规范化方法。该方法能够统一描述分布式建模和再工程任务中使用的合法域配置。规范方法支持开发适当的（重新）设计工具，并且该方法本身是工具支持18结构化操作语义（SOS）是一种流行而强大的语言规范，提供了丰富的数学理论和完善的方法论。在像UML这样的可视化建模技术中，抽象语法由Meta模型指定，即，描述模型静态结构的类图或模式。一个具体的模型，通常由一组相互关联的各种图表给出，表示为符合此模式的抽象语法图。为了指定图解语言的操作语义（即，动态Meta模型），在[CHM00]中，SOS方法被应用于图形抽象语法。我们的想法是取代SOS程序条款与抽象的语法图，增强与表示的状态，并使用图形转换技术指定的操作语义。4结构方面4.1分布式图转换在[Tae 96]中提出的分布式图和图变换（DGT）的新方法允许在两个抽象级别（网络和局部级别）上使用结构化图变换网络层包含系统拓扑结构的描述。地方一级关注的是描述状态及其在地方系统中的过渡。本地状态转换可以依赖于使用合适的同步机制的其他状态转换。本文将Schneider提出的范畴图文法的主要分布概念与Ehrig等人提出的分布图变换的代数双推出方法相结合，将[TK 97]中的分布图变换理论推广到属性图上，用部分代数描述数据和数据操作，从而得到一种强大而灵活的图变换属性机制。在[Tae 99]中，通过考虑局部图的分裂和连接以及局部系统中的并行变换，进一步扩展了该方法。分布式系统对规范技术提出了许多要求，这些要求在非分布式软件的开发中不必考虑。在[FKTV99]中，提出了分布式系统可视化设计的新概念，它是基于DGT作为底层形式化规范技术。该技术的核心是研究具有网络和局部两个抽象层次的结构图及其变换。在网络层上，系统的（可能的）动态拓扑结构被指定。本地层包含本地对象和数据结构的图形描述，其中部分对象和数据结构可以在远程网络节点中复制。这些结构可以使用基于子动作的交互机制独立地或与远程结构同步地演化。该方法说明了一个参考应用程序建模的分布式版本管理系统的任何类型的文件。19为了支持多个开发人员的分布式系统设计，在[FKTV99，FKT 00]中引入了局部视图。分布式系统上的本地视图由一个本地系统、其导入和导出接口以及连接的远程接口组成。局部系统的行为由一组仅适用于系统的局部视图的图形规则本地系统通过它们的导入和导出接口同步或异步地进行通信。异步通信采用图规则的顺序应用，同步通信采用图规则的融合。分布式算法和动态分布式数据结构是分布式系统的基本方面，它们通常由不同的规范技术分别建模。在相互访问le系统的运行示例中，[TE00]中显示了无法通过单独建模处理的典型问题。本文讨论了如何通过分布式图变换将分布式算法和动态数据结构集成规范来解决这些问题。在[TGM99，GMT99，TGM00，GEMT00a，GEMT00b]中，分布式图变换在分布式系统的动态体系结构配置和面向视点的软件开发中得到了不同的应用。 在[TGM99]和[TGM00]中讨论了在分布式系统中指定动态变化的问题。分布式系统的变化至少涉及两个层次。一个是分布式系统的本地节点中的变化的管理另一方面是改变分布式系统本身的结构。这意味着例如向/从分布式系统添加和/或移除本地节点或整个子系统。在[TGM00]中讨论了如何使用分布式图转换来实现变更模型。一个例子-一个环形数据库-展示了如何使用XML在一个小型但不平凡的分布式系统中对这些更改进行建模。为了在软件开发中支持多个视角，需要一个明确表达所有观点的方案，这些观点由不同的持有者持有，如需求工程师，软件架构师，客户，用户等。ViewPoint框架在过去已经被开发为一个概念模型，用于表达软件开发项目中的多个视角。在[GEMT00a]中，DGT对该框架进行了形式化描述，并通过一个非平凡的示例系统证明了该方法的适用性。在[GEMT00b]中，提出了ViewPoint工具，该工具支持基于上述方法的多视图的定义和使用。[Tae02]提出了一种基于图变换的分布式对象系统可视化建模技术。它包括网络的图形化描述及其动态重构，以及组件接口和局部对象系统及其行为。典型问题在dis-20像远程对象交互、对象迁移和复制、通信和同步这样的分布式系统在该技术中是可表达的。这种符号接近UML，在需要的地方进行了扩展在[MR99]中提出了一种相关的方法，它基于这样一个事实，即图和图语法可以有效地用于对以同步方式行为的分布式系统进行建模。事实上，图可以表示进程的网络，并且基于经由同步机制的简单上下文无关产生式的组合的合适的图重写规则为了解决产品的有效组合问题，本文提出了使用著名的约束传播技术，它可以帮助减少每个