Behavior and confluence analysis of M-adhesive transformation systems using M-functors

For modeling dynamic systems, various graphical modeling formalisms exist. In particular, rule-based graph transformation formalisms have proven to be adequate, both to capture system behavior and system adaptations. For some graph transformation-based formalisms there already exist well-established tools, enabling modelers to analyze important semantical properties of considered transformation systems. Yet, there are many further adaptations and variants of such formalisms which, on the one hand, ease their application in certain contexts but, on the other hand, require new analysis techniques and tools. To avoid the implementation of further formalism-specific analysis tools for all these formalism variants, it would be helpful to develop and use a formal mapping of the considered formalisms to a kernel formalism for which analysis techniques and tools do already exist. Therefore, in this thesis, for a broad class of transformation-based modeling formalisms, we have introduced a technique to relate two formalisms with respect to their semantical properties of interest. The provided connection enables the usage of the analysis methods and tools available for the target formalism also for the source formalism. As a class of considered formalisms we have chosen M-adhesive transformation systems based on M-adhesive categories, which share common technical properties and include many relevant notions used for the modeling of system behavior and adaptation. The investigated semantical properties include behavioral equivalence, (local) confluence, termination, functional behavior as well as parallel and sequential independence of transformations. To establish the described formal relationship between different M-adhesive transformation systems, we have developed an abstract framework of M-functors. This framework is introduced first for transformation systems containing only rules without nested application conditions and is then extended to rules with nested application conditions. This extension is non-trivial concerning the technical aspects and is most important for transformation systems in practice. The developed abstract framework is instantiated for two relevant modeling formalisms. We related both, hypergraph transformation systems and Petri net transformation systems with individual tokens with typed attributed graph transformation systems. The instantiation is executed by providing concrete M-functors from the M-adhesive category of the source transformation system to the M-adhesive category of the target transformation system and by verifying sufficient technical properties required by the developed theory for the involved categories and the constructed concrete M-functors. The common target transformation system of typed attributed graphs is a reasonable choice since, for example, the well-established tool AGG, purpose-built for typed attributed graph transformation systems, allows for modeling, simulation, and, in particular, critical pair analysis, which is the first step towards the confluence analysis.

Author dc:creator

• Maximova, Maria

Advisor dc:contributor.advisor

• Nestmann, Uwe

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Language dc:language.iso

en

Identifier URI

http://dx.doi.org/10.14279/depositonce-9454

OAI identifier oai:identifier

oai:depositonce.tu-berlin.de:11303/10521