Graphs, Recognizability and Verification (GaReV)

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

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.