Graphs, Recognizability and Verification (GaReV)

图形、可识别性和验证 (GaReV)

• 批准号: 173310673
• 负责人: Professorin Dr. Barbara König
• 金额: --
• 依托单位: Lehrstuhl Theoretische Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2010
• 资助国家: 德国
• 起止时间: 2009-12-31 至 2015-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/173310673?language=en
• 关键词: Graphs; Recognizability; Verification; GaReV

This project is aimed at providing verification techniques for concurrent and distributed systems, modelled by graph transformation. For this we will use techniques from the areas of formal languages (especially recognizable graph languages) and graph theory (especially graph minor theory), between which close ties are known to exist. We will further develop methods based on recognizable graph languages due to Courcelle and apply them to invariant checking, termination analysis and regular model checking. In this context we will also use monadic second-order logic for specifying graph languages. In the second part of the project we will employ graph-theoretical results in order to obtain backwards analysis techniques for graph transformation systems. This is a new and original direction of research since so far little graph theory has been used for the verification of graph transformation. In addition we will implement our techniques (or continue working on existing prototype tools) and apply them to various case studies.

这个项目的目的是提供验证技术的并发和分布式系统，建模的图形转换。为此，我们将使用来自形式语言（特别是可识别的图语言）和图论（特别是图子理论）领域的技术，已知它们之间存在密切联系。我们将进一步开发基于可识别的图形语言由于Courcelle的方法，并将其应用于不变式检查，终止分析和定期模型检查。在这种情况下，我们也将使用一元二阶逻辑来指定图形语言。在项目的第二部分，我们将采用图论的结果，以获得向后分析技术的图形转换系统。这是一个新的和原始的研究方向，因为到目前为止，很少有图论已被用于验证图转换。此外，我们将实施我们的技术（或继续在现有的原型工具上工作），并将其应用于各种案例研究。

项目成果

A General Framework for Well-Structured Graph Transformation Systems

结构良好的图转换系统的通用框架

• DOI: 10.1007/978-3-662-44584-6_32
• 发表时间: 2014
• 作者: Barbara König;Jan Stückrath
• 通讯作者: Jan Stückrath

Robustness and closure properties of recognizable languages in adhesive categories

粘合剂类别中可识别语言的鲁棒性和封闭性

• DOI: 10.1016/j.scico.2014.08.006
• 发表时间: 2015
• 期刊: Sci. Comput. Program.
• 作者: H.J. Sander Bruggink;Barbara König;Sebastian Küpper
• 通讯作者: Sebastian Küpper

Verification Techniques for Graph Rewriting (Tutorial)

图重写的验证技术（教程）

• DOI: 10.4230/dagrep.5.11.1
• 发表时间: 2015
• 作者: Parosh Aziz Abdulla;Fabio Gadducci;Barbara König;Viktor Vafeiadis
• 通讯作者: Viktor Vafeiadis

Well-structured graph transformation systems

结构良好的图形转换系统

• DOI: 10.1016/j.ic.2016.03.005
• 期刊: Inf. Comput.
• 作者: Barbara König;Jan Stückrath
• 通讯作者: Jan Stückrath

Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

具有全邻域操作的图转换系统的参数化验证

• DOI: 10.1007/978-3-319-11439-2_6
• 发表时间: 2014
• 期刊: ArXiv
• 作者: Giorgio Delzanno;Jan Stückrath
• 通讯作者: Jan Stückrath