Behavior and Conuence Analysis of
M
-Adhesive
Transformation Systems using
M
-Functors
vorgelegt von
Dipl. Inform.
Maria Maximova
ORCID: 0000-0001-9275-806X
von der Fakultät IV Elektrotechnik und Informatik
der Technischen Universität Berlin
zur Erlangung des akademischen Grades
Doktor der Naturwissenschaften
Dr. rer. nat.
genehmigte Dissertation
Promotionsausschuss:
Vorsitzender: Prof. Dr. Stephan Kreutzer
Gutachter: Prof. Dr. Uwe Nestmann
Gutachterin: Prof. Dr. Barbara König
Gutachterin: Prof. Dr. Julia Padberg
Gutachterin: Dr. Claudia Ermel
Tag der wissenschaftlichen Aussprache: 26. März 2019
Berlin 2019
ABSTRACT
For modeling dynamic systems, various graphical modeling formalisms exist. In partic-
ular, 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 im-
portant 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 forma-
lisms, 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 anal-
ysis 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, ter-
mination, functional behavior as well as parallel and sequential independence of trans-
formations.
To establish the described formal relationship between different M-adhesive transfor-
mation systems, we have developed an abstract framework of M-functors. This frame-
work 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 forma-
lisms. 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 transforma-
tion 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 transfor-
mation systems, allows for modeling, simulation, and, in particular, critical pair analysis,
which is the first step towards the confluence analysis.
iii
ZUSAMMENFASSUNG
Komplexe dynamische Systeme können unter Einsatz von graphischen Formalismen ad-
äquat modelliert werden. Insbesondere regelbasierte Graphtransformationsformalismen
werden erfolgreich eingesetzt, um sowohl das Systemverhalten als auch Systemverände-
rungen zu erfassen. Für einige Graphtransformationsformalismen wurden bereits Werk-
zeuge zur Analyse von semantischen Eigenschaften entwickelt. Weiterführende Entwick-
lungen von Graphtransformationsformalismen vereinfachen einerseits ihre Anwendung
in verschiedenen Kontexten, erfordern jedoch andererseits neue Analysetechniken und
Analysewerkzeuge. Um die Entwicklung von solchen zusätzlichen formalismusspezifi-
schen Werkzeugen zu vermeiden, ist die Erforschung und Bereitstellung von formalen
Abbildungen solcher Formalismen in einen Kernformalismus mit bereits existierender
adäquater Werkzeugunterstützung hilfreich.
In dieser Arbeit haben wir für eine große Klasse von transformationsbasierten Mo-
dellierungsformalismen eine Technik entwickelt, um Instanzen von zwei Formalismen
(einem Quell- und einem Zielformalismus) miteinander in Beziehung zu setzen. Diese
Beziehung garantiert, dass bestimmte relevante semantische Eigenschaften der Instanz
des Zielformalismus (wie Verhaltensäquivalenz, (lokale) Konfluenz, Terminierung, funk-
tionales Verhalten sowie parallele und sequentielle Unabhängigkeit von Transformatio-
nen) auch von der Instanz des Quellformalismus erfüllt werden. Die entwickelte Tech-
nik ermöglicht somit den Einsatz der Analysewerkzeuge des Zielformalismus auch für
Instanzen des Quellformalismus. Mit unserer entwickelten Technik setzen wir Forma-
lismen aus der wohletablierten Klasse von M-adhäsiven Transformationssystemen in
Beziehung, einer Klasse von Formalismen die zahlreiche relevante graphische Model-
lierungsformalismen umfasst. Diese Formalismen basieren auf M-adhäsiven Kategorien,
die durch eine Liste von fundamentalen technischen Eigenschaften charakterisiert sind
und relevante Begrifflichkeiten für die Modellierung und Analyse von Systemverhalten
und Systemveränderungen bereitstellen.
Aus formaler Sicht stellen wir die Beziehung zwischen zwei M-adhäsiven Transforma-
tionssystemen mit Hilfe von sogenannten M-Funktoren her. Die hierfür benötigte Theo-
rie entwickeln wir im ersten Schritt für Transformationssysteme ohne verschachtelten
Anwendungsbedingungen und verallgemeinern diese nachfolgend für Transformations-
systeme mit verschachtelten Anwendungsbedingungen. Der Erweiterungsschritt ist for-
mal anspruchsvoll jedoch von großer praktischer Bedeutung, da die Verwendung von
verschachtelten Anwendungsbedingungen die Ausdrucksmächtigkeit der Transformati-
onssysteme erhöht und eine breite Verwendung bei der Modellierung findet.
Wir demonstrieren die Anwendbarkeit unseres auf der Ebene von M-adhäsiven Trans-
formationssystemen entwickelten abstrakten Ansatzes durch seine Instanziierung für
konkrete relevante Modellierungsformalismen. Wir setzen sowohl Hypergraphtransfor-
mationssysteme als auch Petri-Netz-Transformationssysteme mit individuellen Marken
jeweils mit den entsprechenden getypten attributierten Graphtransformationssystemen
in Beziehung. Für diese Instanziierung definieren wir zunächst jeweils einen konkre-
ten M-Funktor zwischen der M-adhäsiven Kategorie des Quelltransformationssystems
und der M-adhäsiven Kategorie des Zieltransformationssystems und verifizieren im An-
schluss, dass der definierte M-Funktor in Verbindung mit den involvierten M-adhäsiven
Kategorien die durch die Theorie vorgegebenen hinreichenden Bedingungen erfüllt.
iv
ACKNOWLEDGEMENTS
It was a very big challenge for me to finish this thesis. That is why I am very grate-
ful to my supervisors, colleagues, family, and friends for their permanent support and
encouragement.
First of all, I want to thank Prof. Dr. Hartmut Ehrig, who, already in my first years
as a student, inspired me for the field of theoretical computer science, woke my interest
for scientific work, believed in my skills, and gave me an opportunity to learn from his
long-time experience as well as from his enthusiasm and precision when doing research.
I am very sad, that Hartmut cannot read the final version of my thesis.
I also want to sincerely thank Prof. Dr. Uwe Nestmann for continuing my supervision
after retirement of Hartmut as well as for giving me an opportunity to work in his group
and to do teaching in the field of theoretical computer science as a student assistant and
as a research assistant.
I am especially grateful to Dr. Claudia Ermel for being, before and after retirement
of Hartmut, my co-supervisor, for supporting me in different kinds of administrative
matters, for motivating me, for being always positive, for giving me feedback, and for
many valuable discussions on theoretical and practical aspects of my work.
Apart of that, I am very thankful to my secondary reviewers and co-supervisors, Prof.
Dr. Barbara König and Prof. Dr. Julia Padberg, for accepting the task of examining my
thesis and their valuable support and positive feedback.
Furthermore, I would also like to thank my former colleagues from the TFS research
group for a great time we spent together while doing research and teaching. Many
thanks go to Olga Runge for moral support, for fruitful discussions, and for help con-
cerning Agg. Additionally, I thank Dr. Tony Modica, Dr. Karsten Gabriel, Dr. Frank
Hermann, and Hanna Schölzel for companionship, for moral support, for sharing the
daily working life, and for feedback provided in many talks and discussions. Moreover,
I am very thankful to Käte Schlicht for her help in all administrative situations.
I would also like to sincerely thank my current boss and my current colleagues from
the Hasso Plattner Institute in Potsdam. I am very grateful to Prof. Dr. Holger Giese for
giving me an opportunity to finish my thesis in his group while working in parallel on
a DFG project and for supporting me without putting me under pressure. Furthermore,
I want to thank Dr. Leen Lambers for her detailed constructive feedback in the final
phase of my work and for continuously encouraging me to go on with the completion
of my thesis. Last but not least, I would like to thank my colleagues Lucas Sakizloglou,
Sona Ghahremani, Jochen Hänsel, Johannes Dyck, Dr. Dominique Blouin, Kerstin Miers,
Thomas Brand, Dr. Thomas Vogel, Matthias Barkowsky, He Xu, Christian Zöllner, and
Christian Adriano for their great companionship, friendship, and moral support in diffi-
cult times.
Finally, I want to express my special thanks to my husband Dr. Sven Schneider for
supporting me in every situation, for bearing me in stressful times, for thousands of
discussions about my work, for proofreading of several parts of the thesis, and for every-
thing else he has done for me. In addition to this, I am very grateful to my dear parents
for believing in me all of the time, for giving me energy to finish this thesis, and for
cheering me up every time I needed it.
v
Loading more pages...