Analysis of Graph Transformation Systems: Native vs Translation-based Techniques

TL;DR

This paper compares native and translation-based analysis techniques for Graph Transformation Systems, examining their design choices, impacts on analysis quality, and providing insights from literature and community discussions.

Contribution

It offers a comprehensive comparison of native and translation-based methods for GTS analysis and discusses how design choices affect analysis effectiveness.

Findings

Translation-based techniques' quality depends heavily on logic and encoding choices.

Native approaches often provide more direct analysis but may lack flexibility.

Design decisions significantly influence analysis complexity and accuracy.

Abstract

The paper summarises the contributions in a session at GCM 2019 presenting and discussing the use of native and translation-based solutions to common analysis problems for Graph Transformation Systems (GTSs). In addition to a comparison of native and translation-based techniques in this area, we explore design choices for the latter, s.a. choice of logic and encoding method, which have a considerable impact on the overall quality and complexity of the analysis. We substantiate our arguments by citing literature on application of theorem provers, model checkers, and SAT/SMT solver in GTSs, and conclude with a general discussion from a software engineering perspective, including comments from the workshop participants, and recommendations on how to investigate important design choices in the future.