标记端口图：一种基于图的编程和建模框架

可在www.sciencedirect.com在线获取理论计算机科学电子笔记338（2018）3-21www.elsevier.com/locate/entcs标号端口图MaribelFern'andez1英国伦敦国王H'el'eneKirchner2因里亚布鲁诺·皮诺3波尔多大学，CNRS UMR 5800 LaBRI，法国摘要我们提出了标记端口图的一般定义，作为基于图的编程和建模框架（语法和语义）的设计基础。 我们表明，这种结构提供了语法的程序，这是由一个初始图，一组规则和战略。表示为标记端口图的规则应用于也表示为标记端口图的状态，并根据给定策略计算其后继者。状态，规则和计算的描述控制的战略，使用标记端口图，详细说明和说明的例子，从P狂欢，一个战略端口图重写环境，用于设计复杂系统的可执行规范关键词：标记端口图，重写规则，策略，基于规则的建模，狂欢1介绍在文献中可以找到各种标记图和属性图的概念，但是为这些概念定义一个适当的图变换理论并不简单，主要是因为标记或属性是在代数框架中解释的，不容易与通常用于图的范畴框架结合起来。然而，在过去的20年里，已经提出了不同的方法来克服这个困难：在[22]中，图被编码为代数和数据代数。1电子邮件：maribel. kcl.ac.uk2电子邮件：helene. inria.fr3电子邮件：bruno. u-bordeaux.frhttps://doi.org/10.1016/j.entcs.2018.10.0021571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。4M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）3是嵌入在图表中的。在[29]中，标号图具有作为代数元素的标号，图变换规则涉及对标号的计算。在[25]中，符号图包括表示属性值的变量节点以及约束这些变量值的一组公式端口图，即，图中的边在称为端口的特定点处连接到节点，已在各种上下文中使用。端口允许以自然的方式对概念进行建模，例如蛋白质相互作用中的结合或磷酸化位点、计算机网络中的通信端口或不同社会网络中的用户链接。端口图用于生化系统建模和指定社交网络的生成和传播算法的示例可以在[3，2，11]中找到。具有与节点、端口和边相关联的属性的端口图（简称为属性端口图）在[13]中被正式定义，其中端口图重写关系使用图变换的单推出方法来指定。自2010年以来，这种正式的结构在PORGY[26]中实现，这是一个可视化环境，允许用户定义端口图和端口图重写规则，并以交互方式或通过使用策略来应用重写规则。为了控制重写规则的应用，PORGY提供了一种策略语言。最新版本的PORGY可以从http://porgy.labri.fr下载，无论是MacOS、Windows还是Linux机器的源代码还是二进制文件在这些工作的基础上，本文重点讨论了标记端口图的形式结构，并解释了它在复杂系统的可执行规范设计中的作用。 标记端口图是端口、节点 并且边携带标签，标签是来自形式语言的表达式，其作为参数连同其解释域一起给出。PORGY中用于定义节点、端口和边的属性的概念可以被看作是标签的一个特殊情况，其中一组内置的函数符号和谓词是可用的（例如，算术运算符和在图域上解释的谓词，例如edge（n，nJ），如果给定图中存在连接节点n和nJ我们证明了图变换系统的所有成分都可以被指定为标记端口图。端口图重写规则被标记为端口图，该端口图由两个端口图（左侧和右侧）和一个特殊节点（箭头节点）组成，该节点链接左侧和右侧的端口。对于mally，箭头节点定义了一个态射，用于为重写提供单一的推出语义。 因为通常有不止一种方法来应用规则 对于生成重写步骤的图，使用策略表达式来选择要应用的规则以及规则应该（或不应该）应用的图中的位置。我们将定位图定义为标记端口图，其包括用于指定重写位置的标签和应该被保护的子图（即，未重写）。重写派生，由策略控制，也可以表示为标记端口图，其节点由图和策略标记这种图重写的方法，其中系统的所有组件都使用一个独特的概念（即标记端口图）表示，从理论和实践的角度来看都具有优势：有一个主要的数据结构，M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）35真正设计和实现，所以实现工作可以集中在这个任务上，并且由于重写规则本身是图形，所以形式主义是通过构造来反映的。引用是逻辑框架中的关键属性，并且便于扩展的设计（参见，例如，重写逻辑[23]）。本文的组织如下：第2节介绍了标记端口图作为一种通用结构的概念，并给出了在PORGY中使用的具体实例。第3节用来自各个领域的例子来说明这种结构规则和重写在第4节中定义，其中表明规则也被标记为端口图，并提出了这种结构上的重写机制。第5节将定位端口图显示为标记端口图。导出图是标记图的另一个实例，在第6节中定义，并用作一种机制，通过标记端口图，重写规则和策略来可视化系统的动态行为。第7节介绍了相关工作，并为今后的工作提供了方向。2标号端口图端口图是节点具有端口的图，端口是连接边的点。标记节点、端口和边缘在本文中，我们提出了符号标签的概念，它是标记端口图定义的一个参数。定义2.1[符号标签]符号标签（或简称标签）ll是形式语言L的一个元素，由其语法和语义给出所有标签都有一个名称，使用L定义2.2[标记端口图]标记端口图G=（V，P，E，D）F，L由下式给出：• 成对不相交集合的4元组（V，P，E，D），其中：· V是节点的有限集合; n，n1，. 节点范围· P是端口的有限集合; p，p1，. 港口范围· E是端口之间的边的有限集合; e，e1，. 边缘范围;两个端口可以由多于一个边缘连接;· D是来自L的标签的集合;• 以及函数Connect、Attach和Label的3元组F，使得：· 对于每个边e∈E，Connect（e）是通过以下方式连接的端口对（p1，p2）：e;· 对于每个端口p∈P，Attach（p）是该端口所属的节点n· Label：V<$P<$E<$→ P（D）是一个标签函数，它为V<$P<$E中的每个元素返回一个有限的标签集。如果边未定向，则可以忽略Connect结果中端口的顺序。例2.3图1给出了标记端口图的一个例子。 V是一组6M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）311个节点，每个节点都标记有分子名称（Raf-1、PDE 8A 1、AKAP、PKA、cAMP或S）。P是一组21个端口，也用它们的名称（S1，S2，P1，. . .当Attach（p）=n时，Attach函数通过将端口p绘制为节点n内的红色或绿色正方形来可视化。每个节点和端口也有一个颜色标签，通过图中元素的颜色可视化。E是一组7条边，在本例中未标记。如果Connect（e）=（p1，p2），则Connect函数由两个端口（p1，p2）之间的线可视化。定义2.2是通用的，因为标签集合D实际上是可以以不同方式实例化的参数。如果D是空的，我们得到普通的（未标记的）端口图，仅由具有端口的节点集合和通过端口连接节点的边组成;如果D是原子标记的集合，我们得到在[1，2，12]中定义的标记端口图的概念。对于图，已经提出了更丰富的标签定义，这带来了更多的表达性：例如，在[25]中，E-图的标签由连接到边和节点的标签节点表示，而在符号图中，它们是受一组公式约束并在代数上解释的变量;在[9]中，属性图标签是给定数据代数的值。下面我们假设熟悉泛代数的基本概念（我们请读者参考[10]了解详细信息）。标签在PORGY中作为记录实现，其字段具有内部值[13]中所描述的。 在狂欢中，标签ll是一个配对（a 1：= v 1，...， a n：= v n），其中a i，称为属性，是集 合 A 中 的常数，或一个集合XA中的变量，vi是ai的值。元素ai是两两不同的。 每个标签ll中的第一个属性是它的名称，用于标识类型标签在以下意义上：对于所有LL= （姓名：=v1，.，a n：= vn），l1 J=（Name：=v1J， . ，aJm：=vmJ），如果v1=v1J，then=m且ak=aJk，1 n。图6显示了交互网络系统中的两条规则，它们定义了0和S（后继）表示的自然数的加法运算。在第一条规则（a）的左侧，代理+和S通过它们的“主端口”连接规则的右侧显示了交互的结果：S的辅助端口（标记为1）现在连接到+。注意，在规则（b）的箭头节点中有一个线端口，用于处理0和数字n相加的结果是n的事实。一般来说，系统的行为是由几个规则建模的。重写系统就是由这组规则组成的端口图构建重写系统M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）313PP图五. 用于描述社交网络中交互的规则。 如果A和C都知道B，如果不认识对方，就应该见面。(a) 描述+和S之间相互作用的规则。(b) 添加0。图第六章定义自然数加法的交互网络系统规则（a）定义了以下两种情况之间的相互作用：施事+和S表示标准归约n+S（m）→S（n+m））。规则（b）指定了0和+之间的相互作用，并表示0+n→n。通过为每个子集添加具有不同名称的新节点并将此节点链接到子集中每个规则的箭头节点，5已定位的图形和规则在PORGY中引入了定位端口图来明确地指示图中应该执行重写的位置[2]。 他们还可以指定图中应该被保护的部分（即，重写的子图禁止）。定义5.1[定位图][13]。一个定位图GQ由一个端口图G和G的两个可区别的子图P和Q组成，这两个子图分别被称为位置子图和禁止子图。在这一点上，很容易将定位图视为标记端口图：我们可以引入两个标签Pos和Ban，它们取两个可能的布尔值on（true）和o_n（false）。在一个定位图GQ中，P是G的子图，它由Pos标签在其上有值的节点和相关的边组成。这是下一步的重点。Q是一个受保护的子图，由带有Ban标签的节点组成，其中禁止变换我们把额外的限制，最初是不可能有相同的节点在位置和禁止的子图。P和Q不相交。14M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）3M′PMMPMLWRMP然后，这个属性通过我们下面定义的重写过程来保持当应用端口图重写规则时，不仅底层图G而且位置和禁止子图也被更新。下面定义的定位重写规则指定了右侧R的两个不相交的子图M和MJ，它们分别用于更新位置和禁止子图。如果M（resp. MJ）不受限制，R（resp. emp tyg（e）被用作缺省值。左边的子图W指定了哪些节点应该在G的位置子图P中。如果W未指定，则要求L中至少有一个节点应该在位置子图中如上所述，L和R中的节点具有标签Pos和Ban，要么是变量x，要么是两个可能值之一。我们在下面给出细节，其中我们使用运算符，，\来表示端口图的并，交和补。这些运算符是在端口图上定义的，来自节点、端口和边的集合上的通常集合运算，除了\，其中当端口不处于不同位置时，连接到端口的边被丢弃，以避免悬挂边。定义5.2[定位重写规则]定位重写规则由端口图重写规则L<$R以及R的两个不相交子图M和MJ给出，其中：M中任何节点n的标签Pos和Ban分别具有值on和o<$，M中任何节点j的标签Pos和Ban分别具有值o <$和on，以及可选的L的子图W，其中节点标签Pos具有值on，标签Ban具有值o <$;对于L中的其余节点，标签Pos是变量（每个节点不同），Ban标签具有值o <$。记作L W<$R M′。我们记为GQ→gGJQMP′ 并说定位图GQ重写为GJQ′使用LW在位置P处避开Q，如果G→LR带态射的GJg满足条件：L中至少存在一个节点n，使得标签n中的Pos与g（n）中的值匹配，即g（n）∈P。换句话说，在定位重写规则LW<$RM′中，W是由Pos标签等于on和Ban标签等于o的节点以及相关边组成的LM是R的子图，由Pos标签等于on和Ban标签等于o的节点组成，具有相关的边。MJ是R的子图，由具有Ban标签的节点和Pos标签的节点组成。在重写步骤中使用的态射g具有定位规则L W<$R M′，使得g（L）<$P = g（W）或简单地g（L）<$P/=<$，如果W不被提供，并且g（L）<$Q=<$。 新的位置子图PJ和禁止子图QJ被定义为PJ=（P\g（L））g（M），QJ=（Qg（MJ）;如果M（resp.MJ）未提供，则我们假设M=R（分别为 MJ=m）。在[14]中，定位图被用来对社交网络中的传播进行建模。例如，在线性阈值传播模型中，传播由图7中给出的两个规则指定。当在连续性试验中应用第一个规则LT时，左侧的活动绿色节点必须对应于位置子图P中的节点，右侧的通知蓝色节点具有等于on的标签Pos，因此其图像属于变换网络中的更新P然后可以选择应用第二规则LT激活。M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）315状态：=知情状态：=活跃状态：=活跃标记：= 0状态：=活跃标记：= 1状态/=活跃状态：=知情T au：=JointInf−θT au≥0(a) LTin accuracy trial：在非活动节点上从活动邻居进行的联合计算（不知道或只是通知）。(b) LT activate：当被通知的节点被成功地激活时，被通知的节点变为活动的。图第七章用于表示线性阈值模型LT的规则。活动节点是绿色的，通知节点是蓝色的，不知道的节点是红色的。双色红/蓝节点可以处于两种状态中的任一种，即不知道或被告知。6导出图和策略重写步骤的序列称为重写派生。这在图8中示出，其中图3的初始交互网络用图6的规则在两个步骤中重写。图八、重写派生的示例虽然重写过程自然地生成派生树，但是一些节点可以是同构的，例如在连续重写系统的情况下。所以一般来说，我们考虑导子图。从形式化为属性端口图的输入状态开始，重写步骤（顺序地、并发地或概率地应用）构建由派生组成的图，其对应于顺序变换。在该图中，节点是状态，并且边表示转换（例如，重写步骤）。标签在这个图表中也很有用边具有记录重写步骤信息的标签不同类型的边缘可以通过颜色和形状标签进行视觉区分。例如，可以创建附加边作为两个状态之间的快捷方式，16M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）3PPQP实例以更简洁的方式表示派生。这样的快捷方式具有记录快捷方式中涉及的步骤序列的标签。图9给出了一个导出图的示例，其中快捷边用绿色表示见图9。从玩具生化过程示例构建的推导图。快捷方式是绿色边缘。 红色节点是故障状态。策略用于控制规则的应用（包括概率应用）并专注于兴趣点：策略定义了应该应用哪些规则以及在哪里应用（参见[17，5，18]的一般定义）。它们还可以表示两个状态之间的快捷方式，如图9所示。 狂欢中使用的语言在[13]中定义了用于端口图重写的写入策略。给定图、规则和策略，我们现在可以引入一个更抽象的概念，即符号导出端口图，它与图程序的操作语义密切相关。定义6.1[图程序]（策略重写）图程序由定位重写规则R的有限图、策略表达式SR（使用策略语言L从R构建）和定位图G组成。当R从在上下文中，我们简单地写（S，GQ）来表示策略重写图程序，称之为图形程序。形式上，图程序（S，GQ）的语义在[13]中使用 转换系统，定义SOS风格的小步操作语义[27]。M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）317PPPP在这里，我们引入符号推导图来表示图形程序及其执行。定义6.2[符号推导图]策略语言L的符号推导图是一个标记端口图，其中节点有两个不同的标签：当前图是一个定位端口图，策略是策略语言L的表达式。边由策略表达式标记。每个节点都有两个端口，分别命名为Parent和Successors。符号推导图中的节点表示图程序，边表示过渡步骤。查看应用于由策略S和当前图G标记的节点的[13]中的小步操作语义的转换规则，每个步骤的应用条件通过策略SJ的新表达式或新端口图GJ（可能由另一个图程序的执行产生）来表示。一个符号导图是有效的，如果只要两个节点标记为（S，GQ）和（SJ，GJQ′）由边连接，在图pro-Q ′之间存在过渡P′′gram（S，GQ）和（SJ，GJQ）的策略语言的操作语义。PP′Q Q′它是完备的，如果对于每个转移（S，GP）−→（SJ，GJP′），根据运算，在逻辑语义上，在由S、G、Q和G标记的节点之间存在边SJ，GJQ′. 后者意味着所有可以从GQ导出的图都符合-普可以在导出图中通过遵循从（S，GQ）。在这个意义上，导出图表示图程序（S，GQ）的执行。7结论我们提出了在本文中的概念的PORGY框架使用的结构标记端口图的符号标签。 这个角度也反映在实现层面：狂欢是在可视化框架TULIP[4]，它基于标记图的概念，其中标签是属性。更准确地说，一个TULIP图基本上是由三个集合：一个节点集合，一个边集合和一个为每个节点和边定义的属性集合。《图利普》中的财产概念与波吉记录中的属性在审视这项工作所开辟的前景之前，让我们先提一下与我们密切相关的其他一些系统或方法7.1相关作品图形在计算机科学中以多种形式和上下文使用，生成、可视化和转换它们导致了实现标记图转换和重写的各种工具的开发。为了在使用UML和Java的软件开发人员社区中推广这些概念，Java是嵌入在Fujaba工具套件[24]中的故事图语言[15]，18M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）3采用了Progres[31]的大部分功能，但避免了与图重写的非确定性相关的回溯机制。GROOVE [30]是另一个与PORGY密切相关的图转换系统。它使用带标签的图，变换由规则和控制指定GROOVE已被用于建模和分析各个领域的复杂系统，如[16]所示。它是一个多功能的工具;但是，它不提供PORGY中可用的可视化和动画功能。GP[28]也是一种密切相关的基于规则的非确定性编程语言，其中程序由图重写规则集和文本策略表达式定义。策略语言有三个主要的控制结构：顺序、重复和条件。由于GP的目标是高效地执行图程序，因此GP只构建一个重写派生，尽管早期版本的GP使用类似Prolog的回溯技术来探索整个派生图。GP不提供可视化派生树的机制，不像PORGY，用户可以在树上交互式导航，可视化替代派生，遵循特定Redex的演变等。与这些系统相比，PORGY图 重 写 也 广 泛 应 用 于 化 学 和 生 物 学 。等 系 统如 BioNetGen[11] ，RuleBender[32]，Mosbie[33]解决了对巨大图建模的问题它们将可视化与基于规则的细胞内生物化学的建模和模拟相结合，但不提供策略语言。然而，这些规则与PORGY的规则非常相似[20]中开发的图转换方法封装在“单元”中规则和控制条件，就像我们的战略重写图程序一样。控制是通过正则表达式来表达的，而正则表达式是一种比我们的策略语言功能更弱的语言但它们的独立性方法适用于所有类型的图，规则，规则应用和控制条件，在某种程度上接近我们所关心的一般结构的标记端口图。7.2观点符号标记和相应的标记端口图的一般概念似乎提供了很多表达性，但提出了几个需要进一步探讨的问题。本文定义的标记端口图重写的语义考虑在[13]中，我们证明了标记端口图的一个大子类是[22]中定义的属性图结构，并探索了上面给出的重写操作概念与单推出（SPO）对象的构造之间的对应关系。然而，这些第一个结果必须扩展到整个类别的标记端口图和图重写定义在本文中，并涵盖例如节点复制和端口图克隆，在[7]提出的方向。另一个研究方向是将一阶公式视为符号标签，如[25]。他们表明，他们的接地符号图符合属性M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）319图，它只考虑标记端口图的DPO/SPO重写语义。符号标签可以特别允许我们考虑约束满足性。在这一行中，我们计划考虑一个更抽象的约束概念，其中在语义域中解释的图结构和标签用于生成图。这种基于约束的标记端口图的通用概念可能对图重写、缩小和完成的推理感兴趣在这项工作中，策略是一种形式语言的表达式，以控制规则的应用。一个开放的问题是将策略表示为标记端口图，其方式类似于将策略表示为rho演算中的rho项[6]。第一步已经完成，因为简化为一个规则的策略已经是一个标记端口图，并且在[3]中提供了这个方向的初步工作。这将为设计基于rho-graph演算的逻辑框架开辟道路。进一步工作的另一个方向是在战略重写程序和标记端口图上引入结构化机制。我们想要探索的一个有前途的方向是多层图的概念，受到多层网络的启发[19]。确认我 们感谢OanaAndrei、GuyMelanMeconcon和OlivierNamet 在最初的PORGY项目（2009-2012）中所做的工作;他们的想法和热情在该工具开发的早期阶段是无价的我们还要感谢Jason Vallet实现了PORGY的几个功能，编写了文档并开发了社交网络传播的例子。我们还要感谢匿名评审，他们的宝贵意见和建议帮助我们改进了本文的第一版引用[1] 安德烈，O.，“A Rewriting Calculus for Graphs: Applications to Biology and Autonomous Systems,”论文，洛林国立综合理工学院（2008年）。[2] 安德烈，O.，M. 弗南德斯，H。 Kir chner，G. MelanPasticon，O. Namet和B. Pinaud，PORGY：Strategy-图的驱动交互变换，在：R。埃查赫德，编辑，第六国际 Workshop on Computing with Terms andGraphs，Electronic Proceedings in Theoretical Computer Science 48，2011，pp. 54比68URLhttp://hal.inria.fr/inria-00563249/en[3] 安 德 烈 岛 和 H. Kirchner ， A Higher-Order Graph Calculus for Autonomic Computing ， in ： GraphTheory ，Computational Intelligence and Thought。 Golumbic Festschrift， Lecture Notes in ComputerScience 5420（2009），pp. 15-26[4] Auber，D.，D. 阿尚博河Bourqui，M.Delest，J.Dubois，A.Lambert，P.玛丽，M。马蒂奥G. 作者声明：A. Renoust和J. Vallet，TULIP5，in：R. Alh ajj和J. Rokne，编辑，《社交网络分析与挖掘》，Springer new-York，2017年。 1-28.[5] Bourdier，T.，H. Cirstea，D. J. Doughnard和H. Kirchner，Extensional and Intensional Strategies，ProceedingsNinthInternationalWorkshoponReductionStrategiesinRewritingandProgramming，Electronic Proceedings in Theoretical Computer Science15，2009，pp.1-19[6] Cirstea，H.和C. Kirchner，重写演算-第一部分和第二部分，纯粹和应用逻辑兴趣小组的逻辑杂志9（2001），pp。427-498.[7] Corradini，A.，D.迪瓦尔河Echahed，F.普罗斯特和L. 图代数变换的拉回-推出方法，见：J.de Lara和D.Plump，editors，Graph Transformation（2017），pp. 3比1920M. 费尔南德斯等人/理论计算机科学电子笔记338（2018）3[8] 达诺斯，五，J. Feret，W.丰塔纳河Harmer，J. Hayman，J. Krivine，C.汤普森-沃尔什和G. Winskel，基于规则的模型的图、重写和路径重构，在：S。D. L- Z. fuer Informatik，editor，FSTTCS2012-IARCSAnnualConferenceonFoundationsofSoftwareTechno