.GReTA-seminar

The seminar gives a very short introduction of gothic churches (the historical and cultural part) and their virtual construction (the CAAD part). The main section shows that about 800 years ago intelligent design principles (algorithmic and parametric design) and reuse techniques (product and process reuse, classes of systems, domain knowledge, agile development) have been used in the design of gothic cathedrals. Two examples, the cathedrals of Reims and York, are discussed in more detail. There are even relations to graph rewriting which, however, are only touched.

Graph transformations that change a graph while preserving consistency wrt a given set of constraints are an important type of transformation in many areas. For example, in search-based optimisation over graphs, aiming to find graph structures (e.g., models) that are optimal wrt some given objective functions, we need to be able to make changes to a graph without introducing violations of consistency constraints so that we can ensure to only generate feasible solutions. However, writing graph-transformation rules that ensure consistency-preservation while still allowing change to the graph is difficult: A change to the graph may introduce a constraint violation and, therefore, the rule must include components that repair any such new violations. Any such repair has the potential to introduce new constraint violations itself and, therefore, the number of potential repair paths to follow can quickly explode exponentially in size. In this talk, I present work addressing these challenges in the context of optimal product-line configuration. We introduce a new data structure – feature-activation diagrams – to capture the dependencies between changes and use this to efficiently derive consistency-preserving graph transformation rules encoded as variability-based rules. The rules we generate allow us to solve existing benchmarks for product-line configuration more efficiently than the state of the art and find more optimal configurations.

The Digital Asset Modelling Language (DAML) enables low-code development of smart contract applications. Starting from a high-level but textual notation, DAML thus implements the lower end of a model-driven development process, from a platform-specific level to implementations on a range of blockchain platforms. We develop a notation based on class diagrams and visual contracts that map directly to DAML smart contracts. The approach supports an operational semantics in terms of graph transformation systems to capture the complex behavioural features of DAML, such as its role-based access control and the order of contract execution and archival. We use the Doodle case study from a DAML tutorial to introduce the mappings between DAML, visual models, and operational semantics. To implement, explore and analyse the operational semantics of the case study we present the graph transformation tool Groove, originally developed by Arend Rensink and his students to support the verification of object-oriented programs. It has since been employed to analyse a range of models, for P2P networks, workflows, component configurations, etc. Our use of Groove for the semantic underpinning and analysis of DAML follows its original purpose of program verification. We will use the opportunity to discuss Groove’s features and illustrate its use for creating and analysing graph transformation systems.

Modern component-based distributed software systems are increasingly required to offer non-stop service and thus their updates must be carried out at runtime. Different authors have already proposed solutions for the safe management of dynamic updates. Our contribution aims at improving their efficiency without compromising safety. We propose a new criterion, called version consistency, which defines when a dynamic update can be safely and efficiently applied to the components that execute distributed transactions. Version consistency ensures that distributed transactions be served as if they were operated on a single coherent version of the system despite possible concurrent updates. The paper presents a distributed algorithm for checking version consistency efficiently, formalizes the proposed approach by means of a graph transformation system, and verifies its correctness through model checking. The paper also presents CONUP, a novel prototype framework that supports the approach and offers a viable, concrete solution for the use of version consistency. Both the approach and CONUP are evaluated on a significant third-party application. Obtained results witness the benefits of the proposed solution with respect to both timeliness and disruption.

Decorated cospans are a general framework for composing open networks and mapping them to dynamical systems. We explain this framework and illustrate it with the example of stock and flow diagrams. These diagrams are widely used in epidemiology to model the dynamics of populations. Although tools already exist for building these diagrams and simulating the systems they describe, we have created a new software package called StockFlow which uses decorated cospans to overcome some limitations of …

The introduction of adhesive categories marked a watershed moment for the algebraic approaches to the rewriting of graph-like structures, as they provide an abstract framework where many general results can be recast and uniformly proved. However, checking that a category satisfies the adhesivity properties is sometimes far from immediate. In this talk we present a new criterion giving a sufficient condition for M,N-adhesivity, a generalisation of the original notion of adhesivity. We apply it …

Graph transformation allows to extend formal language theory to the generation of graph languages. This has applications in areas such as model-driven software engineering, natural language processing, and shape analysis of programs.

We start from the well-established theory of context-free grammars based on hyperedge replacement (HR) and introduces a modest extension, contextual hyperedge replacement (CHR), in order to extend their generative power. We discuss the generative power and other …

Last year we proposed PBPO+, which extends the Pullback-Pushout (PBPO) approach by Corradini et al. with strong matching. Now, we have proved that in the setting of quasitoposes (and assuming regular monic matching), PBPO+ can define all rewrite relations definable by PBPO, AGREE, SqPO and DPO – as well as additional ones. In this sense, PBPO+ can be considered a unifying theory in this setting. In this talk we reflect on the notion of a quasitopos, and explain how from its many nice properties our result can be obtained. This is joint work with Jörg Endrullis and Aloïs Rosset.

This talk will present recent results in the area of sequential and concurrent model synchronisations based on Triple Graph Grammars (TGGs). Sequential model synchronisation is the task of propagating information from one model to another. In contrast, in the concurrent case, both models have been modified independently from each other and conflicts may arise such that synchronization may additionally comprise the non-trivial task of conflict resolution. We will present our newly developed approaches for both synchronization scenarios. Their central qualities are that they have a solid formal foundation in the theory of algebraic graph rewriting and work far more incremental then previous approaches. In the first part, we will introduce TGGs and discuss a new concept for TGG-based concurrent model synchronisation. The second part of this talk will in particular stress the theoretical advances that allowed us to develop our approaches and illustrate the key ideas of the synchronization algorithms using non-trivial examples.